Mercurial > hg > Papers > 2023 > soto-master

comparison slide/memo.md @ 23:016e82a71407

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Add slide
author soto <soto@cr.ie.u-ryukyu.ac.jp>
date Tue, 07 Feb 2023 02:27:53 +0900
parents b37e4cd69468
children 83e28d9da152
comparison
equal deleted inserted replaced
22:b37e4cd69468 23:016e82a71407
1 #
2
3 # 目的 1 # 目的
4 2
3 そのまま読むかな
5 4
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 どの哲学者がどのフォークを取るのか決まっているため