|
37
|
1 -title: 証明と関数型言語、Agda
|
|
|
2
|
|
|
3 問題は、メールでSubjectを (a01 の 問題2.5ならば)
|
|
|
4 Subject: Report on Automan Lecture 2.5
|
|
|
5 として、問題毎に提出すること。
|
|
|
6
|
|
|
7 kono@ie.u-ryukyu.ac.jp まで送ること。
|
|
|
8 番号のついてない問題はオプションです。
|
|
|
9
|
|
|
10 学籍番号をメールの中に記述すること。
|
|
|
11 問題番号は正確に記述すること。
|
|
|
12 出席しない場合でも、問題解答を送れば出席扱いとします。
|
|
|
13
|
|
|
14 提出期限は ura.ie.classes.automaton で知らせます。
|
|
|
15
|
|
|
16
|
|
|
17 --証明と関数型言語の関係
|
|
|
18
|
|
|
19 証明とは、論理式それを結ぶ推論からなる数学的な構造である。また、関数型言語は集合である型とそれを結ぶ関数からなる数学的構造である。
|
|
|
20
|
|
|
21 型つきλ計算と論理が対応するように、データ構造と論理演算子(∧とか∨)を対応させることにより
|
|
|
22
|
|
|
23 論理式を型として表し、推論を型つきλ計算の項とすると、この二つは似ていることがわかる。
|
|
|
24
|
|
|
25
|
|
|
26 --あらすじ
|
|
|
27
|
|
|
28 1) 論理式を変数とそれを結ぶ演算子(connectives)で定義する
|
|
|
29 これは構文定義、あるいは、論理式の作り方に相当する
|
|
|
30
|
|
|
31 2) 演算子を導入する推論と、除去する推論を定義する。
|
|
|
32 これには証明図を使う
|
|
|
33
|
|
|
34 3) 推論に対応する関数を表す項を考える
|
|
|
35 項は関数型言語の要素になる
|
|
|
36
|
|
|
37 項の導入 ... データ構造のconstructor
|
|
|
38 項の除去 ... データ構造のaccesor
|
|
|
39
|
|
|
40 導入は関数の出力の型に現れる
|
|
|
41 除去は関数の入力の型に現れる
|
|
|
42
|
|
|
43 これを演算子の数の分だけ繰り返す。
|
|
|
44
|
|
|
45 次に等式論理を学ぶ。
|
|
|
46
|
|
|
47 4) x = x の導入と除去
|
|
|
48
|
|
|
49 5) 項が等しいとはとういうことかを学ぶ
|
|
|
50 正規形
|
|
|
51
|
|
|
52 正規形を得ることが関数型言語の計算(項の操作)
|
|
|
53
|
|
|
54 以上のことを Agda (Haskell に似た構文を持つ証明支援系)で記述する。
|
|
|
55
|
|
|
56 --証明の基本
|
|
|
57
|
|
|
58 A は論理式を表す変数。あるいは型Aという集合。論理式は変数と論理演算子で表される木構造。変数や演算子は構文要素。
|
|
|
59
|
|
|
60 A → B
|
|
|
61
|
|
|
62 これは「AならばB」というのに対応する。関数の視点からは、Aという型からBという型への関数。
|
|
|
63 AとBは型を表す論理式。
|
|
|
64
|
|
|
65 A
|
|
|
66 -----------
|
|
|
67 B
|
|
|
68
|
|
|
69 Aを仮定して、Bが証明されたことを表す図。証明図。
|
|
|
70
|
|
|
71 --関数適用による証明
|
|
|
72
|
|
|
73 導入 除去
|
|
|
74
|
|
|
75 A
|
|
|
76 :
|
|
|
77 B A A → B
|
|
|
78 ------------- ------------------
|
|
|
79 A → B B
|
|
|
80
|
|
|
81 対応する項。項とは、関数型プログラムを構成する構文要素。木構造で表される。
|
|
|
82
|
|
|
83
|
|
|
84 λ x → y
|
|
|
85
|
|
|
86 x は変数、y は項。y は複雑な項(関数のbody)でも良い。これは構文定義でもある。変数 x と項yから
|
|
|
87 λ x → y という項を作れる。 x は構文的にスコープを持っている。つまり、関数の引数と同じ扱いとする。
|
|
|
88
|
|
|
89 項には型が対応する。これは、再帰的に定義される
|
|
|
90
|
|
|
91 x : A
|
|
|
92
|
|
|
93 は、x という項が型Aを持つと言うのを表している。
|
|
|
94
|
|
|
95 x : A かつ y : B の時に、
|
|
|
96
|
|
|
97 λ x → y : A → B
|
|
|
98
|
|
|
99 と定義する。
|
|
|
100
|
|
|
101 ---問題2.1 Agdaによる関数と証明
|
|
|
102
|
|
|
103
|
|
|
104 以下の agda の ? の部分を埋めよ。対応する証明図をコメントで書くこと。
|
|
|
105
|
|
|
106 <a href="agda/lambda.agda"> lambda </a> <!--- Exercise 2.1 --->
|
|
|
107
|
|
|
108
|
|
|
109 ---Agdaの構文
|
|
|
110
|
|
|
111 型と値
|
|
|
112
|
|
|
113 名前の作り方
|
|
|
114
|
|
|
115 indent
|
|
|
116
|
|
|
117 implicit variable
|
|
|
118
|
|
|
119 infix operator and operator order
|
|
|
120
|
|
|
121 <a href="agda.html"> agda の細かい構文の話 </a>
|
|
|
122
|
|
|
123 --record または ∧
|
|
|
124
|
|
|
125 導入 除去
|
|
|
126
|
|
|
127 A B A ∧ B A ∧ B
|
|
|
128 ------------- ----------- π1 ---------- π2
|
|
|
129 A ∧ B A B
|
|
|
130
|
|
|
131 除去は複数あるので名前を区別する必要がある。つまり、それぞれに項を用意する必要がある。
|
|
|
132
|
|
|
133 A ∧ B は新しく導入した型である。
|
|
|
134 型Aと型Bから作るデータ構造であり、オブジェクトあるいは構造体だと思って良い。
|
|
|
135 π1 π2 は構造体から field を抜き出す accesor によって実装できる。
|
|
|
136
|
|
|
137
|
|
|
138
|
|
|
139 record によって
|
|
|
140
|
|
|
141 record _∧_ A B : Set
|
|
|
142 field
|
|
|
143 π1 : A
|
|
|
144 π2 : B
|
|
|
145
|
|
|
146 _∧_ は中置演算子を表す。
|
|
|
147
|
|
|
148 _∧_ A B
|
|
|
149
|
|
|
150 は
|
|
|
151
|
|
|
152 A ∧ B
|
|
|
153
|
|
|
154 とかける。(Haskell では (∧) を使う)
|
|
|
155
|
|
|
156 は、型Aと型Bから作るデ0ータ構造である。オブジェクトあるいは構造体だと思って良い。
|
|
|
157
|
|
|
158 record { π1 = x ; π2 = y }
|
|
|
159
|
|
|
160
|
|
|
161 ---例題
|
|
|
162
|
|
|
163 A → B ∧ B → C → A → C
|
|
|
164
|
|
|
165 まず、正しくかっこを付ける。
|
|
|
166
|
|
|
167 (( A → B ) ∧ ( B → C )) → ( A → C )
|
|
|
168
|
|
|
169 線を上に引く。
|
|
|
170
|
|
|
171 :
|
|
|
172 -------------------------------------------------
|
|
|
173 (( A → B ) ∧ ( B → C )) → ( A → C )
|
|
|
174
|
|
|
175 : はこれから埋めていく部分。まず適用するのは→のintro duction である。 ( A → B ) ∧ ( B → C )を仮定で使えるようになる。
|
|
|
176
|
|
|
177 :
|
|
|
178 A → C
|
|
|
179 -------------------------------------------------
|
|
|
180 (( A → B ) ∧ ( B → C )) → ( A → C )
|
|
|
181
|
|
|
182 さらに→introを使う。Aを仮定で使えるようになる。
|
|
|
183
|
|
|
184 :
|
|
|
185 C
|
|
|
186 -------------------------------------------------
|
|
|
187 A → C
|
|
|
188 -------------------------------------------------
|
|
|
189 (( A → B ) ∧ ( B → C )) → ( A → C )
|
|
|
190
|
|
|
191 仮定でCを生成できるのは B → C しかない。
|
|
|
192
|
|
|
193 B B → C
|
|
|
194 ---------------------
|
|
|
195 C
|
|
|
196
|
|
|
197 これは→elim である。 B → C は仮定( A → B ) ∧ ( B → C )の左側が使える
|
|
|
198
|
|
|
199 ( A → B ) ∧ ( B → C )
|
|
|
200 --------------------- π2
|
|
|
201 B → C
|
|
|
202
|
|
|
203 B の方もがんばると、最終的に
|
|
|
204
|
|
|
205 [ ( A → B ) ∧ ( B → C )]*1
|
|
|
206 --------------------------------- π1
|
|
|
207 [A]*2 A → B [ ( A → B ) ∧ ( B → C ) ]*1
|
|
|
208 ---------------- →elim ------------------------------- π2
|
|
|
209 B B → C
|
|
|
210 ----------------------------------------------- →elim
|
|
|
211 C
|
|
|
212 ------------------------------------------------- →intro 2
|
|
|
213 A → C
|
|
|
214 ------------------------------------------------- →intro 1
|
|
|
215 (( A → B ) ∧ ( B → C )) → ( A → C )
|
|
|
216
|
|
|
217 となる。
|
|
|
218
|
|
|
219 Agda では、
|
|
|
220
|
|
|
221 lemma : (( A → B ) ∧ ( B → C )) → ( A → C )
|
|
|
222 lemma = ?
|
|
|
223
|
|
|
224 とすると、A B C が未定義だと言われる。
|
|
|
225
|
|
|
226 lemma : {A B C : Set } → (( A → B ) ∧ ( B → C )) → ( A → C )
|
|
|
227 lemma = ?
|
|
|
228
|
|
|
229 引数が一つあるので、それに名前を付ける。
|
|
|
230
|
|
|
231 lemma : {A B C : Set } → (( A → B ) ∧ ( B → C )) → ( A → C )
|
|
|
232 lemma f∧g = ?
|
|
|
233
|
|
|
234 いや引数は二つだった。
|
|
|
235
|
|
|
236 lemma : {A B C : Set } → (( A → B ) ∧ ( B → C )) → ( A → C )
|
|
|
237 lemma f∧g a = ?
|
|
|
238
|
|
|
239 f∧g は直積なので、
|
|
|
240
|
|
|
241 π1 f∧g : A → B
|
|
|
242 π2 f∧g : B → C
|
|
|
243
|
|
|
244 なことを考えると、
|
|
|
245
|
|
|
246 lemma : {A B C : Set } → (( A → B ) ∧ ( B → C )) → ( A → C )
|
|
|
247 lemma f∧g a = π2 f∧g ?
|
|
|
248
|
|
|
249 ここで、π2 f∧g ? は (π2 f∧g) ? であることを思い出そう。最終的に、
|
|
|
250
|
|
|
251 lemma : {A B C : Set } → (( A → B ) ∧ ( B → C )) → ( A → C )
|
|
|
252 lemma f∧g a = π2 f∧g (π1 f∧g) a
|
|
|
253
|
|
|
254 (ここで、(π2 f∧g (π1 f∧g)) a と書かなくても良いのは何故か?)
|
|
|
255
|
|
|
256 前の証明図と、Agdaで証明とどこがどう対応しているのかを考えてみよう。
|
|
|
257
|
|
|
258 ---問題2.2 Agdaのrecord
|
|
|
259
|
|
|
260 以下の agda の ? の部分を埋めよ。対応する証明図をコメントで書くこと。
|
|
|
261
|
|
|
262 <a href="agda/record1.agda"> record </a> <!--- Exercise 2.2 --->
|
|
|
263
|
|
|
264
|
|
|
265 --data または 排他的論理和(Sum)
|
|
|
266
|
|
|
267 ここで扱っている論理(直観主義論理)では∧に対称的な形で∨を定義することはしない。導入は対称的になるが除去はおかしくなってしまう。
|
|
|
268 そこで次のように定義することになっている。
|
|
|
269
|
|
|
270 除去 導入
|
|
|
271 A B
|
|
|
272 : :
|
|
|
273 A ∨ B C C A B
|
|
|
274 ------------------------ ----------- p1 ---------- p2
|
|
|
275 C A ∨ B A ∨ B
|
|
|
276
|
|
|
277
|
|
|
278 data _∨_ (A B : Set) : Set where
|
|
|
279 p1 : A → A ∨ B
|
|
|
280 p2 : B → A ∨ B
|
|
|
281
|
|
|
282 dataはCで言えばcase文とunion に相当する。Scala のCase Classもこれである。Cと違いunionにはどの型が入っているかを区別するtagが付いている。
|
|
|
283
|
|
|
284 p1 と p2 は A ∨ B を構成する constructor (推論ではintroduction)であり、case 文が eliminator に相当する。
|
|
|
285
|
|
|
286 Haskellと同様にp1/p2はパターンマッチで場合分けする。
|
|
|
287
|
|
|
288 ex3 : {A B : Set} → ( A ∨ A ) → A
|
|
|
289 ex3 = ?
|
|
|
290
|
|
|
291 場合分けには、? の部分にcursolを合わせて C-C C-C すると場合分けを生成してくれる。
|
|
|
292
|
|
|
293 ex3 : {A B : Set} → ( A ∨ A ) → A
|
|
|
294 ex3 (p1 x) = ?
|
|
|
295 ex3 (p2 x) = ?
|
|
|
296
|
|
|
297
|
|
|
298 ---問題2.3 Agdaのdata
|
|
|
299
|
|
|
300
|
|
|
301 <a href="agda/data1.agda"> data </a> <!--- Exercise 2.3 --->
|
|
|
302
|
|
|
303 --有限な集合と Nat
|
|
|
304
|
|
|
305 data は有限な要素を持つ集合を構成できる。
|
|
|
306
|
|
|
307 data Three : Set where
|
|
|
308 t1 : Three
|
|
|
309 t2 : Three
|
|
|
310 t3 : Three
|
|
|
311
|
|
|
312 open Three
|
|
|
313
|
|
|
314 data 3Ring : (dom cod : Three) → Set where
|
|
|
315 r1 : 3Ring t1 t2
|
|
|
316 r2 : 3Ring t2 t3
|
|
|
317 r3 : 3Ring t3 t1
|
|
|
318
|
|
|
319 これは、三つのVertexとEdgeを持つグラフをdataで表してみたものである。
|
|
|
320
|
|
|
321 任意の個数を表すためには自然数(Natural Number)を作る必要がある。ペアノの公理が有名だが、dataを使って以下のように構成する。
|
|
|
322
|
|
|
323 data Nat : Set where
|
|
|
324 zero : Nat
|
|
|
325 suc : Nat → Nat
|
|
|
326
|
|
|
327 add : ( a b : Nat ) → Nat
|
|
|
328 add zero x = x
|
|
|
329 add (suc x) y = suc ( add x y )
|
|
|
330
|
|
|
331 mul : ( a b : Nat ) → Nat
|
|
|
332 mul zero x = ?
|
|
|
333 mul (suc x) y = ?
|
|
|
334
|
|
|
335 --問題1.4 Nat
|
|
|
336
|
|
|
337 ? を埋めて掛け算を完成させよう。
|
|
|
338
|
|
|
339 --Equality
|
|
|
340
|
|
|
341 自然数を導入したので方程式を記述したい。そのためには等式を導入する必要がある。導入は
|
|
|
342
|
|
|
343 ---------------
|
|
|
344 x == x
|
|
|
345
|
|
|
346 だが、ここには隠れた仮定がある。x は何かの集合の要素なはず。
|
|
|
347
|
|
|
348 { x : A }
|
|
|
349 ---------------
|
|
|
350 x == x
|
|
|
351
|
|
|
352 さらに左辺と右辺は等しいが、
|
|
|
353
|
|
|
354 add zero zero == zero
|
|
|
355
|
|
|
356 では左辺と右辺は項として同じではない。計算して同じということにして欲しい。つまり、
|
|
|
357
|
|
|
358 Agdaの項には計算していくと決まった形に落ちる
|
|
|
359
|
|
|
360 という性質があって欲しい。この計算はλ項に対して定義する必要がある。この計算をreduction(縮約)、
|
|
|
361 決まった形をnormal form(正規形)と言う。
|
|
|
362
|
|
|
363 <a href="reduction.html">Reduction</a>
|
|
|
364
|
|
|
365 Agda での定義は以下のようになる。
|
|
|
366
|
|
|
367 data _==_ {A : Set } : A → A → Set where
|
|
|
368 refl : {x : A} → x == x
|
|
|
369
|
|
|
370 refl は reflection (反映) の略である。refl は 等式のconstructorになる。
|
|
|
371
|
|
|
372 Elmination は変数の置き換えになる。
|
|
|
373
|
|
|
374 x == y f x y
|
|
|
375 ------------------------
|
|
|
376 f x x
|
|
|
377
|
|
|
378 x == y は入力の型であり、refl とうパターンでしか受けられない。この時に、x と y が等しい必要がある。
|
|
|
379
|
|
|
380 しかし、x と y は項なので変数を含むことがある。Agda に等しいことを確信させる必要がある。
|
|
|
381 この問題はパターンマッチの時にもすででていた。これは項(正規化された)を再帰的に比較していく
|
|
|
382 手順が必要になる。これは単一化(Unification)と呼ばれる。
|
|
|
383
|
|
|
384 <a href="unification.html">Unification</a>
|
|
|
385
|
|
|
386 ex1 : {A : Set} {x : A } → x == x
|
|
|
387 ex1 = ?
|
|
|
388
|
|
|
389 ex2 : {A : Set} {x y : A } → x == y → y == x
|
|
|
390 ex2 = ?
|
|
|
391
|
|
|
392 ex3 : {A : Set} {x y z : A } → x == y → y == z → x == z
|
|
|
393 ex3 = ?
|
|
|
394
|
|
|
395 ex4 : {A B : Set} {x y : A } { f : A → B } → x == y → f x == f y
|
|
|
396 ex4 = ?
|
|
|
397
|
|
|
398 以上の証明を refl を使って完成させてみよう。
|
|
|
399
|
|
|
400 <a href="agda/equality.agda"> equality </a> <!--- Exercise 2.4 --->
|
|
|
401
|
|
|
402 --集合のLevel
|
|
|
403
|
|
|
404 論理式は型であり、それは基本的はSetになっている。例えば、A → B は Set である。
|
|
|
405
|
|
|
406 ex1 : { A B : Set} → Set
|
|
|
407 ex1 {A} {B} = A → B
|
|
|
408
|
|
|
409 Agda は高階論理なので、論理式自体を返す論理式も作ることができる。
|
|
|
410
|
|
|
411 ex2 : { A B : Set} → ( A → B ) → Set
|
|
|
412 ex2 {A} {B} A→B = ex1 {A} {B}
|
|
|
413
|
|
|
414
|
|
|
415 では、これを論理式を要素として持つ直積を作ってみよう。
|
|
|
416
|
|
|
417 record FuncBad (A B : Set) : Set where
|
|
|
418 field
|
|
|
419 func : A → B → Set
|
|
|
420
|
|
|
421 Agda は以下のように文句をいう。
|
|
|
422
|
|
|
423 The type of the constructor does not fit in the sort of the
|
|
|
424 datatype, since Set₁ is not less or equal than Set
|
|
|
425 when checking the definition of FuncBad
|
|
|
426
|
|
|
427 自己参照的な集合の定義を避けるために集合には階(level)という概念が導入されている。
|
|
|
428
|
|
|
429 open import Level
|
|
|
430 record Func {n : Level} (A B : Set n ) : Set (suc n) where
|
|
|
431 field
|
|
|
432 func : A → B → Set n
|
|
|
433
|
|
|
434 のように集合の階(Level)を明示する必要がある。
|
|
|
435
|
|
|
436 --問題1.5 集合のLevel
|
|
|
437
|
|
|
438 level が合うように ? を埋めよ。
|
|
|
439
|
|
|
440 <a href="agda/level1.agda"> level </a> <!--- Exercise 2.5 --->
|
|
|
441
|
|
|
442 --問題2.6 List
|
|
|
443
|
|
|
444 List は cons か nil かどちらかの構造で、cons は List を再帰的に含んでいる。
|
|
|
445
|
|
|
446 postulate A : Set
|
|
|
447
|
|
|
448 postulate a : A
|
|
|
449 postulate b : A
|
|
|
450 postulate c : A
|
|
|
451
|
|
|
452
|
|
|
453 infixr 40 _::_
|
|
|
454 data List (A : Set ) : Set where
|
|
|
455 [] : List A
|
|
|
456 _::_ : A → List A → List A
|
|
|
457
|
|
|
458
|
|
|
459 infixl 30 _++_
|
|
|
460 _++_ : {A : Set } → List A → List A → List A
|
|
|
461 [] ++ ys = ys
|
|
|
462 (x :: xs) ++ ys = x :: (xs ++ ys)
|
|
|
463
|
|
|
464 l1 = a :: []
|
|
|
465 l2 = a :: b :: a :: c :: []
|
|
|
466
|
|
|
467 l3 = l1 ++ l2
|
|
|
468
|
|
|
469 等式の変形を利用して、List の結合法則を証明してみよう。
|
|
|
470
|
|
|
471 open import Relation.Binary.PropositionalEquality
|
|
|
472
|
|
|
473 ++-assoc : (L : Set ) ( xs ys zs : List L ) → (xs ++ ys) ++ zs ≡ xs ++ (ys ++ zs)
|
|
|
474 ++-assoc A [] ys zs = let open ≡-Reasoning in
|
|
|
475 begin -- to prove ([] ++ ys) ++ zs ≡ [] ++ (ys ++ zs)
|
|
|
476 ( [] ++ ys ) ++ zs
|
|
|
477 ≡⟨ refl ⟩
|
|
|
478 ys ++ zs
|
|
|
479 ≡⟨⟩
|
|
|
480 [] ++ ( ys ++ zs )
|
|
|
481 ∎
|
|
|
482 ++-assoc A (x :: xs) ys zs = let open ≡-Reasoning in ?
|
|
|
483
|
|
|
484 ≡⟨⟩ などの定義はどこにあるのか?
|
|
|
485
|
|
|
486 --問題2.6 List
|
|
|
487
|
|
|
488 lemma を等式の変形を利用して証明してみよ。
|
|
|
489
|
|
|
490 <a href="agda/list.agda"> List </a> <!--- Exercise 2.6 --->
|
|
|
491
|
|
|
492 --DAGと否定
|
|
|
493
|
|
|
494 グラフには接続されてない二点が存在する。それを表現するために否定¬と矛盾⊥を導入する。
|
|
|
495
|
|
|
496 ⊥
|
|
|
497 ------------- ⊥-elim
|
|
|
498 A
|
|
|
499
|
|
|
500 矛盾からは何でも導くことができる。この場合、A はSetである。⊥ を導入する推論規則はない。
|
|
|
501
|
|
|
502 これは、contructor のない data で表すことができる。
|
|
|
503
|
|
|
504 data ⊥ : Set where
|
|
|
505
|
|
|
506 ⊥-elim は以下のように証明できる。
|
|
|
507
|
|
|
508 ⊥-elim : {A : Set } -> ⊥ -> A
|
|
|
509 ⊥-elim ()
|
|
|
510
|
|
|
511 () は「何にもmatchしないパターン」である。これは型を指定した時に「可能な入力がない」必要がある。つまり、このケースは起こり得ない
|
|
|
512 ことを Agda が納得する必要がある。納得できないと error message がでる。
|
|
|
513
|
|
|
514 λ ()
|
|
|
515
|
|
|
516 という構文も存在する。
|
|
|
517
|
|
|
518 ⊥ を使って否定は以下のように定義される。
|
|
|
519
|
|
|
520 ¬_ : Set → Set
|
|
|
521 ¬ A = A → ⊥
|
|
|
522
|
|
|
523 否定には入力があることを意識しておこう。
|
|
|
524
|
|
|
525 f0
|
|
|
526 -----→
|
|
|
527 t0 t1
|
|
|
528 -----→
|
|
|
529 f1
|
|
|
530
|
|
|
531 というグラフは以下のように記述する。
|
|
|
532
|
|
|
533 data TwoObject : Set where
|
|
|
534 t0 : TwoObject
|
|
|
535 t1 : TwoObject
|
|
|
536
|
|
|
537
|
|
|
538 data TwoArrow : TwoObject → TwoObject → Set where
|
|
|
539 f0 : TwoArrow t0 t1
|
|
|
540 f1 : TwoArrow t0 t1
|
|
|
541
|
|
|
542 ループのあるグラフを作ってみよう。
|
|
|
543
|
|
|
544 r0
|
|
|
545 -----→
|
|
|
546 t0 t1
|
|
|
547 ←-----
|
|
|
548 r1
|
|
|
549
|
|
|
550 data Circle : TwoObject → TwoObject → Set where
|
|
|
551 r0 : Circle t0 t1
|
|
|
552 r1 : Circle t1 t0
|
|
|
553
|
|
|
554 矢印をたどって繋がっている点は接続(connected)されていると言う。
|
|
|
555
|
|
|
556 data connected { V : Set } ( E : V -> V -> Set ) ( x y : V ) : Set where
|
|
|
557 direct : E x y -> connected E x y
|
|
|
558 indirect : { z : V } -> E x z -> connected {V} E z y -> connected E x y
|
|
|
559
|
|
|
560 直接繋がっているか、間接的に繋がっているかどちからになる。この構造は自然数に似ている。
|
|
|
561
|
|
|
562 t0 と t1 が TwoArrow の場合に繋がっていることを証明してみる。
|
|
|
563
|
|
|
564 lemma1 : connected TwoArrow t0 t1
|
|
|
565 lemma1 = ?
|
|
|
566
|
|
|
567 t1 から t0 にはいけない。
|
|
|
568
|
|
|
569 lemma2 : ¬ ( connected TwoArrow t1 t0 )
|
|
|
570 lemma2 = ?
|
|
|
571
|
|
|
572 dag (Directed Acyclic Graph) は、すべての点(Vertex)で自分自身につながる経路(Edge)がないグラフ
|
|
|
573
|
|
|
574 dag : { V : Set } ( E : V -> V -> Set ) -> Set
|
|
|
575 dag {V} E = ∀ (n : V) → ¬ ( connected E n n )
|
|
|
576
|
|
|
577 --問題2.7 DAGと否定
|
|
|
578
|
|
|
579 TwoArrow が dag で、Circle が dag ではないことを証明してみよう。
|
|
|
580
|
|
|
581 lemma4 : dag TwoArrow
|
|
|
582 lemma4 = ?
|
|
|
583
|
|
|
584 lemma5 : ¬ ( dag Circle )
|
|
|
585 lemma5 = ?
|
|
|
586
|
|
|
587 <a href="agda/dag.agda"> DAG </a> <!--- Exercise 2.7 --->
|
|
|
588
|
