HiveBrain v1.2.0
Get Started
← Back to all entries
patternMinor

How is `y λx.x y` parsed using the standard pure untyped lambda calculus conventions?

Submitted by: @import:stackexchange-cs··
0
Viewed 0 times
thepureuntypedcalculusstandardusinghowconventionsparsedlambda

Problem

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 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 "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.

Solution

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).

Context

StackExchange Computer Science Q#135794, answer score: 4

Revisions (0)

No revisions yet.