Agda \cite{agda} は純粋関数型言語である。
Agda は依存型という型システムを持ち、型を第一級オブジェクトとして扱う。

Agda の記述ではインデントが意味を持ち、スペースの有無もチェックされる。
コメントは \verb/-- comment/ か \verb/{-- comment --}/ のように記述される。
また、\verb/_/でそこに入りうるすべての値を示すことができ、
\verb/?/でそこに入る値や型を不明瞭なままにしておくことができる。

%% データについて
Agda では型をデータや関数に記述する必要がある。
Agda における型指定は \verb/:/ を用いて \verb/name : type/ のように記述する。
このとき \verb/name/ に 空白があってはいけない。
データ型は、代数的なデータ構造で、その定義には \verb/data/ キーワードを用いる。
\verb/data/ キーワードの後に \verb/data/ の名前と、型、 \verb/where/ 句を書きインデントを深くし、
値にコンストラクタとその型を列挙する。

Code \ref{agda-nat}は自然数の型である $\mathbb{N}$ (Natural Number)を例である。

\lstinputlisting[label=agda-nat, caption=自然数を表すデータ型 Nat の定義] {src/nat.agda.replaced}

\verb/Nat/ では \verb/zero/ と \verb/suc/ の2つのコンストラクタを持つデータ型である。
\verb/suc/ は $\mathbb{N}$ を受け取って $\mathbb{N}$ を表す再帰的なデータになっており、
\verb/suc/ を連ねることで自然数全体を表現することができる。

$\mathbb{N}$ 自身の型は \verb/Set/ であり、これは Agda が組み込みで持つ「型集合の型」である。
\verb/Set/ は階層構造を持ち、型集合の集合の型を指定するには \verb/Set1/ と書く。
%% \verb/Level/ を用いることで異なる \verb/Set/ を表現できる。

Agda には C 言語における構造体に相当するレコード型というデータも存在する、
例えば \verb/x/ と \verb/y/ の二つの自然数からなるレコード \verb/Point/ を定義する。Code \ref{agda-record}のようになる。
\lstinputlisting[label=agda-record, caption=Agdaにおけるレコード型の定義] {src/env.agda.replaced}
レコードを構築する際は \verb/record/ キーワード後の \verb/{}/ の内部に \verb/FieldName = value/ の形で値を列挙する。
複数の値を列挙するには \verb/;/ で区切る必要がある。

%% 関数について
Agda での関数は型の定義と、関数の定義をする必要がある。
関数の型はデータと同様に \verb/:/ を用いて \verb/name : type/ に記述するが、入力を受け取り出力返す型として記述される。$\rightarrow$ 、 または\verb/→/ を用いて \verb/input → output/ のように記述される。
また、\verb/_+_/のように関数名で\verb/_/を使用すると引数がその位置にあることを意味し、中間記法で関数を定義することもできる。
関数の定義は型の定義より下の行に、\verb/=/ を使い \verb/name input = output/ のように記述される。

例えば引数が型 \verb/A/ で返り値が型 \verb/B/ の関数は \verb/A → B/ のように書くことができる。
また、複数の引数を取る関数の型は \verb/A → A → B/ のように書ける。
例として任意の自然数$\mathbb{N}$を受け取り、\verb/+1/した値を返す関数はCode \ref{agda-function}のように定義できる。
\lstinputlisting[label=agda-function, caption=Agda における関数定義] {src/agda-func.agda.replaced}


引数は変数名で受けることもでき、具体的なコンストラクタを指定することでそのコンストラクタが渡された時の挙動を定義できる。
これはパターンマッチと呼ばれ、コンストラクタで case 文を行なっているようなものである。
例として自然数$\mathbb{N}$の加算を関数で書くとCode \ref{agda-plus}のようになる。

\lstinputlisting[label=agda-plus, caption=自然数での加算の定義] {src/agda-plus.agda.replaced}
%% \lstinputlisting[label=agda-not, caption=Agdaにおける関数 not の定義] {src/AgdaNot.agda.replaced}

パターンマッチでは全てのコンストラクタのパターンを含む必要がある。
例えば、自然数$\mathbb{N}$を受け取る関数では \verb/zero/ と \verb/suc/ の2つのパターンが存在する必要がある。
なお、コンストラクタをいくつか指定した後に変数で受けることもでき、その変数では指定されたもの以外を受けることができる。
例えばCode \ref{agda-pattern}の減算では初めのパターンで2つ目の引数が\verb/zero/のすべてのパターンが入る。


\lstinputlisting[label=agda-pattern, caption=自然数の減算によるパターンマッチの例] {src/agda-pattern.agda.replaced}

Agda には$\lambda$計算が存在している。$\lambda$計算とは関数内で生成できる無名の関数であり、
\verb/\arg1 arg2 → function/ または $\lambda$\verb/arg1 arg2 → function/ のように書くことができる。
Code \ref{agda-function} で例とした \verb/+1/ をラムダ計算で書くとCode \ref{agda-lambda}の\verb/$\lambda$+1/ように書くことができる。この二つの関数は同一の動作をする。

\lstinputlisting[label=agda-lambda, caption=Agda におけるラムダ計算] {src/AgdaLambda.agda.replaced}

Agda では特定の関数内のみで利用できる関数を \verb/where/ 句で記述できる。
スコープは \verb/where/句が存在する関数内部のみであるため、名前空間が汚染させることも無い。
例えば自然数3つを取ってそれぞれ3倍して加算する関数 \verb/f/ を定義するとき、 \verb/where/ を使うとリストCode \ref{agda-where} のように書ける。
これは \verb/f'/ と同様の動作をする。
\verb/where/ 句は利用したい関数の末尾にインデント付きで \verb/where/ キーワードを記述し、改行の後インデントをして関数内部で利用する関数を定義する。

\lstinputlisting[label=agda-where, caption=Agda における where 句] {src/AgdaWhere.agda.replaced}

また Agda では停止性の検出機能が存在し、プログラム中に停止しない記述が存在するとコンパイル時にエラーが出る。
\verb/{-# TERMINATING #-}/のタグを付けると停止しないプログラムをコンパイルすることができるがあまり望ましくない。
Code \ref{term} で書かれた、\verb/loop/ と \verb/stop/ は任意の自然数を受け取り、0になるまでループして0を返す関数である。
\verb/loop/ では $\mathbb{N}$ の数を受け取り、 \verb/loop/ 自身を呼び出しながら 数を減らす関数 pred を呼んでいる。しかし、\verb/loop/の記述では関数が停止すると言えないため、定義するには\verb/{-# TERMINATING #-}/のタグが必要である。
\verb/stop/ では自然数がパターンマッチで分けられ、\verb/zero/のときは \verb/zero/を返し、 \verb/suc n/ のときは \verb/suc/ を外した \verb/n/ で stop を実行するため停止する。

\lstinputlisting[label=term, caption=停止しない関数 loop、停止する関数 stop] {src/termination.agda.replaced}

このように再帰的な定義の関数が停止するときは、何らかの値が減少する必要がある。


\section{定理証明支援器としての Agda}
Agda での証明では関数の記述と同様の形で型部分に証明すべき論理式、 $\lambda$ 項部分にそれを満たす証明を書くことで証明を行うことが可能である。
証明の例として Code Code \ref{proof} を見る。
ここでの \verb/+zero/ は右から \verb/zero/ を足しても ≡ の両辺は等しいことを証明している。
これは、引数として受けている \verb/y/ が \verb/Nat/ なので、 \verb/zero/ の時と \verb/suc y/ の二つの場合を証明する必要がある。
\lstinputlisting[caption=等式変形の例,label=proof]{src/zero.agda.replaced}
\verb/y = zero/ の時は $zero \equiv zero$ とできて、左右の項が等しいということを表す \verb/refl/ で証明することができる。
\verb/y = suc y/ の時は $x \equiv y$ の時 $fx \equiv fy$ が成り立つという
Code \ref{cong}の \verb/cong/ を使って、y の値を 1 減らしたのち、再帰的に \verb/+zero y/
を用いて証明している。
\lstinputlisting[caption=cong,label=cong]{src/cong.agda.replaced}

%% \begin{lstlisting}[caption=等式変形の例,label=proof]
%% +zero : { y : ℕ } → y + zero  ≡ y
%% +zero {zero} = refl
%% +zero {suc y} = cong ( λ x → suc x ) ( +zero {y} )
%%
%% -- cong : ∀ (f : A → B) {x y} → x ≡ y → f x ≡ f y
%% -- cong f refl = refl
%% \end{lstlisting}

また、他にも $\lambda$ 項部分で等式を変形する構文がいくつか存在している。
ここでは \verb/rewrite/ と ≡\verb/-Reasoning/ の構文を説明するとともに、等式を変形する構文の例として加算の交換則について示す。

\verb/rewrite/ では 関数の \verb/=/ 前に \verb/rewrite 変形規則/ の形で記述し、複数の規則を使う場合は \verb/rewrite/ 変形規則1 \verb/|/ 変形規則2 のように \verb/|/を用いて記述する。
Code \ref{agda-term-post} にある \verb/+-comm/ で \verb/x/ が \verb/zero/ のパターンが良い例である。
ここでは、\verb/+zero/ を利用し、 \verb/zero + y/ を \verb/y/ に変形することで $y \equiv y$となり、左右の項が等しいことを示す \verb/refl/ になっている。

\lstinputlisting[caption=等式変形の例3/3,label=agda-term-post]{src/agda-term3.agda.replaced}
Code \ref{agda-term-post} では \verb/suc (y + x)/ $equiv$ \verb/y + (suc x)/ という等式に対して $equiv$ の対称律 \verb/sym/ を使って左右の項を反転させ\verb/y + (suc x)/ $equiv$ \verb/suc (y + x)/の形にし、\verb/y + (suc x)/が\verb/suc (y + x)/ に変形できることを \verb/+-suc/ を用いて示した。
これにより等式の左右の項が等しくなったため \verb/+-comm/ が示せた。

Agda ではこのような形で等式を変形しながら証明を行う事ができる。