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?

  • 2
    $\begingroup$ 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.) $\endgroup$ – Andrej Bauer Jul 18 '18 at 13:39

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Browse other questions tagged or ask your own question.