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