数理論理学（数学基礎論）　その14

5 ：１３２人目の素数さん：2019/03/24(日) 07:17:00.84 ID:N4FNRVCO.net

Yコンビネータ

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

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

実際に関数gを適用することによって、この関数が不動点コンビネータとして動作する
のが分かる。

Y g = (λf . (λx . f (x x)) (λx . f (x x))) g (Yの定義より)
= (λx . g (x x)) (λx . g (x x)) (λfのβ簡約、主関数をgに適用)
= (λy . g (y y)) (λx . g (x x)) (α変換、束縛変数の名前を変える)
= g ((λx . g (x x)) (λx . g (x x))) (λyのβ簡約、左の関数を右の関数に適用)
= g (Y g) (第2式より)

これをそのままラムダ計算で使うと、評価戦略が値渡しだった場合には (Y g) が
(g (Y g)) と展開された後も、引数の値を先に求めようとして
(g (g (Y g))) →...→ (g ... (g (Y g))...) のように無限に展開され続けて
止まらなくなってしまうので、次節で示すZコンビネータのように修正する。

評価戦略が名前渡しの場合はこのまま使える。 このカリーによるコンビネータのみを
Yコンビネータとすることもあるが、実装などでは不動点コンビネータを指す名前として
他の形であってもYという名前を使っていることもある。

SKIコンビネータ計算では次のようになる。
Y = S (K (S I I)) (S (S (K S) K) (K (S I I)))