不動点

型付ラムダ計算

それと型がつけられるかということがどうも正則性公理と関わっている気がして、この公理ってないほうが楽しくないかな。

と書いたら
くるるさんから正則性公理
にお返事をもらった。

むしろ言及したいのは「この公理ってないほうが」の部分でありまして。正則性公理がある意味adhocな公理であることは間違いないです。そして、そのことを攻撃するのは論理的には全く正しいし、ない方が楽しいかもねと言われればおき得ることの範囲が広がるんだから確かにそうかもしれないとしか言いようがありません。
ですが、正則性公理が現代集合論ではとても強力に使われていることだけは主張しておいたほうが良いかと思います。

それは確かに分かるのですが、「ZF のモデルが標準モデルと同型になる条件が無限降下列の非存在」とか、いかにも正則性公理が adhoc であることを示しているように見えませんかね。あ、正則性公理なかったら、こんな定理ありませんね。
でも、正則性公理を否定する自然に見える公理があってもよいと思えるのです。

あ、あと、「気がして」とかぼかしているけれども、多少は関係があります。λ式は計算が停止しないことがあるけれども、
(たとえば、)
型がつけられるようなラムダ式は集合論の関数にきちんと対応させることが出来て、かつ、必ず計算可能になります。rank が存在すれば、たしかに適応していくたびに、たまねぎの皮がだんだんむけていって最後にはなくなるような感じで、あ、そんな単純じゃないか。
けれども、上のラムダも、たまねぎの皮をむいても同じ大きさのたまねぎがでてくるような集合を考えれば、型(??)がつけられますね。
haskell には という型があるので、この意味での型付け可能では、計算可能は不成立です。
たとえば、有名なところでは不動点を求める Y コンビネータは

y f = f (y f)

と書けて、y id は停止しません。実際、
y の型は、id の型は ですね。