# 目的

そのまま読むかな

# agdaの基本
たぶんここの説明全部実際のコードでやったほうがいいらしい

# record
論文にもかいてあるし三段論法を
取り扱ったほうが見る人も面白いのでは

# CbC
goto文のやつは消すかな

# normal levelとmetalevel
ポインタの操作は含まれない

上の方は normal level の実装

下の方が meta level の計算を可視化したもの

例えば、変数がメモリのある番地に存在していれば、
Meta Data Gear がその番地を持っている。
(なので Data Gear に wrap されているというイメージ)

Meta Code Gear がそのメモリから取り出して、

普通の Code Gear が実行をするという流れ、

後ろのほうでまた新しく保存したいデータがあれば
Meta Code Gear が保存して、

最後の Meta Data Gear が新しいデータのメモリ番地を
持っているという流れになります。

プログラムをする際は上のようにシンプルな実装をするが、
実際には内部でメタ計算が走っているのが理想ですね

Gears Agda 

# Gears Agda

この矢印tが Gears Agda のミソで、

この定義を見ると、While loop はEnvとCode を受け取ってtを返します。

この While loop を code Gear に
見立てるなら、次に遷移する関数を指定する必要があります

それがCodeになります。
なので、Gears Agda では次に受け取る関数を受け取る用にしていて、それがnextになります。

このようにして、CbC の継続という概念を
矢印tで表現しています。

(CbCのCodeGear はDataGearをうけとってそれを元に実行することはnextがEnvを受け取って実行すること)

(CodeGear の実行終了時に、次の CodeGearに
DataGearを与えることもnextにEnvを与えていることからわかると思います)


<!-- 実行の文を持ってくるんだっけな -->

- with 文
with文で展開してパターンマッチすることもできる。
ここでは less than がそれにあたる
0とvarnを比較して
false だった場合、trueだった場合をcase文のように
書ける

- `{-# TERMINATING #-}`
Agdaが停止性を理解できない場合に、このようにアノテーションすることで停止することを示せます

# loopの接続

reduceがあるため、Agdaは

で、前回のものは最初から構造体（record）に値が格納されている状態から始まっていたので
proofGearsTermS では、入力が自然数で、recordの定義から検証を行っている

そしてそれを行っているのが最初の関数であるwhileTest'で
ここでvarnが入力c10と一致し、variが0であることを証明している

次の関数であるversionでは、whileTest'のrecord定義時のConditionから

loop時のconditionを生成しています

- これで Gears Agda にて While Loop を Hoare Logic を使って検証することができた。

# テストと定理証明の違い

# 定理証明とモデル検査の違い

# DPPの実装
pidは哲学者をindexで管理するために必要
どの哲学者がどのフォークを取るのか決まっているため

# 直すところ

AとかBはここでは型だけど、
命題だと思っても良い
並列実行はメタかな。可能な実
Shinji Kono から全員に 03:40 PM
引数の説明が雑だな
TerminatingLoopS 自体の証明も
コストが高い低いは正確性に欠
並列実行の検証は難しいけど
モデル検査自体が並列実行の定
モデル検査はωオートマトンの実
仕様は時相論理とかωオートマト
それを満たすかどうかを証明に
このdataは、G
Code GearのProgram Counterみ
Process (ここではContext)毎にあ
pickup-lfork は目が潰れるが…
-c と -p があるのか
++ は　List の append
zero 以外のコードは? 以下同様的な?!
「乱数がでる」?
分岐の数って、いくつ? 0,1,2 だけ?
deadlock とかは時相論理の変数だな
時相論理式を定義して持ち歩くべきだな
普通は深さ優先探索と状態データベースだが…
状態が変化し続ける場合はどうなるの?
exclude-same-env は何を弾くの?
モデル検査自体の停止性は示せるの?
DPPでは何が有限なの?
State List はRedBlack木が良いとは言えない

Agdaでインタプリタではなくコンパイル