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 asx(yz)
.Applicative order:
Normal order (left outermost):
So both reductions reach the same result:
(cc)c
, which is the same asccc
.