λ. 不動点演算子はチャーチ数での無限大? @mametterさん が「Church numerals で無限大を考えるとしたら、Y コンビネータと同じになるのだろうか」と書いていたので、考えてみた。 普通の自然数の型は Nat = μX. X+1 で、集合の世界で考えるとこれには無限大は含まれない一方、その双対の CoNat = νX. X+1 は集合の世界で考えると自然数の集合に無限大∞を付加してやったような集合になるので、これを使って考えてやれば良いのではないかというのを最初に考えた。 ただ、チャーチ数の型 ∀X. (X⇒X)⇒X⇒X はNatのチャーチエンコーディング ∀X. (X+1⇒X)⇒X を変形したものであって、CoNatのチャーチエンコーディング ∃Y. Y×(Y⇒Y+1) = ∀X. (∀Y.Y×(Y⇒Y+1)⇒X)⇒X とは違い、そのままではうまくいかないので、結局N