How is `y λx.x y` parsed using the standard pure untyped lambda calculus conventions? 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 &quot;applications are left associative&quot; rule is first applied, we get (y (λx.x)) y, and if the &quot;abstraction extends as far right as possible&quot; 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 as y (λ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 &quot;abstraction extends as far right as possible&quot; 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 &quot;applications are left associative&quot; rule would kick in first.
The left associativity of applications is only relevant when you have a sequence of applications. If it were correct to interpret y λx.x y as y (λx.x) y, then the left associativity rule would disambiguate it to (y (λx.x)) y. But that interpretation violates the rule that abstractions extend as far right as possible.
Normally one never writes y λx.x y unparenthesized, so I think it's best for parsers to reject it, but if I saw it I would guess that it means y (λx.x y).