エントリーの編集
エントリーの編集は全ユーザーに共通の機能です。
必ずガイドラインを一読の上ご利用ください。
記事へのコメント2件
- 注目コメント
- 新着コメント
注目コメント算出アルゴリズムの一部にLINEヤフー株式会社の「建設的コメント順位付けモデルAPI」を使用しています
- バナー広告なし
- ミュート機能あり
- ダークモード搭載
関連記事
Coqでラムダ計算を証明してみた - みずぴー日記
前からずっと取り組んでいた「Coqで単純型付きラムダ計算を証明してみよう」が一段落しました。 動機 le... 前からずっと取り組んでいた「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. 証明した定理 型
2009/12/01 リンク