# CFG for $\lambda$-calculus with minimal parentheses

The typical presentation of the syntax of the $\lambda$-calculus is as an ambiguous CFG (or BNF) like the following:

$$T \rightarrow \lambda X . T \mid T ~ T \mid X \mid (T)$$

Where we permit $X$ to range over an infinite number of variable names. To disambiguate $\lambda$ terms two conventions are usually established:

1. application left associates, and
2. abstractions extend as far as possible.

So according to these rules $\lambda x . x ~ y ~ \lambda z . z$ should be interpreted as $(\lambda x . ((x ~ y) ~ (\lambda z . z)))$. It's clear to me how you could modify the CFG to specify left-associative application.

$$T \rightarrow \lambda X . T \mid U ~ T \mid U$$ $$U \rightarrow X \mid (T)$$

What I'm unsure of is how you would rewrite the grammar to enforce the second rule, that abstractions extend as far as possible, in a CFG. My attempt at this was to make the precedence of application higher.

$$T \rightarrow \lambda X . T \mid P$$ $$P \rightarrow U P \mid U$$ $$U \rightarrow X \mid (T)$$

However this would be unable to parse the $\lambda$-term given above. To be parsed it would have to be $\lambda x . x ~ y ~ (\lambda z . z)$. My intuition is that you couldn't do this with a CFG, but I'm not positive. Is it possible to write a CFG that enforces the second convention? If so how, and if not why not (and is proof of such a fact possible)? Would it be possible for a context-sensitive grammar?

• As far as I am concerned, it is bad manners to write $\lambda$-abstractions in applications without parentheses. That is, instead of $x \lambda y . y$ you should write $x (\lambda y . y)$. (But this doesn't answer your question, it's just a comment about unreasonable syntax.) – Andrej Bauer Jul 18 '18 at 13:39