日々の流転

λ. 秋学期修士最終試験

中高の入試と被っていたので朝バスは凄い状態になっているのではないかと思ったが、8:40〜9:00ごろには空いていた。受験生はもっと早い時間だったのかな。

発表ではPowerpointの発表者ツールが使えずに焦ったが、発表時間の調整は発表練習の時よりもうまく行っていた。不思議だ。そして、質疑応答もそれなりにうまくこなせた。人事は尽くしたし、あとは天命を待つだけ。

発表スライド:

発表を終え、会場を後にする修士たちの姿(まだ未発表の人もM2じゃない人もいるけど)。赤松さんによる写真。

λ. Haskellと高階論理の土台は異なるか?

宮本の日記（仮）のGHCは気色悪いという話に関して。コメントとして書こうと思ったのだけど、色々と書き足しそうなので、こっちに書く。

∀x. (a → b → x) → x が a ∧ b と同型になることは通常パラメトリシティを用いて示されるが、Haskellのような言語ではパラメトリシティは完全には成り立たない。また、高階論理であってもパラメトリックでないモデルを考えれば両者は同型にはならないのではないかと思う。

次に ∀a,b. a → b という型を持つ閉項が存在するという話について。全ての型に対して不動点演算子 fix が存在する言語では、全ての型が閉項 fix(λx. x) を持ち、論理体系としては矛盾した体系になる。それゆえ、不動点演算子はパラドキシカル演算子と呼ばれることもある。 Haskellのように再帰的定義が自由に行える言語では fix f = f (fix f) によって不動点演算子を定義でき、論理体系として解釈すると矛盾した体系になっている。通常の論理では無矛盾であることが基本なのに対して、通常のプログラミング言語は論理体系としては矛盾していることが前提なため、ある意味「土台」が異なっていると言えると思う。

その点に関して、A note on inconsistencies caused by fixpoints in a cartesian closed category (20061110#p01参照) では「The results indicate the different nature of domain theory and set=topos theory or, in other words, that programming requires other foundations than even a constructive set theory.」と述べられていたりする。

また、この話については「自己言及の論理と計算」 (20030629#p03参照) は非常に面白く書けていると思う。

この辺りの話は結構面白く、幾らでも書けそうな気がするけど、とりあえずこの辺りで。

(2/5 追記) seqとパラメトリシティ

seqとパラメトリシティの話は知ってはいました(20050315#p03)が、面倒だったので触れていませんでした(それにseqが存在しなくともパラメトリックでないモデルを作ることは出来るはずだし)。そしたら早速指摘が。

• sumiiさんのseqとパラメトリシティ
• KeisukeNakanoさんのパラメトリシティとseq

今回の話の個人的な収穫は以下の点。Pittsのアプローチには詳しくないため、TT-closedness は admissibility と同じようなものだと思っていたが、KeisukeNakanoさんによれば「TT-closed は admissibility より強すぎる」とのこと。うーむ……