# HG changeset patch
# User atton <atton@cr.ie.u-ryukyu.ac.jp>
# Date 1485826208 -32400
# Node ID 451c510825dee91f5ae4bd6a880eb02d02310062
# Parent  7f1b5c33b28203c0c33cabb5f9f3b69f13bb564d
Add natural deduction and curry-howard isomorphism

diff -r 7f1b5c33b282 -r 451c510825de paper/agda.tex
--- a/paper/agda.tex	Mon Jan 30 16:59:53 2017 +0900
+++ b/paper/agda.tex	Tue Jan 31 10:30:08 2017 +0900
@@ -1,7 +1,282 @@
 \chapter{証明支援系言語 Agda による証明手法}
 \label{chapter:agda}
-\section{依存型を持つ証明支援系言語 Agda}
+第~\ref{chapter:type}章では形無し算術式と型付き算術式による型システムの定義、ラムダ計算によるプログラミング言語の抽象化、部分型の導入とCbCの型が部分型で示せることを確認した。
+部分型を用いて具体的なCbCの型システムを定義する前に、型システムの一方のメリットである証明について触れる。
+依存型という型を持つ証明支援系言語 Agda を用いて証明が行なえることを示す。
+
+% {{{ Natural Deduction
 \section{Natural Deduction}
+まず始めに証明を行なうためにNatural Deduction(自然演繹)を示す。
+
+証明には natural deduction(自然演繹)を用いる。
+natural deduction は Gentzen によって作られた論理と、その証明システムである~\cite{Girard:1989:PT:64805}。
+命題変数と記号を用いた論理式で論理を記述し、推論規則により変形することで求める論理式を導く。
+
+natural deduction において
+
+\begin{eqnarray}
+    \vdots \\ \nonumber
+    A \\ \nonumber
+\end{eqnarray}
+
+と書いた時、最終的に命題Aを証明したことを意味する。
+証明は木構造で表わされ、葉の命題は仮定となる。
+仮定には dead か alive の2つの状態が存在する。
+
+\begin{eqnarray}
+    \label{exp:a_implies_b}
+    A \\ \nonumber
+    \vdots \\ \nonumber
+    B \\ \nonumber
+\end{eqnarray}
+
+式\ref{exp:a_implies_b}のように A を仮定して B を導いたとする。
+この時 A は alive な仮定であり、証明された B は A の仮定に依存していることを意味する。
+
+ここで、推論規則により記号 $ \Rightarrow $ を導入する。
+
+\begin{prooftree}
+    \AxiomC{[$ A $]}
+    \noLine
+    \UnaryInfC{ $ \vdots $}
+    \noLine
+    \UnaryInfC{ $ B $ }
+    \RightLabel{ $ \Rightarrow \mathcal{I} $}
+    \UnaryInfC{$ A \Rightarrow B $}
+\end{prooftree}
+
+$ \Rightarrow \mathcal{I} $ を適用することで仮定 A は dead となり、新たな命題 $ A \Rightarrow B $ を導くことができる。
+A という仮定に依存して B を導く証明から、「A が存在すれば B が存在する」という証明を導いたこととなる。
+このように、仮定から始めて最終的に全ての仮定を dead とすることで、仮定に依存しない証明を導ける。
+なお、dead な仮定は \verb/[A]/ のように \verb/[]/ で囲んで書く。
+
+alive な仮定を dead にすることができるのは $ \Rightarrow \mathcal{I} $ 規則のみである。
+それを踏まえ、 natural deduction には以下のような規則が存在する。
+
+\begin{itemize}
+    \item Hypothesis
+
+        仮定。葉にある式が仮定となるため、論理式A を仮定する場合に以下のように書く。
+
+        $ A $
+
+    \item Introductions
+
+        導入。証明された論理式に対して記号を導入することで新たな証明を導く。
+
+
+\begin{prooftree}
+    \AxiomC{ $ \vdots $}
+    \noLine
+    \UnaryInfC{ $ A $ }
+    \AxiomC{ $ \vdots $}
+    \noLine
+    \UnaryInfC{ $ B $ }
+    \RightLabel{ $ \land \mathcal{I} $}
+    \BinaryInfC{$ A \land B $}
+\end{prooftree}
+
+\begin{prooftree}
+    \AxiomC{ $ \vdots $}
+    \noLine
+    \UnaryInfC{ $ A $ }
+    \RightLabel{ $ \lor 1 \mathcal{I} $}
+    \UnaryInfC{$ A \lor B $}
+\end{prooftree}
+
+\begin{prooftree}
+    \AxiomC{ $ \vdots $}
+    \noLine
+    \UnaryInfC{ $ B $ }
+    \RightLabel{ $ \lor 2 \mathcal{I} $}
+    \UnaryInfC{$ A \lor B $}
+\end{prooftree}
+
+\begin{prooftree}
+    \AxiomC{[$ A $]}
+    \noLine
+    \UnaryInfC{ $ \vdots $}
+    \noLine
+    \UnaryInfC{ $ B $ }
+    \RightLabel{ $ \Rightarrow \mathcal{I} $}
+    \UnaryInfC{$ A \Rightarrow B $}
+\end{prooftree}
+
+\item Eliminations
+
+    除去。ある論理記号で構成された証明から別の証明を導く。
+
+\begin{prooftree}
+    \AxiomC{ $ \vdots $}
+    \noLine
+    \UnaryInfC{ $ A \land B $ }
+    \RightLabel{ $ \land 1 \mathcal{E} $}
+    \UnaryInfC{$ A $}
+\end{prooftree}
+
+\begin{prooftree}
+    \AxiomC{ $ \vdots $}
+    \noLine
+    \UnaryInfC{ $ A \land B $ }
+    \RightLabel{ $ \land 2 \mathcal{E} $}
+    \UnaryInfC{$ B $}
+\end{prooftree}
+
+\begin{prooftree}
+    \AxiomC{ $ \vdots $}
+    \noLine
+    \UnaryInfC{ $ A \lor B $ }
+
+    \AxiomC{[$A$]}
+    \noLine
+    \UnaryInfC{ $ \vdots $}
+    \noLine
+    \UnaryInfC{ $ C $ }
+
+    \AxiomC{[$B$]}
+    \noLine
+    \UnaryInfC{ $ \vdots $}
+    \noLine
+    \UnaryInfC{ $ C $ }
+
+    \RightLabel{ $ \lor \mathcal{E} $}
+    \TrinaryInfC{ $ C $ }
+\end{prooftree}
+
+\begin{prooftree}
+    \AxiomC{ $ \vdots $}
+    \noLine
+    \UnaryInfC{ $ A $ }
+
+    \AxiomC{ $ \vdots $}
+    \noLine
+    \UnaryInfC{ $ A \Rightarrow B $ }
+
+    \RightLabel{ $ \Rightarrow \mathcal{E} $}
+    \BinaryInfC{$ B $}
+\end{prooftree}
+
+\end{itemize}
+
+記号 $ \lor, \land, \Rightarrow $ の導入の除去規則について述べた。
+natural deduction には他にも $ \forall, \exists, \bot $ といった記号が存在するが、ここでは解説を省略する。
+
+それぞれの記号は以下のような意味を持つ
+\begin{itemize}
+    \item $ \land $
+        conjunction。2つの命題が成り立つことを示す。
+        $ A \land B $ と記述すると A かつ B と考えることができる。
+
+    \item $ \lor $
+        disjunction。2つの命題のうちどちらかが成り立つことを示す。
+        $ A \lor B $ と記述すると A または B と考えることができる。
+
+    \item $ \Rightarrow $
+        implication。左側の命題が成り立つ時、右側の命題が成り立つことを示す。
+        $ 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) $ }
+    \BinaryInfC{ $ B $ }
+
+    \AxiomC{ [$ (A \Rightarrow B) \land (B \Rightarrow C)$] $_{(2)}$ }
+    \RightLabel{ $ \land 2 \mathcal{E} $ }
+    \UnaryInfC{ $ (B \Rightarrow C) $ }
+
+    \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) $}
+\end{prooftree}
+
+まず、三段論法を論理式で表す。
+
+「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は 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つを仮定する。
+条件を $ \land 1 \mathcal{E} $ $ \land 2 \mathcal{E} $ により分解する。
+A と $ A \Rightarrow B$ から B を、 B と $ B \Rightarrow C $ から C を導く。
+ここで $ \Rightarrow \mathcal{I} $ により $ A \Rightarrow C $ を導く。
+この際に dead にする仮定は A である。
+数回仮定を dead にする際は $_{(1)} $ のように対応する \verb/[]/の記号に数値を付ける。
+これで残る 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
 \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
+
+型構築子 $ \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
+                        & 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}
+% }}}
+
+\section{依存型を持つ証明支援系言語 Agda}
 \section{Reasoning}
 
diff -r 7f1b5c33b282 -r 451c510825de paper/type.tex
--- a/paper/type.tex	Mon Jan 30 16:59:53 2017 +0900
+++ b/paper/type.tex	Tue Jan 31 10:30:08 2017 +0900
@@ -638,7 +638,7 @@
 例えば $ (\lambda x . \lambda y . s) \; v \; w $ は $ (\lambda y . [x \mapsto v] s) w $ に簡約され、 $ [y \mapsto w][x \mapsto v]s $ に簡約される。
 なお、複数の引数を取る関数を高階関数に変換することはカリー化と呼ばれる。
 
-% TODO: ラムダの再帰とかペアとかの解説
+% TODO: ラムダの再帰とかペアとかの解説 直積直和
 
 ラムダ計算の帰納的な項は以下のように定義される。
 
@@ -1155,6 +1155,7 @@
 こうすることにより、 Meta DataSegment はプログラム中に出現する DataSegment を必ず持つため、Meta DataSegment は任意の DataSegment の部分型となる。
 もしくは各 DataSegment の全てのフィールドを含むような1つの構造体でも良い。
 第~\ref{chapter:cbc-type}章における Meta DataSegment はそのように定義している。
+なお、GearsOSでは DataSegment の共用体をプログラムで必要な数だか持つ実装になっている。
 
 具体的な CbC における Meta DataSegment であるContext (リスト~\ref{src:type-mds})は、 DataSegment の集合を値として持っているために明らかに DataSegment よりも多くの情報を持っている。
 \lstinputlisting[label=src:type-mds, caption=CbC の Meta DataSegment である Context] {src/type-mds.h}