型付きラムダ計算のモデルをデカルト閉圏で作れるのだけど、ちょっとした注意と工夫が必要です。Cがデカルト閉圏だとして、ラムダ項Mに対して、Mの表示（denotation）をC内に直接作るもんだと思っている人がいるかも知れませんが、それはあんまりウマくない…

圏のなかで指数（exponential, exponentiation）演算が登場することがあります。例えば、Cがデカルト閉圏*1だとして、カリー化／反カリー化による同型は次のように書けます。 C(A×B, C) C(A, CB) ここで出てきたCBが指数です。Cが集合圏のときは、CBは関数集…

僕が豊饒圏の話をするとき、定義を最後まで書き切らないで「他にいくつかの法則を満たす必要があります」みたいな言い方でお茶を濁しています。その理由は、定義を書くだけでもとてもめんどくさいからです。ちゃんと（若干の省略がありますけどね）記述して…

うーむ、話はそんなに単純じゃないみたい。「Coq小ネタ：関数の外延的等値性とか」において、f, g:A→B に対して、f ≡ g ⇔ ∀x.(f(x) = g(x)) として、関数の外延的等値性「≡」を定義したのですが、これではすぐにボロが出ますね。f ≡ g を定義するために f(x)…

A, Bが集合で、f, g:A→B のとき、Coqの組み込みのイコールによる f = g はあんまり具合がよくないようです。普通「関数が等しい」とは、「Aのすべての点において関数値が等しい」ことです。Coqのイコールはそうなってないのです。そこで、ユーザー定義のイコ…

Coqと一緒にOCamlもあったほうがいいのかな、と。インストールするだけで終わるかもしんないけど。 http://protz.github.io/ocaml-installer/ から ocaml-4.01.0-i686-mingw64-installer3.exe をダウンロード。これは普通のインストーラーです。 デフォルト…

Coqをいじっていると、カリー／ハワード対応の威力を実感します。一方で、証明といえども所詮は計算なんだな、とも思います。中学校くらいでやる代入計算の直接的な延長線上に証明の合成操作があるんですよね。中学レベルの計算と形式的証明では、用語や記号…