本当は読書メータの感想のところに書こうと思ったのだが字数が溢れてしまったのでここに書いておく。
あんまり真面目に読んでないんだ、ごめんね。
気にはなっていたのだか積読で、一念発起して興味あるところだけ読むことにした。そういうわけで全体の話はしてません。
公理的意味論は(他の意味論のスタイルと明確な区別があるわけではないが)プログラムの構文に、その文が意味する数学的対象を直接割り付けるもの。プログラムが停止しないなどのエラーをうまく扱えるその数学的対象としては部分関数が便利で、その順序をうまく扱うためにcpo(complete partial order)という順序集合のクラスを用いる。そうするとこの上で不動点の議論ができ、それが再帰やwhile文といった自明には意味が定義できないものにも意味を割り付けることができる。この議論の後に、λにいくらかの基本型と再帰を許す関数定義μを追加したPCF(Programming language for Computable Function)を定義し、それに対して意味論を与える。
型なしラムダ計算に公理的意味論を与えるのに素朴に集合論で言うところの関数を割り当てようとすると、自由な関数適用のせいで矛盾が起こってしまう。これに対処するには、X→Xの関数がXに埋め込めるようなcpo Xを見つけなければいけない。このような要求を方程式風に書くとX=[X→X]というようになるが、このようなcpoの対象についての方程式を領域方程式という。この方程式の解が見つかれば、そこから型なしラムダ計算の意味論(モデル？)を作ることができるが、実際この解として2点以上の集合Dから埋め込みを繰り返して無限直積を取り作ったcpoであるD∞が解であることを確かめる。なお、この領域方程式を解く方法を研究したり、この状況をcpoだけではなくω-完全な圏でのcolimitを考えて本質を捉えようとするというような議論もこの本ではなされているが、とりあえず具体に興味があったのでそこは読まなかった。
疑問として、そんな風にして意味論を作ってそれで「型なしラムダ計算の理解が深まった」と言えるのか、普通にラムダ式を適当な同値関係で割ったものそのものを眺めるのと比べて何かいいのかという疑問は残ったが、真面目に読んでないからかもしれない。
(8/27追記)公理的意味論がつけば、(λx.xx)(λx.xx)に⊥が対応することがわかるよと教えてもらいました。そういう意味では公理的意味論は数学で言うところの不変量みたいな感じで使えるんですね。
