Function

Coqによる証明駆動開発で Merge Sort プログラムをつくってみた

OCaml合宿で帰りの車の中でid:zyxwv さんにMergeSortの正しさをどうやって証明するか聞かれてとっさに証明できなかったので、合宿から帰ったあとに一生懸命証明してみた。プログラムと証明の全体はこちら: yoshihiro503 / mergesort / source / — Bitbucket…

Coqで同値関係

最近仕事でlistの要素を仲間分けしてリストのリストを返す 次のような関数をOCamlで定義した。 let rec classify rel l = match l with | [] -> [] | x::xs -> let (ys,zs) = List.partition (fun y -> rel x y) xs in (x, ys) :: classify rel zs この関数…