\chapter{定理証明支援系言語 Agda}


%\section{Agda}

Agda とは定理証明支援器であり、関数型言語である。Agda は依存型という型システ
ムを持ち、型を第一級オブジェクトとして扱うことが可能である。また、型システムは
Curry-Howard 同型対応により命題と型付きラムダ計算が一対一で対応するため Agda で
は記述したプログラムを証明することができる。

\section{Agdaの基本}
本節ではAgdaの基本事項についてソースコードを例に出しながら説明を行う。

\subsection{関数の実装}
Agdaでの関数の 定義方法について \coderef{plus} を例として解説する。
基本事項として、$ \mathbb{N} $ というのは自然数 (Natulal Number) のことである。
また - (ハイフン) が2つ連続して並んでいる部分はコメントアウトであり、
ここでは関数を実行した際の例を記述している。
したがって、これは2つの自然数を受け取って足す関数であることが推測できる。

\lstinputlisting[label=plus, caption=plusの実装] {src/agda/plus.agda}

この関数の定義部分の説明をする。コードの1行目に : (セミコロン)がある。
この : の前が関数名になり、その後ろがその関数の定義となる。
: 以降の (x y : $ \mathbb{N} $) は関数は x, y の自然数2つを受けとるという意味になる。
$ \rightarrow $ 以降は関数が返す型を記述している。
まとめると、この関数 plus は、型が自然数である2つの変数 x, y を受け取り、
自然数を返すという定義になる。

Agda では関数の定義をしたコードの直下で実装を行うのが常である。
関数名を記述した後に引数を記述して受け取り、= (イコール) 以降で
引数に対応した実装をする。

今回の場合 plus x zero であれば +0 である為、そのまま x を返す。
実装2行目の方で受け取った y の値を減らし、x の値を増やして再び plus の関数に
遷移している。
受け取った y を +1 されていたとして y の値を減らしている。

関数の実装全体をまとめると、x と y の値を足す為に y から x に数値を1つずつ渡す。
y が 0 になった際に計算が終了となっている。
指折りでの足し算を実装していると捉えても良い。

\subsection{三項演算子の実装}
\_ (アンダースコア) を用いることで入力を受け取る事ができる。
これを用いることで、三項演算子を実装することができる。
以下に、三項演算子を使用した \coderef{plus} と同義の関数の例を
以下 \coderef{plus2} 挙げる。

\lstinputlisting[label=plus2, caption=三項演算子を用いたplusの実装, firstline=5] {src/agda/plus2.agda}

利点としては、直感的な記号論理の記述ができる。
以下、記号論理は基本的に三項演算子を使用して記述する。

\begin{comment}
\subsection{Agdaにおけるラムダ計算}
\lambda
\end{comment}

\subsection{Data 型の実装}
Deta 型とは分岐のことである。
そのため、それぞれの動作について実装する必要がある。
例として既出の Data 型である $ \mathbb{N} $ の実装を \coderef{Nat} に示す。

\lstinputlisting[label=Nat, caption=Natural の定義] {src/agda/Nat.agda}

実装から、$ \mathbb{N} $ という型は zero と suc の2つのコンストラクタを持っていることが分かる。
それぞれの仕様を見てみると、zeroは $ \mathbb{N} $ のみであるが、
suc は (n : $ \mathbb{N} $ ) $ \rightarrow \  \mathbb{N} $ である。
つまり、suc 自体の型は $ \mathbb{N} $ であるが、そこから $ \mathbb{N} $  に遷移するということである。
そのため、suc からは suc か zero に遷移する必要があり、また zero に遷移することで停止する。
したがって、数値は zero に遷移するまでの suc が遷移した数によって決定される。

Data型にはそれぞれの動作について実装する必要があると述べたが、
言い換えればパターンマッチをする必要があると言える。
これは puls 関数で suc 同士の場合と、zeroが含まれる場合の両方を実装していることの説明となる。

% \subsection{パターンマッチ}

\subsection{Record 型の実装}
Record 型とはオブジェクトあるいは構造体ののようなものである。
\coderef{And}は AND の関数となる。p1で前方部分が取得でき、p2で後方部分が取得できる。

\lstinputlisting[label=And の定義, caption=And] {src/agda/And.agda}

また、Agda の関数定義では\_(アンダースコア)で囲むことで三項演算子を定義することができる。

これを使用して三段論法を定義することができる。
定義は「AならばB」かつ「BならばC」なら「AならばC」となる。
\coderef{syllogism}を以下に示す。

\lstinputlisting[label=syllogism の実装, caption=syllogism] {src/agda/syllogism.agda}

コードの解説をすると、引数として x と a が関数に与えられている。
引数 x の中身は ((A $ \rightarrow $ B) ∧ (B $ \rightarrow $ C)) 、引数 a の中身
は A である。したがって、(\_∧\_.p1 x a) で (A $ \rightarrow $ B) に A を与えて B を取得し、
\_∧\_.p2 x で (B $ \rightarrow $ C) であるため、これに B を与えると C が取得できる。
よって A を与えて C を取得することができたため、三段論法を定義できた。

\section{本論で使用する Agda の記法}
本論では、ソースコードを出しながら実施内容について述べるが、
特殊な記法を用いている場合があるので、前もって解説をする。

\subsection{Agdaの省略記法}
Recode が入力された場合のことを考える。この際、入力時に record を展開してしまうと、
コードが長くなってしまい、煩雑になってしまう。
これを防ぐために、withを使用し、必要な変数のみ取り出してパターンマッチを行う。
例を \coderef{abridgement} に示す。

\lstinputlisting[label=abridgement, caption=入力を省略する Agda コードの例, firstline=5] {src/agda/abridgement.agda}

patternmatch-default は入力されている record をそのまま展開することで、
値を取得している。

patternmatch-extraction では、with を使用して入力されているrecordの中から対象の
値だけ取得している。このように、入力時にrecordを展開せずに中の値を取得することも
できる。

patternmatch-extraction' では、入力が同じ場合に ... で省略ができることを使用し、
さらに省略を行っている。

今後のソースコードでは、必要な変数のみ取り出すことでコードを見やすくする。

%\subsection{<-cmp}
% 式変形の方が需要があるかもしれない

% \lstinputlisting[label=syllogism, caption=syllogism, firstline=7,lastline=14] {src/agda/cmp.agda}