日々の流転

λ. 不動点演算子はチャーチ数での無限大?

@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 とは違い、そのままではうまくいかないので、結局NatとCoNatが一致するような世界で考える必要がある。領域理論的な世界ではそれが言える。

Haskellで自然数型とチャーチ数の型、それらの間の対応、そして無限大を以下のように定義する。 Haskellに対応する圏では本物の直和がないので、上の話とはちょっと違っちゃうんだけど、まあそれはそれ。

{-# LANGUAGE Rank2Types #-}

data Nat = Succ Nat | Zero
type ChurchNumeral = forall a. (a->a)->(a->a)

build :: ChurchNumeral -> Nat
build c = c Succ Zero

unbuild :: Nat -> ChurchNumeral
unbuild n s z = foldNat s z n

foldNat :: (a -> a) -> a -> Nat -> a
foldNat s z Zero = z
foldNat s z (Succ n) = s (foldNat s z n)

infinity :: Nat
infinity = Succ infinity

なお、infinity は Succ の唯一の不動点である(CoNatのfinalityから言える)。

ここで、不動点結合子を使って無限大っぽいチャーチ数を定義してみる。

infinity' :: ChurchNumeral
infinity' s z = fix s

すると、build infinity' = infinity' Succ Zero = fix Succ で、infinityはSuccの唯一の不動点なので、build infinity' = infinity となる。

逆に infinity をチャーチ数に変換してみると、unbuild infinity s z = foldNat s z infinity = foldNat s z (Succ infinity) = s (foldNat s z infinity) となるので、unbuild infinity s z は s の不動点。また、最小不動点である事も領域理論的な推論で容易に示す事ができる。

というわけで、まあ、不動点演算子はチャーチ数での無限大と言って良さそうだ。

この辺りをもっとちゃんと考えると、P.S. Mulry. Strong monads, algebras and fixed points のような話になるのだと思うけど、この論文、読もう読もうと思いつつずっと読んでなかった……