Writing a grammar for lambda calculus

I'm trying to write a context-free grammar (to be feeded to lark) for parsing lambda calculus expressions. Basic version of it, as presented by most sources, looks like:

expr: variable | "(" expr ")" | application | abstraction
abstraction: "λ" variable "." expr
application: expr expr


I'd like the grammar to unambiguously parse expressions taking advantage of the notational conventions mentioned here on Wikipedia. While I'm able to modify the grammar to follow most of them, I got stuck with implementing this one: "The body of an abstraction extends as far right as possible".

For example, there are two parse trees for λx.x λa.a - it can be both an application of two abstractions ( (λx.x)(λa.a) ) or an abstraction with an application in its body ( λx.(x(λa.a)) ). If the abstraction was greedy as it should be, only the second one would be correct.

Is it possible to write a grammar that would force (i.e., make it the only choice) greedy interpretation of abstractions? If so, how to do it?

• I'd make abstraction to be $(\lambda x.\, e)$ and application to be $(e_1\ e_2)$, adding explicit parentheses to both. In this way, abstraction extends until the matching parenthesis. Application is now unambiguous (while it's very common to read $x\ y\ z$ as $(x\ y)\ z$, the original grammar allows both parses)
– chi
May 28, 2019 at 15:33
• @chi thank you very much for the idea, that's another good approach to try. However I aim to be as close to "handwritten" lambda calculus as possible, and forcing brackets around abstractions and applications, while making the gramar unambiguous, also makes it differ from the "handwritten".
– hugo
May 28, 2019 at 16:00

If your motivation is practicability, you could have a look at the grammar for lambda in the PL Zoo. Start reading below the comment saying "main syntax tree", and you may safely ignore the mark_position business which just tags the syntax tree with positions in the file. What's left is an unambiguous context-free grammar.

We can summarize the grammar as follows:

expr ::=
| LAMBDA binders PERIOD expr
| app_expr

app_expr ::=
| simple_expr
| app_expr simple_expr

simple_expr ::=
| name
| LPAREN expr RPAREN

binders ::= name+

name ::= NAME


Here NAME is a lexing token carrying a variable name and R+ means "one or more repetitions of R".

Note however that while textbooks say that the body of a $$\lambda$$-application should extend to the right as far as possible, they do not specify how brackets are to be used in an application. In particular, most people would find $$x \lambda a . a$$ to be confusing, even though it obviously means $$x (\lambda a . a)$$.

You should also pay attention to the associativity of application, i.e., is $$A B C$$ equal to $$(A B) C$$ or $$A (B C)$$?

So if you want a realistic grammar you should require certain restriction in an application. To see what precisely these could be, consult the lambda grammar linked to above.

• Well, I am not sure, that depends on the audience. It's a valid question within the context of proof assistants, but may be a bit on the "help me read syntax" side. Dec 20, 2021 at 13:14
• But to answer your question, yes, why wouldn't x (λ a . a) be valid? It follows the rules of the above (abstract syntax) grammar. Dec 20, 2021 at 13:15
• If you are implementing concrete syntax then you should use parenthesis. If you are specifying abstract syntax, you should not use parenthesis. See this lecture. Dec 20, 2021 at 16:13
• We're discussing two versions of concrete syntax for $\lambda$-calculus, it seems. I don't see how this is very interesting. Obviously we can devise different sets of conventions about how we write sequences of symbols from left to right. Dec 20, 2021 at 19:37
• I see. I would be surprised if people could ever agree on concrete syntax. We have Wadler's law after all. Dec 21, 2021 at 7:21

As @chi wrote, one good solution would be to enforce parenthesis around both applications and abstractions.

Because I want to be as close to "handwritten" lambda calculus (so I'd like to eliminate parenthesis as much as possible), I tried another approach, which eventually worked. I blocked applications from having abstractions (not parenthesised abstractions, just abstractions) on their left side, so that λx.x M will never parse to (λx.x)M. This will force the greedy parsing of abstractions - λx.(xM), exactly as I want.

The grammar doing that might look like this:

atom: "(" expression ")" | variable
expr: atom | abstraction | application
abstraction: "λ" variable "." expr
application: atom | application (atom | abstraction)