迷路の試験問題を解いてみた - にわとり小屋でのプログラミング
参考：人材獲得作戦・４ 試験問題ほか: 人生を書き換える者すらいた。 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の長さ
Coqで、クイックソート - にわとり小屋でのプログラミング
（＊ 注意：今回はCoq 8.1以上を使用。 ＊） 今回は、らくがきえんじんで、昔 言及されていた、クイックソートに挑戦してみる。 Coqで、再帰する関数を書く場合は、Definitionコマンドではなく、Fixpointコマンドを使う。 しかし、Fixpointによる関数定義では、明らかに停止する構造を持つ必要がある。 Coqでは、必ず停止する関数のみが定義できる、という制限のため、このように再帰する関数を定義するのは難しいが、Coqで作った関数は、必ず停止して結果を返す、という性質を保っている。 しかし、Fixpointによる定義では、簡単に定義できない再帰関数もある。 例えば、次のように、クイックソートの関数を素直にかいてみると、以下のようなエラーになる。 (* クイックソートの定義 失敗例 *) Fixpoint qsort (l : list A) : list A := mat
1
リリース、障害情報などのサービスのお知らせ
最新の人気エントリーの配信
処理を実行中です
j次のブックマーク
k前のブックマーク
lあとで読む
eコメント一覧を開く
oページを開く
