Papers/2015/atton-thesis: agda.tex comparison

comparison agda.tex @ 57:5f0e13923cfd

Fixes

author	Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
date	Mon, 16 Feb 2015 16:24:42 +0900
parents	bf136bd59e7a
children

comparison

equal deleted inserted replaced

-:398b42a1ac19
+:5f0e13923cfd
 第\ref{chapter:category}章では functor, natural transformation, monad の定義を行ない、第\ref{chapter:functional_programming}章では functional programming における対応を述べた。
 その中で、 Functor 則や Monad 則といった満たすべき性質がいくつか存在した。
 functional programming において、あるデータ型と対応する計算が Functor 則を満たすかの保証は言語の実装に依存している。
 例えば、 Haskell において functor は型クラスによって提供されるため、型レベルのチェックを行なう。
 そのため、型チェックは通るが Functor 則を満たさない functor が定義できてしまう。
-よって Haskell において Delta Monad を定義しただけでは証明が存在しない。
+よって Haskell において Delta Monad を定義しただけでは Delta Monad が Monad であるかの証明が存在しない。
 そこで証明支援系言語 Agda を用いて、 Delta が Functor 則と Monad 則を満たすことを証明する。
 第\ref{chapter:agda}章は Agda における証明手法について述べる。
 % {{{ Natural Deduction
 \RightLabel{ $ \Rightarrow \mathcal{I} $}
 \UnaryInfC{$ A \Rightarrow B $}
 \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}
 \item Hypothesis
 「A は B であり、 B は C である。よって A は C である」 が証明するべき命題である。
 まず、「A は B であり」から、Aから性質Bが導けることが分かる。これが $ A \Rightarrow B $ となる。
 次に、「B は C である」から、Bから性質Cが導けることが分かる。これが $ B \Rightarrow C $ となる。
 そしてこの2つは同時に成り立つ。
-よって  $ (A \Rightarrow B) \land (B \Rightarrow C)$ が前提となる。
+よって  $ (A \Rightarrow B) \land (B \Rightarrow C)$ が仮定となる。
-この条件2つが成り立つ時に「Aは Cである」が成りたつ。
+この仮定が成り立つ時に「Aは Cである」を示せば良い。
-条件と同じように「A は C である」は、 $ A \Rightarrow C $ と書けるため、証明するべき論理式は $ ((A \Rightarrow B) \land (B \Rightarrow C)) \Rightarrow (A \Rightarrow 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/[]/の記号に数値を付けてある。
+数回仮定を dead にする際は $_{(1)} $ のように対応する \verb/[]/の記号に数値を付ける。
-これで残る仮定は $ (A \Rightarrow B) \land (B \Rightarrow C)$ となり、これから $ A \Rightarrow C $ を導くことができたためにさらに $ \Rightarrow \mathcal{I} $ を適用する。
+これで残る 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) $ が導けたために証明終了となる。
 % }}}
 % {{{ Curry-Howard Isomorphism
 プログラムにおいて、変数 x は内部の値により型が決定される。
 特に、x の値が未定である場合は未定義の変数としてエラーが発生する。
 しかし、 x を取って x を返す関数は定義することはできる。
 これは natural deduction の $ \Rightarrow \mathcal{I} $ により仮定を discharge することに相当する。
-このように、 natural deduction における証明はそのまま 型付き $ \lambda $ 計算にエンコードすることができる。
+このように、 natural deduction における証明はそのまま 型付き $ \lambda $ 計算に変換することができる。
 それぞれの詳細な対応は省略するが、表\ref{tbl:curry_howard_isomorphism} のような対応が存在する。
 \begin{center}
 \begin{table}[htbp]
 \caption{natural deuction と 型付き $ \lambda $ 計算との対応}
 \label{tbl:curry_howard_isomorphism}
 \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}
 \end{table}
 \section{Agda による証明}
 \label{section:agda}
 \ref{section:curry_howard_isomorphism}節において型を用いて証明を行なう手法を述べた。
 しかし、Haskell における型システムは証明を記述するために用いるものではない。
-よって、依存型を持つ証明支援言語 Agda を用いて証明を記述していく。
+よって、依存型を持つ証明支援言語 Agda を用いて証明を記述する。
 依存型とは値に依存した型を作ることができる型であり、非常に表現能力が高い。
 値に型を使うことができるために証明に基づいた証明を記述することができる。
 $ \Rightarrow \mathcal{E} $ に対応する関数適用を Agda で記述するとリスト\ref{src:apply_function_in_agda}のようになる。
 \begin{table}[html]
 \lstinputlisting[label=src:product, caption=Agdaにおける直積型の例] {src/product.agda.replaced}
 \end{table}
 関数の定義時に \verb/_/ とした部分には項を入れることで関数が適用される。
-つまり \verb/_x_/ とすれば中置関数を作成することができる。
+つまり \verb/_/$ \times $\verb/_/ とすれば中置関数を作成することができる。
-データ型 \verb/_x_/ は型 A と B を持つ型である。
+データ型 \verb/_/$ \times $\verb/_/ は型 A と B を持つ型である。
-データ型 \verb/_x_/ はコンストラクタ \verb/<_,_>/ により構成され、コンストラクタは A と B を取ることで \verb/A x 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/<_,_>/のみである。
+受けとる引数の型は $ A \times B $ であるため、ありえるコンストラクタは \verb/<_,_>/のみである。
-よって引数を取る際に \verb/< a , b >/ のように対応するコンストラクタと変数を用意することで、コンストラクタに基づいて型を分解することができる。
+よって引数を取る際に \verb/< a , b >/ のように対応するコンストラクタと変数を用意することで、コンストラクタに基づいて値を分解することができる。
-\verb/A x B/ 型から B を取るため、\verb/A x B/ 型の変数を直接束縛せずにコンストラクタで分解し、a と b に束縛することで A と B が得られる。
+$ A \times B$ 型から B を取るために、$ A \times B$ 型の引数を変数にを直接束縛せずにコンストラクタで分解し、a と b に束縛することで A と B を得る。
+b を返すことで型 B の値を返すことができる。
 そのため、 patternMathProduct は $ \land 2 \mathcal{E} $ そのものである。
 % }}}
 % {{{ Reasoning
 \lstinputlisting[label=src:nat_add, caption=Agdaにおける自然数型に対する加算の定義] {src/nat_add.agda}
 \end{table}
 加算は中置関数 \verb/_+_/ として定義する。
 2つの Nat を取り、Natを返す。
-パターンマッチにより処理を変える。
+関数 \verb/_+_/ はパターンマッチにより処理を変える。
 0に対して m 加算する場合は m であり、 n の後続数に対して m 加算する場合は n に m 加算した数の後続数とする。
 S を左の数から右の数へ1つずつ再帰的に移していくような加算である。
 例えば 3 + 1 といった計算は (S (S (S O))) + (S O) のように記述される。
 ここで 3 + 1 が 4と等しいことの証明を行なう。
 等式の証明には agda の standard library における Relation.Binary.Core の定義を用いる。
 \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})。
 \begin{table}[html]
 この等式は + の定義により $ O + (S m) \equiv S (m + O) $ と変形できる。
 $ S (m + O) $ は $ m + O $ に S を加えたものであるため、 cong を用いて再帰的に \verb/addSym/ を実行することで証明できる。
 この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
 $ (S n) + O \equiv O + (S n) $ を証明する。
 addToRight の証明の解説は省略する。
 addToRight を用いることで \verb/S ((S m) + n)/ から \verb/(S m) + (S n)/を得られた。
 これで等式 $ (S m) + (S n) \equiv (S n) + (S m) $  の証明が完了した。
 自然数に対する + の演算を考えた時にありえるコンストラクタの組み合せ4パターンのいずれかでも交換法則の等式が成り立つことが分かった。
-また、定義した + の演算のみでは加法の交換法則は証明できず、さらに等式を証明する必要があった。
 このように、Agda における等式の証明は、定義や等式を用いて右辺と左辺を同じ項に変形することで行なわれる。
 % }}}

Mercurial > hg > Papers > 2015 > atton-thesis

comparison agda.tex @ 57:5f0e13923cfd