2

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.

TheDarkHoarse
  • 145
  • 1
    Use more parentheses. Specifically, use fully parenthesized expressions as you are making mistakes by interpreting things different ways. That is, you are producing expressions that are (implicitly) parenthesized one way, but are using them as if they are parenthesized another. – Derek Elkins left SE Feb 20 '18 at 19:55

1 Answers1

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.

Euge
  • 171