[Math] Normative vs applicative order in reduction in the Lambda Calculus

lambda-calculus

Ok, so I am attempting to learn reduction of terms in lambda calculus in detail. The only thing seemingly that I don't quite get is the sense of "order of operations" in the lambda calculus. I understand that in lambda calculus variable and function application is normative, (i.e. the leftmost applications are to be done first), but in an example like this:

(λab.(λb.abb)b) (λa.aa)c

I'm confused by the normative/normal order. In the applicative, it's straightforward as you just go with the innermost application:

1(λab.(λb.abb)b) (λa.aa)c
2(λab.abb) (λa.aa)c         [beta-substitution, [b/b] in the body of λb.abb]
3(λab.abb)cc                [" ", [c/a] in the body of λa.aa]
4(ccc)                      [" ", [c/a] and [c/b] in the body of λab.abb]

Or at least that is how I understand it, correct me if I am wrong. But how is it reduced in the normative order (normal order in lambda calc)? I'm not sure of the order of things, specifically what to do in line 2.

Best Answer

As you said, applicative order reduction goes with inner beta redex first. But be careful with the associativity. Application in lambda calculus is left-associative, so xyz is interpreted as (xy)z and not as x(yz).

Applicative order:

1(λab.(λb.abb)b) (λa.aa)c
2(λab.abb) (λa.aa)c         [beta-substitution, [b/b] in the body of λb.abb]
3(λa.aa)cc                  [" ", [(λa.aa)/a][c/b] in the body of λab.abb]
4(cc)c                      [" ", [c/a] in the body of λa.aa]

Normal order (left outermost):

1(λab.(λb.abb)b)(λa.aa)c
2(λb.(λa.aa)bb)c            [beta-substitution, [(λa.aa)/a][c/b] in the body of λab.(λb.abb)b]
3(λa.aa)cc                  [" ", [c/b] in the body of λb.(λa.aa)bb]
4(cc)c                      [" ", [c/a] in the body of λa.aa]

So both reductions reach the same result: (cc)c, which is the same as ccc.

Related Question