lambda calculus precedence of application and abst

2019-08-23 01:13发布

Application has higher precedence than abstraction.

In this sense, what is lambda calculus abstraction? I'm confused at what there is to have precedence over?

1条回答
smile是对你的礼貌
2楼-- · 2019-08-23 01:43

Lambda abstraction is λx.M, for some variable x and arbitrary term M.
Application is (MN), for some arbitrary terms M and N.

Precdence is the question which of several operation is to be performed first if more than one reading is possible because the term is ambiguous due to ommission of brackets. For example in arithmetic, multiplication by convention has precedence over addition, which means that 5+2×3 is read as 5+(2×3) and not as (5+2)×3. The multiplication operator is evaluated first and binds the terms closest to it, and addition comes secondary, embedding the multiplication term.

W.r.t. to lambda calculus, the convention that application has higher precedence than abstraction means that in case of doubt because brackets have been ommitted, you will first try to form an application and only afterwards perform abstraction, so application "binds" stronger, and an abstraction term will be formed later and subsume the application term.

E.g., λx.M N could in principle be read as either λx.(MN) or (λx.M)M, but since application has precedence over application, you first form the possible application (MN) and then the abstraction λx.(MN). If it were the other way round, i.e. if abstraction had precedence over application, then you would first try to form an abstraction term (λx.M), then application with the term you already got ((λx.M)M).
So by defining that application has precedence over abstraction, λx.M N = λx.(MN), and not ((λx.M)M).

查看更多
登录 后发表回答