Lambda reduction

Question

I'm having trouble understanding how to reduce lambda terms to normal form. could someone help me to understand how to reduce this lambda expression? I don't know exactly where to start.

(λx. ( λa. (λx. x a)) x) 20 (λx. x+3)

Thank you in advance

Answer 1

I'll just focus on your expression. For a deeper explanation, you could read the answer to this question.

First of all, let's consider how brackets could be interpreted on these expressions. Consider the following expression:

(λx. x*x) 5 => 5*5 => 25

So, evaluation of this expression is done replacing the x by value 5 outside brackets.

Now, let's put some brackets from left to right on your expression:

(((λx. ( λa. (λx. x a)) x) 20) (λx. x+3))

Let's call (λa. (λx. x a)) the variable z as a simplification. So, we'll have:

(((λx. z x) 20) (λx. x+3))

and the expression is now similar to our first example. Replacing x by value 20, we'll have:

((z 20) (λx. x+3))

which is the same as:

(((λa. (λx. x a)) 20) (λx. x+3))

Again, we can replace a by 20 resulting

((λx. x 20) (λx. x+3))

Afterwards, we could replace x at the left expression by the whole expression on the right (λx. x+3).

((λx. x+3) 20)

Finally, we could replace x by 20:

((λx. x+3) 20) => 20+3 = 23

Answer 2

Proceed by substitution, left-to-right:

(λx.      ( λa. (λx. x a )) x )  20  (λx. x+3)
~~
([x:= 20] ( λa. (λx. x a )) x )      (λx. x+3)
~~
          ( λa. (λx. x a )) 20       (λx. x+3)
~~
      ( [a:=20] (λx. x a ))          (λx. x+3)
~~
                (λx. x 20)           (λx. x+3)
~~
     ([x:=(λx. x+3)] x 20)
~~
          (λx. x+3)    20
~~
      ([x:=20] x+3)
~~
              20+3

There's no more reductions to perform, thus this is the normal form of the original lambda term.