Есть одна свободная переменная, f
. j
, x
и y
связаны абстракцией.
Существует два способа достижения нормальной формы. Либо выполните два бета-сокращения
(λj.λx.f(j x)) (λy.f y) == (λx.f(<b>(λy.f y)</b> x)) <i>apply (λj.λx.f(j x)) to (λy.f y) </i>
== (λx.f(<b>f x</b>)) <i> apply (λy.f y) to x</i>
, либо выполните eta-сокращение с последующим бета-уменьшением.
(λj.λx.f(j x)) (λy.f y) == (λj.λx.f(j x)) <b>f</b> <i> replace (λy.f y) with f</i>
== (λx.f(<b>f</b> x)) <i> apply (λj.λx.f(j x)) to f</i>