Hoare Logic

割と昔からの技術でさ、2018年にもやったんだけど、なんかいまいちで。

木下先生がAgdaで書いたのも動かしたんですが、割と煩雑な割に停止性とか怪しくて...

Agda は loop の停止性が自明でないと文句言うのだが、それをループの回数でなんとかするという方式らしい。

なのだが、夢で「型じゃなくて、値つまり、証明その物を渡せばいいんじゃないか?」ってのが降ってきて。

ところが実際に書いてみると「あれ、ちゃんと値が回ってきてるじゃん」

　　proof1 : whileTest 10 (λ env → whileLoop env (λ e → (vari e) ≡ 10 ))
　　proof1 = refl

今までは、こんな風にしてたんだな。それだと、自分で値を作らないとだめ。だから refl なわけ。

　　whileTestSpec1 : (c10 : ℕ) →　(e1 : Env ) → vari e1 ≡ c10 → ⊤
　　whileTestSpec1 _ _ x = tt

そうじゃなくて、こういう風に入力で仕様を受けてやればよい。実際、PostCondtion は証明が渡されてるからこれでよい。

ということなので、2018年の時点で十分だったということで終わり。え、何もしないの。

なんだが、停止性も「自然数の減少列に写像する」という当たり前の方法が使える。当然のように、Agdaで高階論理で記述できる。

TerminatingLoopS : {l : Level} {t : Set l} (Index : Set ) → (Invraiant : Index → Set )
　 → (ExitCond : Index → Set) → ( reduce : Index → ℕ)
　 → (loop : (r : Index)　→ Invraiant r → (next : (r1 : Index)　→ Invraiant r1 → reduce r1 < reduce r　→ t ) → (exit : (re : Index) → ExitCond re → t) → t)
　 → (r : Index) → (p : Invraiant r)　→ (exit : (re : Index) → ExitCond re → t)　→ t

まぁ、なんのこっちゃかんもあるが。

Hoare Logic だと、プログラムをコマンドに分解したりとかの手間もあるのだが、こっちの方がプログラムに埋め込める分、簡単ならしい。

続きは、プロシンかな。　

http://www.cr.ie.u-ryukyu.ac.jp/hg/Members/ryokka/HoareLogic/file/tip/whileTestGears.agda