Search code examples
lambda-calculus

What is the normal form of this lambda calculus and are there any free variables?

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)
Solution

  • 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