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

Coq


前からずっと取り組んでいた「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 (The MIT Press)

Types and Programming Languages (The MIT Press)

元ネタ。

Interactive Theorem Proving and Program Development: Coq’Art: The Calculus of Inductive Constructions (Texts in Theoretical Computer Science. An EATCS Series)

Interactive Theorem Proving and Program Development: Coq’Art: The Calculus of Inductive Constructions (Texts in Theoretical Computer Science. An EATCS Series)

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

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

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

TAPLで納得できないところは、こっちで確認してました。特に、変数束縛が発生する場合のsubstitutionの定義でお世話になりました。
日本語なのにTAPLより難しく感じました。
絶版していて手にいれれなかったので、図書館で借りてコピーしました。

感想

  • straightforwardはやめてください。難しいよ、その証明(><)
  • 一発で正しい定義はなかなかできない。(Coqのおかげで見つけれたバグ - みずぴー日記)
  • さらっと「変数は重複して登場しないものとする」って書かないで! 難しいよ、その証明(><)