Lambda Calculus reduction

16
votes

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?

3
lambdalambda-calculusreduction
I think you have the right idea. One question - do lambdas associate from left to right or right to left? In your example, for instance, you are associating them from right to left. – danben
Also - what is (λ f x. x)? Is that some kind of shorthand for (λ f. λx. x)? – danben
@danben: Function application is left associative and abstraction is right associative. The above is abstraction if I am correct? ! And yes that is a shorthand. – name_masked
@danben: Does Lambda calculus not come under Functional programming? – name_masked
@darkie15 - no, this is like tagging a question about big O analysis with 'C++'. – danben

3 Answers

20
votes

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.

4
votes

Where you're going wrong is that in the first step, you can't have 

M = (λf x. x)(λ f x. f x)

because the original expression doesn't include that application expression. To make this clear, you can put in the implicit parentheses following the rule that application is left-associative (using [ and ] for the new parens and putting in some missing "."s):

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

From here, find an expression of the form (λv.E) M some where inside and reduce it by replacing v with M in E. Be careful that it really is an application of the function to M: it isn't if you have something like N (λv.E) M, since then N is applied to the function and M as two arguments.

If you're still stuck, try putting in the parens for each lambda also - basically a new "(" after each ".", and a matching ")" that goes as far to the right as possible while still matching the new "(". As an example, I've done one here (using [ and ] to make them stand out):

( (λm . λn . λa . [λb . m (n a b) b]) (λ f x. x) ) (λ f x. f x)
0
votes

Just substitute a thing for its corresponding thing:

(λm λn λa λb . m          (n            a b) b) (λ f x. x) (λ f x. f x)
= ~            ^________                        ~~~~~~~~~~
   (λn λa λb . (λ f x. x) (n            a b) b)            (λ f x. f x)
=    ~                     ^__________                     ~~~~~~~~~~~~
      (λa λb . (λ f x. x) ((λ f x. f x) a b) b)
=                 ~       ~~~~~~~~~~~~~~~~~~
      (λa λb .   (λ x. x)                    b)
=                   ~  ^                     ~
      (λa λb .         b                      )

That is all.