Local Lexing

TL;DR

This paper introduces local lexing, a new parsing approach that unifies lexing and parsing stages, enabling more flexible language design and integrated error handling, supported by a verified Earley's algorithm extension.

Contribution

It presents the concept of local lexing, an extension of Earley's algorithm, with formal correctness proof, allowing dependency-aware lexing and integrated error handling.

Findings

Formal verification of the local lexing algorithm in Isabelle/HOL

Extension of Earley's algorithm for local lexing

Enhanced language design flexibility with integrated error handling

Abstract

We introduce a novel parsing concept called local lexing. It integrates the classically separated stages of lexing and parsing by allowing lexing to be dependent upon the parsing progress and by providing a simple mechanism for constraining lexical ambiguity. This makes it possible for language design to be composable not only at the level of context-free grammars, but also at the lexical level. It also makes it possible to include lightweight error-handling directly as part of the language specification instead of leaving it up to the implementation. We present a high-level algorithm for local lexing, which is an extension of Earley's algorithm. We have formally verified the correctness of our algorithm with respect to its local lexing semantics in Isabelle/HOL.

Equations

$${\mathcal{L}}_{\text{prefix}}=\left\{w\in {\mathfrak{T}}^{\ast }|\exists \alpha \in (\mathfrak{N}\cup \mathfrak{T}{)}^{\ast }.\mathfrak{S}\stackrel{\ast }{\Rightarrow }w\alpha \right\}.$$

$$\small\dfrac{\texttt{$c$}}{\textsl{$t$}}$$

$$\text{textsl}Sel(A,B)=A\cup \left\{x\in B\mid \forall y\in B.\neg x{<}_{\text{textsl}Sel}y\right\}.$$

$${\mathcal{X}}_k=\left\{x\in \mathfrak{T}\times {\Sigma }^{\ast }\mid x\in \text{textsl}Lex([x])(D,k)\right\}$$

$${\mathcal{W}}_k^0=\left\{x\in {\mathcal{X}}_k|\exists p\in {\mathcal{P}}_k^0.|\overline{p}|=k\wedge [px]\in {\mathcal{L}}_{\text{prefix}}\right\}.$$

$${\mathcal{Z}}_k^1=\text{textsl}Sel(\varnothing ,{\mathcal{W}}_k^0)$$

$${\mathcal{P}}_k^1={\mathrm{Append}}_k{\mathcal{Z}}_k^1{\mathcal{P}}_k^0,$$

$${\mathrm{Append}}_{k}TP=P\cup$$

$$\left\{pt\mid p\in P\wedge |\overline{p}|=k\wedge t\in T\wedge [pt]\in {\mathcal{L}}_{\text{prefix}}\right\},$$

$${\mathcal{P}}_k^1=\mathrm{limit}({\mathrm{Append}}_k{\mathcal{Z}}_k^1){\mathcal{P}}_k^0,$$

$$\mathrm{limit}fX=\bigcup _{n=0}^{\infty }{f}^n(X).$$

$$\begin{array}[]{ccccccc}\mathcal{W}_{k}^{0}&\subseteq&\mathcal{W}_{k}^{1}&\subseteq&\mathcal{W}_{k}^{2}&\subseteq&\ldots\\[2.27621pt] \rotatebox{90.0}{$\subseteq$}&&\rotatebox{90.0}{$\subseteq$}&&\rotatebox{90.0}{$\subseteq$}&&\\ \mathcal{Z}_{k}^{0}&\subseteq&\mathcal{Z}_{k}^{1}&\subseteq&\mathcal{Z}_{k}^{2}&\subseteq&\ldots\\[2.84526pt] \mathcal{P}_{k}^{0}&\subseteq&\mathcal{P}_{k}^{1}&\subseteq&\mathcal{P}_{k}^{2}&\subseteq&\ldots\end{array}$$

$$\begin{array}[]{rcl}\mathcal{W}_{k}^{u}&=&\left\{x\in\mathcal{X}_{k}\ |\ \exists\,p\in\mathcal{P}_{k}^{u}.\ |\overline{p}|=k\ \wedge\ [px]\in\mathcal{L}_{\text{prefix}}\right\}\\[5.69054pt] \mathcal{Z}_{k}^{u+1}&=&\textsl{Sel}(\mathcal{Z}_{k}^{u},\mathcal{W}_{k}^{u+1})\\[5.69054pt] \mathcal{P}_{k}^{u+1}&=&\operatorname{limit}\ {(\operatorname{Append}_{k}\ {\mathcal{Z}_{k}^{u+1}})}\ {\mathcal{P}_{k}^{u}}.\end{array}$$

$${\mathcal{P}}_k^{\infty }=\bigcup _{u=0}^{\infty }{\mathcal{P}}_k^u$$

$$\ell \ell (D)=\left\{p\in \mathfrak{P}\mid |\overline{p}|=|D|\wedge [p]\in \mathcal{L}\right\}.$$

$$(r_1,t_1)\dots (r_n,t_n).$$

$$\text{textsl}Lex(t_i)(D,k)=\{(t_i,c)\},$$

$$(t_i,c){<}_{\text{textsl}Sel}(t_j,d)\text{iff}|c|<|d|\vee (|c|=|d|\wedge i<j).$$

$$\mathfrak{R}=\left\{\begin{array}[]{rcl}\textsl{S}&\rightarrow&\textsl{S}\,T,\\ \textsl{S}&\rightarrow&\varepsilon,\\ \textsl{T}&\rightarrow&t_{1},\\ &\vdots&\\ \textsl{T}&\rightarrow&t_{n}\end{array}\right\}.$$

$$\ell\ell(\texttt{aa})=\left\{\small\dfrac{\texttt{aa}}{\textsl{$t_{1}$}},\small\dfrac{\texttt{aa}}{\textsl{$t_{1}$}}\small\dfrac{\texttt{$\varepsilon$}}{\textsl{$t_{1}$}},\small\dfrac{\texttt{aa}}{\textsl{$t_{1}$}}\small\dfrac{\texttt{$\varepsilon$}}{\textsl{$t_{1}$}}\small\dfrac{\texttt{$\varepsilon$}}{\textsl{$t_{1}$}},\small\dfrac{\texttt{aa}}{\textsl{$t_{1}$}}\small\dfrac{\texttt{$\varepsilon$}}{\textsl{$t_{1}$}}\small\dfrac{\texttt{$\varepsilon$}}{\textsl{$t_{1}$}}\small\dfrac{\texttt{$\varepsilon$}}{\textsl{$t_{1}$}},\ldots\right\},$$

$${<}_{\text{textsl}Sel}=\varnothing ,$$

$$\frac{\text{a}}{\text{textsl}symbol}\frac{\text{-}}{\text{textsl}minus}\frac{\text{b}}{\text{textsl}id}\frac{\text{+}}{\text{textsl}plus}\frac{\text{c}}{\text{textsl}id}\notin \ell \ell (D),$$

$$\ell\ell(\texttt{a-b+c})={\small\left\{\begin{tabular}[]{l}\small$\dfrac{\texttt{a}}{\textsl{id}}$\ \small$\dfrac{\texttt{-}}{\textsl{minus}}$\ \small$\dfrac{\texttt{b}}{\textsl{id}}$\ \small$\dfrac{\texttt{+}}{\textsl{plus}}$\ \small$\dfrac{\texttt{c}}{\textsl{id}}$\ ,\\[8.5359pt] \small$\dfrac{\texttt{a}}{\textsl{id}}$\ \small$\dfrac{\texttt{-}}{\textsl{minus}}$\ \small$\dfrac{\texttt{b}}{\textsl{id}}$\ \small$\dfrac{\texttt{+}}{\textsl{plus}}$\ \small$\dfrac{\texttt{c}}{\textsl{symbol}}$\ ,\\[8.5359pt] \small$\dfrac{\texttt{a}}{\textsl{id}}$\ \small$\dfrac{\texttt{-}}{\textsl{minus}}$\ \small$\dfrac{\texttt{b}}{\textsl{symbol}}$\ \small$\dfrac{\texttt{+}}{\textsl{plus}}$\ \small$\dfrac{\texttt{c}}{\textsl{id}}$\ ,\\[8.5359pt] \small$\dfrac{\texttt{a}}{\textsl{id}}$\ \small$\dfrac{\texttt{-}}{\textsl{minus}}$\ \small$\dfrac{\texttt{b}}{\textsl{symbol}}$\ \small$\dfrac{\texttt{+}}{\textsl{plus}}$\ \small$\dfrac{\texttt{c}}{\textsl{symbol}}$\ ,\\[8.5359pt] \small$\dfrac{\texttt{a}}{\textsl{id}}$\ \small$\dfrac{\texttt{-b}}{\textsl{symbol}}$\ \small$\dfrac{\texttt{+}}{\textsl{plus}}$\ \small$\dfrac{\texttt{c}}{\textsl{id}}$\ ,\\[8.5359pt] \small$\dfrac{\texttt{a}}{\textsl{id}}$\ \small$\dfrac{\texttt{-b}}{\textsl{symbol}}$\ \small$\dfrac{\texttt{+}}{\textsl{plus}}$\ \small$\dfrac{\texttt{c}}{\textsl{symbol}}$\ ,\\[8.5359pt] \small$\dfrac{\texttt{a-b}}{\textsl{symbol}}$\ \small$\dfrac{\texttt{+}}{\textsl{plus}}$\ \small$\dfrac{\texttt{c}}{\textsl{id}}$\ ,\\[8.5359pt] \small$\dfrac{\texttt{a-b}}{\textsl{symbol}}$\ \small$\dfrac{\texttt{+}}{\textsl{plus}}$\ \small$\dfrac{\texttt{c}}{\textsl{symbol}}$\end{tabular}\right\}}$$

$$x{<}_{\text{textsl}Sel}y\text{iff}[x]=\text{textsl}symbol\wedge [y]\in \{\text{textsl}id,\text{textsl}minus\}.$$

$$\ell \ell (\text{a-b+c})=\left\{\frac{\text{a}}{\text{textsl}id}\frac{\text{-}}{\text{textsl}minus}\frac{\text{b}}{\text{textsl}id}\frac{\text{+}}{\text{textsl}plus}\frac{\text{c}}{\text{textsl}id}\right\},$$

$$x{<}_{\text{textsl}Sel}y\text{iff}|x|<|y|.$$

$$\ell\ell(\texttt{a-b+c})=\small\left\{\begin{tabular}[]{l}\small$\dfrac{\texttt{a-b}}{\textsl{symbol}}$\ \small$\dfrac{\texttt{+}}{\textsl{plus}}$\ \small$\dfrac{\texttt{c}}{\textsl{id}}$\ ,\\[8.5359pt] \small$\dfrac{\texttt{a-b}}{\textsl{symbol}}$\ \small$\dfrac{\texttt{+}}{\textsl{plus}}$\ \small$\dfrac{\texttt{c}}{\textsl{symbol}}$\end{tabular}\right\},$$

$$|x|<|y|\vee (|x|=|y|\wedge [x]=\text{textsl}symbol\wedge [y]=\text{textsl}id).$$

$$\ell \ell (\text{a-b+c})=\left\{\frac{\text{a-b}}{\text{textsl}symbol}\frac{\text{+}}{\text{textsl}plus}\frac{\text{c}}{\text{textsl}id}\right\},$$

$$\displaystyle\mathfrak{R}=\left\{\begin{array}[]{rcl}\textsl{Expr}&\rightarrow&\textsl{Mul},\\ \textsl{Expr}&\rightarrow&\textsl{Cast},\\ \textsl{Expr}&\rightarrow&\textsl{Deref},\\ \textsl{Expr}&\rightarrow&\textsl{id},\\ \textsl{Expr}&\rightarrow&\textsl{left}\ \textsl{Expr}\ \textsl{right},\\ \textsl{Mul}&\rightarrow&\textsl{Expr}\ \textsl{asterisk}\ \textsl{Expr},\\ \textsl{Cast}&\rightarrow&\textsl{left}\ \textsl{Type}\ \textsl{right}\ \textsl{Expr},\\ \textsl{Deref}&\rightarrow&\textsl{asterisk}\ \textsl{Expr},\\ \textsl{Type}&\rightarrow&\textsl{typeid}\end{array}\right\}.$$

$$\ell\ell(\texttt{(a)*b})=\small\left\{\begin{tabular}[]{l}\small$\dfrac{\texttt{(}}{\textsl{left}}$\ \small$\dfrac{\texttt{a}}{\textsl{id}}$\ \small$\dfrac{\texttt{)}}{\textsl{right}}$\ \small$\dfrac{\texttt{*}}{\textsl{asterisk}}$\ \small$\dfrac{\texttt{b}}{\textsl{id}}$\ ,\\[8.5359pt] \small$\dfrac{\texttt{(}}{\textsl{left}}$\ \small$\dfrac{\texttt{a}}{\textsl{typeid}}$\ \small$\dfrac{\texttt{)}}{\textsl{right}}$\ \small$\dfrac{\texttt{*}}{\textsl{asterisk}}$\ \small$\dfrac{\texttt{b}}{\textsl{id}}$\\[8.5359pt] \end{tabular}\right\}.$$

Full text

We present a high-level algorithm for local lexing, which is an extension of Earley’s algorithm. We have formally verified the correctness of our algorithm with respect to its local lexing semantics in Isabelle/HOL.

1 Introduction

The traditional approach to specifying the syntax of a computer language is to define two components, a lexer (also called scanner) and a parser. The lexer partitions the input document consisting of a sequence of characters into a sequence of tokens. Each token is uniquely associated with a terminal, such that the sequence of tokens can be viewed as a sequence of terminals. The parser is typically defined by a context-free grammar (CFG), and checks if the sequence of terminals is in the language generated by the CFG.

CFGs are a powerful language design tool. A most important property of CFGs is composability. Given two or more CFGs, it is easy to combine them into a single CFG in various ways in order to specify a language as a mashup of several other languages, which is a common scenario in modern programming environments.

The lexer component of this traditional setup is problematic though in such a mashup scenario. A keyword in one language might be an identifier in another language, rendering the lexers of these two languages incompatible with each other. The problem is that lexers are not supposed to be composed in the traditional setup. Practical solutions to this problem usually involve some form of ad-hoc communication between parser and lexer stages, thus shifting an issue which should be dealt with at the language design level to the implementation level.

The main reasons for the traditional split of syntax recognition into lexing and parsing are speed, expressivity and convenience:

Speed

Typically terminals are specified via regular expressions that can be recognized with deterministic finite state machines. This is usually much faster than parsing with respect to a CFG.

Expressivity

Despite CFGs being more expressive than regular expressions, two common lexing rules cannot be expressed with CFGs: longest-match, and priority. The longest-match rule states that if multiple terminals are associated with regular expressions that could all match prefixes of the rest of the sequence of characters to be scanned, then the terminals which match the longest prefix are to be preferred. The priority rule comes into play if after application of the longest-match rule there are still at least two different terminals left as possible candidates: then a linear priority order among terminals is assumed, and the terminal with the highest priority among all candidates is picked.

Convenience

In this setup, whitespace and comments are usually special terminals which do not appear in any grammar rule, but which are filtered out of the sequence of terminals during the lexing stage.

Scannerless parsing scannerless proposes to solve our lexing problem by relinquishing separate lexing, effectively identifying characters, tokens and terminals. This negatively affects all three mentioned advantages of a separate lexing stage, the most severely affected being expressivity: in order to approximate the missing longest-match and priority rules, scannerless parsing introduces follow restrictions and reject productions, which are awkard additions to the elegant formalism of context-free grammars because they destroy the nice composability properties of context-free grammars. A scannerless parsing technique called packrat parsing goes even further and does away with context-free grammars entirely, employing parsing expression grammars instead peg , again to the detriment of composability.

Instead, we propose a new parsing semantics which we call local lexing. Local lexing keeps the distinction between lexing and parsing, and between characters, tokens and terminals. But instead of deterministically converting a sequence of characters into a sequence of tokens, local lexing converts a sequence of characters into a set of token sequences, applying lexing and parsing in an intertwined manner.

The contributions of this paper are as follows: We first define the novel concept of local lexing in Section 2. We then present examples of applications of local lexing in Section 3. These examples show that local lexing is a generalisation of the traditional setup, and that local lexing readily allows integrated access at the language design level to issues such as lexical composability and error-handling. In Section 4 we describe a high-level algorithm which implements local lexing as an extension of Earley’s algorithm. We have formally verified the correctness of this algorithm in Isabelle/HOL isabelle , and provide an outline of this correctness proof in Section 5. The full proof (a total of 11411 lines or about 230 pages) is available in locallexingtheories . We also provide a practical library for local lexing locallexingprototype , written in Scala/Scala.js scala ; scalajs . The library contains examples of its application to the examples in Section 3. Before concluding, we discuss further related work in Section 6.

2 Definition of Local Lexing

Before defining local lexing, we remind the reader of a few basic notions. For a set $U$ we let $U^{*}$ denote the set of sequences with elements in $U$, $\varepsilon\in U^{*}$ denotes the empty sequence, and for two sequences $\alpha\in U^{*}$ and $\beta\in U^{*}$ we let $\alpha\beta\in U^{*}$ denote their concatenation. Given a sequence $\alpha\in U^{*}$, we denote its length by $\left|{\alpha}\right|$ and let $\alpha_{i}\in U$ denote the $i$-th element of $\alpha$ for $i\in\{0,\ldots,|\alpha|-1\}$. A context-free grammar is a quadruple $(\mathfrak{N},\mathfrak{T},\mathfrak{R},\mathfrak{S})$, where $\mathfrak{N}$ is the set of nonterminals, $\mathfrak{T}$ the set of terminals (such that $\mathfrak{N}$ and $\mathfrak{T}$ are disjoint), $\mathfrak{R}\subseteq\mathfrak{N}\times(\mathfrak{N}\cup\mathfrak{T})^{*}$ the rules of the grammar and $\mathfrak{S}\in\mathfrak{N}$ the start symbol. Instead of $(\textsl{N},\alpha)\in\mathfrak{R}$ we often write $\textsl{N}\rightarrow\alpha$. For $\alpha,\beta\in(\mathfrak{N}\cup\mathfrak{T})^{*}$ we say $\alpha\Rightarrow\beta$ iff there are $\alpha_{0},\textsl{N},\alpha_{1}$ and $\gamma$ such that $\alpha=\alpha_{0}\textsl{N}\alpha_{1}$, $\beta=\alpha_{0}\gamma\alpha_{1}$ and $\textsl{N}\rightarrow\gamma$. Furthermore, we write $\overset{*\ }{\Rightarrow}$ for the reflexive and transitive closure of $\Rightarrow$. We define the language $\mathcal{L}$ of a grammar $G$ as the set of all sequences of terminals derivable from the start symbol, $\mathcal{L}=\{w\in\mathfrak{T}^{*}\,|\,\mathfrak{S}\overset{*\ }{\Rightarrow}w\}$. Furthermore we define the set of prefixes $\mathcal{L}_{\text{prefix}}$ of $G$ via

[TABLE]

Definition 2.1** (Token).**

Given a set of terminals $\mathfrak{T}$, and a set of characters $\Sigma$, a token $x$ is a pair $x=(t,c)\in\mathfrak{T}\times\Sigma^{*}$. In examples we will often use the notation

[TABLE]

for the token $x$. We call the token empty iff $|c|=0$. We define $[x]=t$ and $\overline{x}=c$. We lift these notations in the obvious manner to sequences of tokens: given a token sequence $q=x_{0}\ldots x_{r}\in(\mathfrak{T}\times\Sigma^{*})^{*}$ we define $[q]=[x_{0}]\ldots[x_{r}]\in\mathfrak{T}^{*}$ and $\overline{q}=\overline{x_{0}}\ldots\overline{x_{r}}\in\Sigma^{*}$.

Definition 2.2** (Local Lexing).**

Given a set of terminals $\mathfrak{T}$, and a set of characters $\Sigma$, we call a pair $(\textsl{Lex},\textsl{Sel})$ a local lexing (with respect to $\mathfrak{T}$ and $\Sigma$) iff:

• •

The lexer Lex assigns to each terminal $t\in\mathfrak{T}$ a lexing function $\textsl{Lex}(t)$ which, given a sequence of characters $D\in\Sigma^{*}$ and a position $k\in\{0,\ldots,|D|\}$, returns a set consisting of tokens $(t,c)$ such that $k+|c|\leq|D|$ and $c_{i}=D_{k+i}$ for all $i$ such that $0\leq i\leq|c|-1$.

• •

The selector Sel takes two token sets $A$ and $B$ such that $A\subseteq B$ and returns a token set $\textsl{Sel}(A,B)$ such that $A\subseteq\textsl{Sel}(A,B)\subseteq B$. We usually define Sel indirectly by defining a strict partial order $<_{\textsl{Sel}}$ on tokens and setting

[TABLE]

Semantics of Local Lexing

Given a local lexing $\ell\ell$, what is its semantics, i.e. how does it convert a sequence $D$ of characters into a set $\ell\ell(D)$ of token sequences? Note that while for defining a particular local lexing $\ell\ell$ we do not need a context-free grammar, just its sets of terminals and characters, the semantics of $\ell\ell$ is dependent upon a grammar. In the following we will often call token sequences paths.

The conversion process works as follows: We go through $D$ from left to right, producing sets of paths $\mathcal{P}_{k}^{u}\subseteq(\mathfrak{T}\times\Sigma^{*})^{*}$ along the way. The index $k\in\{0,\ldots,|D|\}$ denotes the position in $D$ we are looking at, and we use the index $u\in\{0,1,\ldots\}$ to track iteratively generated $\mathcal{P}_{k}^{0}$, $\mathcal{P}_{k}^{1}$, $\ldots$ at this position. Let’s assume now that we have reached position $k$ in $D$, having so far produced the set of paths $\mathcal{P}_{k}^{0}$; in case we are at the very beginning of $D$ such that $k=0$ we assume $\mathcal{P}_{0}^{0}=\{\varepsilon\}$. We will have been careful to only produce $p\in\mathcal{P}_{k}^{0}$ such that $[p]\in\mathcal{L}_{\text{prefix}}$. Now, which token should we produce next? For sure, the token to produce next must be a member of the set

[TABLE]

because according to Lex these are the only tokens which start at position $k$ in $D$. Furthermore, we are only interested in the subset $\mathcal{W}_{k}^{0}$ of those members of $\mathcal{X}_{k}$ which can continue a sequence in $\mathcal{P}_{k}^{0}$ to a sequence of terminals in $\mathcal{L}_{\text{prefix}}$:

[TABLE]

The selector decides whether and how to constrain any remaining ambiguity in the token selection: The set

[TABLE]

contains those tokens we use to create the next set of paths $\mathcal{P}_{k}^{1}$.

If $\mathcal{Z}_{k}^{1}$ does not contain any empty tokens, then $\mathcal{P}_{k}^{1}$ is just

[TABLE]

where

[TABLE]

and because we only added paths $q$ with $|\overline{q}|>k$ we can simply proceed to position $k+1$ via $\mathcal{P}_{k+1}^{0}=\mathcal{P}_{k}^{1}$.

But if $\mathcal{Z}_{k}^{1}$ does indeed contain empty tokens, then there might be newly added paths $q$ with $|\overline{q}|=k$, and we might be able to extend these paths even further. Therefore we define $\mathcal{P}_{k}^{1}$ more generally as

[TABLE]

where

[TABLE]

The fact that now $\mathcal{P}_{k}^{1}\setminus\mathcal{P}_{k}^{0}$ may contain paths $q$ with $|\overline{q}|=k$ means that potentially more tokens in $\mathcal{X}_{k}$ become eligible to extends paths which stop at position $k$. We therefore keep repeating the above procedure (potentially infinitely often) until we are sure to have produced all eligible tokens at position $k$ by forming monotone chains

[TABLE]

where for $u\in\{0,1,2,\ldots\}$ we recursively define

[TABLE]

We finalize the generation of token sequences at position $k$ by defining

[TABLE]

and move on to position $k+1$ via $\mathcal{P}_{k+1}^{0}=\mathcal{P}_{k}^{\infty}$. To complete the given set of recursive equations, we define $\mathcal{Z}_{k}^{0}=\emptyset$ for all positions $k$.

Once we have arrived at the end of the character sequence $D$, we finish the conversion of $D$ into the set $\ell\ell(D)$ of token sequences via defining $\mathfrak{P}=\mathcal{P}_{|D|}^{\infty}$ and

[TABLE]

Note that the local lexing semantics does not depend on the particular form of the grammar, but only on $\mathcal{L}$ and $\mathcal{L}_{\text{prefix}}$. If the grammar contains no unproductive nonterminals, i.e. if for all $X\in\mathfrak{N}$ there is $w\in\Sigma^{*}$ such that $X\overset{*\ }{\Rightarrow}w$, then $\mathcal{L}_{\text{prefix}}$ is uniquely determined by $\mathcal{L}$ and thus in this case the local lexing semantics only depends on $\mathcal{L}$ alone.

Let us also comment on why the selector takes two arguments. It is tempting (and indeed this was the first thing we tried) to let the selector act only on a single argument, as in $\mathcal{Z}_{k}^{u+1}=\textsl{Sel}\ \mathcal{W}_{k}^{u+1}$, but this destroys the property that the $\mathcal{Z}_{k}^{u}$ form a monotone chain, which turned out to be important for the correctness of our algorithm for local lexing (see Section 5).

3 Applications of Local Lexing

In this section we explore local lexing and its applications through a range of examples.

Example 3.1** (Traditional Lexical Specifications).**

Turning a traditional lexical specification into the definition of a local lexing is straightforward. Let the traditional specification be defined over an input alphabet $\Sigma$ and given by $n$ pairs

[TABLE]

The $r_{i}$ are regular expressions over $\Sigma$, none of which match $\varepsilon\in\Sigma^{*}$, and the set of terminals $\mathfrak{T}$ consists of $n$ different terminals $t_{1},\ldots,t_{n}$. For each $t_{i}\in\mathfrak{T}$ we then define

[TABLE]

where $c$ is the longest prefix of $D_{k}\ldots D_{|D|-1}$ such that $r_{i}$ matches $c$. If $r_{i}$ matches no prefix of $D_{k}\ldots D_{|D|-1}$ then we define $\textsl{Lex}(t_{i})(D,k)=\emptyset$.

We define a strict partial order $<_{\textsl{Sel}}$ on the set of tokens which encodes the longest-match and priority rules:

[TABLE]

This implies that $\textsl{Sel}(\emptyset,X)$ will be either empty or a singleton because $<_{\textsl{Sel}}$ is total on all possible $X$.

To endow the local lexing $\ell\ell=(\textsl{Lex},\textsl{Sel})$ with the equivalent semantics to traditional lexing, we define the context-free grammar $G=(\{\textsl{S},\textsl{T}\},\mathfrak{T},\mathfrak{R},\textsl{S})$ where

[TABLE]

Because of $\mathcal{L}_{\text{prefix}}=\mathcal{L}=\mathfrak{T}^{*}$ this grammar poses no additional constraints on the local lexing process, and therefore $\ell\ell(D)=\emptyset$ iff traditional lexing of $D$ would lead to an error, and $\ell\ell(D)=\{p\}$ iff traditional lexing of $D$ would yield the token sequence $p$.

Example 3.2** (Infinite Set of Token Sequences).**

We change the previous example slightly and allow the $r_{i}$ to also match the empty character sequence $\varepsilon$. As a concrete example consider $\Sigma=\{\texttt{a}\}$, $n=1$ and let $r_{1}$ be a regular expression which matches any (possibly empty) sequence of a’s. Then using the same grammar $G$ as in the previous example, we obtain for example

[TABLE]

which is an infinite set.

Because local lexing intertwines lexing and parsing, determining for a character sequence $D\in\Sigma^{*}$ all possible token sequences $\ell\ell(D)$ involves finding valid parses of $[p]$ for all $p\in\ell\ell(D)$. The following examples demonstrate this interplay between lexing and parsing and the role of the selector Sel in it.

Example 3.3**.**

Consider the grammar $H=(\mathfrak{N},\mathfrak{T},\mathfrak{R},\mathfrak{S})$ where $\mathfrak{N}=\{\textsl{S},\ \textsl{A},\ \textsl{E}\}$, $\mathfrak{T}=\{\textsl{plus},\ \textsl{minus},\ \textsl{id},\ \textsl{symbol}\}$, $\mathfrak{R}=\{\textsl{S}\rightarrow\textsl{S}\ \textsl{plus}\ \textsl{A},\ \textsl{S}\rightarrow\textsl{S}\ \textsl{minus}\ \textsl{A},\ \textsl{S}\rightarrow\textsl{A},\ \textsl{A}\rightarrow\textsl{A}\ \textsl{E},\ \textsl{A}\rightarrow\textsl{E},\ \textsl{E}\rightarrow\textsl{id},\ \textsl{E}\rightarrow\textsl{symbol}\}$, $\mathfrak{S}=\textsl{S}$. The input characters are $\Sigma=\{\texttt{+},\texttt{-},\texttt{a},\texttt{b},\texttt{c}\}$. As previously, we specify Lex simply by associating the terminals with regular expressions: The terminal plus recognizes the character +, minus recognizes the character -, id recognizes any nonempty sequence of letters and symbol recognizes any nonempty sequence of letters and hyphens -. Let $D$ denote the character sequence a-b+c.

We choose the simplest option for $<_{\textsl{Sel}}$ and define

[TABLE]

i.e. no token has a higher priority than another token. This implies $\textsl{Sel}(A,B)=B$ for all token sets $A\subseteq B$. The result of determining $\ell\ell(D)$ is shown in Figure 1. Because symbol overlaps with both identifier and minus, $D$ can be interpreted in eight different ways as a token sequence. Because of the longest-match rule for regular expressions,

[TABLE]

excluded together with several other token sequences which would otherwise qualify.

For all $p\in\ell\ell(D)$ the terminal sequence $[p]$ yields a valid parse tree, i.e. there are 8 different ways to parse $D$ although $H$ by itself is an unambiguous grammar; all of them are jointly depicted in the parse graph in Figure 2. Ambiguities are depicted as dashed lines in the graph: whenever there are multiple ways to proceed with the derivation of a nonterminal, each alternative is connected with the nonterminal by a dashed line.

Example 3.4**.**

We use the same grammer $H$ and the same lexer Lex as in Example 3.3, but choose a selector Sel such that symbol has lower priority than id and minus:

[TABLE]

This results in a unique lexing of a-b+c,

[TABLE]

and thus also in a unique parsing as shown in Figure 3.

Example 3.5**.**

We again leave $H$ and Lex fixed. This time we define $<_{\textsl{Sel}}$ such that longer tokens have higher priority:

[TABLE]

This yields two possible lexings for a-b+c,

[TABLE]

and leads to the ambiguous parsing shown on the left hand side of Figure 4.

Example 3.6**.**

We choose to modify the previous example such that its remaining ambiguity is resolved in favour of id by defining $x<_{\textsl{Sel}}y$ iff

[TABLE]

This leads to a unique lexing for a-b+c,

[TABLE]

and yields the unique parsing depicted on the right hand side of Figure 4.

Example 3.7** (The Lexer Hack).**

Consider the expression (a)*b given in the programming language C. The meaning of this expression depends on whether a is a type identifier or a variable identifier. If it is a type identifier, then the expression is to be interpreted as a type cast, otherwise as a multiplication. Because type identifiers cannot be distinguished from variable identifiers by their look, in traditional parsing a problem arises, because the lexer phase is supposed to happen before the parsing phase and any semantic analysis, but the terminal type of a really depends on information from the semantic analysis. The traditional solution, to manually direct feedback from the semantic analysis back into the lexer, is known as the lexer hack lexerhack . With local lexing, the lexer / parser can offer both alternatives, and let later stages of the analysis pick the right one, thus decoupling parsing and semantic analysis. The grammar $C$ demonstrates this, where $\mathfrak{T}=\{\textsl{typeid},\textsl{id},\textsl{asterisk},\textsl{left},\textsl{right}\}$ and

[TABLE]

The lexer Lex is chosen in the obvious way, together with an empty $<_{\textsl{Sel}}$. The resulting ambiguous parse graph for (a)*b is shown in Figure 5, and

[TABLE]

Schrödinger’s Token

Example 3.7 is a special case of a scenario where the conversion from character sequences to token sequences is ambiguous, but where the token boundaries are always the same in all alternative token sequences. The tokens appearing in such a scenario have been christened Schrödinger’s tokens schroedingerstoken . Local lexing is more powerful than the Schrödinger’s token approach and (at least conceptually) subsumes it.

Ruby Slippers

The Marpa parser marpa is an Earley-based parsing library which advocates the use of a technique called Ruby Slippers rubyslippers . This technique takes advantage of the fact that the Earley parser ”knows” which tokens it expects at any given stage of the parse progress. Marpa has an interface through which the parser can communicate with the scanner to negotiate which token to scan next, thus allowing for sophisticated error handling.

Ruby Slippers and local lexing are both children of the same insight, namely that the scanning and parsing stages should communicate because the parser has information about which tokens it expects next. Local lexing though takes this insight to a new level which in principle is independent from a particular parsing algorithm like Earley. In this sense, local lexing can be seen as providing a rigorous semantics for certain uses of the Ruby Slippers technique.

The next example demonstrates how local lexing can be used to specify lightweight error recovery as part of the language design.

Example 3.8** (Error Recovery).**

Consider a grammar for simple arithmetic expressions, where the nonterminals are given by $\{\textsl{Expr},\ \textsl{Sum},\ \textsl{Mul},\ \textsl{Atom}\}$, the terminals by $\{\textsl{plus},\ \textsl{mul},\ \textsl{id},\ \textsl{num},\ \textsl{left},\ \textsl{right}\}$, and the rules by

[TABLE]

The input characters are $\Sigma=\{\texttt{+},\texttt{*},\texttt{(},\texttt{)},\texttt{0}\dots\texttt{9},\texttt{a}\dots\texttt{z}\}$, and Lex is specified such that plus recognizes the character +, mul recognizes the character *, left recognizes the opening bracket (, right recognizes the closing bracket ), id recognizes any nonempty sequence of letters and digits starting with a letter, and num recognizes any nonempty sequence of digits. Consider now the following string $w$ which is invalid with respect to the language we just specified:

[TABLE]

Instead of simply diagnosing that there is some parse error at position $k=1$, we would like to recover some of the structure of $w$, for example for providing better error messages or for a rich interactive editing experience. To simplify this task, we first make our grammar more permissive by adding the rule $\textsl{Mul}\ \rightarrow\ \textsl{Mul}\ \textsl{Atom}$. This has the effect that a string like 2x becomes legal, representing the multiplication of 2 and x. Such notation is common mathematical practice and thus seems like a justifiable design choice. We then introduce three new terminals: e-atom and e-right both recognize the empty string $\varepsilon$ only, and e-superfluous recognizes the closing bracket ). We incorporate these new terminals into the grammar by adding the following rules:

[TABLE]

Finally, we choose the selector Sel such that the three added error terminals have lower priority than all other terminals. Paths in $\ell\ell(D)$ that contain error terminals will only be considered by us if $\ell\ell(D)$ contains no paths without error terminals. Figure 6 shows the result of applying the updated grammar to $w$. The corresponding path is

[TABLE]

Testing convinces us that the updated grammar can indeed successfully parse all $D\in\Sigma^{*}$, and does so unambiguously.

Whitespace

In our examples we have avoided to make use of whitespace. In traditional parsing there are essentially two different ways of dealing with whitespace:

One approach is to explicitly incorporate whitespace terminals into the grammar rules. This can become cumbersome and error-prone if done manually, because usually whitespace can legally appear almost everywhere. 2. 2.

The other approach is to handle whitespace at the lexical stage exclusively.

The first approach applies to local lexing as well. The second approach does not directly apply, as there is no single lexical stage anymore with local lexing. Nevertheless, it seems that local lexing allows to combine the convenience of the second approach with the fine-grained control of the first one by using extended attribute grammars to specify layout constraints, making it possible to tackle layout-sensitive languages. The combination of local lexing with layout-sensitivity is work in progress and beyond the scope of this paper.

4 Implementing Local Lexing

Given a grammar $G$ and a local lexing $\ell\ell$, let us define the character language $\mathcal{L}_{\Sigma}$ of $G$ and $\ell\ell$ by

[TABLE]

How do we build a recognizer for $\mathcal{L}_{\Sigma}$?

Lexing Driving Parsing

Our first attempt might be to directly apply the semantics of local lexing after having picked a parsing algorithm which is capable of recognizing both the prefixes $\mathcal{L}_{\text{prefix}}$ and the language $\mathcal{L}$ of $G$. Most of the popular parsing algorithms would be suitable for this, such as LL, LR or Earley parsing.

While this approach will work in many cases, it is inefficient to treat the parsing algorithm as a black box which is repeatedly asked whether a given sequence of terminals is in $\mathcal{L}_{\text{prefix}}$ or not. More importantly, as Example 3.2 shows there are finite grammars which nevertheless produce infinite sets of token sequences and for which this approach would therefore fail by getting stuck in a non-terminating path generating loop.

Parsing Driving Lexing

A better approach seems to be to inverse above approach and to let the parsing progress drive the lexing process. Often it will be possible to predict from the internal parser state which terminal is expected next. For this to work, we need to modify the parsing algorithm so that it not only knows about terminals $\mathfrak{T}$, but also about characters $\Sigma$. The Earley algorithm seems to be best suited to be adapted to such a purpose, as it works on all context-free grammars, copes gracefully with ambiguity, and is easily extended with top-down, left-right, and bottom-up parametricity. This is why Earley-based parsing is our main focus here. Nevertheless, studying how to modify other parsing algorithms for local lexing is interesting and of potentially great practical interest as well; experiments indicate that in particular the LR(1) parsing algorithm can be modified to facilitate local lexing in a natural and simple way.

Earley’s Algorithm

We first describe (a high-level version of) Earley’s original algorithm, assuming $\Sigma=\mathfrak{T}$. To recognize an input $D\in\Sigma^{*}$ as belonging to $\mathcal{L}$, it computes items; an item is a quadruple $(r,d,i,j)$ where $r=(N\rightarrow\alpha\beta)\in\mathfrak{R}$ is a rule of the grammar, $d=|\alpha|$ is a position within that rule demarking the current parsing progress, $i\in\{0,\ldots,|D|\}$ is the origin of the item, and $j\in\{i,\ldots,|D|\}$ is the bin of the item. An alternative way to write the item is as

[TABLE]

Earley’s algorithm builds a monotone chain of item sets

[TABLE]

To this end, we define an initial item set $\operatorname{Init}$ and monotone operators $\operatorname{Predict}$, $\operatorname{Complete}$ and $\operatorname{Scan}$ which all take a position $k\in\{0,\ldots,|D|\}$ and an item set $I$ and return an augmented item set (Figure 7).

We then define for $k\in\{0,\ldots,|D|\}$ the operator $\pi_{k}$ by

[TABLE]

reusing the $\operatorname{limit}$ operator introduced in Section 2, and use $\pi_{k}$ to recursively define the sets $\mathcal{I}_{k}$ by

[TABLE]

Theorem 4.1** (Correctness of Earley’s Algorithm).**

Earley’s algorithm is both sound and complete, i.e.

[TABLE]

Proof.

This is covered by Theorem 4.2 for the special case

[TABLE]

∎

Earley’s Algorithm with Local Lexing

We now assume that we have a local lexing $\ell\ell$ and thus $\Sigma$ and $\mathfrak{T}$ do not necessarily coincide anymore. We leave $\operatorname{Init}$, $\operatorname{Predict}$ and $\operatorname{Complete}$ unchanged, but we need an updated $\operatorname{Scan}$ operator that works on tokens instead of characters, and a new operator $\operatorname{Tokens}$ (Figure 8).

The operation $\operatorname{Tokens}T\ k\ I$ first determines all the candidate terminals that could possibly appear next at position $k$ in $D$ according to $I$. It then determines which of those candidate terminals can actually be lexed as tokens at that position. It applies the selector Sel to it and returns the resulting set of tokens. Finally, the $\operatorname{Scan}$ operator is easily adapted to work on tokens instead of single characters. We iteratively compute the sets $\mathcal{T}_{k}^{0}$, $\mathcal{T}_{k}^{1}$, $\ldots$ of tokens at position $k$, and these act as arguments $T$ to both $\operatorname{Tokens}$ and $\operatorname{Scan}$. Accordingly, we need to update the definition of $\pi_{k}$ to take the additional argument $T$ into account:

[TABLE]

Furthermore, it is now possible that scanning at position $k$ might add new items to bin $k$ due to the existence of empty tokens, therefore enlarging the set of eligible terminals at position $k$. To cope with this we keep applying the operator $\pi_{k}$ with updated token sets until it converges:

[TABLE]

Note that in case of $\mathcal{J}_{k}^{u+1}=\mathcal{J}_{k}^{u}$ we have $\mathcal{I}_{k}=\mathcal{J}_{k}^{u}$, thus the computation of $\mathcal{I}_{k}$ can stop at that point. In particular, if $\mathcal{T}_{k}^{1}$ does not contain any empty tokens, then the computation of $\mathcal{I}_{k}$ simplifies to $\mathcal{I}_{k}=\mathcal{J}_{k}^{1}$.

Above equations for computing $\mathfrak{I}=\mathcal{I}_{|D|}$ show an obvious correspondence to the equations we used for defining $\mathfrak{P}$ in Section 2. And indeed, Earley’s algorithm with local lexing is correct with respect to the local lexing semantics:

Theorem 4.2** (Correctness of Earley’s Algorithm with Local Lexing).**

Earley’s algorithm with local lexing is both sound and complete, i.e.

[TABLE]

Proof.

See Section 5.∎

The above correctness result comes with a caveat: It may be the case that the computation requires an infinite amount of time and space. If the grammar is finite though, then for an input $D\in\Sigma^{*}$ the size of $\mathfrak{I}$ is bounded by

[TABLE]

and thus the computation will require only a finite amount of time and space (assuming Sel and Lex require only a finite amount in the first place).

Practical Implementation

We have developed a practical library for local lexing written in Scala/Scala.js which can be used to try out the examples in Section 3 locallexingprototype . It is a fairly naive proof-of-concept implementation and not optimized for data structures at all. For future versions of the library we plan to examine which of the many established ideas for making Earley parsing faster also apply (at least partially) to our case.

5 Proof of Theorem 4.2

In this section we give a short outline of the proof of Theorem 4.2. The full formal proof is available as Isabelle/HOL 2016 theory files and has been fully machine-checked for correctness locallexingtheories . To convince yourself that the formal proof really proves Theorem 4.2 we recommend first studying theories CFG, LocalLexing and LLEarleyParsing. These contain the basic definitions in (almost) the same notation as presented in this paper. You should then proceed to look at theory MainTheorems. It contains the theorem Correctness which is the machine-checked counterpart of Theorem 4.2.

Proof Outline

There is an intuitive correspondence between the sets $\mathcal{P}_{k}^{u}$ and the sets $\mathcal{J}_{k}^{u}$. Clarifying this correspondence is the most important step towards proving the correctness of the algorithm.

Definition 5.1** (Valid and Generated Items).**

We call an item

[TABLE]

$p$-valid for some token sequence $p\in\mathfrak{P}$ iff there is $u\in\{0,\ldots,|p|\}$ such that

[TABLE]

For $P\subseteq\mathfrak{P}$ we say that $P$ generates $\langle{P}\rangle$, where

[TABLE]

This notion of validity has been inspired by the one introduced in jones-earley where it has been defined as an absolute property of an item. To make it work in our context, we had to define it not absolutely, but relatively with respect to a path.

The bulk of the proof consists then in proving $\mathfrak{I}=\langle{\mathfrak{P}}\rangle$. We will not delve into the rather technical proof of this here, but we want to point out the following supporting theorem about paths:

Theorem 5.1**.**

For all inputs $D$, for all $k\in\{0,\ldots,|D|\}$ and for all $u\in\{0,1,2,\ldots\}$ the following holds: Given $p,q\in\mathcal{P}_{k}^{u}$ such that $|\overline{p}|=|\overline{q_{0}\ldots q_{n-1}}|\leq k$ for some $n\in\{0,\ldots,|q|\}$ and $[p\,q_{n}\ldots q_{|q|-1}]\in\mathcal{L}_{\text{prefix}}$, it follows that $p\,q_{n}\ldots q_{|q|-1}\in\mathcal{P}_{k}^{u}$.

Intuitively this means that when there are two paths $p\in\mathfrak{P}$ and $q\in\mathfrak{P}$ which meet at some position $k$, i.e. $p=ab$ and $q=cd$ with $|\overline{a}|=|\overline{c}|=k$, then they can crossover, i.e. both $ad$ and $cb$ will be in $\mathfrak{P}$ as long as this makes sense with respect to the grammar. But $p$ and $q$ are not guaranteed to arrive at the same time $u$ at position $k$, and so it might be that tokens that were around when $p$ arrived are not there anymore when $q$ arrives, and vice versa. The fact that the token sets $\mathcal{Z}_{k}^{u}$ form a monotone chain at position $k$ means that this cannot happen.

The semantics of local lexing is defined by mutually recursive equations which intertwine lexing and parsing, but once all token sets $\mathcal{Z}_{k}^{\infty}=\bigcup_{u=0}^{\infty}\mathcal{Z}_{k}^{u}$ have been established it is possible to disentangle lexical and grammatical matters again as another supporting theorem about paths shows:

Theorem 5.2**.**

Let $p$ be a sequence of tokens. Then $p\in\mathfrak{P}$ iff

[TABLE]

From $\mathfrak{I}=\langle{\mathfrak{P}}\rangle$ and with the help of Theorem 5.2 it is then straightforward to prove Theorem 4.2:

Proof.

Let us first assume $D\in\mathcal{L}_{\Sigma}$. This implies $\ell\ell(D)\neq\emptyset$, which implies that there is a $p\in\mathfrak{P}$ with $|\overline{p}|=|D|$ and $\mathfrak{S}\overset{*\ }{\Rightarrow}[p]$. This means there is an $\alpha$ such that $\mathfrak{S}\rightarrow\alpha$ and $\alpha\overset{*\ }{\Rightarrow}[p]$. Therefore, $(\mathfrak{S}\rightarrow\alpha\makebox[7.0pt]{\textbullet},0,|D|)$ is $p$-valid and thus

[TABLE]

On the other hand, let us assume that there is an $\alpha$ with above property. This means that $(\mathfrak{S}\rightarrow\alpha\makebox[7.0pt]{\textbullet},0,|D|)$ is $p$-valid for some $p\in\mathfrak{P}$, i.e. there is $u\in\{0,\ldots,|p|\}$ with

[TABLE]

Above facts together with Theorem 5.2 show that by dropping the first $u$ empty tokens from $p$ we obtain a path

[TABLE]

∎

6 Further Related Work

A strong influence on our work has been the idea of blackbox Earley parsing presented in blackbox . A blackbox is a (possibly third-party) parser component plugged into the Earley parsing framework by associating the blackbox with a nonterminal. Our Lex component can basically be viewed as a collection of blackboxes, but instead of associating them with nonterminals, we associate them with terminals. This makes it possible to treat blackboxes as a concept that is in principle independent from Earley parsing. Unlike the original work on blackboxes we also provide a method for disambiguation, via the selector Sel.

7 Conclusion

With hindsight local lexing is a simple concept, but it has taken us over two years to arrive at the concept as it is presented in this paper. Our algorithm for local lexing and the semantics of local lexing developed side-by-side during this time. There have been enough missteps along the way to finally make us formally verify our algorithm. Despite its simplicity, the examples from Section 3 show that local lexing is a versatile and unifying concept for designing syntax. We hope that you may find it useful, too.