lambdalambda-calculusreduction

Lambda Calculus reduction

All,

Below is the lambda expression which I am finding difficult to reduce i.e. I am not able to understand how to go about this problem.

(λm λn λa λb . m (n a b) b) (λ f x. x) (λ f x. f x)

This is what I tried, but I am stuck:

Considering the above expression as : (λm. E) M equates to

E = (λn λa λb. m (n a b) b)  
M = (λf x. x) (λ f x. f x)  

 => (λn λa λb. (λ f x. x) (λ f x. f x) (n a b) b)

Considering the above expression as (λn. E) M equates to

E = (λa λb. (λ f x. x) (λ f x. f x) (n a b) b)  
M = ??

.. and I am lost!!

Can anyone please help me understand that, for ANY lambda calculus expression, what should be the steps to perform reduction?

Solution

  • You can follow the following steps to reduce lambda expressions:

    1. Fully parenthesize the expression to avoid mistakes and make it more obvious where function application takes place.
    2. Find a function application, i.e. find an occurrence of the pattern (λX. e1) e2 where X can be any valid identifier and e1 and e2 can be any valid expressions.
    3. Apply the function by replacing (λx. e1) e2 with e1' where e1' is the result of replacing each free occurrence of x in e1 with e2.
    4. Repeat 2 and 3 until the pattern no longer occurs. Note that this can lead to an infinite loop for non-normalizing expressions, so you should stop after 1000 iterations or so ;-)

    So for your example we start with the expression

    ((λm. (λn. (λa. (λb. (m ((n a) b)) b)))) (λf. (λx. x))) (λf. (λx. (f x)))

    Here the subexpression (λm. (λn. (λa. (λb. (m ((n a) b)) b)))) (λf. (λx. x)) fits our pattern with X = m, e1 = (λn. (λa. (λb. (m ((n a) b)) b)))) and e2 = (λf. (λx. x)). So after substitution we get (λn. (λa. (λb. ((λf. (λx. x)) ((n a) b)) b))), which makes our whole expression:

    (λn. (λa. (λb. ((λf. (λx. x)) ((n a) b)) b))) (λf. (λx. (f x)))

    Now we can apply the pattern to the whole expression with X = n, e1 = (λa. (λb. ((λf. (λx. x)) ((n a) b)) b)) and e2 = (λf. (λx. (f x))). So after substituting we get:

    (λa. (λb. ((λf. (λx. x)) (((λf. (λx. (f x))) a) b)) b))

    Now ((λf. (λx. (f x))) a) fits our pattern and becomes (λx. (a x)), which leads to:

    (λa. (λb. ((λf. (λx. x)) ((λx. (a x)) b)) b))

    This time we can apply the pattern to ((λx. (a x)) b), which reduces to (a b), leading to:

    (λa. (λb. ((λf. (λx. x)) (a b)) b))

    Now apply the pattern to ((λf. (λx. x)) (a b)), which reduces to (λx. x) and get:

    (λa. (λb. b))

    Now we're done.