まず、(\lambda x. F(x x)) (\lambda x. F(x x)) という式をβ簡約してみると、
\begin{aligned}
& (\lambda x. F(x x)) (\lambda x. F(x x)) \\
\to &[(\lambda x. F(x x)) / x] F(x x) \\
= & F ((\lambda x. F(x x)) (\lambda x. F(x x)))
\end{aligned}
となる。つまり M_F = (\lambda x. F(x x)) (\lambda x. F(x x))とおくと、=_{\beta}
をβ簡約を含む最小の同値関係として、
となるから、M_F は関数 F の不動点である。
次に、Y = \lambda f. M_f = \lambda f. (\lambda x. f(x x)) (\lambda x. f(x x)) とすると、
前の結果と同様に、
このことから、Y は任意の関数 F を引数として受け取ってその F の不動点を返すような関数（不動点演算子）になっていることがわかる。
不動点演算子 Y を使うことで、ラムダ計算で再帰を表現することができる。
表現したい再帰関数 F がある関数 G の不動点になっていることが分かれば、Y G によって F を定められるという仕組みだ。
例えば、階乗を求める fact をラムダ計算で表現したいとする。 fact は等式
f = \lambda n. \ \mathrm{if} \ n = 0 \ \mathrm{then} \ 1 \ \mathrm{else} \ n \cdot f (n - 1)
を満たす。ここで、
factgen = \lambda f. \lambda n. \ \mathrm{if} \ n = 0 \ \mathrm{then} \ 1 \ \mathrm{else} \ n \cdot f (n - 1)
と定義してやれば、fact は f = factgen \ f を満たすことになるので、fact は factgen の不動点になっていることがわかる。
よって、不動点演算子を用いて fact = Y \ factgen と書ける。
実際にプログラミング言語で実装してみよう。ただし、不動点演算子 Y（Yコンビネータと呼ばれる）をこの形のまま乗せることはできない
（引数を評価しないまま式が再帰的に展開され、無限ループに陥ってしまうため）。そこで、
η変換（M \to \lambda x. M x）を Yコンビネータに施した、
\lambda f. (\lambda x. f(\lambda y. x x y)) (\lambda x. f(\lambda y.x x y))
を代わりに使おう（これはZコンビネータと呼ばれる）。
Python での実装例:
Z = lambda f: (lambda x: f (lambda y: x(x)(y)))(lambda x: f (lambda y: x(x)(y)))
factgen = lambda f: (lambda n: 1 if (n == 0) else n * f (n - 1))
fact = Z (factgen)
fact(10)
Discussion