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?
Lambda abstraction is λx.M
, for some variable x
and arbitrary term M
.
Application is (MN)
, for some arbitrary terms M
and N
.
Precedence 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 omission 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 abstraction, 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)
.