Theoretical Computer Science Stack Exchange is a question and answer site for theoretical computer scientists and researchers in related fields. It only takes a minute to sign up.
Sign up to join this community
I am playing with a lambda calculus and faced a question I find hard to reason about.
On the screenshot you may find the lambda calculus grammar. Is it an instance of the LL(k) grammar such that a recursive descent parser could handle it? How do you proof such a statement? What would be the best hint here?
After some trivial factorization, I think it should be easy to prove it's LL(1) by constructing the LL(1) table for it. The grammar would be:
M ::= x | ( N )
N ::= λx.M | M M
Without the factorization, if you consider the simpler, obvious grammar:
M ::= x | (λx.Μ) | (Μ Μ)
it's not LL(1), as the second and third alternative share a common prefix (, but it's LL(2). In any case, you can definitely construct a recursive descent parser for it.
Edit: Adding a (non-standard, I must say) rule for redundant parentheses around terms complicates things. The following grammar is not LL(k) for any value of k:
M ::= x | (λx.Μ) | (Μ Μ) | (M)
The reason is that, in order to decide between the third and the fourth alternative, a predictive parser would have to read the common prefix (M, which can be arbitrarily long.
However, after factorization, the following equivalent grammar is again LL(1):
M ::= x | (N)
N ::= λx.Μ | Μ L
L ::= Μ | ε
(x) for example or ((\x . x)), right?
$\endgroup$
M := (M) case, which indeed was not mentioned at the screenshot I've posted, yet assumed.
$\endgroup$