2
$\begingroup$

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?

Improve this question
$\endgroup$
2
  • $\begingroup$ 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) $\endgroup$
    – chi
    Commented May 28, 2019 at 15:33
  • $\begingroup$ @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". $\endgroup$
    – hugo
    Commented May 28, 2019 at 16:00

2 Answers 2

Reset to default
3
$\begingroup$

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.

Improve this answer
$\endgroup$
2
  • $\begingroup$ 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. $\endgroup$
    – Andrej Bauer
    Commented Dec 20, 2021 at 16:13
  • 1
    $\begingroup$ I see. I would be surprised if people could ever agree on concrete syntax. We have Wadler's law after all. $\endgroup$
    – Andrej Bauer
    Commented Dec 21, 2021 at 7:21
1
$\begingroup$

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)
Improve this answer
$\endgroup$

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Not the answer you're looking for? Browse other questions tagged or ask your own question.