\chapter{証明支援系言語 Agda による証明手法}
\label{chapter: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}