|
0
|
1 # Agda入門
|
|
|
2
|
|
|
3 間違いもあると思うが一応記録していく。
|
|
|
4
|
|
|
5 ## 基本動作
|
|
|
6 基本的なコードを以下に記載する。
|
|
|
7
|
|
|
8 ```agda:hello.agda
|
|
|
9 module hello where
|
|
|
10
|
|
|
11 test1 : Set → Set
|
|
|
12 test1 x = x
|
|
|
13 ```
|
|
|
14
|
|
|
15 書いた定義を
|
|
|
16 C-c C-l でコンパイルすることができる。
|
|
|
17
|
|
|
18 書いたコードの解説をすると、
|
|
|
19 - `module hello where`は必要な宣言で、`module`の次にファイル名を記述する。
|
|
|
20 - `test :`の行は関数の宣言と仕様の記述をしている。
|
|
|
21 - `:`の前で関数名を定義している
|
|
|
22 - `:`の後で仕様の記述をしている。
|
|
|
23 - 意味はこの関数は**型**がSetの引数を受けとり、返り値として**型**がSetのものを返す。
|
|
|
24 - `test =`の行は関数の実装を記述している。
|
|
|
25 - `=`の前にxがあるが、これは関数が引数としてxを受け取ったことを表している。
|
|
|
26 - 余談だがHaskellでも同じように関数の後ろに引数を記述する。
|
|
|
27 - 仕様として、引数で受け取った物をそのまま返しても成り立つ
|
|
|
28 - Setを受け取りSetを返すだけなのでこれで良い
|
|
|
29
|
|
|
30 また、`=`から後方を削除し、`?`を入力しC-c C-lすることもできる。その際に`{ }`が表示される。
|
|
|
31 - その中でC-c C-, すると引数に何が格納されているのか見ることができる。
|
|
|
32 - また、C-c C-a するとAuto (proof search)ができ、自動でできるならAgdaが自動的に補完をしてくれる。
|
|
|
33
|
|
2
|
34 関数を実行したい際にはC-c C-n で実行することができる。
|
|
|
35
|
|
0
|
36 コマンド群は[ここ](https://agda.wiki.fc2.com/wiki/コマンド一覧)にも記載されている。
|
|
2
|
37 特殊文字などもみんなのagdaに記載されている。
|
|
0
|
38
|
|
|
39 ## 関数定義
|
|
2
|
40 関数定義の際に基本となる記述を記載しておく。
|
|
0
|
41
|
|
2
|
42 ```agda:func.agda
|
|
|
43 test2 : (A : Set) → Set
|
|
|
44 test2 a = a
|
|
|
45
|
|
|
46 -- 引数を増やすこともできる。
|
|
|
47 test3 : (A B : Set) → Set
|
|
|
48 test3 a b = b
|
|
|
49
|
|
|
50 -- ()ではなく{}で方を定義することもできる。その場合{}で定義した部分の変数を隠すことができる。
|
|
|
51 test4 : {A B : Set} → A → (A → B) → B
|
|
|
52 test4 a x = x a
|
|
|
53
|
|
|
54 -- {}で定義した部分を取得することも可能
|
|
|
55 test5 : {A B : Set} → A → (A → B) → B
|
|
|
56 test5 {A} {B} a x = x a
|
|
|
57
|
|
|
58 -- 上記の{}で定義した物を()で書き換えると以下のようになる
|
|
|
59 test6 : (A B : Set) → A → (A → B) → B
|
|
|
60 test6 A B a x = x a
|
|
|
61 -- あまりスマートではないし定義の意味が{}で記述した場合と違う
|
|
|
62 ```
|
|
0
|
63
|
|
|
64 ## data型
|
|
|
65
|
|
2
|
66 ```agda:data.agda
|
|
|
67 -- 次はdata型とrecord型の説明
|
|
|
68 -- 記号などはみんなのagdaにほとんど載っていたり、普通にググっても出る。
|
|
0
|
69
|
|
2
|
70 data _∨_ (A B : Set) : Set where
|
|
|
71 front : A → A ∨ B
|
|
|
72 back : B → A ∨ B
|
|
|
73 -- 関数名として_∨_を定義しているが、これで中置演算子を定義することができる。
|
|
|
74 -- 実際にやっていることは下記に定義している関数と同じ
|
|
|
75
|
|
|
76 data or (A B : Set) : Set where
|
|
|
77 front : A → or A B
|
|
|
78 back : B → or A B
|
|
|
79 ```
|
|
|
80 data型というのは分岐のことであり、「どちらか一方が必ず動作する。」ということになる。
|
|
|
81
|
|
|
82 わかり易い例としてBool型の定義がある。
|
|
|
83 ```
|
|
|
84 data Bool : Set where
|
|
|
85 true : Bool
|
|
|
86 false : Bool
|
|
|
87 ```
|
|
|
88 data型を使用した例としてジャンケンを定義してみる。
|
|
|
89 ```agda:rps.agda
|
|
|
90 data hand : Set where
|
|
|
91 r : hand
|
|
|
92 p : hand
|
|
|
93 s : hand
|
|
|
94
|
|
|
95 -- 「手」を二つ受け取って勝った方の手を返すように設計すると
|
|
|
96 -- 定義は「handを2つ受け取る。最終的にhandを返す」となり、以下のようになる。
|
|
|
97 rps : (A B : hand) → hand
|
|
|
98 -- rps : hand → hand → hand これでも良い
|
|
|
99 -- rps : (_ _ : hand) → hand これでもできるかもしれない
|
|
|
100 rps r r = r
|
|
|
101 rps r p = p
|
|
|
102 rps r s = r
|
|
|
103 rps p r = p
|
|
|
104 rps p p = p
|
|
|
105 rps p s = s
|
|
|
106 rps s r = r
|
|
|
107 rps s p = s
|
|
|
108 rps s s = s
|
|
|
109 ```
|
|
|
110 場合分けの数が足りない場合、agdaが親切に怒ってくれる。
|
|
|
111
|
|
|
112
|
|
|
113 ## record型
|
|
|
114 data型とは違い、
|
|
|
115 オブジェクトあるいは構造体のようなもの。
|
|
|
116 以下の関数はAND。p1で前方部分が取得でき、p2で後方部分が取得できる。
|
|
|
117
|
|
|
118 ``` agda:record.agda
|
|
|
119 record _∧_ (A B : Set) : Set where
|
|
|
120 field
|
|
|
121 p1 : A
|
|
|
122 p2 : B
|
|
|
123
|
|
|
124 -- 普通にANDの後ろの方を取得することもできる
|
|
|
125 datatest1 : {A B C : Set} → (A ∧ (B → C )) → (B → C)
|
|
|
126 datatest1 x b = _∧_.p2 x b
|
|
|
127
|
|
|
128
|
|
|
129 -- ANDの後ろの方を取得した結果を使用することもできる。
|
|
|
130 datatest : {A B C : Set} → B → (A ∧ (B → C )) → C
|
|
|
131 datatest b x = _∧_.p2 x b
|
|
|
132 ```
|
|
|
133
|
|
|
134 これらを使用して三段論法を定義することができる。
|
|
|
135 定義は「AならばB」かつ「BならばC」なら「AならばC」となる。
|
|
|
136 ```
|
|
|
137 syllogism : {A B C : Set} → ((A → B) ∧ (B → C)) → (A → C)
|
|
|
138 syllogism x a = _∧_.p2 x (_∧_.p1 x a)
|
|
|
139 ```
|
|
|
140
|
|
|
141
|
|
|
142
|
|
|
143
|
|
|
144
|
|
|
145
|
|
|
146
|
|
|
147
|
|
|
148
|
|
|
149
|
|
|
150
|
|
|
151
|
|
|
152
|
|
|
153
|
|
|
154
|
|
|
155
|
|
|
156
|
|
|
157
|
|
|
158
|
|
|
159
|
|
|
160
|
