Just $ A sandbox

プログラミングと計算機科学とかわいさ

無限ループによる証明

Software FoundationsのIMPあたりをやってて疑問が湧いた.

w = while True do Skip endが停止しないことを示したい.
つまり, $\langle w, s \rangle \to s' \Rightarrow False$ を示したい. ($s, s' : \mathbb{Z} \to \mathbb{Z}$ は変数の値を保持する環境)

普通に証明するなら以下のようになると思う:
証明図の高さに関する帰納法による. まず高さが0のとき, 明らかに<w,s>→s'は公理から導くことはできないので高さ0の証明図を持たない. よって$\langle w, s \rangle \to s' \Rightarrow False$である.
次に, $\forall s, s'. \langle w, s \rangle \to s'$が高さnの証明図をもたないと仮定し, $\langle w, s \rangle \to s'$が高さ(n+1)の証明図をもたないことを証明する. $\langle w, s \rangle \to s'$が高さ(n+1)の証明図をもつことを仮定すると, wの定義とwhile-loopに関する推論規則より$\langle w, s \rangle \to s'$が高さnの証明図で示せる. これは帰納法の仮定に矛盾するので証明が完了する.

Agdaなどの依存型を持つ言語では, prop :: w -> Falseに対応する函数を作ってやればよい.
<w,s>→s'にあたるデータ型を再帰的に定義している場合, 例えばこの証明は無限ループを使ってprop (While-Loop True _ k) = kみたいにすると, 証明図の仮定に当たる, 「一つ前の」<w,s>→s'を使うことができる.
けれど一体これは何を証明していることになるんだろう?
明らかに上の証明とは違う気がするし, そもそも無限ループになっているのに証明が完了しているというのがよく分からない. 直観的には「<w,s>→s'を仮定すると全く同じ形が仮定の部分に出現する」ということが重要なんだろうという気がするけれど、そこからどうやって矛盾を導いているんだろう.

ちなみにIsabelleでは以下のようにやった.
上の証明の気持ちがある程度反映されているつもり. (と言っても証明だけでは伝わらない気もするけど)

lemma while_induction:
  assumes red: "(WHILE b DO c END) %: st ⇓ st'"
  and base: "⋀t t'. ⟦ beval3 t b = False; t' = t ⟧ ⟹ P t t'"
  and step: "⋀t t' t''. ⟦ beval3 t b = True; c %: t ⇓ t'; (WHILE b DO c END) %: t' ⇓ t''; P t' t'' ⟧ ⟹ P t t''"
  shows "P st st'"
proof-
  have "(WHILE b DO c END) %: st ⇓ st' ⟹ P st st'"
    using ceval.induct [of _ _ _ "λc0 t t'. WHILE b DO c END = c0 ⟶ P t t'"] apply rule
    apply (simp, auto, simp add: base)
    apply (fastforce simp add: step)
    apply (fastforce simp add: step)
    done
  thus ?thesis by (simp add: red)
qed
 
theorem loop_never_stops: "¬ (loop %: st ⇓ st')"
proof (unfold loop_def, auto)
  assume p: "WHILE BTrue DO SKIP END %: st ⇓ st'"
  show "False"
    using while_induction [of BTrue SKIP st st' "λ_. λ_. False"]
    by (rule, simp add: p, auto)
qed