Hatena::Groupcoq

mzpの日記

 | 

2009-11-26

Coqでラムダ計算を証明してみた

f:id:mzp:20091122200215j:image

前からずっと取り組んでいた「Coqで単純型付きラムダ計算を証明してみよう」が一段落しました。

動機

  • let多相の実装はしたから、次は証明だろ
  • 最近、流行っているCoqを覚えたい

扱えるラムダ式

型は、Bool型と関数型のみ。

Inductive type : Set :=
  | BoolT : type
  | FunT  : type -> type -> type.

式は、変数参照、真偽値、ラムダ(関数抽象)、関数適用、if式。

Inductive term : Set :=
    Var     : string -> term
  | Bool    : bool   -> term
  | Lambda  : string -> type -> term -> term
  | Apply   : term  -> term -> term
  | If      : term -> term -> term -> term.

証明した定理

型が付くなら、それは値か評価できるかのどちらか。

Theorem Progress : forall t r,
  Typed t empty_env r -> Value t \/ (exists t', Eval t t').

評価しても型は代わらない。

Theorem preservation: forall t t' tenv T,
  Typed t tenv T -> Eval t t' -> Typed t' tenv T.

あと、これを証明するのに必要な補題を何個か証明しています。

ソースコード

詳しい証明のついたソースコードはgithubにあります。

http://github.com/mzp/lambda/tree/simple-typed

参考文献

Types and Programming Languages (MIT Press)

Types and Programming Languages (MIT Press)

元ネタ。

Coqの本。Coqの中の話がメインらしいですが、ボクはタクティクスの利用例集としてぐらいしか、使えていません。

プログラミング言語の基礎理論 (情報数学講座)

プログラミング言語の基礎理論 (情報数学講座)

TAPLで納得できないところは、こっちで確認してました。特に、変数束縛が発生する場合のsubstitutionの定義でお世話になりました。

日本語なのにTAPLより難しく感じました。

絶版していて手にいれれなかったので、図書館で借りてコピーしました。

感想

  • straightforwardはやめてください。難しいよ、その証明(><)
  • 一発で正しい定義はなかなかできない。(id:mzp:20091124)
  • さらっと「変数は重複して登場しないものとする」って書かないで! 難しいよ、その証明(><)
 |