\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}
型システムを用いて証明を行なうことができる言語に Agda が存在する。% ref Agda のref
Agda は依存型という強力な型システムを持っている。
依存型とは型も第一級オブジェクトとする型であり、型を引数に取る関数や値を取って型を返す関数、型の型などが記述できる。
この節では Agda の文法的な紹介を行なう~\cite{agda-documentation}。 % ref pdf のアレ

まず Agda のプログラムは全てモジュールの内部に記述されるため、まずはトップレベルにモジュールを定義する必要がある。
トップレベルのモジュールはファイル名と同一となる。
例えば \verb/AgdaBasics.agda/ のモジュール名定義はリスト~\ref{src:agda-module}のようになる。

\lstinputlisting[label=src:agda-module, caption=Agdaのモジュールの定義する] {src/AgdaBasics.agda}

また、Agda はインデントに意味を持つ言語であるため、インデントはきちんと揃える必要がある。

まず Agda におけるデータ型について触れていく。
Agda における型指定は $:$ を用いて行なう。
例えば、変数xが型Aを持つ、ということを表すには \verb/x : A/ と記述する。

データ型は Haskell や ML に似て代数的なデータ構造のパターンマッチを扱うことができる
データ型の定義は \verb/data/ キーワードを用いる。
\verb/data/キーワードの後に \verb/where/ 句を書きインデントを深くした後、値にコンストラクタとその型を列挙する。
例えば Bool 型を定義するとリスト~\ref{src:agda-bool}のようになる。

\lstinputlisting[label=src:agda-bool, caption=Agdaにおけるデータ型 Bool の定義] {src/AgdaBool.agda}

Bool はコンストラクタ \verb/true/ か \verb/false/ を持つデータ型である。
Bool 自身の型は \verb/Set/ であり、これは Agda が組み込みで持つ「型の型」である。
Set は階層構造を持ち、型の型の型を指定するには Set1 と書く。

関数の定義は Haskell に近い。
関数名と型を記述した後に関数の本体を \verb/=/ の後に指定する。
関数の型は単純型付き $ \lambda$ 計算と同様に $ \rightarrow $ を用いる。
なお、$\rightarrow$に対しては糖衣構文 \verb/->/ も用意されている。
引数は変数名で受けることもできるが、具体的なコンストラクタを指定することでそのコンストラクタが渡された時の挙動を定義できる。
これはパターンマッチと呼ばれ、コンストラクタで case 文を行なっているようなものである。
例えば Bool 型の値を反転する \verb/not/ 関数を書くとリスト~\ref{src:agda-not}のようになる。

\lstinputlisting[label=src:agda-not, caption=Agdaにおける関数 not の定義] {src/AgdaNot.agda}

パターンマッチは全てのコンストラクタのパターンを含まなくてはならない。
パターンマッチは上からマッチされていくため、優先順位が存在する。
なお、コンストラクタをいくつか指定した後に変数で受けると、変数が持ちうる値は指定したコンストラクタ以外となる。
例えばリスト~\ref{src:agda-pattern}のnot は x には true しか入ることは無い。

\lstinputlisting[label=src:agda-pattern, caption=Agdaにおけるパターンマッチ] {src/AgdaPattern.agda}

なお、マッチした値を変数として利用しない場合は \verb/_/ を用いて捨てることもできる。

単純型で利用した自然数もデータ型として定義できる(リスト~\ref{src:agda-nat})。
自然数のコンストラクタは2つあり、片方は自然数ゼロ、片方は自然数を取って後続数を返すものである。
例えば3は \verb/suc (suc (suc zero))/ となる。

\lstinputlisting[label=src:agda-nat, caption=Agdaにおける自然数の定義] {src/AgdaNat.agda}

自然数に対する演算は再帰関数として定義できる。
例えば自然数どうしの加算は二項演算子\verb/+/としてリスト~\ref{src:agda-plus}のように書ける。

この二項演算子は正確には中置関数である。
前置や後置で定義できる部分を関数名に \verb/_/ として埋め込んでおくことで、関数を呼ぶ時にあたかも前置演算子のように振る舞う。
また、Agda は関数が停止するかを判定できる。
この加算の二項演算子は左側がゼロに対しては明かに停止する。
左側が1以上の時の再帰時には \verb/suc n/ から \verb/n/へと減っているため、再帰で繰り返し減らすことでいつかは停止する。

\lstinputlisting[label=src:agda-plus, caption=Agda における自然数の加算の定義] {src/AgdaPlus.agda}

次に依存型について見ていく。
依存型で最も基本的なものは関数型である。
依存型を利用した関数は引数の型に依存して返す型を決定できる。

Agda で \verb/(x : A) -> B/ と書くと関数は型 A を持つx を受け取り、Bを返す。
ここで B の中で x を扱っても良い。
例えば任意の型に対する恒等関数はリスト~\ref{src:agda-id}のように書ける。

\lstinputlisting[label=src:agda-id, caption=依存型を持つ関数の定義] {src/AgdaId.agda}

この恒等関数 \verb/identitiy/ は任意の型に適用可能である。
実際に Nat へ適用した例が \verb/id-zero/ である。

依存型を用いることで任意の型に適用可能な多相の恒等関数を定義した。
しかし型を明示的に指定せずとも \verb/zero/ を渡された場合は恒等関数の型は自明に \verb/Nat -> Nat/である。
その場合、型を推論することで実際に引数として渡さないようにできる。
これを暗黙的な引数(implicit arguments) と言い、記号 \verb/{}/ でくくる。

例えば恒等関数の型を暗黙的な引数にするとリスト~\ref{src:agda-implicit-id}のようになる。
この恒等関数を利用する際は値を渡すだけで型が自動的に推論される。
よって関数を利用する際は \verb/id-true/ のように記述できる。
なお、関数の本体で暗黙的な引数を利用したい場合は \verb/{variableName}/ で束縛することもできる。

\lstinputlisting[label=src:agda-implicit-id, caption=Agdaにおける暗黙的な引数を持つ関数] {src/AgdaImplicitId.agda}

Agda にはレコード型も存在する。
定義を行なう際は \verb/record/キーワードの後にレコード名、型、\verb/where/ の後に \verb/field/ キーワードを入れた後、フィールド名と型名を列挙する。
例えば x と y の二つの自然数からなるレコード \verb/Point/ を定義するとリスト~\ref{src:agda-record}のようになる。
レコードを構築する際は \verb/record/ キーワードの後の \verb/{}/ の内部に \verb/fieldName = value/ の形で値を列挙していく。
複数の値を列挙する際は \verb/;/ で区切る。

\lstinputlisting[label=src:agda-record, caption=Agdaにおけるレコード型の定義] {src/AgdaRecord.agda}

構築されたレコードから値を取得する際には \verb/RecordName.fieldName/ という名前の関数を適用する(リスト~\ref{src:agda-record-proj} 内2行目) 。
なお、レコードにもパターンマッチが利用できる(リスト~\ref{src:agda-record-proj} 内5行目)。
また、値を更新する際は \verb/record oldRecord {field = value ; ... }/ という構文を利用する。
Point の中の x の値を5増やす関数 \verb/xPlus5/ はリスト~\ref{src:agda-record-proj}の 7,8行目のように書ける。

\lstinputlisting[label=src:agda-record-proj, caption=Agda におけるレコードの射影、パターンマッチ、値の更新] {src/AgdaRecordProj.agda}

Agda における部分型のように振る舞う機能として Instance Arguments が存在する。
とあるデータ型が、ある型と名前を持つ関数を持つことを保証する。
これは Haskell における型クラスや Java におけるインターフェースに相当する。
Agda における部分型の制約は、必要な関数を定義した record に相当し、その制約を保証するにはその record を instance として登録することになる。
例えば、同じ型と比較することができる、という性質を表すとリスト~\ref{src:agda-type-class}のようになる。
具体的にはとある型 A における中置関数 \verb/_==_/ を定義することに相当する。

\lstinputlisting[label=src:agda-type-class, caption=Agdaにおける部分型制約] {src/AgdaTypeClass.agda}

ある型 T がこの部分型制約を満たすことを示すには、型 T でこのレコードを作成できることを示し、それを instance 構文で登録する。
型Nat が Eq の上位型であることを記述するとリスト~\ref{src-agda-instance}のようになる。

\lstinputlisting[label=src:agda-instance, caption=Agdaにおける部分型関係の構築] {src/AgdaInstance.agda}

これで \verb/Eq/ が要求される関数に対して Nat が適用できるようになる。
例えば型 A の要素を持つ List A から要素を探してくる elem を定義する。
部分型のインスタンスは \verb/{{}}/ 内部に名前と型名で記述する。
なお、名前部分は必須である。
仮に変数として受けても利用しない場合は \verb/_/ で捨てると良い。
部分型として登録した record は関数本体において \verb/{{variableName}}/ という構文で変数に束縛できる。

\lstinputlisting[label=src:agda-use-instance, caption=Agdaにおける部分型を使う関数の定義] {src/AgdaElem.agda.replaced}

この \verb/elem/ 関数はリスト~\ref{src:agda-elem-apply} のように利用できる。
Nat型の要素を持つリストの内部に4が含まれるか確認している。
この \verb/listHas4/ は \verb/true/ に評価される。
なお、 \verb/--/ の後はコメントである。

\lstinputlisting[label=src:agda-elem-apply, caption=部分型を持つ関数の適用] {src/AgdaElemApply.agda.replaced}


% TODO: 必要なら with の解説

\section{Reasoning}