Normative vs applicative order in reduction in the Lambda Calculus

Question

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.

Answer 1

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.