john7rv

ラムダ計算は数学の計算を全てラムダ関数で表現しようと
するものです。
そのため数字もチャーチ数で表します。
ループもラムダ関数で表せなければなりません。
そのためにはFixedPoint演算子を使う必要があります

ラムダ式でFixedPointを考えると
FixedPoint = (λx.(F(xx)))(λx.(F(xx)))
となります

(λx.(F(xx)))が２つ連続しており
後ろの(λx.(F(xx)))を前の(λx.(F(xx)))のxにβ変換すれば
F(xx) ← (λx.(F(xx))) xにβ変換
(F( (λx.(F(xx))) (λx.(F(xx)) ))
となり
(λx.(F(xx)))(λx.(F(xx))) = (F(λx.(F(xx)))(λx.(F(xx))))
という形になり
FixedPointになっています

これは
任意のラムダ式FにおいてX＝FXとなるラムダ式Xがある
という定理になります

チャーチはラムダ計算において
任意の再帰はfix(FixedPointFunction)と非再帰に分割できることを示しました