nfunatoのブックマーク - はてなブックマーク

迷路の試験問題を解いてみた - にわとり小屋でのプログラミング
参考：人材獲得作戦・４試験問題ほか: 人生を書き換える者すらいた。 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の長さ
nfunato 2017/03/19
coq
リンク
にわとり小屋でのプログラミング日記
この記事はTppMark11の問題をCoqでやってみたという内容である。問題はこちら: docs.google.com 命題論理式と同値であることの定義命題論理式の定義 Inductive Term := | Var(v : Var.T) | Neg(t : Term) | And(t1: Term)(t2: Term) | Or(t1: Term)(t2: Term) | Impl(t1: Term)(t2: Term) | TRUE | FALSE . 同値であることの定義変数環境を表すctxを Var.T -> bool の関数で表現し、命題論理式のevalを次で定義した。 Fixpoint eval ctx t : bool := match t with | Var v => ctx v | Neg t => negb (eval ctx t) | And t1 t2 =>
nfunato 2017/03/19
coq
リンク
OCamlとCoqを連携してIO処理をモナディックに扱う - にわとり小屋でのプログラミング
この記事は OCaml Advent Calendar の5日目の記事です。 OCamlと連携して、CoqでもIO処理ができるようにするためのライブラリを作った。 http://github.com/yoshihiro503/coqio このライブラリを使えば、例えば次のようなコードを書くことができる。 Require Import Monad IO. Open Scope string_scope. Definition main : IO unit := do _ <- print "Hello" ; println ", world!". Haskell風のdo式みたいな記法が便利だね。print関数には文字列だけでなく、Showクラスのインスタンスとなる型を持つ式ならばなんでも与えることができる*1。このコードを次のコマンドでExtractすればcoq.mlというOCamlのソー
nfunato 2012/12/06
ocaml

monad
リンク
1