Mercurial > hg > Papers > 2018 > nozomi-master

--- a/paper/agda.tex	Thu Feb 09 13:57:35 2017 +0900
+++ b/paper/agda.tex	Thu Feb 09 15:36:52 2017 +0900
@@ -348,15 +348,15 @@
 \begin{itemize}
     \item $ \land $
         conjunction。2つの命題が成り立つことを示す。
-        $ A \land B $ と記述すると A かつ B と考えることができる。
+        $ A \land B $ と記述すると、 A かつ B と考えることができる。

     \item $ \lor $
         disjunction。2つの命題のうちどちらかが成り立つことを示す。
-        $ A \lor B $ と記述すると A または B と考えることができる。
+        $ A \lor B $ と記述すると、 A または B と考えることができる。

     \item $ \Rightarrow $
         implication。左側の命題が成り立つ時、右側の命題が成り立つことを示す。
-        $ A \Rightarrow B $ と記述すると A ならば B と考えることができる。
+        $ A \Rightarrow B $ と記述すると、 A ならば B と考えることができる。
 \end{itemize}

 例として、natural deduction で三段論法を証明する。
@@ -367,12 +367,14 @@
     \AxiomC{ [$ (A \Rightarrow B) \land (B \Rightarrow C)$] $_{(2)}$ }
     \RightLabel{ $ \land 1 \mathcal{E} $ }
     \UnaryInfC{ $ (A \Rightarrow B) $ }
+    \RightLabel{ $ \Rightarrow \mathcal{E} $}
     \BinaryInfC{ $ B $ }

     \AxiomC{ [$ (A \Rightarrow B) \land (B \Rightarrow C)$] $_{(2)}$ }
     \RightLabel{ $ \land 2 \mathcal{E} $ }
     \UnaryInfC{ $ (B \Rightarrow C) $ }

+    \RightLabel{ $ \Rightarrow \mathcal{E} $}
     \BinaryInfC{ $ C $ }
     \RightLabel{ $ \Rightarrow \mathcal{I} _{(1)}$}
     \UnaryInfC{ $ A \Rightarrow C $}
@@ -402,71 +404,73 @@

 % }}}

-% {{{ Curry-Howard Isomorphism TODO: もっと増やす(Agda でラムダ計算を説明する)
+% {{{ Curry-Howard Isomorphism
 \section{Curry-Howard Isomorphism}
 \label{section:curry_howard_isomorphism}
-\ref{section:natural_deduction}節では natural deduction における証明手法について述べた。
-natural deduction における証明はほとんど型付き $ \lambda $ 計算のような形をしている。
-実際、Curry-Howard Isomorphism により Natural Deduction と型付き $ \lambda $ 計算は対応している。% ref TaPL 104
-Curry-Howard Isomorphism の概要を~\ref{section:curry_howard_isomorphism} 節に述べる。
-
-関数型 $ \rightarrow $ のみに注目した時
-
-\begin{enumerate}
-    \item 導入規則(T-ABS) は、その型の要素がどのように作られるかを記述する
-    \item 除去規則(T-APP) は、その型の要素がどのように作られるかを記述する
-\end{enumerate}
-
-
-例えば命題Aが成り立つためには A という型を持つ値が存在すれば良い。
-しかしこの命題は A という alive な仮定に依存している。
-natural deduction では A の仮定を dead にするために $ \Rightarrow \mathcal{I} $ により $ \Rightarrow $ を導入する。
-これが $ \lambda $ による抽象化(T-ABS)に対応している。
-
-\begin{eqnarray*}
-    x : A \\
-    \lambda x . x : A \rightarrow A
-\end{eqnarray*}
-
-プログラムにおいて、変数 x は内部の値により型が決定される。
-特に、x の値が未定である場合は未定義の変数としてエラーが発生する。
-しかし、 x を取って x を返す関数は定義することはできる。
-これは natural deduction の $ \Rightarrow \mathcal{I} $ により仮定を discharge することに相当する。
-
-また、仮定Aが成り立つ時に結論Bを得ることは、関数適用(T-APP)に相当している。
-
-\begin{prooftree}
-    \AxiomC{$A$}
-    \AxiomC{$A \rightarrow B $}
-    \RightLabel{T-APP}
-    \BinaryInfC{$B$}
-\end{prooftree}
-
-このように、 natural deduction における証明はそのまま 型付き $ \lambda $ 計算に変換することができる。
-
-それぞれの詳細な対応は省略するが、表\ref{tbl:curry_howard_isomorphism} のような対応が存在する。
+\ref{section:natural_deduction}節では Natural Deduction における証明手法について述べた。
+Natural Deduction はプログラム上では型付きのラムダ式として表現できる。
+これは Curry-Howard Isomorphism と呼ばれ、 Natural Deduction と型付き $ \lambda $ 計算が同じ構造であることを表している。
+Curry-Howard Isomorphism の概要を表~\ref{table:curry}に示す。

 \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 $ 計算との対応(Curry-Howard Isomorphism)}
-        \label{tbl:curry_howard_isomorphism}
-    \end{table}
+\begin{table}[htbp]
+\begin{tabular}{|c|c|} \hline
+ Natural Deduction           & 型付き $ \lambda $ 計算  \\ \hline \hline
+ $ A $                       & 型 A を持つ変数 x \\ \hline
+ $ A \Rightarrow B $         & 型 A を取り型 B の変数を返す関数 f \\ \hline
+ $ \Rightarrow \mathcal{I} $ & ラムダの抽象化 \\ \hline
+ $ \Rightarrow \mathcal{E} $ & 関数適用 \\ \hline
+ $ A \land B $               & 型 A と型 B の直積型 を持つ変数 x \\ \hline
+ $ \land \mathcal{I} $       & 型A,Bを持つ値から直積型へのコンストラクタ \\ \hline
+ $ \land 1 \mathcal{E} $     & 直積型からの型Aを取り出す射影fst \\ \hline
+ $ \land 2 \mathcal{E} $     & 直積型からの型Bを取り出す射影snd \\ \hline
+ $ A \lor B $                & 型 A と型 B の直和型 を持つ変数 x \\ \hline
+ $ \lor \mathcal{I} $        & 型A,Bの値から直和型へのコンストラクタ \\ \hline
+ $ \lor \mathcal{E} $        & 直和型から型Cの値を返す関数f \\ \hline
+\end{tabular}
+\caption{natural deuction と 型付き $ \lambda $ 計算との対応(Curry-Howard Isomorphism)}
+\label{table:curry}
+\end{table}
 \end{center}
+
+型付きラムダ計算における命題は型に相当する。
+例えば恒等関数id の型は $ \text{A} \rightarrow \text{A}$ という型を持つが、これは「Aが成り立つならAが成り立つ」という命題と等しい。
+命題の仮定は引数となって表れ、証明はその型を導くための式となる。
+
+例えば Natural Deduction における三段論法は $ ((A \Rightarrow B) \land (B \Rightarrow C)) \Rightarrow (A \Rightarrow C) $ という形をしていた。
+仮定は $ ((A \Rightarrow B) \land (B \Rightarrow C)) $ となる。
+
+直積に対応する型には直積型が存在する。
+Agda において直積型に対応するデータ構造 \verb/Product/ を定義するとリスト~\ref{src:agda-product}のようになる。
+例えば \verb/Int/ 型と \verb/String/ 型を取る直積型は \verb/Int/ $ \times $ \verb/String/ 型となる。
+これは二つの型を取る型であり、Natural Deduction の $ \land $ に相当する。
+
+直積型から値を射影する関数 \verb/fst/ と \verb/snd/ を定義する。
+これらは Natural Deduction における $ \land 1 \mathcal{E} $ と $ \land 2 \mathcal{E} $ に相当する。
+
+なお、直積型は型Aを持つフィールド\verb/fst/と型Bを持つフィールド\verb/snd/を持つレコード型と考えても良い。
+
+\lstinputlisting[label=src:agda-product, caption=Agda における直積型] {src/AgdaProduct.agda}
+
+三段論法の証明は 「1つの仮定から $ \land 1 \mathcal{E} $ と $ \land 2 \mathcal{E} $ を用いて仮定を二つ取り出し、それぞれに $ \Rightarrow \mathcal{E} $ を適用した後に仮定を $ \Rightarrow \mathcal{I}$ で dead にする」形であった。
+
+$ \Rightarrow \mathcal{I}$ に対応するのは関数適用である。
+よってこの証明は「一つの変数から \verb/fst/ と \verb/snd/ を使って関数を二つ取り出し、それぞれを関数適用する」という形になる。
+これをラムダ式で書くとリスト~\ref{src:agda-modus-ponens}のようになる。
+仮定 A $ \times $ B と仮定 A から A $ \rightarrow $ C を導いている。
+
+\lstinputlisting[label=src:agda-modus-ponens, caption=Agda における三段論法の証明] {src/AgdaModusPonens.agda.replaced}
+
+このように Agda では証明を記述することができる。
+
 % }}}

 % {{{ Reasoning

 \section{Reasoning}
-次に Agda における証明を記述していく。
+次に依存型を利用して等式の証明を記述していく。
+
 例題として、自然数の加法の可換法則を示す。
-
 証明を行なうためにまずは自然数を定義する。
 今回用いる自然数の定義は以下のようなものである。
Binary file paper/atton-master.pdf has changed
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/paper/src/AgdaModusPonens.agda	Thu Feb 09 15:36:52 2017 +0900
@@ -0,0 +1,2 @@
+f : {A B C : Set} -> (A -> B) × (B -> C) -> (A -> C)
+f = (\p x -> snd p ((fst p) x))
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/paper/src/AgdaProduct.agda	Thu Feb 09 15:36:52 2017 +0900
@@ -0,0 +1,8 @@
+data _×_ (A B : Set) : Set where
+  <_,_> : A -> B -> A × B
+
+fst : {A B : Set} -> A × B -> A
+fst < a , _ > = a
+
+snd : {A B : Set} -> A × B -> B
+snd < _ , b > = b
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/paper/src/AgdaProp.agda	Thu Feb 09 15:36:52 2017 +0900
@@ -0,0 +1,2 @@
+prop : Bool
+prop = true