|
127
|
1 -title: Agda
|
|
|
2
|
|
|
3 Agda は関数型プログラミング言語で、テキストで記述していく。Haskell に似た構文を持つ。Haskell で実装されている。
|
|
|
4
|
|
|
5 プログラムは必ず以下のように始める。
|
|
|
6
|
|
|
7 module lambda where
|
|
|
8
|
|
|
9 この時に、このファイルは、
|
|
|
10
|
|
|
11 lambad.agda
|
|
|
12
|
|
|
13 と同じ名前を持つ必要がある。
|
|
|
14
|
|
|
15 プログラムは、
|
|
|
16
|
|
|
17 name : type
|
|
|
18 name = value
|
|
|
19
|
|
|
20 という形で関数型言語での関数の型と定義を与える形式。
|
|
|
21
|
|
|
22 仮定なしに使えるのは Set という型しかない。あとは、これから構成していく。構成する要素には、
|
|
|
23
|
|
|
24 関数 ( 型は A → B、値は λ x → y )
|
|
|
25 record
|
|
|
26 data
|
|
|
27
|
|
|
28 の三種類。この三種類だけ憶えればよい。
|
|
|
29
|
|
|
30 Agdaの操作は、
|
|
|
31
|
|
|
32 load と型のチェック 何か入力して、C-C C-L
|
|
|
33 値の計算 C-C C-N の後に式を入力 (プログラムの実行に相当する)
|
|
|
34
|
|
|
35 の二つだけ。その他には、C-C C-C (case文の生成)などがある。
|
|
|
36
|
|
|
37 Agda は indent でblockを構成する文法を持ち、Haskell に近い。しかし、以下のことに気をつけよう。
|
|
|
38
|
|
|
39 (){}. は変数名には使えない(それ以外は全部使える = とかも)
|
|
|
40 : と = と → の前後には空白が必要
|
|
|
41
|
|
|
42 空白がないと「ひと続きの名前」として扱われたり、エラーになったりする。-> でも→でも良い。\ x -> y でも λ x → y でも良い。統一しよう。
|
|
|
43
|
|
|
44 A → B → C は、 A → ( B → C ) のこと
|
|
|
45
|
|
|
46 f x y は (f x) y のこと
|
|
|
47
|
|
|
48 これは複数引数の関数を「少ない引数の関数を返す高階関数」と見るカーリー化に対応している。
|
|
|
49
|
|
|
50 f : A → B → C
|
|
|
51
|
|
|
52 の時に f x は B → C という型を持つ関数を返していると考える。これは Haskell でも同じ。
|
|
|
53
|
|
|
54
|
|
|
55 型と値は組で書く。型は省略できるが、Agda で重要なのは論理式に相当する型の方である。
|
|
|
56
|
|
|
57 name : type
|
|
|
58 name = value
|
|
|
59
|
|
|
60 定義抜きに使えるのは Set のみである。(正確には Set と、レベルの付いた Set n 。Set は Set zero の省略形)
|
|
|
61
|
|
|
62 引数には{}を付けることができる。
|
|
|
63
|
|
|
64 id : ( A : Set ) → A → A
|
|
|
65 id x = x
|
|
|
66
|
|
|
67 は引数の数があっていないので怒られる。
|
|
|
68
|
|
|
69 id : ( A : Set ) → A → A
|
|
|
70 id A x = x
|
|
|
71
|
|
|
72 しかし、A は使われていない。使われてない変数は _ で省略できる。
|
|
|
73
|
|
|
74 id : ( A : Set ) → A → A
|
|
|
75 id _ x = x
|
|
|
76
|
|
|
77 ここでAに{}を付ける。
|
|
|
78
|
|
|
79 id : { A : Set } → A → A
|
|
|
80 id {_} x = x
|
|
|
81
|
|
|
82 推論できる{}な変数は省略することが可能である。
|
|
|
83
|
|
|
84 id : { A : Set } → A → A
|
|
|
85 id x = x
|
|
|
86
|
|
|
87 省略された呼出を明示することもできる。
|
|
|
88
|
|
|
89 f1 : Nat → Nat
|
|
|
90 f1 = id {Nat}
|
|
|
91
|
|
|
92 Haskell で id x = x で定義された id の型を調べてみよう。
|
|
|
93
|
|
|
94 --Agda の infix operator
|
|
|
95
|
|
|
96 _・_
|
|
|
97
|
|
|
98 と書くことにより、
|
|
|
99
|
|
|
100 a ・ b
|
|
|
101
|
|
|
102 は
|
|
|
103
|
|
|
104 _・_ a b
|
|
|
105
|
|
|
106 と同じに扱われる。infix により演算子の順位などを制御することができる。(・の代わりに.を使うと構文エラーになる)
|
|
|
107
|
|
|
108 --Agda での?
|
|
|
109
|
|
|
110 わからない部分には ? と書くことができる。
|
|
|
111
|
|
|
112 _・_ : {A : Set } → ?
|
|
|
113 f ・ g = λ x → f ( g x )
|
|
|
114
|
|
|
115 この? を埋めていく作業が証明になる。
|
|
|
116
|
|
|
117 --Agda でのエラー
|
|
|
118
|
|
|
119 C-C C-L の時に、Agda は
|
|
|
120
|
|
|
121 赤 型が衝突していることを示す (書き直しが必要)
|
|
|
122 黄 十分に引数が具体化(instanciate)されてないことを示す
|
|
|
123 緑 ? で、まだ決めてない部分
|
|
|
124
|
|
|
125 などのerrorを出す。これをなくすごとが証明の目標である。
|
|
|
126
|
|
|
127 黄色の場合は、{}で省略された型変数を指定するとなおることがある。
|
|
|
128
|
|
|
129 エラーが残っている modulde を import することはできない。
|
|
|
130
|
|
|
131 他にも
|
|
|
132
|
|
|
133 f = f
|
|
|
134 Termination checking failed for the following functions:
|
|
|
135 f
|
|
|
136
|
|
|
137 などのerrorがでる。
|
|
|
138
|
|
|
139 --Agda の設定
|
|
|
140
|
|
|
141 % brew info agda
|
|
|
142
|
|
|
143 を見ると、
|
|
|
144
|
|
|
145 ==> Caveats
|
|
|
146 To use the Agda standard library by default:
|
|
|
147 mkdir -p ~/.agda
|
|
|
148 echo /usr/local/lib/agda/standard-library.agda-lib >>~/.agda/libraries
|
|
|
149 echo standard-library >>~/.agda/defaults
|
|
|
150
|
|
|
151 とある。~/.agda がちゃんと設定されているかどうかを確認しよう。
|
|
|
152
|
|
|
153 文字がずれる場合は、
|
|
|
154
|
|
|
155 <a href="https://attonblog.blogspot.com/2016/11/homebrew-agda-2512.html"> atton のblog </a>
|
|
|
156
|
|
|
157 を参考にして、eaw.el を入れます。
|
|
|
158
|
|
|
159
|
|
|
160
|
|
|
161
|
|
|
162
|
|
|
163
|
|
|
164
|
