|
4
|
1 \section{Agda}
|
|
6
|
2
|
|
4
|
3 Agda とは定理証明支援器であり、関数型言語である。Agda は依存型という型システ
|
|
|
4 ムを持ち、型を第一級オブジェクトとして扱うことが可能である。また、型システムは
|
|
|
5 Curry-Howard 同型対応により命題と型付きラムダ計算が一対一で対応するため Agda で
|
|
|
6 は記述したプログラムを証明することができる。
|
|
|
7
|
|
6
|
8 \subsection{プログラムの読み方}
|
|
|
9 以下は Agda プログラムの一例となる。
|
|
8
|
10 本節ではAgdaの基本事項について解説する。
|
|
7
|
11
|
|
|
12 基本事項として、ℕ というのは自然数 (Natulal Number) のことである。
|
|
|
13 また - (ハイフン) が2つ連続して並んでいる部分はコメントアウトであり、
|
|
|
14 ここでは関数を実行した際の例を記述している。
|
|
|
15 したがって、この関数は2つの自然数を受け取って足す関数であることが推測できる。
|
|
|
16
|
|
6
|
17 \lstinputlisting[label=plus, caption=plus] {src/agda/plus.agda}
|
|
4
|
18
|
|
7
|
19 この関数の定義部分の説明をする。コードの1行目に : (セミコロン)がある。
|
|
|
20 この : の前が関数名になり、その後ろがその関数の定義となる。
|
|
|
21 : 以降の (x y : ℕ ) は関数は x, y の自然数2つを受けとるという意味になる。
|
|
|
22 → 以降は関数が返す型を記述している。
|
|
|
23 まとめると、この関数 plus は、型が自然数である2つの変数が x, y を受け取り、
|
|
|
24 自然数を返すという定義になる。
|
|
|
25
|
|
|
26 関数の定義をしたコードの直下で実装を行うのが常である。
|
|
|
27 関数名を記述した後に引数を記述して受け取り、= (イコール) 以降で
|
|
|
28 引数に対応した実装をする。
|
|
|
29
|
|
|
30 今回の場合 plus x zero であれば +0 である為、そのまま x を返す。
|
|
|
31 実装2行目の方で受け取った y の値を減らし、x の値を増やして再び plus の関数に
|
|
|
32 遷移している。
|
|
|
33 受け取った y を +1 されていたとして y の値を減らしている。
|
|
|
34
|
|
|
35 関数の実装全体をまとめると、x と y の値を足す為に y から x に数値を1つずつ渡す。
|
|
|
36 y が 0 になった際に計算が終了となっている。
|
|
8
|
37 指折りでの足し算を実装していると捉えても良い。
|
|
6
|
38
|
|
|
39 \subsection{Data 型}
|
|
|
40 Deta 型とは分岐のことである。
|
|
|
41 そのため、それぞれの動作について実装する必要がある。
|
|
|
42 例として既出で Data 型である ℕ の実装を見てみる。
|
|
|
43
|
|
|
44 \lstinputlisting[label=Nat, caption=Nat] {src/agda/Nat.agda}
|
|
|
45
|
|
|
46 実装から、ℕ という型は zero と suc の2つのコンストラクタを持っていることが分かる。
|
|
|
47 それぞれの仕様を見てみると、zeroは ℕ のみであるが、suc は (n : ℕ) → ℕ である。
|
|
|
48 つまり、suc 自体の型は ℕ であるが、そこから ℕ に遷移するということである。
|
|
|
49 そのため、suc からは suc か zero に遷移する必要があり、また zero に遷移することで停止する。
|
|
|
50 したがって、数値は zero に遷移するまでの suc が遷移した数によって決定される。
|
|
|
51
|
|
|
52 Data型にはそれぞれの動作について実装する必要があると述べたが、
|
|
|
53 言い換えればパターンマッチをする必要があると言える。
|
|
|
54 これは puls 関数で suc 同士の場合と、zeroが含まれる場合の両方を実装していることの説明となる。
|
|
|
55
|
|
|
56
|
|
|
57
|
|
|
58 \subsection{Record 型}
|
|
|
59 Record 型とはオブジェクトあるいは構造体ののようなものである。
|
|
|
60 以下の関数は AND となる。p1で前方部分が取得でき、p2で後方部分が取得できる。
|
|
|
61
|
|
|
62 \lstinputlisting[label=And, caption=And] {src/agda/And.agda}
|
|
|
63
|
|
|
64 また、Agda の関数定義では\_(アンダースコア)で囲むことで三項演算子を定義することができる。
|
|
|
65
|
|
|
66 これを使用して三段論法を定義することができる。
|
|
|
67 定義は「AならばB」かつ「BならばC」なら「AならばC」となる。
|
|
|
68 コードを以下に示す。
|
|
|
69
|
|
|
70 \lstinputlisting[label=syllogism, caption=syllogism] {src/agda/syllogism.agda}
|
|
|
71
|
|
|
72 コードの解説をすると、引数として x と a が関数に与えられている。
|
|
|
73 引数 x の中身は((A → B) ∧ (B → C))、引数 a の中身は A である。
|
|
|
74 したがって、(\_∧\_.p1 x a) で (A → B) に A を与えて B を取得し、
|
|
|
75 \_∧\_.p2 x で (B → C) であるため、これに B を与えると C が取得できる。
|
|
|
76 よって A を与えて C を取得することができたため、三段論法を定義できた。
|
|
4
|
77
|
|
|
78 %\subsection{Agdaの基本操作}
|
|
|
79
|
|
|
80 %\subsection{定理証明支援器としての Agda}
|
|
|
81
|
|
|
82 %\subsectoin{}
|
|
|
83
|
|
|
84
|
