# HG changeset patch # User Yasutaka Higa # Date 1424071482 -32400 # Node ID 5f0e13923cfd96429ff45ca6a5f85a3ba211a98f # Parent 398b42a1ac19b85a9c3ca0b15b232582e82f53f9 Fixes diff -r 398b42a1ac19 -r 5f0e13923cfd agda.tex --- a/agda.tex Mon Feb 16 15:05:11 2015 +0900 +++ b/agda.tex Mon Feb 16 16:24:42 2015 +0900 @@ -5,7 +5,7 @@ functional programming において、あるデータ型と対応する計算が Functor 則を満たすかの保証は言語の実装に依存している。 例えば、 Haskell において functor は型クラスによって提供されるため、型レベルのチェックを行なう。 そのため、型チェックは通るが Functor 則を満たさない functor が定義できてしまう。 -よって Haskell において Delta Monad を定義しただけでは証明が存在しない。 +よって Haskell において Delta Monad を定義しただけでは Delta Monad が Monad であるかの証明が存在しない。 そこで証明支援系言語 Agda を用いて、 Delta が Functor 則と Monad 則を満たすことを証明する。 第\ref{chapter:agda}章は Agda における証明手法について述べる。 @@ -53,10 +53,11 @@ \end{prooftree} そうすると、仮定 A は dead となり、新たな命題 $ A \Rightarrow B $ を導くことができる。 -A という仮定に依存して B を導く証明から、A が存在すれば B が存在するという証明を導いたこととなる。 +A という仮定に依存して B を導く証明から、「A が存在すれば B が存在する」という証明を導いたこととなる。 このように、仮定から始めて最終的に全ての仮定を dead とすることで、仮定に依存しない証明を導くことができる。 +なお、dead な仮定は \verb/[A]/ のように \verb/[]/ で囲んで書く。 -alive な仮定を dead にすることができるのは $ \Rightarrow I $ 規則のみである。 +alive な仮定を dead にすることができるのは $ \Rightarrow \mathcal{I} $ 規則のみである。 それを踏まえ、 natural deduction には以下のような規則が存在する。 \begin{itemize} @@ -209,18 +210,18 @@ まず、「A は B であり」から、Aから性質Bが導けることが分かる。これが $ A \Rightarrow B $ となる。 次に、「B は C である」から、Bから性質Cが導けることが分かる。これが $ B \Rightarrow C $ となる。 そしてこの2つは同時に成り立つ。 -よって $ (A \Rightarrow B) \land (B \Rightarrow C)$ が前提となる。 -この条件2つが成り立つ時に「Aは Cである」が成りたつ。 -条件と同じように「A は C である」は、 $ A \Rightarrow C $ と書けるため、証明するべき論理式は $ ((A \Rightarrow B) \land (B \Rightarrow C)) \Rightarrow (A \Rightarrow C) $ になる。 +よって $ (A \Rightarrow B) \land (B \Rightarrow C)$ が仮定となる。 +この仮定が成り立つ時に「Aは Cである」を示せば良い。 +仮定と同じように「A は C である」は、 $ A \Rightarrow C $ と書けるため、証明するべき論理式は $ ((A \Rightarrow B) \land (B \Rightarrow C)) \Rightarrow (A \Rightarrow C) $ となる。 証明の手順はこうである。 -まず条件$ (A \Rightarrow B) \land (B \Rightarrow C)$とAを2つ仮定する。 +まず条件$ (A \Rightarrow B) \land (B \Rightarrow C)$とAの2つを仮定する。 条件を $ \land 1 \mathcal{E} $ $ \land 2 \mathcal{E} $ により分解する。 -A と $ A \Rightarrow B$ から B を、 B から $ B \Rightarrow C $ から C を導く。 +A と $ A \Rightarrow B$ から B を、 B と $ B \Rightarrow C $ から C を導く。 ここで $ \Rightarrow \mathcal{I} $ により $ A \Rightarrow C $ を導く。 この際に dead にする仮定は A である。 -そのために $_{(1)} $ と対応する \verb/[]/の記号に数値を付けてある。 -これで残る仮定は $ (A \Rightarrow B) \land (B \Rightarrow C)$ となり、これから $ A \Rightarrow C $ を導くことができたためにさらに $ \Rightarrow \mathcal{I} $ を適用する。 +数回仮定を dead にする際は $_{(1)} $ のように対応する \verb/[]/の記号に数値を付ける。 +これで残る alive な仮定は $ (A \Rightarrow B) \land (B \Rightarrow C)$ となり、これから $ A \Rightarrow C $ を導くことができたためにさらに $ \Rightarrow \mathcal{I} $ を適用する。 結果、証明すべき論理式$ ((A \Rightarrow B) \land (B \Rightarrow C)) \Rightarrow (A \Rightarrow C) $ が導けたために証明終了となる。 % }}} @@ -257,7 +258,7 @@ しかし、 x を取って x を返す関数は定義することはできる。 これは natural deduction の $ \Rightarrow \mathcal{I} $ により仮定を discharge することに相当する。 -このように、 natural deduction における証明はそのまま 型付き $ \lambda $ 計算にエンコードすることができる。 +このように、 natural deduction における証明はそのまま 型付き $ \lambda $ 計算に変換することができる。 それぞれの詳細な対応は省略するが、表\ref{tbl:curry_howard_isomorphism} のような対応が存在する。 @@ -275,7 +276,7 @@ \end{table} \end{center} -\ref{section:natural_deduction}節でも行なった三段論法の証明を Haskell により行なうとリスト\ref{src:modus_ponens} +\ref{section:natural_deduction}節でも行なった三段論法の証明を Haskell により行なうとリスト\ref{src:modus_ponens}となる。 \begin{table}[html] \lstinputlisting[label=src:modus_ponens, caption=Haskell における三段論法の証明] {src/modus_ponens.txt} @@ -306,7 +307,7 @@ \label{section:agda} \ref{section:curry_howard_isomorphism}節において型を用いて証明を行なう手法を述べた。 しかし、Haskell における型システムは証明を記述するために用いるものではない。 -よって、依存型を持つ証明支援言語 Agda を用いて証明を記述していく。 +よって、依存型を持つ証明支援言語 Agda を用いて証明を記述する。 依存型とは値に依存した型を作ることができる型であり、非常に表現能力が高い。 値に型を使うことができるために証明に基づいた証明を記述することができる。 @@ -346,18 +347,19 @@ \end{table} 関数の定義時に \verb/_/ とした部分には項を入れることで関数が適用される。 -つまり \verb/_x_/ とすれば中置関数を作成することができる。 -データ型 \verb/_x_/ は型 A と B を持つ型である。 -データ型 \verb/_x_/ はコンストラクタ \verb/<_,_>/ により構成され、コンストラクタは A と B を取ることで \verb/A x B/ 型を返す。 +つまり \verb/_/$ \times $\verb/_/ とすれば中置関数を作成することができる。 +データ型 \verb/_/$ \times $\verb/_/ は型 A と B を持つ型である。 +データ型 \verb/_/$ \times $\verb/_/ はコンストラクタ \verb/<_,_>/ により構成され、コンストラクタは A と B を取ることで $ A \times B $ 型を返す。 例えば型A と B から 直積型 $ A \times B $ が作成できる証明は constructProduct である。 -任意の型AとBを受けとり、コンストラクタ \verb/<_,_>/を用いて $ A \times B $ に相当する \verb/A x B/を返す。 +任意の型AとBを受けとり、コンストラクタ \verb/<_,_>/を用いて $ A \times B $ に相当する値を返す。 -また、型に対応するコンストラクタはパターンマッチにより分解することができる。 +また、コンストラクタは引数にてパターンマッチにより分解することができる。 その例が patternMatchProduct である。 -受けとる引数の型は \verb/ A x B/ であるため、ありえるコンストラクタは \verb/<_,_>/のみである。 -よって引数を取る際に \verb/< a , b >/ のように対応するコンストラクタと変数を用意することで、コンストラクタに基づいて型を分解することができる。 -\verb/A x B/ 型から B を取るため、\verb/A x B/ 型の変数を直接束縛せずにコンストラクタで分解し、a と b に束縛することで A と B が得られる。 +受けとる引数の型は $ A \times B $ であるため、ありえるコンストラクタは \verb/<_,_>/のみである。 +よって引数を取る際に \verb/< a , b >/ のように対応するコンストラクタと変数を用意することで、コンストラクタに基づいて値を分解することができる。 +$ A \times B$ 型から B を取るために、$ A \times B$ 型の引数を変数にを直接束縛せずにコンストラクタで分解し、a と b に束縛することで A と B を得る。 +b を返すことで型 B の値を返すことができる。 そのため、 patternMathProduct は $ \land 2 \mathcal{E} $ そのものである。 % }}} @@ -412,7 +414,7 @@ 加算は中置関数 \verb/_+_/ として定義する。 2つの Nat を取り、Natを返す。 -パターンマッチにより処理を変える。 +関数 \verb/_+_/ はパターンマッチにより処理を変える。 0に対して m 加算する場合は m であり、 n の後続数に対して m 加算する場合は n に m 加算した数の後続数とする。 S を左の数から右の数へ1つずつ再帰的に移していくような加算である。 @@ -424,7 +426,7 @@ \begin{table}[html] \lstinputlisting[label=src:equiv, caption= Relation.Binary.Core による等式を示す型 $ \equiv $] {src/equiv.agda.replaced} \end{table} -等式は等式を示すデータ型 $ \equiv $ により定義される。 +Agda において等式は、等式を示すデータ型 $ \equiv $ により定義される。 $ \equiv $ は同じ両辺が同じ項に簡約される時にコンストラクタ refl で構築できる。 実際に 3 + 1 = 4 の証明は refl で構成できる(リスト\ref{src:three_plus_one})。 @@ -476,9 +478,10 @@ この2つの証明はこのような意味を持つ。 n が 0 であるとき、 m も 0 なら簡約により等式が成立する。 - n が 0 であるとき、 m が 0 でないとき、 m は後続数である。 + n が 0 であり、 m が 0 でないとき、 m は後続数である。 よって m が (S x) と書かれる時、 x は m の前の値である。 前の値による交換法則を用いてからその結果の後続数も + の定義により等しい。 + ここで、 \verb/addSym/ に渡される m は1つ値が減っているため、最終的には n = 0, m = 0 である refl にまで簡約され、等式が得られる。 \item n = S n, m = O @@ -527,8 +530,6 @@ これで等式 $ (S m) + (S n) \equiv (S n) + (S m) $ の証明が完了した。 自然数に対する + の演算を考えた時にありえるコンストラクタの組み合せ4パターンのいずれかでも交換法則の等式が成り立つことが分かった。 -また、定義した + の演算のみでは加法の交換法則は証明できず、さらに等式を証明する必要があった。 - このように、Agda における等式の証明は、定義や等式を用いて右辺と左辺を同じ項に変形することで行なわれる。 % }}} diff -r 398b42a1ac19 -r 5f0e13923cfd category.tex --- a/category.tex Mon Feb 16 15:05:11 2015 +0900 +++ b/category.tex Mon Feb 16 16:24:42 2015 +0900 @@ -36,14 +36,14 @@ \begin{itemize} \item 全ての object について identity mapping が存在する - identity mapping とは domain と codomain が同じ morphism のことである。 - identity mappping は id と略する。 + identity mapping とは domain と codomain が同じobject を指す morphism のことである。 + identity mapping は id と略する。 id は全ての object に存在するため、 object A に対する id は $ id_A $ と書く。 \item 同じ obejct が domain と codomain になっている2つのmorphismは合成することができ、合成の順番は結果に影響しない。 morphism の合成には記号 $ \circ $ を用いる。 - object B から C への morpshim f と object A から B への morphism g があった時、 f と g を合成すると式\ref{exp:morphism_compose}となる。 + object B から C への morphism f と object A から B への morphism g があった時、 f と g を合成すると式\ref{exp:morphism_compose}となる。 \begin{equation} f \circ g : A \rightarrow C @@ -61,7 +61,7 @@ \end{eqnarray} \end{itemize} -例えば、object A,B と A から B への moprhism を持つ category は図\ref{fig:simple_category}のようになる。 +例えば、object A,B と A から B への morphism を持つ category は図\ref{fig:simple_category}のようになる。 \begin{figure}[htbp] \begin{center} @@ -73,7 +73,7 @@ なお、id は全ての object に存在するために省略して書くことが多いため、これからは省略する。 -object を点、morphism を線とした図を commutative diagram (可換図式) と呼ぶ。 +object を点、morphism を矢印とした図を commutative diagram (可換図式) と呼ぶ。 ある object から object への morphism の合成の path に関わらず結果が同じである時、その図を commutative (可換)と呼ぶ。 例えば、式\ref{exp:morphism_composition_law}の category の commutative diagram は図\ref{fig:morphism_composition_law}のようになる。 @@ -86,7 +86,7 @@ \end{figure} -commutative diagram が commutative である時、moprhism の合成順序が異なっても結果が同じであることを利用して等価性の証明を行なうことを diagram chasing と呼ぶ。 +commutative diagram が commutative である時、morphism の合成順序が異なっても結果が同じであることを利用して等価性の証明を行なうことを diagram chasing と呼ぶ。 ある性質を category に mapping し、diagram chasing を用いて証明を導くことで性質を解析していく。 % }}} diff -r 398b42a1ac19 -r 5f0e13923cfd delta.tex --- a/delta.tex Mon Feb 16 15:05:11 2015 +0900 +++ b/delta.tex Mon Feb 16 16:24:42 2015 +0900 @@ -10,10 +10,10 @@ \section{Delta Monad の定義} まずはプログラムを定義する。 -プログラムは型付けされた値と、値を値へと写像する関数のみで構成されるものとする。 +プログラムは型付けされた値と、値を値へと写像する関数のみで構成される。 プログラムの実行は関数の値への適用とする。 -入出力といった、値や関数で表現できない計算はメタ計算とする。 -メタ計算をある性質を持つデータ構造に対応させ、メタ計算が必要な関数は値をデータ構造へと写像することで入出力といった処理を実現する。 +入出力といった、値や関数のみで表現できない計算はメタ計算とする。 +メタ計算を特定のデータ構造に対応させ、メタ計算が必要な関数は値をデータ構造へと写像することで入出力といった処理を実現する。 メタ計算とデータ構造の対応に用いる性質が Monad である。 例えば、失敗する可能性があるメタ計算 T は式\ref{exp:partiality}のように定義できる。 @@ -24,11 +24,10 @@ \end{equation} 型 A の値に対応するメタ計算 T は、A と $ \bot $ の論理和として表現できる。 -成功した際は A を返し、失敗した場合は $ \bot $ を返す。 +計算に成功した際は A を返し、失敗した場合は $ \bot $ を返す。 -ここで、失敗しない前提で作成されたプログラムに対して、失敗する可能性を表現するメタ計算を対応させるとする。 -プログラムは型付けされた値と、関数の組み合せで構成される。 -例えば、型 A の値x と、型 A の値を取り型 B の値を返す関数f, 型B の値を取り型Cの値を返す関数g によって構成されるとする(式\ref{exp:non_failure_program})。 +ここで、失敗しない前提で作成されたプログラムに対して、失敗する可能性を表現するメタ計算を対応させる。 +プログラムは型 A の値x と、型 A の値を取り型 B の値を返す関数f, 型B の値を取り型Cの値を返す関数g によって構成されるとする(式\ref{exp:non_failure_program})。 \begin{equation} g ( f ( x )) @@ -37,14 +36,14 @@ ここで関数f は失敗する可能性があるとする。 その時、f が失敗した場合の計算を考える必要がある。 -計算の実現方法はいくつか存在する。 -計算g に失敗の判断を追加したり、例外機構により失敗を補足することで呼び出し元の関数で行なうことで実現できる。 +この計算の実現方法はいくつか存在する。 +計算g に失敗の判断を追加したり、例外機構により失敗を補足することで呼び出し元の関数で判断するなどがある。 実現方法の1つとして、 Monad を用いたメタ計算がある。 Monad により失敗した際の計算をメタ計算としてデータ構造に紐付ける。 式\ref{exp:partiality} で定義したように、計算の成功は型 A 値を返し、失敗は $ \bot $ を返す。 計算に失敗した際に対応するメタ計算を定義し、関数をそのメタ計算で拡張することで失敗に対する処理が実現できる。 -例えば、 A に対してはそのまま関数の適用を行ない、 $ \bot $ に対しては $ \bot $ を返すようなメタ計算を定義することで、計算が失敗した時に計算を終了することが実現できる。 +例えば、 A に対してはそのまま関数の適用を行ない、 $ \bot $ に対しては $ \bot $ を返すようなメタ計算を定義することで、計算が失敗した時に計算を終了することができる。 型A を持つx の値をメタ計算と対応して型 T A とした値を x' 、メタ計算による関数の拡張を * と記述すると、式\ref{exp:non_failure_program} の式は式\ref{exp:failure_program} のように書ける。 @@ -57,22 +56,21 @@ メタ計算が無い関数 $ f $ とメタ計算を持つ関数 $ f^{*} $ が1対1に対応することは Monad により保証されている。 このように、値と関数で表されたプログラムにおいてメタ計算を用いることで、計算を拡張することができる。 -プログラムの変更をメタ計算として記述することを考える。 +プログラムとメタ計算の関係としての Monad について述べたところで、プログラムの変更をメタ計算として記述することを考える。 -ここで、プログラムの変更とは関数や値が変更されることであり、変更される量には単位がある。 +プログラムの変更とは関数や値が変更されることであり、変更される量には単位がある。 最初の変更単位をバージョン1とし、変更された後のプログラムはバージョンが1増加する。 任意の型Aに対するメタ計算Tを考えた時、プログラムの変更は式\ref{exp:meta_computation_definition}のように定義する。 \begin{equation} - T A = V A + T A = V_A \label{exp:meta_computation_definition} \end{equation} -V はプログラムの全てバージョンの集合であり、V AとすることでAに対応する値の集合を返すものとする。 +V はプログラムの全てバージョンの集合であり、$ V_A $ とすることでAに対応する値の集合を返すものとする。 -ここで、プログラムが変更される際に過去のバージョンのプログラムも保存するメタ計算を提案する。 -全ての変更単位で変更されたプログラムを保存し、それらを比較することでプログラムの変更を表現しようと考えた。 -このメタ計算を表す Monad を Delta Monad と呼ぶ。 +式\ref{exp:meta_computation_definition}のメタ計算として、全ての変更単位で変更されたプログラムを保存する計算を提案する。 +このメタ計算を Delta Monad と呼ぶ。 なお、この Delta Monadが Monad であることの証明は \ref{chapter:proof_delta} 章で行なう % }}} @@ -116,7 +114,7 @@ 関数 return は任意の型aを受けとり、メタ計算と対応された型に対応させて返す。 \verb/>>=/ は中置関数であり、left operand と right operand を取る。 -left operand であるメタ計算と対応された値と、right operand であるメタ計算と対応された値を返す関数を取り、メタ計算を行ないながら関数を適用する。 +left operand にメタ計算と対応された値と、right operand にメタ計算と対応された値を返す関数を取り、メタ計算を行ないながら関数を適用する。 データ型 Delta に対応するメタ計算を Monad を用いてリスト\ref{src:delta_instance_monad}のように定義する。 @@ -133,7 +131,9 @@ \item 中置関数 \verb/>>=/ - メタ計算を含んだ関数の適用であるため、値と関数の同じバージョンを計算して返すものとなる。 + メタ計算を含んだ関数の適用である。 + 通常の関数の適用に加え、バージョンを含んだ計算も行なう。 + 値と関数のそれぞれにおいて同じバージョン選択し、関数を適用する。 もしバージョン1であった場合はコンストラクタは Mono であるため、Mono が持っている値に対して関数を適用することとなる。 もしバージョンが1で無い場合のコンストラクタは Delta であるため、先頭の値を用いて計算し、残りの値と結合することとなる。 その際、先頭の値を取り出すために headDelta 関数を、先頭以外の値を取り出すために tailDelta 関数を用いる。 @@ -194,7 +194,7 @@ Haskell において実装した Delta Monad はプログラムの変更を含めた計算もメタ計算としてHaskellで実行する。 これはプログラムの変更からどのような処理を導くかをメタ計算として Haskell で実行可能であることを意味する。 つまり、図\ref{fig:non_delta_example}のようにプログラムにおいてバージョンが変わるごとにバージョン間の関係が存在しない状態から、図\ref{fig:delta_example}のようにプログラムの変更を含めてプログラムを実行可能となったことを意味する。 -例えば、プログラムの実行時にバージョン間の挙動の比較することで過去の挙動との差異を指摘することなどが可能となる。 +メタ計算を変更することでプログラムの実行時にバージョン間の挙動の比較することも可能となる。 \begin{figure}[htbp] \begin{center} @@ -223,7 +223,7 @@ まず最初に挙げられるものがプログラムの変更を保存するメタ計算である。 これは Delta Monad として実際に定義できた。 -プログラムの変更を保存した場合、以下のような方法により信頼性の向上が見込めると考える。 +プログラムの変更を保存した場合、以下のような計算可能となる。 \begin{itemize} @@ -231,10 +231,10 @@ プログラムの変更列から任意のバージョン2つを取り出し、同時に実行するプログラムを構成する。 プログラムを同時に実行することで以下のようなメリットがある。 - なお、任意の要素の組み合せは category において product として表現されるため、 product と対応があると考えている。 + なお、任意の要素どうしの組み合せは category において product として表現されるため、 product と対応があると考えている。 \begin{itemize} - \item 実行系とサブの実行系を実行することができる。 + \item 実行系とサブの実行系を実行する 例えば、あるバージョンでリリースしたプログラムがあるとする。 変更を加え、ベータ版としてリリースしたいが動作が不安定である。 @@ -245,7 +245,7 @@ 異なるバージョン間でプロトコルに互換が無いプログラムを考える。 バージョン間の互換を含めてメタ計算として定義し、全てのバージョンに対して互換を持つプログラムを構築する。 - そうすることによりどのバージョンのプロトコルとも互換を持つような変換器を作成できる。 + そうすることで、どのバージョンのプロトコルとも互換を持つような変換器を作成できる。 \end{itemize} @@ -258,8 +258,8 @@ \begin{itemize} \item 過去のバージョンの挙動を破壊する時を検出する - プログラムの変更の際、トレースを変えてはいけない部分が存在するとする。 - 変更の際にトレースが変更したことを検出することにより、トレースが保存される変更のみを受けつけるようにする。 + プログラムの変更の際、トレースを変えてはいけない部分を指定する。 + 変更の際にトレースが保存される変更のみを受けつけるようにする。 \item トレースが変化していないことを確認する @@ -284,8 +284,8 @@ \end{itemize} 他にもプログラムの変更そのものを処理するプログラムを定義することもできる。 -この機構を言語処理系に組込むことにより、プログラムの変更方法も言語の仕様に含めることができる。 -例えば、プログラムの変更は許可されたオペレーション内で行なうといった制約を含めることが可能となる。 +この機構を言語処理系に組込むことにより、言語の仕様にプログラムの変更方法も含めることができる。 +例えば、プログラムの変更は許可されたオペレーション内で行なうといった制約を加えることが可能となる。 さらにユーザによりプログラムの変更に対するメタ計算を自由に定義できるような言語処理系を作るとする。 その処理系ではこれまでに挙げた全てのメタ計算の例から使いたい機能を選んだり自分で追加することが可能となる。 diff -r 398b42a1ac19 -r 5f0e13923cfd delta_with_monad.tex --- a/delta_with_monad.tex Mon Feb 16 15:05:11 2015 +0900 +++ b/delta_with_monad.tex Mon Feb 16 16:24:42 2015 +0900 @@ -24,15 +24,15 @@ データ型 DeltaM は2つの型引数を持つ。 型引数a と型引数を持つ型引数 m である。 -m に対して a を適用した型を持つ DeltaM から DeltaM コンストラクタを用いて DeltaM 型を構成できる。 +m が Monad であり、 a が Monad が内包する型を表す。 +m a 型を内部に持つ Delta から DeltaM コンストラクタを用いて DeltaM 型を構成できる。 型名とコンストラクタ名が同一になっているので注意が必要である。 -m が Monad であり、 a が Monad が内包する型を表す。 次にいくつかの関数を定義する。 unDeltaM は DeltaM から Delta へと戻す関数である。 -headDeltaM はDelta から先頭の値を取り出す。 +headDeltaM はDeltaM から先頭の値を取り出す。 バージョン管理された Delta から最新のバージョンを取り出すことに相当する。 -tailDeltaM はDelta から先頭の値を取り除く。 +tailDeltaM はDeltaM から先頭の値を取り除く。 これはバージョン管理された Delta から最新以外のバージョンに対して処理を行う時に用いる。 DeltaM の instance 定義では \verb/>>=/ ではなく mu を介して行なう。 @@ -83,12 +83,12 @@ \lstinputlisting[label=src:deltaM_example, caption= DeltaM を用いたプログラムの例] {src/deltaM_example.hs} \end{table} -Writer と組み合せた Delta を DeltaWithLog 型として定義する。 +Writer と組み合せた DeltaM を DeltaWithLog 型として定義する。 型の定義には type 構文を用い、ある型の別名として再定義する。 まず、 Writer で記録する型を String の List とし、その型を DeltaLog とする。 DeltaLog を内包する DeltaM として DeltaWithLog 型定義した。 -また、値をログとするために関数 returnW を定義した。 +また、値を文字列のログとするために関数 returnW を定義した。 これは通常の値から DeltaLog を生成するための関数である。 tell 関数を用いてログを Writer に書き込み、値を return で保持する。 diff -r 398b42a1ac19 -r 5f0e13923cfd functional_programming.tex --- a/functional_programming.tex Mon Feb 16 15:05:11 2015 +0900 +++ b/functional_programming.tex Mon Feb 16 16:24:42 2015 +0900 @@ -9,10 +9,9 @@ \section{Category} \label{section:category_in_program} \ref{section:monad}節では Monad の定義について述べた。 -これからプログラムにおける Monad について述べていく。 -そのために\ref{section:category_in_program}節はプログラムと category の対応について述べる。 +\ref{section:category_in_program}節はプログラムと category の対応について述べる。 -プログラムには値と関数のみが存在するとする。 +プログラムには値と関数のみが存在する。 任意の値は型付けられるとする。 変数x が型 A を持つ時、式\ref{exp:value_in_program}のように記述する。 @@ -32,7 +31,7 @@ そして、引数と返り値の型が等しい関数は関数結合できるとする。 関数結合の記号には $ \circ $ を用いる。 -例えば、 A を取り B を返す関数 f と B を取り C を返す関数 g の合成は式\ref{exp:function_compose_in_program}のようになる。 +例えば、 A を取り B を返す関数 f と、 B を取り C を返す関数 g の合成は式\ref{exp:function_compose_in_program}のようになる。 \begin{eqnarray} \label{exp:function_compose_in_program} @@ -49,11 +48,11 @@ \item 全ての object について identity mapping が存在する 任意の型 A に対し $ A \rightarrow A $ である関数 id が定義できれば identitiy mapping が存在することになる。 - 任意の型の値x を受けとり、その値を返す関数が id となる。 + 任意の型の値x を受けとり、その値をそのまま返す関数が id となる。 \item 同じ obejct が domain と codomain になっている2つのmorphismは合成することができ、合成の順番は結果に影響しない。 - morpshim は関数である。 + morphism は関数である。 つまり domain は引数の型であり、 codomain は返り値の型となる。 morphism の合成は関数合成に相当し、合成の順序によらず引数と返り値の型は同じとなる。 \end{itemize} @@ -97,19 +96,18 @@ そしてデータ型が functor であることを示すためには、 fmap という関数を定義すれば良いことが分かる。 fmap は型a から型bへの関数を取り、f a を取り f b を返す。 つまり、f でない型への演算をfの型においても適用するために変換する関数である。 -morpshim は関数であるため、 $ A \rightarrow B $ の morphism を $ F A \rightarrow F B $ へと mapping する役割を担っていることが分かる。 -よって morphism を morphism へと mapping することができるため functor となる。 +プログラムにおいて morpshim は関数であるため、fmap は $ A \rightarrow B $ の morphism を $ F A \rightarrow F B $ へと mapping する役割を担っている。 +なお、 fmap の型を \verb/ fmap :: (a -> b) -> ((f a) -> (f b))/ と読むことで、関数を受けとりfにおける関数に変換していることが分かりやすくなる。 また、fmap の型に $ f a $ が存在するように、 f は型を引数として受けとっている。 ここで object は型であるため、 $ A $ の object を $ F(A) $ への mapping する役割をf が担っていることが分かる。 よって型引数を持つ型f と対応する fmap を定義することにより functor が定義できる。 -なお、 fmap の型を \verb/ fmap :: (a -> b) -> ((f a) -> (f b))/ と読むことで、関数を受けとりfにおける関数に変換していることが分かりやすくなる。 functor の例として、型がInt である変数 x と Int から Bool を返す even 関数を考える。 -このプログラムがなす category C は object が Int であり、 morphism が show となる。 +このプログラムがなす category C は object が Int であり、 morphism が even となる。 category C を functor によって別の category に写すことができる。 -例えば List がなす category がある。 +例えば List がなす category Dがある。 まずHaskell において List を定義する。 List は任意の型 a を取り、 List a とする。 @@ -135,7 +133,6 @@ \lstinputlisting[label=src:exec_list_in_haskell, caption=Haskell における List の実行例] {src/exec_list_in_haskell.txt} \end{table} -なお、 Haskell において型Aを持つ値xは $ x :: A $ のように記述される。 x と even からなるプログラムから、型List と fmap を用いることにより List におけるプログラムでも同じように Bool が得られる。 これを通常のプログラムから List のプログラムへの functor とみなす。 @@ -176,10 +173,11 @@ natural transformationは図\ref{fig:natural_transformation}で示したような可換図が可換になるような t であった。 つまりある functor f と g があった時に、 f において morphism を適用してtを適用しても、t を適用してから g において morphism を適用しても結果が変わらないような t を提供できれば良い。 -プログラムにおける natural transformation は t は図\ref{fig:natural_transformation}を満たすような関数として表現される。 +プログラムにおける natural transformation t は図\ref{fig:natural_transformation}を満たすような関数として表現される。 Haskell において特定の関数が持つ性質を制約として記述することはできないため、Haskell において natural transformation の具体的な定義は存在しない。 List における natural transformation の例としては、List の先頭を除いた List を返す tail 関数がある(\ref{src:natural_transformation_in_haskell})。 +tail 関数を Functor List から Functor List への natural transformation とみなすのである。 \begin{table}[html] \lstinputlisting[label=src:natural_transformation_in_haskell, caption=List の先頭を除いた List を返す tail 関数] {src/natural_transformation_list.hs} @@ -252,18 +250,24 @@ List は nondeterminism (非決定性)を表現するデータ構造である。 List に対する演算を行なう際、結果としてありうる値を全て列挙することにより非決定性を表現しようとするものである。 -List において非決定性を表現する時、$ \eta $ は通常の値から List を構築する関数、 $ \mu $ は List の List から List を返す concat 関数となる。 -$ \mu $ で何故非決定性を表現できるかと述べる。 -まず、List a と、 a から List a を返す関数を考える。 -List a がありうる値の集合で、関数が値から取りうる値を計算して返すものだとする。 -List a に対して fmap することで、ありうる値に対して全ての取りうる値を計算することができる。 +List において非決定性を表現する時、$ \eta $ は値から長さ1の List を構築する関数、 $ \mu $ は List の List から List を返す concat 関数となる。 + +この $ \eta $ と $ \mu $ を用いて非決定性を表現する。 +List a はありうる値の集合であるとする。 +関数は値を取り、値から取りうる値をList として返す。 +この関数を List a に対して fmap することで、ありうる値に対して全ての取りうる値を計算することができる。 この際、 List a に対して a から List a を返す関数を適用するために List a を持つ List が構築される。 ネストされた List を、全ての取りうる値として通常の List に戻すために concat を用いる。 +concat することで、値と関数から全ての取りうる値が計算できた。 -ここで、Haskell における monad の型クラスを振り返る(リスト\ref{src:monad_class})。 +ここで concat は ネストした List から List への関数であるため、 $ TT A \rightarrow T A $ に相当する $ \mu $ となっている。 +$ \eta $ は長さ1の List を返すため、 $ A \rightarrow T A $ となっている。 +このように、非決定性演算は List データ型と $ \eta $ と $ \mu $ として Monad を用いて定義できる。 + +Haskell における monad の型クラスを振り返る(リスト\ref{src:monad_class})。 Haskell においては monad は Monad 型クラスとして提供されているが、$ \eta $ と $ \mu $ による記述はされていない。 これは、Haskell がメタ計算との対応として Kleisli Category の triple を採用しているからである。 -monad と Kleisli category は互いに同型であるために相互に変換することができる。 +monad と Kleisli triple は互いに同型であるために相互に変換することができる。 また、 category や program の文脈が変わることで $ \eta $ を unit と呼んだり、 $ \mu $ を join と呼んだり、 \verb/>>=/ を bind と呼んだりする。 しかし今までの解説には $ \eta $ と $ \mu $ を用いているために、このまま $ \eta $ と $ \mu $ で解説していくこととする。 @@ -275,7 +279,7 @@ では List を用いて非決定性を表現した例を示す。 -まずは List を monad とする(リスト\ref{src:list_monad})。 +まずは List を Monad 型クラスのインスタンスとする(リスト\ref{src:list_monad})。 \begin{table}[html] \lstinputlisting[label=src:list_monad, caption= Haskell における List に対する monad の定義] {src/list_monad.hs} diff -r 398b42a1ac19 -r 5f0e13923cfd future.tex --- a/future.tex Mon Feb 16 15:05:11 2015 +0900 +++ b/future.tex Mon Feb 16 16:24:42 2015 +0900 @@ -1,8 +1,8 @@ \chapter{まとめと今後の課題} 本研究ではプログラムの変更を Monad を用いて形式化した。 -特にプログラミング言語 Haskell において Delta Monad として変更を保存するメタ計算を実装した。 -変更を保存するメタ計算により、複数のバージョンを持つプログラムを表現でき、複数のバージョン同時に実行した。 -加えて Delta Monad は他の Monad と組み合せることができることを示すために DeltaM を定義した。 +特にプログラミング言語 Haskell において Delta Monad としてプログラムの変更を保存するメタ計算を実装した。 +変更を保存するメタ計算により、複数のバージョンを持つプログラムを表現でき、複数のバージョンを持つプログラムを同時に実行した。 +加えて Delta Monad は DeltaM を用いて Monad と組み合せることができる。 DeltaM を用いたプログラムでは複数のバージョンを持つプログラムがそれぞれどのような過程で実行されたかのトレースを得ることができた。 トレースを比較することにより、デバッグやテストに有用な情報を提供することができる。 さらに Delta と DeltaM が Monad 則を満たすことを Agda において証明した。 @@ -12,8 +12,8 @@ 本研究ではプログラムの変更に対応するメタ計算として過去のプログラムを保存するメタ計算を提案した。 そのメタ計算は Delta Monad として実装し、さらにメタ計算を行なう場合は Monad との組み合せとした。 今回例として挙げた Monad は Writer のみであるが、他にも信頼性の向上に用いることができる Monad があると思われる。 -例えば並列実行や、バージョン毎による IO の切り分け、バージョン間の互換性などがあると考えている。 +例えば変更に制約を加えるメタ計算や、バージョン毎による IO の切り分け、バージョン間の互換性などがあると考えている。 次に、 category theory によるプログラムの変更に対する意味付けがある。 -category theory は category の構造から性質を導いたり、他の category への関連を導くことができる。 +category theory では category の構造から性質を導いたり、他の category への関連を導くことができる。 プログラムの変更を Monad として表した時に持つ意味や、 category が持つ有益な性質をプログラムに適用したい。 特に、複数のプログラムを同時に実行するのは product に、全てのプログラムを生成できる Delta 全体を表す集合は colimit に関連があると考えている。 diff -r 398b42a1ac19 -r 5f0e13923cfd introduction.tex --- a/introduction.tex Mon Feb 16 15:05:11 2015 +0900 +++ b/introduction.tex Mon Feb 16 16:24:42 2015 +0900 @@ -4,14 +4,16 @@ 本研究ではプログラムの信頼性の向上を目標とする。 プログラムの信頼性とはプログラムが正しく動く保証性であり、信頼性は多くの原因により損なわれる。 -例えば仕様が未定義の挙動によってプログラムが停止したり、プログラム内の誤った条件式により計算結果が仕様と異なったり、実行環境やパラメタが変化した際に望まない動作が発生することなどがある。 -信頼性を低下させる原因が増えるタイミングの多くはプログラムを変更した時である。 -よって、プログラムの変更を形式化することにより、プログラムの信頼性が損なわれる変更を定義する。 +例えば仕様が未定義の挙動によってプログラムが停止することやプログラム内の誤った条件式による誤った計算結果、実行環境やパラメタの変化による誤動作などがある。 +信頼性を低下させるタイミングの一つにプログラムの変更がある。 +プログラムの変更を形式化することにより、プログラムの信頼性が損なわれる変更を定義する。 本研究ではプログラムの変更を Monad を用いて形式化する。 プログラムにおけるMonad とはデータ構造とメタ計算の対応である~\cite{Moggi:1991:NCM:116981.116984}。 メタ計算とは計算を実現するための計算であり、プログラムの変更をメタ計算として定義することで、プログラムの変更そのものを計算として実行することができる。 -例えば、プログラムが変更された際に変更前と変更後のプログラムの挙動を比較する機構を考える。 -もし挙動の変化が望ましくない場合、信頼性が損なわれる変更だと判定できる。 -このように、プログラムの変更に対するメタ計算を定義することで信頼性を保ちながら開発するための手法を提案する。 -加えて、形式化した論理の観点からプログラムの変更が持つ性質などを解析し、ソフトウェア開発手法の指針を提案する。 +変更を計算可能にすることで、信頼性の解析に利用可能な機構を計算として定義できる。 +例えば、プログラムが変更された際に変更前と変更後のプログラムの挙動を比較する機構を提供できる。 +もし挙動の変化が望ましくない場合、信頼性が損なわれる変更だと変更時に判定できる。 +このように、プログラムの変更に対するメタ計算を定義することで信頼性を保ちながら開発することが可能となる。 +本研究ではプログラムの変更をメタ計算として定義し、Monad則を満たすことを証明する。 +%加えて、形式化した論理の観点からプログラムの変更が持つ性質などを解析し、ソフトウェア開発手法の指針を提案する。 diff -r 398b42a1ac19 -r 5f0e13923cfd proof_delta.tex --- a/proof_delta.tex Mon Feb 16 15:05:11 2015 +0900 +++ b/proof_delta.tex Mon Feb 16 16:24:42 2015 +0900 @@ -62,12 +62,12 @@ Agda ではある性質を持つデータは record 構文によって記述する。 record の値は record の定義時に要請した field を全て満たすことで構築される。 よって、あるデータAが持つべき性質は field に定義し、A を用いた証明によって field を満たす。 -field を満たすことにより record が構成できることで A がある性質を満たすことを証明する。 +field を満たすことで record が構成できた場合、A がある性質を満たすことを Agda において証明したことになる。 -record Funcor は implicit な値 level と、型引数を持つ関数 F を持つ。 +record Functor は implicit な値 level と、型引数を持つ関数 F を持つ。 record Functor が取る F は Set l を取り Set l を取る関数である。 Set l が証明の対象となるプログラムであるため、関数F はプログラムのlevel で表現する。 -よって、プログラムの level l を取り、プログラムの level l の Set を返すようにする。 +よって、プログラムの level l を取り、変更せずに level l の Set を返すようにする。 それに対し、 F に対する証明となる record Functor は、証明の対象とするプログラムそのものではない。 よって suc により level を一段上げる。 これは、証明の対象となるプログラムと証明そのものを混同しないためである。 @@ -79,7 +79,7 @@ Functor に要請される、category から category への map 関数である。 型の定義はほとんど Haskell と同じである。 - fmap は任意の型に対して適用可能でなくてはいけないため、map する対象の型Aと map される対象の型Bは implicit である。 + fmap は任意の型に対して適用可能でなくてはいけないため、map する対象の型Aと map される対象の型Bは implicit とする。 \item preserve-id @@ -136,7 +136,7 @@ mono の場合はfmapの定義により同じ項に変形されるために relf で証明できる。 delta の場合、delta の 第一引数は mono の時のように同じ項に変形できる。 しかし第二引数は fmap の定義により \verb/delta-fmap d id/ に変形される。 - 見掛け上は等式の左辺と変わらないように見えるが、先頭1つめを除いているため、引数で受けたバージョンよりも1値が下がっている。 + 見掛け上は等式の左辺と変わらないように見えるが、先頭1つめを除いているため、引数で受けたバージョンよりも1つだけ値が下がっている。 よって最終的にバージョン1である mono になるまで再帰的に delta-preserve-id 関数を用いて変形した後に cong によって先頭1つめを適用し続けることで証明ができる。 \item fmap は関数の合成を保存する @@ -195,7 +195,7 @@ 最後に $ triple (T, \eta, \mu) $ に対する Monad 則に相当する等式を記述する。 Monad則は可換図として与えられたTに対する演算の可換性と、Tに対する演算の単位元を強制するものであった。 Tに対する演算の可換性は association-law として、単位元の強制は unity-law として記述できる。 -unity-law はTに対する演算が右側からか左側からかの二種類があるため、 right-unity-law と left-unity-law に分割した。 +unity-law はTに対する演算が右側と左側の二種類があるため、 right-unity-law と left-unity-law に分割した。 これら全ての field を満たすような証明を記述できれば、 $ triple (T, \eta, \mu) $ は Monad であると言える。 @@ -220,16 +220,15 @@ $ \eta $ に相当する delta-eta はメタ計算における T を1つ増やす演算に相当する。 内包する値のバージョンに依存して Delta が持つバージョンが決まるため、 Nat の値によりバージョン数を決められるようにしておく。 -これは Delta でない値に対してはバージョン1とし、Deltaである値はDeltaのバージョンと同じバージョンを返すようにする。 なお、パターンマッチの項に存在する \verb/{}/ は、 implicit な値のパターンマッチに用いられる。 -例えば \verb/{n = S x}/ とすれば、 implicit な値 n は S により構成され、残りの値は x に束縛される。 +例えば \verb/{n = S x}/ とすれば、 implicit な値 n は S により構成される時にこの定義が実行され、S を省いた残りの値は x に束縛される。 次に $ \mu $ に相当する delta-mu を定義する。 delta-mu は複数の \verb/TT -> T/に対応するメタ計算であるため、1段ネストされた Delta を受けとり、Deltaとして返す。 これはバージョン管理された値に対し、バージョン管理された関数を適用した場合の値の選択に相当する。 例えばバージョンが5であった場合、全ての組み合せは5パターン存在する。 その中から5つを選ぶルールとして $ \mu $ を定義する。 -$ \mu $ は値と関数が同じバージョンであるような結果を選ぶように定義する。 +$ \mu $ は値と関数が同じバージョンであるような計算結果を選ぶように定義する。 同じバージョンである値を選ぶため、先頭のバージョンの値を取る headDelta 関数と、先頭以外のバージョン列を取る tailDelta 関数を用いている。 @@ -336,3 +335,4 @@ 全ての Delta が同じバージョンを持つ時、 $ triple(T, \eta, \mu) $ は Monad則を満たすことを示せた。 % }}} +