# 目的

そのまま読むかな

# 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で管理するために必要
どの哲学者がどのフォークを取るのか決まっているため