Mercurial > hg > Papers > 2015 > atton-thesis

changeset 78:6f699b37dc55

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Add original number count
author Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
date Wed, 18 Feb 2015 12:26:17 +0900
parents ce7701e4a308
children 0fc51df4c15c
files paper/agda.tex paper/delta.tex paper/future.tex paper/introduction.tex paper/main.pdf paper/proof_delta.tex paper/src/delta_example.hs paper/src/numberCount1.hs paper/src/numberCount2.hs
diffstat 9 files changed, 85 insertions(+), 62 deletions(-) [+]
line wrap: on
line diff
--- a/paper/agda.tex	Wed Feb 18 11:10:19 2015 +0900
+++ b/paper/agda.tex	Wed Feb 18 12:26:17 2015 +0900
@@ -434,8 +434,8 @@
     \lstinputlisting[label=src:three_plus_one, caption= Agda における 3 + 1 の結果が 4 と等しい証明] {src/three_plus_one.agda}
 \end{table}
 
-3+1 という関数を定義し、その型として証明すべき式 \verb/(S (S (S O))) + (S O)≡(S (S (S (S O))))/ を記述する。
-そして証明すべき式を関数の定義として記述する。
+3+1 という関数を定義し、その型として証明すべき式を記述し、証明を関数の定義として定義する。
+証明する式は \verb/(S (S (S O))) + (S O)≡(S (S (S (S O))))/ である。
 今回は \verb/_+_/ 関数の定義により \verb/ (S (S (S (S O)))) / に簡約されるためにコンストラクタ refl が証明となる。
 
 $ \equiv $ によって証明する際、必ず同じ式に簡約されるとは限らないため、いくつかの操作が Relation.Binary.PropositionalEquality に定義されている。
--- a/paper/delta.tex	Wed Feb 18 11:10:19 2015 +0900
+++ b/paper/delta.tex	Wed Feb 18 12:26:17 2015 +0900
@@ -147,16 +147,16 @@
 \section{Delta Monad を用いたプログラムの変更の記述例}
 \label{section:delta_example}
 プログラムの変更を表現するメタ計算に対応するデータ型 Delta が記述できた。
+2つのバージョンを持つプログラムを Delta によって表現した例を述べる。
 
-実際に Haskell で Delta を用いたプログラムの変更例をリスト\ref{src:delta_example}に示す。
+まずは Delta を用いずに記述したプログラムを示す(リスト\ref{src:numberCount1})。
 
 \begin{table}[html]
-    \lstinputlisting[label=src:delta_example, caption=Deltaを用いたプログラムの例] {src/delta_example.hs}
+    \lstinputlisting[label=src:numberCount1, caption= numberCount バージョン1] {src/numberCount1.hs}
 \end{table}
 
-リスト\ref{src:delta_example}は1からnの間の整数に含まれる特定の数の個数を調べるプログラム numberCount である。
-
-このプログラムは3つの関数からなり、2つのバージョンを含む。
+1からnの間の整数に含まれる特定の数の個数を調べるプログラム numberCount である。
+このプログラムは以下の3つの関数により定義される。
 
 \begin{itemize}
     \item generator
@@ -167,7 +167,7 @@
     \item numberFilter
 
         数のリストから特定の数のみを絞り込む関数である。
-        バージョン1では素数の数のみを絞り込み、バージョン2では偶数の数のみを絞り込んでいる。
+        バージョン1では素数の数のみを絞り込む。
 
     \item count
 
@@ -175,22 +175,39 @@
         整数はリストで与えられるため、リストの長さが個数であるとした。
 \end{itemize}
 
-これらの関数3つをMonad の \verb/>>=/ によってメタ計算を含む関数呼び出しとして実行する。
-3つの関数を実行する関数が numberCount 関数であり、この関数がプログラム本体である。
-numberCount を実行すると \ref{txt:delta_example_result}のような結果が得られる。
+ここで numberFilter 関数の定義を変更し、素数による絞り込みから偶数による絞り込みにする。
+変更後の numberCount プログラムをリスト\ref{src:numberCount2}に示す。
+
+\begin{table}[html]
+    \lstinputlisting[label=src:numberCount2, caption= numberCount バージョン2] {src/numberCount2.hs}
+\end{table}
+
+変更は下線の部分で、filter する条件を isPrime から even とした。
+
+ numberCount プログラムを Delta によって変更も含めて記述する(リスト \ref{src:delta_example})。
+
+\begin{table}[html]
+    \lstinputlisting[label=src:delta_example, caption=Deltaを用いたプログラムの例] {src/delta_example.hs}
+\end{table}
+
+変更が無い関数 generator と count の値はバージョン1であることを示すために Mono を用いる。
+変更が存在する numberFiler 関数は Delta を用いて2種類の処理を保存している。
+それぞれのプログラムに対応する部分は下線で示した部分である。
+
+これらの関数3つをMonad の \verb/=<</ によってメタ計算を含む関数呼び出しとして実行する。
+中置関数 \verb/=<</ は \verb/>>=/ の左右のオペランドを交換したものである。
+2つのバージョンを含めた numberCount を実行すると \ref{txt:delta_example_result}のように、全てのバージョンの結果が得られる。
 
 \begin{table}[html]
     \lstinputlisting[label=txt:delta_example_result, caption=numberCountプログラムの実行結果] {src/delta_example_result.txt}
 \end{table}
 
-これはnに1000を与えた結果である。
+これは numberCount プログラムに1000を与えた結果である。
 バージョン1の時は素数の数を求めるため計算結果は168であり、バージョン2の時は偶数の数を求めるために計算結果は500となる。
+Delta によりプログラムの変更を表現し、かつ同時に実行することができた。
 
-3つの関数で構成されたプログラムに対して1つの変更を加えたプログラムを表現することができた。
-つまり、Monad によってプログラムの変更をメタ計算として定義できたと言える。
-
-Haskell において実装した Delta Monad はプログラムの変更を含めた計算もメタ計算としてHaskellで実行する。
-これはプログラムの変更からどのような処理を導くかをメタ計算として Haskell で実行可能であることを意味する。
+なお、Delta Monad はプログラムの変更に対する計算もメタ計算としてHaskellで実行している。
+よってメタ計算を変更することで、変更に対する計算を任意に定義し実行する可能となった。
 つまり、図\ref{fig:non_delta_example}のようにプログラムにおいてバージョンが変わるごとにバージョン間の関係が存在しない状態から、図\ref{fig:delta_example}のようにプログラムの変更を含めてプログラムを実行可能となったことを意味する。
 メタ計算を変更することでプログラムの実行時にバージョン間の挙動の比較することも可能となる。
 
@@ -212,16 +229,14 @@
 
 % }}}
 
-% プログラムの変更に対するメタ計算の例 {{{
+% Delta を用いた信頼性向上 {{{
 
-\section{プログラムの変更に対するメタ計算の例}
+\section{Delta を用いた信頼性向上}
 \label{section:delta_merit}
 \ref{section:delta_example}節ではプログラムの変更に対して、変更前と変更後の挙動を保存した例を述べた。
-\ref{section:delta_merit}節ではプログラムの変更に対するメタ計算の例を述べる。
+プログラムの変更形式化することによって可能となる信頼性向上手法について\ref{section:delta_merit}節で述べる。
 
-まず最初に挙げられるものがプログラムの変更を保存するメタ計算である。
-これは Delta Monad として実際に定義できた。
-プログラムの変更を保存した場合、以下のような計算可能となる。
+プログラムの変更を保存することで、以下のようなことが可能となる。
 
 \begin{itemize}
 
@@ -285,9 +300,8 @@
 この機構を言語処理系に組込むことにより、言語の仕様にプログラムの変更方法も含めることができる。
 例えば、プログラムの変更は許可されたオペレーション内で行なうといった制約を加えることが可能となる。
 さらにユーザによりプログラムの変更に対するメタ計算を自由に定義できるような言語処理系を作るとする。
-その処理系ではこれまでに挙げた全てのメタ計算の例から使いたい機能を選んだり自分で追加することが可能となる。
+その処理系ではこれまでに挙げた全てのメタ計算の例を自由に使用、追加することが可能となる。
 
-このように、プログラムの変更を形式化することで多くのメタ計算が扱えるようになる。
-さらに、メタ計算の内容によっては信頼性の向上に用いたり変更も含めた上でプログラムを作成することが可能になる。
+このように、プログラムの変更を形式化し、変更に基いたメタ計算を定義することで信頼性を向上できる。
 
 % }}}
--- a/paper/future.tex	Wed Feb 18 11:10:19 2015 +0900
+++ b/paper/future.tex	Wed Feb 18 12:26:17 2015 +0900
@@ -1,20 +1,16 @@
 \chapter{まとめと今後の課題}
-本研究ではプログラムの変更を Monad を用いて形式化した。
-特にプログラミング言語 Haskell において Delta Monad としてプログラムの変更を保存するメタ計算を実装した。
-変更を保存するメタ計算により、複数のバージョンを持つプログラムを表現でき、複数のバージョンを持つプログラムを同時に実行した。
-加えて Delta Monad は DeltaM を用いて Monad と組み合せることができる。
-DeltaM を用いたプログラムでは複数のバージョンを持つプログラムがそれぞれどのような過程で実行されたかのトレースを得ることができた。
-トレースを比較することにより、デバッグやテストに有用な情報を提供することができる。
-さらに Delta と DeltaM が Monad 則を満たすことを Agda において証明した。
+本研究ではプログラムの変更を Monad を用いて形式化した Delta Monad を提案した。
+Delta Monad の実装例として Haskell におけるメタ計算でプログラムの変更を定義した。
+Delta Monad により、複数のバージョンを持つプログラムを表現し、全てのバージョンを同時に実行した。
+加えてデータ型 DeltaM を定義することで、Delta Monad が他の Monad と組み合せられることを示した。
+例として Writer Monad を組み合せることで複数のバージョンを同時に実行しながら個々のトレースを得た。
+トレースを比較することにより、デバッグやテストに有用な情報を提供できることを示した。
+また、定義した Delta と DeltaM が Monad 則を満たすことを Agda において証明した。
 
-今後の課題は大きく分けて2つが挙げられる。
-まず1つめはメタ計算のさらなる定義である。
-本研究ではプログラムの変更に対応するメタ計算として過去のプログラムを保存するメタ計算を提案した。
-そのメタ計算は Delta Monad として実装し、さらにメタ計算を行なう場合は Monad との組み合せとした。
-今回例として挙げた Monad は Writer のみであるが、他にも信頼性の向上に用いることができる Monad があると思われる。
-例えば変更に制約を加えるメタ計算や、バージョン毎による IO の切り分け、バージョン間の互換性などがあると考えている。
+課題として挙げられるのは Delta Monad により表現可能な変更の定義である。
+プログラムに対する可能な変更を全て Delta Monad で表現可能である証明は行なっていない。
+証明可能かを確認し、不可能ならば Delta Monad により表現できる変更を定義する。
 次に、 category theory によるプログラムの変更に対する意味付けがある。
 category theory では category の構造から性質を導いたり、他の category への関連を導くことができる。
 プログラムの変更を Monad として表した時に持つ意味や、 category が持つ有益な性質をプログラムに適用したい。
 特に、複数のプログラムを同時に実行するのは product に、全てのプログラムを生成できる Delta 全体を表す集合は colimit に関連があると考えている。
-% TODO 本当に Delta で任意の変更を表わすことができるのか
--- a/paper/introduction.tex	Wed Feb 18 11:10:19 2015 +0900
+++ b/paper/introduction.tex	Wed Feb 18 12:26:17 2015 +0900
@@ -1,18 +1,15 @@
 \chapter{プログラムの変更の形式化}
 \label{chapter:introduction}
-
-本研究ではプログラムの信頼性の向上を目標とする。
-
 プログラムの信頼性とはプログラムが正しく動く保証性であり、信頼性は多くの原因により損なわれる。
-例えば未定義の挙動によりプログラムが停止することやプログラム内の誤った条件式による誤った計算結果、実行環境やパラメタの変化による誤動作などがある。
+例えば未定義の挙動によりプログラムが停止すること、プログラム内の誤った条件式による誤った計算結果、実行環境やパラメタの変化による誤動作などがある。
 プログラムの変更は信頼性を低下させるきっかけとなる。
-変更を形式化することでプログラムの信頼性の変化を指摘し、プログラムの信頼性を向上させる。
+変更を形式化することでプログラムの信頼性の変化を指摘する。
 
 プログラムの変更の形式化には Monad を用いる。
 プログラムにおけるMonad とはデータ構造とメタ計算の対応である~\cite{Moggi:1991:NCM:116981.116984}。
-プログラムの変更をメタ計算として定義することで、プログラムの変更そのものを計算として実行する。
-変更を計算可能にすることで、信頼性の解析に利用可能な機構を計算として定義できる。
+プログラムの変更をメタ計算として定義することで、プログラムの変更そのものを計算可能にする。
+メタ計算として信頼性の解析に利用可能な機構を定義することで、信頼性を保ちながらソフトウェアを開発できることを示す。
 例えば、プログラムが変更された際に変更前と変更後のプログラムの挙動を比較する機構を提供できる。
-もし挙動の変化が望ましくない場合、信頼性が損なわれる変更だと変更時に判定できる。
-このように、プログラムの変更に対するメタ計算を定義することで信頼性を保ちながら開発することが可能となる。
-本研究ではプログラムの変更をメタ計算として定義し、それがMonad則を満たすこと証明支援系Agda~\cite{agda}により証明する。
+また、定義したメタ計算の Monad と対応を保証するために、メタ計算が Monad則を満たすこと証明支援系Agda~\cite{agda}により証明する。
+加えて他の Monad との組み合せが可能であることも証明する。
+
Binary file paper/main.pdf has changed
--- a/paper/proof_delta.tex	Wed Feb 18 11:10:19 2015 +0900
+++ b/paper/proof_delta.tex	Wed Feb 18 12:26:17 2015 +0900
@@ -310,8 +310,7 @@
         よって \verb/Delta (Delta (Delta A))/から \verb/Delta A/ とする演算の等式となる。
 
         バージョンが1である場合はやはり同じ項に簡約される。
-        しかしバージョンが1以上である場合は複雑な式変形を行なう。
-        こちらでも部分的な証明\verb/delta-fmap-mu-to-tail/ を定義し、$ \mu $ が適用できない項を変形している。
+        しかしバージョンが1以上である場合は複雑な式変形を行うため、部分的な証明\verb/delta-fmap-mu-to-tail/ を定義し、$ \mu $ が適用できない項を変形している。
 
         \verb/delta-fmap-mu-to-tail/ に加え、 $ \mu $ が natural transformation であることを利用して再帰的に定義し証明した。
 
--- a/paper/src/delta_example.hs	Wed Feb 18 11:10:19 2015 +0900
+++ b/paper/src/delta_example.hs	Wed Feb 18 12:26:17 2015 +0900
@@ -1,21 +1,16 @@
-module Example.Delta where
-
-import Data.Numbers.Primes
-import Delta
-
 generator :: Int -> Delta [Int]
 generator x = let intList = [1..x] in
-                  return intList
+                  Mono intList
 
 numberFilter :: [Int] -> Delta [Int]
-numberFilter xs = let primeList = filter isPrime xs
-                      evenList  = filter even xs    in
+numberFilter xs = let primeList = @ {\underline {filter isPrime}} $ _1 $ @ xs
+                      evenList  = @ {\underline {filter even}} $ _2 $ @ xs    in
                   Delta evenList (Mono primeList)
 
 count :: [Int] -> Delta Int
 count xs = let primeCount = length xs in
-           return primeCount
+           Mono primeCount
 
 numberCount :: Int -> Delta Int
-numberCount x = generator x >>= numberFilter >>= count
+numberCount x = count =<< numberFilter =<< generator x
 
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/paper/src/numberCount1.hs	Wed Feb 18 12:26:17 2015 +0900
@@ -0,0 +1,11 @@
+generator :: Int  -> [Int]
+generator x     = [1..x]
+
+numberFilter :: [Int]  -> [Int]
+numberFilter xs = filter @ {\underline {isPrime}} $ _1 $ @ xs
+
+count :: [Int] -> Int
+count xs        = length xs
+
+numberCount :: Int -> Int
+numberCount x = count (numberFilter (generator x))
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/paper/src/numberCount2.hs	Wed Feb 18 12:26:17 2015 +0900
@@ -0,0 +1,11 @@
+generator :: Int  -> [Int]
+generator x     = [1..x]
+
+numberFilter :: [Int]  -> [Int]
+numberFilter xs = filter @ {\underline {even}} $ _2 $ @ xs
+
+count :: [Int] -> Int
+count xs        = length xs
+
+numberCount :: Int -> Int
+numberCount x = count (numberFilter (generator x))