tmiyaさんがCoq入門者向けの問題をブログで紹介していたので解いてみた。 Functional Programming Memo: [Coq] Coq-99 : Part 1 この問題はCoqを使う人だけでなく論理的な思考力を鍛える良い問題ばかりなので、ぜひとも挑戦してみるとよいと思う。このような…

普通のフィボナッチ関数とCPS変換したフィボナッチ関数をそれぞれ定義して、それらが等価であるということを証明してみた。CPS変換についてちょっと理解できた気がする。http://ideone.com/3CQOnしかしfib_cps関数をもっと美しく定義できないものだろうか。[…

発表者の皆さん。お手伝いいただいた皆さん。ありがとうございました。たくさんのCoqerが集まって、大変濃密な時間を過ごす事ができました。スライドは以下から参照できます。 Coq庵 - coqグループ

今日はProofCafeでCPDTの三章を読み進めたが、そこでCoqではInductive型のコンストラクタの引数が関数のとき、その関数の左側に自分自身が現れてはいけないということを学んだ。もしそれを可能にしてしまうと無限ループが定義でき、公理系が矛盾してしまうか…

TDD Boot Camp名古屋に参加しました。id:t-wadaさんの講演はすばらしく、TDDをずっと推し進めている経験に基づく具体的な知見は大変わかりやすく勉強になりました。 当日のスライドはid:t-wadaさんのブログで見ることができます。TDD Boot Camp 名古屋に登壇…

7/12に名古屋市工業技術研究所で行われた id:kencobaさんによる Alloyセミナーに、講師補佐としてお手伝いさせてもらいました。当日の資料はこちらから辿れます。Alloy Analyzer入門セミナー - kencobaの日記TDDBC名古屋で2日間テスト駆動開発を行った直後で…

http://d.hatena.ne.jp/kikx/20100629#1277831079 の素晴らしい足し算の存在証明を見つけたので、その存在が一意(ユニーク)であることを証明した。元々のネタはこちら http://d.hatena.ne.jp/m-hiyama/20100629/1277774676まずは集合AとA上の掛け算とサクセ…

変数全体の集合varを{}というように自然数の対応で与えられると考え、式expを以下のように定義する。 Inductive exp : Set := | Var : var -> exp | Const : nat -> exp | Binop : binop -> exp -> exp -> exp. ここで binop型の値は二項演算子(binary opera…

第3回FormalMethods勉強会 : ATND (via fm-forum @ ウィキ - トップページ) 場所は喫茶ルノアールというところの中にある会議室でした。 前半Alloyの話をid:kencobaさんが、後半はCoqの話をtmiyaさんがするという形式でした。13時から19時まで6時間でしたが…

このBaseモジュールをインストールすれば、写真の用なコードを書くことが出来る。ダウンロード: http://sourceforge.jp/projects/coqbase/具体的には以下のことを定義した。 標準出力へ出力するprint, println関数 命令をつなげるセミコロン演算子 依存型を…

参考：人材獲得作戦・４ 試験問題ほか: 人生を書き換える者すらいた。 Lv4に評価されるためには、最短性の完全なチェックが必要だったのでCoqで証明してみた。まず、accessiblesという関数を定義し、以下の性質を証明した。 ここでplengthはパスの長さを計る…