\section{Agda}

Agda とは定理証明支援器であり、関数型言語である。Agda は依存型という型システ
ムを持ち、型を第一級オブジェクトとして扱うことが可能である。また、型システムは
Curry-Howard 同型対応により命題と型付きラムダ計算が一対一で対応するため Agda で
は記述したプログラムを証明することができる。
\begin{comment}
\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 を受け取り、
自然数を返すという定義になる。
		
関数の定義をしたコードの直下で実装を行うのが常である。
関数名を記述した後に引数を記述して受け取り、= (イコール) 以降で
引数に対応した実装をする。

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

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