How would the following term in the pure untyped lambda calculus be parsed:
y λx.x y
The relevant conventions listed on https://en.wikipedia.org/wiki/Lambda_calculus_definition#Notation (as well as many texts on this subject) state:
- Applications are assumed to be left associative:
M N P
is parenthesised as((M N) P)
- The body of an abstraction extends as far right as possible: λx.M N is parenthesised as
(λx.(M N))
and not((λx.M) N)
There is no priority specified between these two conventions.
In the case of y λx.x y
, if the "applications are left associative" rule is first applied, we get (y (λx.x)) y
, and if the "abstraction extends as far right as possible" rule is first applied, we get y (λx.x y)
. Which one is considered correct, and on what basis?
Observations and thoughts:
I have tried this on some online tools, and this is what I observed:
- https://projectultimatum.org/cgi-bin/lambda parses
y λx.x y
asy (λx.x y)
- https://crypto.stanford.edu/~blynn/lambda/simply.html cannot parse
y λx.x y
(result is a parse error) - https://jacksongl.github.io/files/demo/lambda/ also results in a parse error.
I initially thought that the rule "abstraction extends as far right as possible" was equivalent to specifying that application binds tighter than abstraction. But this assumption may be wrong. Under this assumption, y λx.x y
would be parsed as (y (λx.x)) y
, since the "applications are left associative" rule would kick in first.