# Is this a correct grammar for untyped lambda calculus?

I am trying to write a recursive-descent parser for untyped lambda calculus. While researching the way of formulating the grammar, I managed to put together something like this:

without left-recursion:
TERM         -> APPLICATION | ABSTRACTION
ABSTRACTION  -> LAMBDA LCID DOT TERM
APPLICATION  -> ATOM APPLICATION'
APPLICATION' -> ATOM APPLICATION' | ε
ATOM         -> LPAREN TERM RPAREN | LCID
LCID         -> 'a' | 'b' | ... | 'z'
DOT          -> '.'
LAMBDA       -> 'λ'


I assume that for writing the parser I do not necessarily need the productions that only expand into terminals.

Can this grammar be used to write a recursive descent parser that only does 1-token lookups? What would be the resulting AST for (λx.x)(λy.y) ?

Your grammar looks fine. You can make a recursive descent parser for it.

The AST for (\x.x)(\y.y) is, if I got everything right,

term
application
atom
lparen
term
abstraction
lambda
lcid
x
dot
term
application
atom
lcid
x
application'
eps
rparen
application'
atom
lparen
term
abstraction
lambda
lcid
x
dot
term
application
atom
lcid
y
application'
eps
rparen
application'
eps

• Thanks for your response. The reason I asked for the parse tree is because I'm having trouble understanding how a parser would determine that the outermost TERM expands into APPLICATION. Is this possible to do using 1-token lookup? – Jan Parzydło Nov 19 '18 at 19:27
• @JanParzydło TERM expands into either APPLICATION or ABSTRACTION. Only the latter begins with LAMBDA. So, if you see LPAREN, you try APPLICATION. – chi Nov 19 '18 at 20:55