|
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 どの哲学者がどのフォークを取るのか決まっているため
|
|
25
|
97
|
|
|
98 # 直すところ
|
|
|
99
|
|
|
100 AとかBはここでは型だけど、
|
|
|
101 命題だと思っても良い
|
|
|
102 並列実行はメタかな。可能な実
|
|
|
103 Shinji Kono から全員に 03:40 PM
|
|
|
104 引数の説明が雑だな
|
|
|
105 TerminatingLoopS 自体の証明も
|
|
|
106 コストが高い低いは正確性に欠
|
|
|
107 並列実行の検証は難しいけど
|
|
|
108 モデル検査自体が並列実行の定
|
|
|
109 モデル検査はωオートマトンの実
|
|
|
110 仕様は時相論理とかωオートマト
|
|
|
111 それを満たすかどうかを証明に
|
|
|
112 このdataは、G
|
|
|
113 Code GearのProgram Counterみ
|
|
|
114 Process (ここではContext)毎にあ
|
|
|
115 pickup-lfork は目が潰れるが…
|
|
|
116 -c と -p があるのか
|
|
|
117 ++ は List の append
|
|
|
118 zero 以外のコードは? 以下同様的な?!
|
|
|
119 「乱数がでる」?
|
|
|
120 分岐の数って、いくつ? 0,1,2 だけ?
|
|
|
121 deadlock とかは時相論理の変数だな
|
|
|
122 時相論理式を定義して持ち歩くべきだな
|
|
|
123 普通は深さ優先探索と状態データベースだが…
|
|
|
124 状態が変化し続ける場合はどうなるの?
|
|
|
125 exclude-same-env は何を弾くの?
|
|
|
126 モデル検査自体の停止性は示せるの?
|
|
|
127 DPPでは何が有限なの?
|
|
|
128 State List はRedBlack木が良いとは言えない
|
|
|
129
|
|
|
130 Agdaでインタプリタではなくコンパイル
|
