にわとり小屋でのプログラミング ブログ

名古屋のCoqエンジニアです。日記は勘で書いてるところがあるので細かいとこが違うことがあります。

CPDT

OCamlでlet recを使わずにfact関数を定義する

今日はProofCafeでCPDTの三章を読み進めたが、そこでCoqではInductive型のコンストラクタの引数が関数のとき、その関数の左側に自分自身が現れてはいけないということを学んだ。もしそれを可能にしてしまうと無限ループが定義でき、公理系が矛盾してしまうか…

Coqで多変数多項式の簡約

変数全体の集合varを{}というように自然数の対応で与えられると考え、式expを以下のように定義する。 Inductive exp : Set := | Var : var -> exp | Const : nat -> exp | Binop : binop -> exp -> exp -> exp. ここで binop型の値は二項演算子(binary opera…