Order of parentheses in lambda calculus if paranthesis are already given?

user_15430134 0
Viewed 170

I know that application is left associative and abstraction is right associative. Also functions are given preference but I came across some questions which already had "some" parenthesis present in the expression. Do these parenthesis cause any difference in the way the expressions should be calculated? Also what does parenthesis before the first expression means?

I am having confusion in deciding between these -

  1. (lambda x. xy)(lambda y. xy)z --- should I start evaluating from left or right in such a case of e1.e2.z ? I will do substitution which is fine but should I replace x of lambda x first or y of lambda y first?

  2. (((λx.λy.λz.((xy)z)(λu.λv.u))A)B) --- in such a case, I am getting confused by the parentheses. Where should I start evaluating from? Which bracket to open first? Should I calculate from inside out or outside in?

lambda-calculus lambda functional-programming
1 Answers

There is no specified evaluation strategy for lambda calculus. It is either defined by your system or environment. Two common strategies are normal order and applicative order. For this particular problem, the answer is the same regardless of strategy. If you are using another unconventional strategy, you can expect the result to vary.

(λx.xy)(λy.xy)z    →β x [x := (λy.xy)]

((λy.xy)y)z        remove unnecessary parens

(λy.xy)yz          →β y [y := y]

(xy)z              remove unnecessary parens

xyz

As you know, application is left-associative. So removing the unnecessary parens makes it much easier to read the expression -

(((λx.λy.λz.((xy)z)(λu.λv.u))a)b)    remove unnecessary parens

(λx.λy.λz.(xyz)(λu.λv.u))ab          →β x [x := a]

(λy.λz.(ayz)(λu.λv.u))b              →β y [y := b]

(λz.(abz)(λu.λv.u))                  remove unnecessary parens

λz.(abz)(λu.λv.u)

In the second example we have reached weak head normal form, ie we have λz. without any arguments to apply to it

user_6331830
Related