以前に、CFMLというものがあるというのを教えてもらった(のは一ヶ月半前)ので、触ってみた。Characteristic Formula generator for MLの略らしい。サイトの下の方に論文リストもあるし、色々なアルゴリズムを証明した例もある http://www.chargueraud.org/so…

http://d.hatena.ne.jp/m-a-o/20110325#p1 の(2)の終わりで、functional extensionalityを仮定しない限り、Coqのtupleは圏論的な意味での直積になってることは言えないと書いた。それでも、モノイダル積にはなってるだろうと思ってたのだけど、実際にCoqで証…

[文献とか] Thierry Coquandのスライド http://www.cse.chalmers.se/~coquand/equality.pdf Mike Shulmanのスライド http://www.math.ucsd.edu/~mshulman/hottseminar2012/01intro.pdf あたりを読めば大筋は分かる気がする現時点で、まとまったレビューや教…

色々とよく分からない話とかまとまらない話。ここで使用しているCoqのバージョンは8.3 (1)TypeとSetとProp この3つ、どう使いわけんの?という話。このうち、Propは他二者との違いは直感的には分かりやすい。問題は、Typeを使うべきか、Setを使うべきか、基準…

Coqのバージョンは8.3 どうでもいい話その1。集合の代わりにSetoidを使うという点について。色々見てると、数学をCoqで形式化する際には、Setoidを使うのが割と普通であるらしい。その正当性は、何によって保証されるのか?とか思うものの、そもそもZFC集合論…

CLTT読書会で最近話題になるネタ。 ConCaT http://coq.inria.fr/pylons/contribs/view/ConCaT/v8.3 というライブラリがあるんで、これをベースにCLTTの証明なんかを書いていけば、色々よいんじゃないか的な。 ドキュメントらしいものはないけど、論文を読む…

Constructive Category Theory圏論を知ってれば、Coqの記号がキモイ以外は読みやすい論文だった。一般の型に属する値は等しいかどうかの判定が可能とは限らないので、ある型とその型の上の同値関係のペアとしてSetoidというのを導入する。同値な要素は、等し…

http://citeseer.ist.psu.edu/321720.html Buchbergerのアルゴリズム(Euclidのアルゴリズムが整数環のイデアルのよい生成元=最大公約数を求めるものであるのに対して、体係数の多項式環のイデアルのよい生成元=グレブナー基底を求めるアルゴリズム)をCoqで生…

いい加減、ベースになってる理論も知っとくべきだとか思ったので、Wikipediaを見た。 http://en.wikipedia.org/wiki/Calculus_of_constructions Calculus of Constructions(CoC)は、型をファーストクラスとして扱える高階型付きラムダ計算です、とのこと。私…

Coq。証明中、Undo機能が欲しいなーと思ってたら、ちゃんとあった。前回の補足のような。Variableで大域変数を宣言したけど、 Coq < forall A B C:Prop , (A->B->C)->(A->B)->(A->C).みたく、forallでローカルに束縛しちゃっていいらしい。Propが型というの…

暫くCoqを弄ってみようかと。Coqは、Calculus of (Co)Inductive Constructionsという謎の体系を背景にしているらしい。実装はOcaml(多分)。CoqをSchemeで書けるようになるくらいまで頑張ろう今日のまとめ ・IDEは全く使い方が分からないので、コマンドライン…