# HG changeset patch
# User Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
# Date 1423535916 -32400
# Node ID 13affa3e65a220faaec94d798a930c59a08abde3
# Parent  61e5659e04a9bf804210109541f3590c35fe9a01
Add curry-howad isomorphism

diff -r 61e5659e04a9 -r 13affa3e65a2 agda.tex
--- a/agda.tex	Mon Feb 09 22:13:18 2015 +0900
+++ b/agda.tex	Tue Feb 10 11:38:36 2015 +0900
@@ -224,7 +224,81 @@
 
 % }}}
 
+% {{{ Curry-Howard Isomorphism
+
 \section{Curry-Howard Isomorphism}
+\label{section:curry_howard_isomorphism}
+\ref{section:natural_deduction}節では natural deduction における証明手法について述べた。
+natural deduction における証明は Curry-Howard Isomorphism により型付き $ \lambda $ 計算と対応している。
+
+$ \lambda $ 計算とは、計算モデルの1つであり、計算の実行を関数への適用としてモデル化したものである。
+関数は $ \lambda $ 式として表され、引数を1つ取りその引数を計算する関数は式\ref{exp:lambda_expression}のように記述される。
+
+\begin{equation}
+    \label{exp:lambda_expression}
+    \lambda x . x
+\end{equation}
+
+値と $ \lambda $ 式には型を付与することができ、その型の計算が natural deduction と対応している。
+
+例えば命題Aが成り立つためには A という型を持つ値が存在すれば良い。
+しかしこの命題は A という alive な仮定に依存している。
+natural deduction では A の仮定を dead にするために $ \Rightarrow \mathcal{I} $ により $ \Rightarrow $ を導入する。
+これが $ \lambda $ による抽象化に対応している。
+
+\begin{eqnarray}
+    x : A \\ \nonumber
+    \lambda x . x : A \rightarrow A
+\end{eqnarray}
+
+プログラムにおいて、変数 x は内部の値により型が決定される。
+特に、x の値が未定である場合は未定義の変数としてエラーが発生する。
+しかし、 x を取って x を返す関数は定義することはできる。
+これは natural deduction の $ \Rightarrow \mathcal{I} $ により仮定を discharge することに相当する。
+
+このように、 natural deduction における証明はそのまま 型付き $ \lambda $ 計算にエンコードすることができる。
+
+それぞれの詳細な対応は省略するが、表\ref{tbl:curry_howard_isomorphism} のような対応が存在する。
+
+\begin{center}
+    \begin{table}[htbp]
+        \begin{tabular}{|c||c|c|} \hline
+                        & natural deduction   & 型付き $ \lambda $ 計算  \\ \hline \hline
+            hypothesis  & $ A $               & 型 A を持つ変数 x \\ \hline
+            conjunction & $ A \land B $       & 型 A と型 B の直積型 を持つ変数 x \\ \hline
+            disjunction & $ A \lor B $        & 型 A と型 B の直和型 を持つ変数 x \\ \hline
+            implication & $ A \Rightarrow B $ & 型 A を取り型 B の変数を返す関数 f \\ \hline
+        \end{tabular}
+        \caption{natural deuction と 型付き $ \lambda $ 計算との対応}
+        \label{tbl:curry_howard_isomorphism}
+    \end{table}
+\end{center}
+
+\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}
+
+証明は $ \lambda $ 式の型として表現される。
+Haskell における $ \lambda $ 式は \verb| \x -> x| のように表される。
+\verb/\/ と \verb/->/ の間が引数であり、 \verb/->/ の後に処理を記述する。
+また、$ \land $ に対応する直積型は tuple として提供される。
+A と B の直積型は $ (A, B) $ として表現される。
+そして、 $ \land 1 \mathcal{E} $ に対応する処理は関数 fst 、 $ \land 2 \mathcal{E} $ に対応する処理は関数 snd として提供される。
+fst と snd が $ \land $ の除去に対応しているのは型を見ることで分かる。
+
+そして三段論法の証明の解説を行なう。
+三段論法の仮定は、$ (A \Rightarrow B) \land (B \Rightarrow C) $ であった。
+この仮定を変数 cond として受けとる。
+cond に対して fst を行なうことで $ (A \Rightarrow B) $ を、snd を行なうことで $ (B \Rightarrow C) $ を証明する。
+ここでさらに仮定 a を導入し、$ (A \Rightarrow B) $ と$ (B \Rightarrow C) $ に適用することで C を得る。
+
+結果、 \verb/\cond -> (\a -> (snd cond ((fst cond) a)))/のような式が得られ、この型を確認すると正しく三段論法の証明となっている。
+なお、型推論の際に A はt2 に、 B は t1 に、 C は t という型名になっている。
+
+% }}}
+
 \section{Agda による証明}
 \section{Reasoning}
 
diff -r 61e5659e04a9 -r 13affa3e65a2 src/modus_ponens.txt
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/modus_ponens.txt	Tue Feb 10 11:38:36 2015 +0900
@@ -0,0 +1,8 @@
+*Main> :type fst
+fst :: (a, b) -> a
+*Main> :type snd
+snd :: (a, b) -> b
+
+*Main> :type \cond -> (\a -> (snd cond ((fst cond) a)))
+\cond -> (\a -> (snd cond ((fst cond) a)))
+  :: (t2 -> t1, t1 -> t) -> t2 -> t