I am trying to learn lambda calculus, but I am having a hard time doing it. So if anyone would explain a little bit, I would greatly appreciate it!
(λj.λx.f(j x)) (λy.f y)
There is one free variable, f
. j
, x
, and y
are all bound by an abstraction.
There are two ways you can reach normal form. Either perform two beta reductions
(λj.λx.f(j x)) (λy.f y) == (λx.f((λy.f y) x)) apply (λj.λx.f(j x)) to (λy.f y)
== (λx.f(f x)) apply (λy.f y) to x
or perform an eta reduction followed by a beta reduction.
(λj.λx.f(j x)) (λy.f y) == (λj.λx.f(j x)) f replace (λy.f y) with f
== (λx.f(f x)) apply (λj.λx.f(j x)) to f