Hatena::Groupcoq

mzpの日記

 | 

2009-11-25

Coqのおかげで見つけれたバグ

最近、Coqで型付きラムダ計算を定義して、ProgressやPreservationを証明するという遊びにはまっています。とてもおもしろいので、みんなもやるといいと思うよ。

で、最近、substitution lemmaの証明にチャレンジして、もろくも敗れ去りました。よくよく見直してみると、そもそもsubstitutionの定義が間違っていました。このバグはなかなか根が深くて、前に作ったトイ・コンパイラ(scalet)でも同じ間違いをしてました。

というわけで、これはCoqのおかげで見つけれたバグだし、人手は見付けづらいバグと言えないこともないので記録しておきます。

バグを含んだSubstitution

まずはバグを含んだSubstitutionです。どこが間違っているか分かりますか? ボクは分かりませんでした。

(* subst *)
Inductive Subst : term -> term -> string -> term -> Prop :=
  | SVar1    : forall (s x : string) (t : term),
      x = s  -> Subst (Var x) t s t
  | SVar2    : forall (s x : string) (t : term),
      x <> s -> Subst (Var x) (Var x) s t
  | SBool    : forall (s : string) (b : bool) (t : term),
      Subst (Bool b) (Bool b) s t
  | SLambda1 : forall (x s : string) (body1 body2 t : term) (ty : type),
      x <> s -> Subst body1 body2 s t ->
      	Subst (Lambda x ty body1) (Lambda x ty body2) s t
  | SLambda2 : forall (x s : string) (body t : term) (ty : type),
      x = s  -> Subst (Lambda x ty body) (Lambda x ty body) s t
  | SApply   : forall (t1 t2 s1 s2 t : term) (x : string),
      Subst t1 s1 x t -> Subst t2 s2 x t -> Subst (Apply t1 t2) (Apply s1 s2) x t
  | SIf      : forall (t1 t2 t3 s1 s2 s3 t : term) (x : string),
      Subst t1 s1 x t -> Subst t2 s2 x t -> Subst t3 s3 x t ->
      	Subst (If t1 t2 t3) (If s1 s2 s3) x t.

正しい定義

そして、こちらがTAPL(asin:0262162091)に載っている正しい定義です。

f:id:mzp:20091104203722p:image

間違っていたところ

で、どこが間違っていたかと言うとFV(s)に関する条件が抜けていました。これのせいで、substitutionが不正になって、結果としてSubstitution lemmaの証明ができませんでした。これが無いと、weaking Lemmaを適用できないんだよね。

f:id:mzp:20091104203904p:image

そのときのTwitterのログ

みずぴー
@mzp
えー、substitution lemma無理だって。これ成り立たねーよ(2009-11-03 19:00:54) link
みずぴー
@mzp
どう考えてもsubstitution lemmaの証明、無理だって。きっと"変数が重複しない"という約束のおかげで、暗黙の前提があるに違いない(2009-11-03 20:54:36) link
みずぴー
@mzp
一晩一晩考えたけsubstitution lemmaが成立しない、ってのはウソな気がしてきた(←当然)。でも、証明ができないってのは依然とそのまま(2009-11-4 08:00:48) link
みずぴー
@mzp
そろそろでかける時間だけど、もうちょっとTAPLの証明を追いかけたいし、iPhoneの同期も終ってないので、まだ家にいる(2009-11-4 08:02:22) link
みずぴー
@mzp
あーーーー、証明できない理由がわかった。substitutionの定義が間違ってるんだ!!(2009-11-4 08:10:17) link
みずぴー
@mzp
TAPLだと「λx.t」のxは常にユニークである、という約束のおかげで、substitutionの定義が簡単になってるのか(2009-11-4 08:11:07) link
みずぴー
@mzp
ん?そんなこともないか。単にボクの実装ミスだ > substitutionの定義(2009-11-4 08:15:16) link
みずぴー
@mzp
今のボクの状態: substitution lemmaの証明ができない-> よく見たらsubstitutionの定義が間違っていた -> ちゃんとsubstitutionを定義するのが難しい! http://github.com/mzp/lambda(2009-11-04 09:51:20) link

ちなみに

書いているCoqのコードはGitHubにあります。

http://github.com/mzp/lambda

ゲスト



トラックバック - http://coq.g.hatena.ne.jp/mzp/20091125
 |