Coqでハノイの塔に関する証明

Coqが今流行っているらしい。twitter経由で偶然ハノイの塔をCoq形式化している記事を見つけた。 なんか巷でCoqがはやっているようなので - 菊やんの雑記帳なんかおもしろそうなので一つ簡単な命題を証明してみた。証明したこと Lemma answer_length : forall…

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

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

OCaml合宿に行ってきた

ocaml-nagoyaのプログラミング合宿に参加してきました。一泊二日で長野の麻績(おみ)に行って、鍋も食べ、焼肉も食べ、酒も飲み、コーディングもして、発表もするというハードなスケジュールでしたが、久しぶりにocaml-nagoyaのメンバーにも会えて非常に充実…

Coqで型クラス(Haskell風 モナドの定義)

Coq version 8.2以降からHaskell風の型クラスが使えるようになったから使ってみることにした。Haskellで型クラスといえばMonadが有名な気がするのでHaskell風のモナドHMonadを定義しよう。Coqでの型クラスは次のように宣言するみたいだ。 Class HMonad (M: T…

OCaml Meeting と FLTV に行ってきました。

OCaml Meeting に行ってきました。 id:camlspotterさんid:osiireさんid:keigoiさんharreさんid:mzpさんid:Gemmaさんそしてid:zyxwvさんおつかれさまでした。OCaml入門者向けから、上級者向けまでさまざまな講演があって非常に楽しめました。OCamlという言語…

オープンソースカンファレンス 名古屋 2009 に行ってきた

オープンソースカンファレンス2009 Nagoya - オープンソースの祭りだぎゃーに行ってきました。 スタッフの皆様おつかれさまでした。ocaml-nagoyaのメンバーは残念ながら今回少なかったですが、セミナーはかなりのお客さんが来てくれました。ブースにも何人か…

オープンソースカンファレンス 名古屋 2009 に行ってきた

Coqで数学的帰納法

プログラムでリストや文字列を扱うことがあるが、これらに関する性質をチェックしたいと思ったらどうしたらよいだろうか?例えばリストを逆順にするrevという関数を定義したときに、rev (rev l) = lという性質が、いかなるリストlでも必ず成り立つということ…

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 この関数…

しりとりの圏をCoqで実装してみた

Coq で しりとりの圏を形式化した記事を見つけた。 型によるしりとりの成立判定 - コンピュータってすごいらしい via 完全実装付きでもう一度お送りします、しりとりの圏 - 檜山正幸のキマイラ飼育記すばらしかったので、私もちょっと真似して実装してみた。…

SICPのEx 2.4 をCoqで解いてみた

SICPを読んでいたら 検証せよ という問題があったので、Coqで検証してみた。問題はペア構造のチャーチエンコーディングの話。Scheme (untyped λ) に比べて Coq (λC) は型が厳格なので、問題の定式化がちょっと大変だったけど、問題自体は簡単に証明できた。 …

Coq 8.2 リリース!

Coqがversion 8.1から8.2にバージョンアップしました。変更点は以下のいろいろ。 Haskellのような type class system が導入されました coqcでコンパイル後のvoファイル を扱うcoqchkというツールが追加されました Setoidのための書き換えタクティック setoi…

今日は娘の誕生日

でした。

Coqで高精度計算サイト 高精度計算サイトというのを見つけた。ここの電卓サービスは素晴らしく、大変感銘したのだが、一つ残念な点があった。 それは大きな数を扱うことができないということである。 例えば10^10000000のような大変大きな計算を実行すると答…

CoqでOCamlのモジュールを使う

CoqではExtractionという機能があるためにOCamlやHaskellなどの関数型言語との連携が容易である。 CoqでOCamlの型や関数を使いたい場合は単に関数の引数として渡せば良いだけだからである。 ただ、沢山の型や関数を一度に渡したい場合、結構面倒である。Coq…

関数型言語haXe

最近、ocaml-nagoya勉強会でhaXeコンパイラのソースコードを読んでいるので、haXeのプログラムを書きたくなってきた。 ということで、ここにいろいろ書いてみます。いろいろ指摘いただけると助かります。http://ocaml-nagoya.g.hatena.ne.jp/yoshihiro503/

定理証明器Isabelleで計算可能性の証明

偶然見つけました。 http://www2.score.cs.tsukuba.ac.jp/4eba3005-1/student/takuya-fujiwara-1/cs30bb30df30ca30fc767a88688cc76599-1/CSseminor2008_Fujiwara_Slides.pdf将来、定理証明器で言語の開発をするようになるのかもしれない。チューリング完全性…

CoqでPrim言語のサブセットのパーサを実装した。

CSNagoyaのコンパイラを作ろう部門での教科書「コンパイラ入門 C#で学ぶ理論と実践(冨沢 高明)」が自宅に届いたので、8章までの部分を復習するために実装してみた。 この本ではC#という言語で実装することを念頭に置かれていたが、Coqが好きなのでCoqで実装…

Lambda Cを実装してみた。

404 Not FoundやはてなダイアリーでλCが話題になっていたので、Lambda C インタプリタを実装してみた。多相型も依存型もサポート。定理証明もできる。Lambda C Interpreterサンプルコード: λ(A:*). λx:A. x (恒等関数) λ(A:*). λ(x:A). λ(y:A). Π(P:Π(a:A)…

Leightweight Language Future (LLFuture) と、等価変換セミナーに行ってきた。

LL Future LL Futureでは、id:sumiiさんがラムダ式や、ユークリッドのアルゴリズムなどの歴史を語っていたのがおもしろかった。数学でのおもしろい概念は何百年後も利用されるのか。 じゃあ今、数学(や計算機科学)でホットな話題が100年後利用されるのかな?…

LLFutureというイベントに行ってきます。

Gallinaについて軽く話します。

Coqで依存型

最近Agdaがはやっているみたいなので、Coqでも依存型(dependent type)を使ってみた。 実装したのは長さ n のベクトル型だ。このベクトル型を使うと、空でないとか、長さが等しいとかを型の段階で保証できるので、より安全なプログラムを書くことができるの…

CoqのソースコードをカッコイイHTMLページにする方法(coqdocを使う)

Coqでプログラムや証明を書いたら、そのソースコードを人に見せたりしたくなるときがある。 そのときに便利なcoqdocという機能がある。coqdocはcoqtopやcoqcなどと一緒のところにある。 使いかたは以下。 $ coqdoc [Coqファイル.v] ここで、(** コメント *)…

CoqでProject Euler (problem 44)

Problem44が解けた? - みずぴー日記に触発されて、Project EulerのProblem 44に挑戦してみた。 問題44: 五角数は Pk = k(3k-1)/2で生成される. 五角数のペア PmとPnについて, 差と和が五角数になるものを考える. 差を D = |Pm - Pn| と書く. 差 D の最小値を…

CSNagoyaでHaskell勉強会

名古屋でHaskellの勉強会をやるという噂を聞いたので、行ってきた。CSNagoyaという勉強会で、教科書は「ふつうのHaskellプログラミング」。みんなで音読していくという方式で、ノートPCを持ってきていない人と持ってきている人でペアプロミングしながら、理…

PPL2008に行ってきた。

Coqでπ計算などで有名なReynald Affeldtさんから、貴重な意見がいただけたり、楽しい話がたくさんあったりで、非常に素晴らしい経験だった。 驚いたこと プログラミング in OCamlでも有名な五十嵐先生のところの研究室では、CALと呼ばれる、小さい証明器を使…

Coqで、クイックソート

(* 注意:今回はCoq 8.1以上を使用。 *)今回は、らくがきえんじんで、昔 言及されていた、クイックソートに挑戦してみる。Coqで、再帰する関数を書く場合は、Definitionコマンドではなく、Fixpointコマンドを使う。 しかし、Fixpointによる関数定義では…

Coqで”無限オブ無限”(証明部分)

ヒビルテで、さかいさんが興味深いCoqのコードを紹介していた。 ⇒ λ. Coqで“無限オブ無限” どうやら元ネタはここ(derive your dreams)らしい。おもしろそうなので、さかいさんのコードを証明してみた。証明した定理は以下。 Theorem main : forall m n:nat, …

セマンティクス

(*****************************************) (** SEMANTICS *) (*****************************************) Require Import List. Section ListAssoc. Variable A B:Set. Variable A_beq : A -> A -> bool. Fixpoint List_assoc (l:list (A*B))(a:A){str…

シンタクス

(*****************************************) (** SYNTAX *) (*****************************************) (** 基本データ構造を二分木構造で定める *) Inductive DATA:Type := | DNIL : DATA | DCONS : DATA -> DATA -> DATA. Inductive VAR : Type := | …