Yの不動点

Y = λf.(λx.f(xx))(λx.f(xx)) — 名前のない関数に再帰を注入する不動点コンビネータの作業場。

不動点コンビネータ Y は 名前を使わずに再帰を作る魔法。Y g = g (Y g) という方程式の解で、Y g は g の不動点。Curry の発見した Y = λf.(λx.f(x x))(λx.f(x x)) を使えば、無名のラムダ式でも factorial や fibonacci を表現できる。
画面で赤色のレデックス(reducible expression) をクリックして β-簡約を進めよう。fact 5 = 120 を出せばクリア。

step0

redex0

size0

strategynormal

例題

達成! 不動点コンビネータで再帰を流し、結果に到達した。
Y は 第二不動点定理の構成的証明。Y g は g の不動点であり、名前なしで再帰を可能にする。call-by-value 言語ではZ = λf.(λx.f(λv.x x v))(λx.f(λv.x x v)) を使う。
横山研のλ計算/コンビネータ論理 (SKI/BCKW) 研究はこの形式系の表現力と、可逆計算への翻訳を扱う。

操作

項中の 赤色のサブターム がレデックス ((λx.M) N の形)。クリックすると β 簡約を1ステップ実行する。Auto-step はノーマル順 (左から最外) で10ステップ進める。

β-redex: (λx.M) N →β M[x:=N] α-conversion で変数捕獲を回避 Y = λf.(λx.f(xx))(λx.f(xx)) Y g = g (Y g) Z = λf.(λx.f(λv.x x v))(λx.f(λv.x x v)) (call-by-value)

SKI 結合子論理では Y は S(K(SII))(S(S(KS)K)(K(SII))) のように構成可能。横山研の可逆コンビネータ研究 (RCC/RC など) では各書換が可逆になる体系を扱う。