# HG changeset patch # User atton # Date 1486622212 -32400 # Node ID 9d154c48a1f64e13c7c82667a479db99ded9f405 # Parent f3ea67a23cf6c3bc3a936dff4eaed61c44f294c7 Update curry-howard isomorphism diff -r f3ea67a23cf6 -r 9d154c48a1f6 paper/agda.tex --- 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 における証明を記述していく。 +次に依存型を利用して等式の証明を記述していく。 + 例題として、自然数の加法の可換法則を示す。 - 証明を行なうためにまずは自然数を定義する。 今回用いる自然数の定義は以下のようなものである。 diff -r f3ea67a23cf6 -r 9d154c48a1f6 paper/atton-master.pdf Binary file paper/atton-master.pdf has changed diff -r f3ea67a23cf6 -r 9d154c48a1f6 paper/src/AgdaModusPonens.agda --- /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)) diff -r f3ea67a23cf6 -r 9d154c48a1f6 paper/src/AgdaProduct.agda --- /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 diff -r f3ea67a23cf6 -r 9d154c48a1f6 paper/src/AgdaProp.agda --- /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