Papers/2018/nozomi-master: paper/agda.tex comparison

comparison paper/agda.tex @ 85:9d154c48a1f6

Update curry-howard isomorphism

author	atton <atton@cr.ie.u-ryukyu.ac.jp>
date	Thu, 09 Feb 2017 15:36:52 +0900
parents	c0199291c58e
children	e437746d6038

comparison

equal deleted inserted replaced

-:f3ea67a23cf6
+:9d154c48a1f6
 それぞれの記号は以下のような意味を持つ
 \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 で三段論法を証明する。
 なお、三段論法とは「A は B であり、 B は C である。よって A は C である」といった文を示す。
 \begin{prooftree}
 \AxiomC{ $ [A] $ $_{(1)}$}
 \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 $}
 \RightLabel{ $ \Rightarrow \mathcal{I} _{(2)}$}
 \UnaryInfC{ $ ((A \Rightarrow B) \land (B \Rightarrow C)) \Rightarrow (A \Rightarrow C) $}
 これで残る 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 TODO: もっと増やす(Agda でラムダ計算を説明する)
+% {{{ Curry-Howard Isomorphism
 \section{Curry-Howard Isomorphism}
 \label{section:curry_howard_isomorphism}
-\ref{section:natural_deduction}節では natural deduction における証明手法について述べた。
+\ref{section:natural_deduction}節では Natural Deduction における証明手法について述べた。
-natural deduction における証明はほとんど型付き $ \lambda $ 計算のような形をしている。
+Natural Deduction はプログラム上では型付きのラムダ式として表現できる。
-実際、Curry-Howard Isomorphism により Natural Deduction と型付き $ \lambda $ 計算は対応している。% ref TaPL 104
+これは Curry-Howard Isomorphism と呼ばれ、 Natural Deduction と型付き $ \lambda $ 計算が同じ構造であることを表している。
-Curry-Howard Isomorphism の概要を~\ref{section:curry_howard_isomorphism} 節に述べる。
+Curry-Howard Isomorphism の概要を表~\ref{table:curry}に示す。
-関数型 $ \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} のような対応が存在する。
 \begin{center}
 \begin{table}[htbp]
-\begin{tabular}{|c||c|c|} \hline
+\begin{tabular}{|c|c|} \hline
-& natural deduction   & 型付き $ \lambda $ 計算  \\ \hline \hline
+Natural Deduction           & 型付き $ \lambda $ 計算  \\ \hline \hline
-hypothesis  & $ A $               & 型 A を持つ変数 x \\ \hline
+$ A $                       & 型 A を持つ変数 x \\ \hline
-conjunction & $ A \land B $       & 型 A と型 B の直積型 を持つ変数 x \\ \hline
+$ A \Rightarrow B $         & 型 A を取り型 B の変数を返す関数 f \\ \hline
-disjunction & $ A \lor B $        & 型 A と型 B の直和型 を持つ変数 x \\ \hline
+$ \Rightarrow \mathcal{I} $ & ラムダの抽象化 \\ \hline
-implication & $ A \Rightarrow B $ & 型 A を取り型 B の変数を返す関数 f \\ \hline
+$ \Rightarrow \mathcal{E} $ & 関数適用 \\ \hline
-\end{tabular}
+$ A \land B $               & 型 A と型 B の直積型 を持つ変数 x \\ \hline
-\caption{natural deuction と 型付き $ \lambda $ 計算との対応(Curry-Howard Isomorphism)}
+$ \land \mathcal{I} $       & 型A,Bを持つ値から直積型へのコンストラクタ \\ \hline
-\label{tbl:curry_howard_isomorphism}
+$ \land 1 \mathcal{E} $     & 直積型からの型Aを取り出す射影fst \\ \hline
-\end{table}
+$ \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 における証明を記述していく。
+次に依存型を利用して等式の証明を記述していく。
 例題として、自然数の加法の可換法則を示す。
 証明を行なうためにまずは自然数を定義する。
 今回用いる自然数の定義は以下のようなものである。
 \begin{itemize}
 \item 0 は自然数である

Mercurial > hg > Papers > 2018 > nozomi-master

comparison paper/agda.tex @ 85:9d154c48a1f6