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 ::= Μ | ε