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. 証明した定理 型
HOASによるラムダ式 - みずぴー日記
30分プログラム、その691。HOASによるラムダ式。 id:keigoiさんに、HOAS(Higher order abstract syntax)なるものを教えてもらいました。 詳しいことは、http://homepages.inf.ed.ac.uk/ratkey/unembedding.pdfに書いてあるらしいです。 今のところの理解は、 Haskellのラムダ式で、ターゲット言語のラムダ式を表現する アルファ変換とか変数補足とかを考えなくてすむ といった感じです。 さっぱり分からないので、上記の論文にのっている例を実装してみました。 使い方 *Main> eval (lambda (\x->x) `apply` (int 42)) 42 ソースコード {-# OPTIONS_GHC -fglasgow-exts #-} import Text.Printf class Lambda
Coqのおかげで見つけれたバグ - みずぴー日記
最近、Coqで型付きラムダ計算を定義して、ProgressやPreservationを証明するという遊びにはまっています。とてもおもしろいので、みんなもやるといいと思うよ。 で、最近、substitution lemmaの証明にチャレンジして、もろくも敗れ去りました。よくよく見直してみると、そもそもsubstitutionの定義が間違っていました。このバグはなかなか根が深くて、前に作ったトイ・コンパイラ(scalet)でも同じ間違いをしてました。 というわけで、これはCoqのおかげで見つけれたバグだし、人手は見付けづらいバグと言えないこともないので記録しておきます。 バグを含んだSubstitution まずはバグを含んだSubstitutionです。どこが間違っているか分かりますか? ボクは分かりませんでした。 (* subst *) Inductive Subst : term ->
1
リリース、障害情報などのサービスのお知らせ
最新の人気エントリーの配信
j次のブックマーク
k前のブックマーク
lあとで読む
eコメント一覧を開く
oページを開く
