The first set of a grammar $𝐴$ may be captured in Lambek${\begin{array}{}\end{array}}^{𝙳}$ via the following proposition:

Or perhaps with ones of the grammars

The followlast set of a grammar $𝐴$ may be captured in Lambek${\begin{array}{}\end{array}}^{𝙳}$ via the following proposition:

Or perhaps with ones of the grammars

A context-free grammar satisfies the LL(1) condition if it satisfies the following three conditions:

• All of its productions have pairwise disjoint first sets
• If a concatenation of nonterminals $𝐴\otimes 𝐵$ appears in a production, then $𝐴$ has a disjoint followlast set from the first set of $𝐵$
• At most one production is nullable

This is essentially the type system of [1], which characterizes the LL(1) condition for context-free expressions.

Intutively, an LL(1) grammar can be parsed unambiguously, and without backtracking, by a predictive parser that only needs one token of lookahead.

The nullability ($\text{𝖭𝗎𝗅𝗅}(\cdot )$) of a grammar $𝐴$ may be captured in Lambek${\begin{array}{}\end{array}}^{𝙳}$ via the following proposition:

Or perhaps with one of the grammars

Grammars $𝐴$ and $𝐵$ are sequentially unambiguous if the followlast set of $𝐴$ is disjoint from the first set of $𝐵$.

We can understand this intuitively by characterizing the behavior of a left-to-right parser of $𝐴\otimes 𝐵$. First it searches for a parse of $𝐴$, then upon finding a character that is not in $\text{𝖥𝖫𝖺𝗌𝗍}(𝐴)$ it may begin trying search for $𝐵$.

That is, there is a unique boundary between the $𝐴$-parse and the $𝐵$-parse.