OCamlでlet recを使わずにfact関数を定義する - にわとり小屋でのプログラミング
今日はProofCafeでCPDTの三章を読み進めたが、そこでCoqではInductive型のコンストラクタの引数が関数のとき、その関数の左側に自分自身が現れてはいけないということを学んだ。もしそれを可能にしてしまうと無限ループが定義でき、公理系が矛盾してしまうからだ。次のシンプルな例を見てみよう。 Inductive t (A: Set) : Set := | T : (t A -> A) -> t A. 一見なんの問題も無さそうな この型定義は失敗し、次のようなコンパイルエラーが出力される。 Error: Non strictly positive occurrence of "t" in "(t A -> A) -> t A".もしこの型が定義できたとすると次のような関数が定義できてしまう。 Definition ワォ (T f) := f (T f). ここで (ワォ (T ワォ)
迷路の試験問題を解いてみた - にわとり小屋でのプログラミング
参考：人材獲得作戦・４ 試験問題ほか: 人生を書き換える者すらいた。 Lv4に評価されるためには、最短性の完全なチェックが必要だったのでCoqで証明してみた。 まず、accessiblesという関数を定義し、以下の性質を証明した。 ここでplengthはパスの長さを計る関数で、Path x pはpがxを起点としたパスであるという述語。endofはパスの終点を求める関数。 Fixpoint accessibles (start : node) (len : nat) : list path := match len with | O => (PUnit start) :: nil | S n' => div_equiv path_equiv_dec @@ (flat_map expand @@ accessibles start n') end. この関数はstartから始まってlenの長さ
1
リリース、障害情報などのサービスのお知らせ
最新の人気エントリーの配信
j次のブックマーク
k前のブックマーク
lあとで読む
eコメント一覧を開く
oページを開く
