|
22
|
1 # 目的
|
|
|
2
|
|
23
|
3 そのまま読むかな
|
|
22
|
4
|
|
23
|
5 # agdaの基本
|
|
|
6 たぶんここの説明全部実際のコードでやったほうがいいらしい
|
|
|
7
|
|
|
8 # record
|
|
|
9 論文にもかいてあるし三段論法を
|
|
|
10 取り扱ったほうが見る人も面白いのでは
|
|
|
11
|
|
|
12 # CbC
|
|
|
13 goto文のやつは消すかな
|
|
|
14
|
|
|
15 # normal levelとmetalevel
|
|
|
16 ポインタの操作は含まれない
|
|
|
17
|
|
|
18 上の方は normal level の実装
|
|
|
19
|
|
|
20 下の方が meta level の計算を可視化したもの
|
|
|
21
|
|
|
22 例えば、変数がメモリのある番地に存在していれば、
|
|
|
23 Meta Data Gear がその番地を持っている。
|
|
|
24 (なので Data Gear に wrap されているというイメージ)
|
|
|
25
|
|
|
26 Meta Code Gear がそのメモリから取り出して、
|
|
|
27
|
|
|
28 普通の Code Gear が実行をするという流れ、
|
|
|
29
|
|
|
30 後ろのほうでまた新しく保存したいデータがあれば
|
|
|
31 Meta Code Gear が保存して、
|
|
|
32
|
|
|
33 最後の Meta Data Gear が新しいデータのメモリ番地を
|
|
|
34 持っているという流れになります。
|
|
|
35
|
|
|
36 プログラムをする際は上のようにシンプルな実装をするが、
|
|
|
37 実際には内部でメタ計算が走っているのが理想ですね
|
|
|
38
|
|
|
39 Gears Agda
|
|
|
40
|
|
|
41 # Gears Agda
|
|
|
42
|
|
|
43 この矢印tが Gears Agda のミソで、
|
|
|
44
|
|
|
45 この定義を見ると、While loop はEnvとCode を受け取ってtを返します。
|
|
|
46
|
|
|
47 この While loop を code Gear に
|
|
|
48 見立てるなら、次に遷移する関数を指定する必要があります
|
|
|
49
|
|
|
50 それがCodeになります。
|
|
|
51 なので、Gears Agda では次に受け取る関数を受け取る用にしていて、それがnextになります。
|
|
|
52
|
|
|
53 このようにして、CbC の継続という概念を
|
|
|
54 矢印tで表現しています。
|
|
|
55
|
|
|
56 (CbCのCodeGear はDataGearをうけとってそれを元に実行することはnextがEnvを受け取って実行すること)
|
|
|
57
|
|
|
58 (CodeGear の実行終了時に、次の CodeGearに
|
|
|
59 DataGearを与えることもnextにEnvを与えていることからわかると思います)
|
|
|
60
|
|
|
61
|
|
|
62 <!-- 実行の文を持ってくるんだっけな -->
|
|
|
63
|
|
|
64 - with 文
|
|
|
65 with文で展開してパターンマッチすることもできる。
|
|
|
66 ここでは less than がそれにあたる
|
|
|
67 0とvarnを比較して
|
|
|
68 false だった場合、trueだった場合をcase文のように
|
|
|
69 書ける
|
|
|
70
|
|
|
71 - `{-# TERMINATING #-}`
|
|
|
72 Agdaが停止性を理解できない場合に、このようにアノテーションすることで停止することを示せます
|
|
|
73
|
|
|
74 # loopの接続
|
|
|
75
|
|
|
76 reduceがあるため、Agdaは
|
|
|
77
|
|
|
78 で、前回のものは最初から構造体（record）に値が格納されている状態から始まっていたので
|
|
|
79 proofGearsTermS では、入力が自然数で、recordの定義から検証を行っている
|
|
|
80
|
|
|
81 そしてそれを行っているのが最初の関数であるwhileTest'で
|
|
|
82 ここでvarnが入力c10と一致し、variが0であることを証明している
|
|
|
83
|
|
|
84 次の関数であるversionでは、whileTest'のrecord定義時のConditionから
|
|
|
85
|
|
|
86 loop時のconditionを生成しています
|
|
|
87
|
|
|
88 - これで Gears Agda にて While Loop を Hoare Logic を使って検証することができた。
|
|
|
89
|
|
|
90 # テストと定理証明の違い
|
|
|
91
|
|
|
92 # 定理証明とモデル検査の違い
|
|
|
93
|
|
|
94 # DPPの実装
|
|
|
95 pidは哲学者をindexで管理するために必要
|
|
|
96 どの哲学者がどのフォークを取るのか決まっているため
|
