日々の流転

λ. ホーア論理

S氏の発表に関するメモ。やっぱ loop invariant って難しい。ところで、ホーア論理では再帰とかが扱えないってホント?

【2009-10-26 追記】 立石さんのコメント通りなのだけど、『算法表現論』(木村　泉，米澤　明憲)に再帰呼び出しに関する規則があったので、ちょっと長いが引用しておく。

ここでは細かい議論には立ち入らないが，再帰的な起動を許す手続きに関しては，帰納法(induction)に類する推論が必要で，たとえば次のような規則*

D7(再帰呼び出しの規則)

    
procedure S(var x~ ; v~); Q(S),  P {T(x~ ; v~)} R ⊢ P {Q(T)} R
────────────────────────────────
P {S(x~ ; v~)} R

が使われる．ただし A⊢B は，一般にAが証明されたと仮定するとBが証明されることを意味する．よって，前提の右側は，P {T(x~; v~)} R という命題が証明されたと仮定して(帰納法の仮説)，手続きSの本体Qの中でSを起動する部分をTで置き換えたもの，すなわちQ(T)の実行に関してP{Q(T)}Rが証明されることを意味する．このような前提が成立するならば，Sをそのまま起動しても実行の直前，直後でPとRが成立する．ただし，再帰的な手続きの実行が終了することは，別に証明しなければならない．

---

* この他に，公理 P {S(x~; v~)} P (ただしx~の中の変数はPの変数として現れない)なども必要となる．

通常の帰納法や余帰納法のような条件がなく、こんな風に証明しようとしている規則をそのまま使っていいのかな?、と疑問になる。 しかし、そのような条件が必要になるのは、停止しないような場合を避けるためで、一方ここで考えているホーア論理の部分正当性ではそもそも停止しない場合のことは考えなくて良いので問題ない。

また、この規則は領域理論の不動点帰納法:

P(⊥)  ∀x. P(x)→P(f(x))  P chain-complete
──────────────────────
P(fix f)

からも得られる。

State を変数から値への関数の空間、Prog を State から平坦ドメイン State_⊥ への関数の空間として、Prog 上の述語 P(C) = {Q1}C{Q2} = ∀s:State. Q1(s)∧(C(s)≠⊥) → Q2(C(s)) を考えると、部分正当性の定義から P(⊥) は常に成り立ち、P が chain-complete であることも容易に示せるので、

∀C:Prog. {Q1}C{Q2} → {Q1}F(C){Q2}
──────────────────
{Q1}fix F{Q2}

が得られる。 これは引数を持たない(再帰呼び出しがある)サブルーチンの、部分正当性の規則とほぼ同じ。

λ. 夕食

ファカルティで「カルビ丼定食」。向井先生のおごり。ごちそうさまでした。