Yコンビネータ - 雑多な感じ

Yコンビネータ

型無しラムダ計算においてよく知られた（そしておそらく最もシンプルな）不動点コンビネータはYコンビネータと呼ばれる。これはハスケル・カリーによって発見されたもので、次のように定義される。

$ Y = (λf . (λx . f (x x)) (λx . f (x x)))

SKIコンビネータ計算では次のようになる。

$ Y = S (K (S I I)) (S (S (K S) K) (K (S I I)))

上のWikipediaでは適用を省略していることに注意

Haskellっぽいかもね

Haskellで型をつけるには一手間必要

自分自身を適用できる、自己言及できる型

Inf a = ((..-> a) -> a) -> a

code:haskell

newtype Inf a = Inf (Inf a -> a)

-- NOINLINEを付けないとインライン展開が無限に続き、コンパイルに失敗する

{-# NOINLINE runInf #-}

runInf :: Inf a -> Inf a -> a

runInf (Inf f) = f

BML分解

Lコンビネータ$ L x y = x (y y) = x (M y)

code:haskell

l :: (a -> b) -> Inf a -> b

l x y = x (m y)

code:haskell

m :: Inf a -> a

m x = runInf x x

code:haskell

b :: (Inf a -> a) -> ((a -> a) -> Inf a -> a) -> (a -> a) -> a

b m l = m . Inf . l

$ \forall x. Lx(Lx) = x(Lx(Lx)) より$ Lx(Lx) は不動点となる

この不動点によってYコンビネータを定義する

$ Y x = Lx(Lx) = M(Lx) = BMLx

code:haskell

y :: (a -> a) -> a

y = b m l