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:
- application left associates, and
- 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?