Parameterized Local Lexing

TL;DR

This paper introduces parameterized local lexing, an extension of local lexing, aiming to improve parsing techniques by incorporating parameters into the lexing process.

Contribution

It presents the novel concept of parameterized local lexing, expanding the capabilities of local lexing for more flexible language processing.

Findings

Demonstrates how parameterized local lexing enhances parsing accuracy.

Shows improved flexibility in language syntax handling.

Provides theoretical foundations for the new approach.

Abstract

Building on the concept of local lexing the concept of parameterized local lexing is introduced.

Equations

$$(\Phi ,\mathfrak{N},\mathfrak{T},\mathfrak{R},\mathfrak{S},{\varphi }_{\text{textsl}start},\Sigma ,\text{textsl}Lex,\text{textsl}Sel)$$

$$\text{textsl}{N}_{f_{k+1}}\to \text{textsl}{X}_1^{f_1}\dots \text{textsl}{X}_k^{f_k}$$

$$\begin{array}[]{ccl}\overline{\mathfrak{N}}&=&(\mathfrak{N}\times\Phi\times\Phi)\cup\{\top,\bot\}\\ \overline{\mathfrak{T}}&=&\mathfrak{T}\times\Phi\times\Phi\end{array}$$

$$\left\{\top \to {\mathfrak{S}}_{\beta }^{{\varphi }_{\text{textsl}start}}\mid \beta \in \Phi \right\}$$

$$\begin{array}[]{l}\phantom{\wedge\ }\text{$f_{1}$ is defined at $\rho_{0}$}\\ \wedge\ \rho_{1}=f_{1}(\rho_{0})\\ \wedge\ \text{$f_{2}$ is defined at $(\rho_{0},\rho_{1},\rho_{2})$}\\ \wedge\ \rho_{3}=f_{2}(\rho_{0},\rho_{1},\rho_{2})\\ \wedge\ \text{$f_{3}$ is defined at $(\rho_{0},\rho_{1},\rho_{2},\rho_{3},\rho_{4})$}\\ \wedge\ \rho_{5}=f_{3}(\rho_{0},\rho_{1},\rho_{2},\rho_{3},\rho_{4})\\ \vdots\\ \wedge\ \text{$f_{u}$ is defined at $(\rho_{0},\rho_{1},\ldots,\rho_{2u-2})$}\\ \wedge\ \rho_{2u-1}=f_{u}(\rho_{0},\rho_{1},\ldots,\rho_{2u-2})\end{array}$$

$$\text{textsl}{N}_{\beta }^{\alpha }\to {\text{textsl}{X}_1}_{{\beta }_1}^{{\alpha }_1}\dots {\text{textsl}{X}_k}_{{\beta }_k}^{{\alpha }_k}$$

$$\text{textsl}{N}_{\beta }^{\alpha }\to {\text{textsl}{X}_1}_{{\beta }_1}^{{\alpha }_1}\dots {\text{textsl}{X}_h}_{{\beta }_h}^{{\alpha }_h}\perp$$

$$\begin{array}[]{l}h\in\{1,\ldots,k\}\wedge\beta\in\Phi\wedge\beta_{h}\in\Phi\\ \wedge\ \alpha\,\alpha_{1}\,\beta_{1}\ldots\alpha_{h}\in\langle{f_{1},\ldots,f_{h}}\rangle\\ \wedge\ \text{$f_{h+1}$ is undefined at $(\alpha,\alpha_{1},\beta_{1},\ldots,\alpha_{h},\beta_{h})$}\end{array}$$

$$\overline{\mathfrak{R}}=\left\{\top \to {\mathfrak{S}}_{\beta }^{{\varphi }_{\text{textsl}start}}\mid \beta \in \Phi \right\}\cup \bigcup _{r\in \mathfrak{R}}\overline{r}$$

$$\overline{\text{textsl}Lex}(t_{\beta }^{\alpha })(D,k)=\left\{(t_{\beta }^{\alpha },c)\mid (t,\alpha ,\beta ,c)\in \text{textsl}Lex(t,\alpha ,D,k)\right\}$$

$$\overline{\text{textsl}Sel}(A,B)=\mathcal{U}(\text{textsl}Sel({\mathcal{U}}^{-1}(A),{\mathcal{U}}^{-1}(B)))$$

$$\sigma (D)=\left\{\beta \mid \exists p.p\in \ell \ell (D)\text{ and }\top \Rightarrow {\mathfrak{S}}_{\beta }^{{\varphi }_{\text{textsl}start}}\stackrel{\ast }{\Rightarrow }[p]\right\}.$$

$${\mathrm{take}}_{2(d+1)}(\alpha ,{\alpha }_1,{\beta }_1,{\alpha }_2,{\beta }_2,\dots ,{\alpha }_k,{\beta }_k,\beta )=\rho .$$

$${\mathrm{take}}_{2(d+1)}(\alpha ,{\alpha }_1,{\beta }_1,{\alpha }_2,{\beta }_2,\dots ,{\alpha }_h)=\rho .$$

$$\overline{I}=\bigcup _{w\in I}\overline{w}$$

$$\mathrm{Init}=$$

$$\{({\mathfrak{S}}_{f_{u+1}}\to \text{makebox}[7.0pt]\text{textbullet}\text{textsl}{X}_1^{f_1}\dots \text{textsl}{X}_u^{f_u},0,0,{\varphi }_{\text{textsl}start}{f}_1({\varphi }_{\text{textsl}start}))\mid$$

$$({\mathfrak{S}}_{f_{u+1}}\to \text{textsl}{X}_1^{f_1}\dots \text{textsl}{X}_u^{f_u})\in \mathfrak{R}$$

$$\wedge \text{f1 is defined at ϕtextslstart}\}$$

$$\mathrm{Predict}kI=I\cup$$

$$\{(\text{textsl}{M}_{g_{u+1}}\to \text{makebox}[7.0pt]\text{textbullet}\text{textsl}{Y}_1^{g_1}\dots \text{textsl}{Y}_u^{g_u},k,k,{\rho }_{2d+1}{g}_1({\rho }_{2d+1}))\mid$$

$$(\text{textsl}{M}_{g_{u+1}}\to \text{textsl}{Y}_1^{g_1}\dots \text{textsl}{Y}_u^{g_u})\in \mathfrak{R}$$

$$\wedge \text{g1 is defined at ρ2d+1}$$

$$\wedge (N_{f_{v+1}}\to \text{textsl}{X}_1^{f_1}\dots \text{textsl}{X}_d^{f_d}\text{makebox}[7.0pt]\text{textbullet}\text{textsl}{X}_{d+1}^{f_{d+1}}\dots \text{textsl}{X}_v^{f_v},i,k,\rho )\in I$$

$$\wedge \text{textsl}{X}_{d+1}=\text{textsl}M\}$$

$$\mathrm{Complete}kI=I\cup$$

$$\{(N_{f_{v+1}}\to \text{textsl}{X}_1^{f_1}\dots \text{textsl}{X}_d^{f_d}\text{textsl}{X}_{d+1}^{f_{d+1}}\text{makebox}[7.0pt]\text{textbullet}\dots \text{textsl}{X}_v^{f_v},i,k,{\rho }^{\prime }{f}_{d+2}({\rho }^{\prime }))\mid$$

$$(N_{f_{v+1}}\to \text{textsl}{X}_1^{f_1}\dots \text{textsl}{X}_d^{f_d}\text{makebox}[7.0pt]\text{textbullet}\text{textsl}{X}_{d+1}^{f_{d+1}}\dots \text{textsl}{X}_v^{f_v},i,j,\rho )\in I$$

$$\wedge (\text{textsl}{M}_{g_{u+1}}\to \text{textsl}{Y}_1^{g_1}\dots \text{textsl}{Y}_u^{g_u}\text{makebox}[7.0pt]\text{textbullet},j,k,\xi )\in I$$

$$\wedge \text{textsl}{X}_{d+1}=M\wedge {\rho }_{2d+1}={\xi }_0\wedge {\rho }^{\prime }=\rho {\xi }_{2u+1}$$

$$\wedge \text{fd+2 is defined at ρ′}\}$$

$$\displaystyle\operatorname{Tokens}\ T\ k\ I=\textsl{Sel}\ T\$$

$$\{x\mid (N_{f_{v+1}}\to \text{textsl}{X}_1^{f_1}\dots \text{textsl}{X}_d^{f_d}\text{makebox}[7.0pt]\text{textbullet}\text{textsl}{X}_{d+1}^{f_{d+1}}\dots \text{textsl}{X}_v^{f_v},i,k,\rho )\in I$$

$$\wedge \text{textsl}{X}_{d+1}\in \mathfrak{T}\wedge x\in \text{textsl}Lex(\text{textsl}{X}_{d+1},{\rho }_{2d+1},D,k)\}$$

$$\mathrm{Scan}TkI=I\cup$$

$$\{(\text{textsl}{N}_{f_{v+1}}\to \text{textsl}{X}_1^{f_1}\dots \text{textsl}{X}_d^{f_d}\text{textsl}{X}_{d+1}^{f_{d+1}}\text{makebox}[7.0pt]\text{textbullet}\dots \text{textsl}{X}_v^{f_v},i,k+|c|,{\rho }^{\prime }{f}_{d+2}({\rho }^{\prime }))\mid$$

$$(\text{textsl}{N}_{f_{v+1}}\to \text{textsl}{X}_1^{f_1}\dots \text{textsl}{X}_d^{f_d}\text{makebox}[7.0pt]\text{textbullet}\text{textsl}{X}_{d+1}^{f_{d+1}}\dots \text{textsl}{X}_v^{f_v},i,k,\rho )\in I$$

$$\wedge (\text{textsl}{X}_{d+1},{\rho }_{2d+1},\beta ,c)\in T\wedge {\rho }^{\prime }=\rho \beta$$

$$\wedge \text{fd+2 is defined at ρ′}\}$$

$$\mathrm{limit}fX$$

$${\pi }_{k}TI$$

$${\mathcal{J}}_0^0$$

$${\mathcal{J}}_k^{u+1}$$

Full text

1 Motivation

We previously introduced local lexing as a new semantics for integrated lexing and parsing, and provided an algorithm (based on Earley’s Algorithm) for it locallexing . This algorithm can handle arbitrary context-free grammars. In principle it can even deal with infinite grammars, but to harness this capability in practice we need a finite representation of such possibly infinite grammars. Parameterized local lexing delivers such a finite representation, and comes with an algorithm tuned to that representation. Of course the finite representation as presented in this paper is not the only possible one, but it is simple and intuitive and yet powerful.

2 Definition

We call a tuple

[TABLE]

a parameterized local lexing iff:

• •

$\Phi$ is a non-empty set of parameters.

• •

$\mathfrak{N}$ and $\mathfrak{T}$ are disjoint sets of nonterminals and terminals.

• •

$\mathfrak{S}\in\mathfrak{N}$ and $\phi_{\textsl{start}}\in\Phi$ are the start symbol and start parameter, respectively.

• •

$\mathfrak{R}$ is a set of parameterized rules. Each rule has the form

[TABLE]

where $\textsl{N},\textsl{X}_{1},\ldots,\textsl{X}_{k}\in\mathfrak{N}$, and $f_{1},\ldots,f_{k},f_{k+1}$ are partial functions with the signatures f_{i}:\Phi^{2i-1}\mathrel{\ooalign{\hfil\mapstochar\mkern 5.0mu$\hfil\cr$\to\cr}}\Phi for $i\in\{1,\ldots,k+1\}$.

• •

$\Sigma$ is a set of characters.

• •

Lex is a function which for each $(t,\alpha,D,k)$ such that $t\in\mathfrak{T}$, $\alpha\in\Phi$, $D\in\Sigma^{*}$ and $k\in\{0,\ldots,|D|\}$ returns a set consisting of tuples $(t,\alpha,\beta,c)$ such that $\beta\in\Phi$, $c\in\Sigma^{*}$, $k+|c|\leq|D|$ and $c_{i}=D_{k+i}$ for all $i$ such that $0\leq i\leq|c|-1$.

• •

Sel takes two sets $A,B\subseteq\mathfrak{T}\times\Phi\times\Phi\times\Sigma^{*}$ such that $A\subseteq B$ and returns a set $\textsl{Sel}(A,B)$ such that $A\subseteq\textsl{Sel}(A,B)\subseteq B$.

3 Semantics

The semantics of parameterized local lexing is provided by translating it to ordinary local lexing. The result is a context-free grammar $(\overline{\mathfrak{N}},\overline{\mathfrak{T}},\overline{\mathfrak{R}},\top)$ together with a lexer $\overline{\textsl{Lex}}$ and selector $\overline{\textsl{Sel}}$ operating on the same character set $\Sigma$ as the parameterized local lexing. The resulting nonterminals and terminals of the new grammar are defined as follows:

[TABLE]

For elements $(N,\alpha,\beta)\in\overline{\mathfrak{N}}$ and $(t,\alpha,\beta)\in\overline{\mathfrak{T}}$ we also write $N_{\beta}^{\alpha}$ and $t_{\beta}^{\alpha}$, respectively. Here $\alpha$ is called the input parameter, and $\beta$ is called the output parameter. The nonterminal $\bot$ represents failure and therefore does not appear on the left hand side of any rule in $\overline{\mathfrak{R}}$. The nonterminal $\top$ is the start symbol of the new grammar and appears only on the left hand side of the rules in the following subset of $\overline{\mathfrak{R}}$:

[TABLE]

Given $u\geq 1$ partial functions $f_{1},\ldots,f_{u}$ with signatures f_{i}:\Phi^{2i-1}\mathrel{\ooalign{\hfil\mapstochar\mkern 5.0mu$\hfil\cr$\to\cr}}\Phi for $i\in\{1,\ldots,u\}$, we define the set $\langle{f_{1},\ldots,f_{u}}\rangle$ to consist of all sequences $\rho\in\Phi^{2u}$ such that

[TABLE]

With each parameterized rule $r=\textsl{N}_{f_{k+1}}\rightarrow\textsl{X}_{1}^{f_{1}}\ldots\textsl{X}_{k}^{f_{k}}$ we associate its induced set of rules $\overline{r}\subseteq\overline{\mathfrak{R}}$. Firstly, $\overline{r}$ contains all rules

[TABLE]

such that $\alpha\,\alpha_{1}\,\beta_{1}\ldots\alpha_{k}\,\beta_{k}\,\beta\in\langle{f_{1},\ldots,f_{k+1}}\rangle$.

Secondly, we also need to somehow take into account those cases where some $f_{i}$ happens to be undefined on its arguments. While these cases do not affect the language $\mathcal{L}$ of the induced context-free grammar, they possibly do affect its prefix language $\mathcal{L}_{\text{prefix}}$. We choose to let $\overline{r}$ contain also all rules

[TABLE]

such that

[TABLE]

The induced set of rules $\overline{\mathfrak{R}}$ is thus defined as

[TABLE]

Defining the induced lexer is straightforward:

[TABLE]

There is an obvious bijection $\mathcal{U}:\mathfrak{T}\times\Phi\times\Phi\times\Sigma^{*}\rightarrow\overline{\mathfrak{T}}\times\Sigma^{*}$ between parameterized tokens and ordinary tokens, given by $\mathcal{U}(t,\alpha,\beta,c)=(t^{\alpha}_{\beta},c)$. Lifted to a bijection between token sets, we use it to define the induced selector:

[TABLE]

A character sequence $D\in\Sigma^{*}$ is said to be in the character language of the parameterized local lexing iff $\ell\ell(D)\neq\emptyset$ with respect to the induced local lexing. Furthermore, we can associate with each $D\in\Sigma^{*}$ the set of its outputs $\sigma({D})\subseteq\Phi$ via

[TABLE]

Obviously, $\ell\ell(D)=\emptyset$ iff $\sigma({D})=\emptyset$.

4 Algorithm

Given $\Phi$, $\mathfrak{N}$, $\mathfrak{T}$ and $\mathfrak{R}$ are all finite, parameterized local lexing can be implemented simply by reducing it via its semantics to ordinary local lexing, and then applying the Earley-based local lexing algorithm (ELLA). This is rather awkward though as the induced grammar is potentially much larger than the original grammar. In particular, $|\overline{\mathfrak{R}}|$ might be much larger than $|\mathfrak{R}|$. Furthermore, we would also like to have the option of doing parameterized local lexing for an infinite set of parameters $\Phi$ like the set of natural numbers, but usually this would lead to an infinite set of rules $\overline{\mathfrak{R}}$.

Luckily it is straightforward to derive from ELLA an algorithm for parameterized local lexing (PELLA) which avoids such a translation to ordinary local lexing but works directly on parameterized items. A parameterized item is a tuple $(r,d,i,j,\rho)$, such that $r=\textsl{N}_{f_{k+1}}\rightarrow\textsl{X}_{1}^{f_{1}}\ldots\textsl{X}_{k}^{f_{k}}\in\mathfrak{R}$, $0\leq d\leq k$ and $0\leq i\leq j\leq|D|$, where $D\in\Sigma^{*}$ is the input under consideration. The sequence $\rho\in\Phi^{2(d+1)}$ records the choices of parameters that have been made so far, and therefore we demand that the invariant $\rho\in\langle{f_{1},\ldots,f_{d+1}}\rangle$ holds for each parameterized item.

Before describing how PELLA operates on parameterized items, let us establish a correspondence between parameterized items and the items of the induced ordinary local lexing. Just how each parameterized rule corresponds to a set of ordinary rules, each parameterized item $x$ corresponds to a set of ELLA items $\overline{x}$. Firstly, for each rule $q=\textsl{N}_{\beta}^{\,\alpha}\rightarrow{\textsl{X}_{1}}_{\beta_{1}}^{\alpha_{1}}\ldots{\textsl{X}_{k}}_{\beta_{k}}^{\alpha_{k}}\in\overline{r}$ the set $\overline{x}$ contains all items $(q,d,i,j)$ such that

[TABLE]

Here $\operatorname{take}_{n}s$ denotes the sequence resulting from taking the first $n$ elements of the sequence $s$. Secondly, for each rule $q=\textsl{N}_{\beta}^{\,\alpha}\rightarrow{\textsl{X}_{1}}_{\beta_{1}}^{\alpha_{1}}\ldots{\textsl{X}_{h}}_{\beta_{h}}^{\alpha_{h}}\ \bot\in\overline{r}$ the set $\overline{x}$ contains all items $(q,d,i,j)$ such that $d\leq h-1$ and

[TABLE]

Theorem 4.1**.**

Let $x$ be a parameterized item. Then $\overline{x}\neq\emptyset$.

Proof.

Let $x=(r,d,i,j,\rho)$, and $r=\textsl{N}_{f_{k+1}}\rightarrow\textsl{X}_{1}^{f_{1}}\ldots\textsl{X}_{k}^{f_{k}}$. We know that $\rho\in\langle{f_{1},\ldots,f_{d+1}}\rangle$.

If there is $\rho^{\prime}\in\Phi^{2(k-d)}$ such that $\xi=\rho\rho^{\prime}\in\langle{f_{1},\ldots,f_{k+1}}\rangle$ then $\overline{x}$ is not empty as $(\textsl{N}^{\xi_{0}}_{\xi_{2k+1}}\rightarrow\textsl{X}^{\xi_{1}}_{\xi_{2}}\ldots\textsl{X}^{\xi_{2k-1}}_{\xi_{2k}},d,i,j)\in\overline{x}$. Otherwise there must be $h$ with $d+1\leq h<k$ and $\rho^{\prime}\in\Phi^{2(h-d-1)}$ such that $\xi=\rho\rho^{\prime}\in\langle{f_{1},\ldots,f_{h}}\rangle$, together with some $\gamma\in\Phi$ such that $f_{h+1}$ is undefined at $\xi\,\gamma$. This means that for any $\beta\in\Phi$, we have $(\textsl{N}^{\xi_{0}}_{\beta}\rightarrow\textsl{X}^{\xi_{1}}_{\xi_{2}}\ldots\textsl{X}^{\xi_{2h-1}}_{\gamma}\bot,d,i,j)\in\overline{x}$. ∎

Given an item set $I$, we define its induced item set $\overline{I}$ as

[TABLE]

The idea of PELLA is that it operates on item sets $I$ just as ELLA would operate on $\overline{I}$. For each of the original building blocks $\operatorname{Init}^{\prime}$, $\operatorname{Predict}^{\prime}$, $\operatorname{Complete}^{\prime}$, $\operatorname{Tokens}^{\prime}$ and $\operatorname{Scan}^{\prime}$ of ELLA we define the corresponding building blocks $\operatorname{Init}$, $\operatorname{Predict}$, $\operatorname{Complete}$, $\operatorname{Tokens}$ and $\operatorname{Scan}$ of PELLA as shown in Figure 1 (the use of the • notation for PELLA items is analogous to its use for ELLA items). Apart from this adaptation of the building blocks to a parameterized setting, PELLA is defined via exactly the same equations as ELLA is, as shown in Figure 2.

Theorem 4.2** (Correctness of PELLA).**

[TABLE]

Indeed, we can prove the correctness of PELLA by exploiting the fact that PELLA simulates ELLA. The proof works by explaining in detail what we mean by this simulation. To this end, we need a notion of correspondence between PELLA item sets $I$ and ELLA item sets $I^{\prime}$. Intuitively, $\overline{I}=I^{\prime}$ is an obvious candidate for such a relation, but this does not work: $I^{\prime}$ may contain items of the form $(\top\rightarrow w_{1}\makebox[7.0pt]{\textbullet}w_{2},i,j)$ or $(N\rightarrow w\makebox[7.0pt]{\textbullet}\bot,i,j)$, both of which will never be in $\overline{I}$. Therefore, we define the correspondence $I\sim I^{\prime}$ instead as $\overline{I}=\operatorname{Norm}\left(I^{\prime}\right)$ where $\operatorname{Norm}\left(I^{\prime}\right)=\left\{(N\rightarrow w_{1}\makebox[7.0pt]{\textbullet}w_{2},i,j)\in I^{\prime}\mid N\neq\top\wedge w_{2}\neq\bot\right\}$. Indeed, with this choice of correspondence the formulas in Figure 3 hold and show that the building blocks of PELLA simulate the building blocks of ELLA.

In the following we will prove the formulas in Figure 3.

Theorem 4.3**.**

[TABLE]

Proof.

From the definitions it follows that

[TABLE]

We first show $\operatorname{Norm}\left(\operatorname{Predict}^{\prime}0\,\operatorname{Init}^{\prime}\right)\subseteq\overline{\operatorname{Init}}$. So assume that $(\mathfrak{S}^{\phi_{\textsl{start}}}_{\beta}\rightarrow\makebox[7.0pt]{\textbullet}w,0,0)\in\operatorname{Norm}\left(\operatorname{Predict}^{\prime}0\,\operatorname{Init}^{\prime}\right)$. There must be $r\in\mathfrak{R}$ such that $(\mathfrak{S}^{\phi_{\textsl{start}}}_{\beta}\rightarrow w)\in\overline{r}$, and $r=\mathfrak{S}_{f_{k+1}}\rightarrow\textsl{X}_{1}^{f_{1}}\ldots\textsl{X}_{k}^{f_{k}}$ for some $f_{1},\ldots,f_{k+1}$ and some $\textsl{X}_{1},\ldots,\textsl{X}_{k}$.

If $w$ does not end with $\bot$, we know there must be $\alpha_{1},\ldots,\alpha_{k}$ and $\beta_{1},\ldots,\beta_{k}$ such that $(\mathfrak{S}^{\phi_{\textsl{start}}}_{\beta}\rightarrow w)=(\mathfrak{S}_{\beta}^{\,\phi_{\textsl{start}}}\rightarrow{\textsl{X}_{1}}_{\beta_{1}}^{\alpha_{1}}\ldots{\textsl{X}_{k}}_{\beta_{k}}^{\alpha_{k}})$, and we also know then that $f_{1}$ is defined on $\phi_{\textsl{start}}$, and that either $k=0\wedge\beta=f_{1}(\phi_{\textsl{start}})$ or $k>0\wedge\alpha_{1}=f_{1}(\phi_{\textsl{start}})$. For the parameterized item $x=(\mathfrak{S}_{f_{k+1}}\rightarrow\makebox[7.0pt]{\textbullet}\textsl{X}_{1}^{f_{1}}\ldots\textsl{X}_{k}^{f_{k}},0,0,\phi_{\textsl{start}}\,f_{1}(\phi_{\textsl{start}}))$ this implies that $x\in\operatorname{Init}$, and that $(\mathfrak{S}^{\phi_{\textsl{start}}}_{\beta}\rightarrow\makebox[7.0pt]{\textbullet}w,0,0)\in\overline{x}\subseteq\overline{\operatorname{Init}}$.

If on the other hand $w$ ends with $\bot$, then $k>0$ and there must be $h\in\{1,\ldots,k\}$, $\alpha_{1},\ldots,\alpha_{h}$ and $\beta_{1},\ldots,\beta_{h}$ such that $(\mathfrak{S}^{\phi_{\textsl{start}}}_{\beta}\rightarrow w)=(\mathfrak{S}_{\beta}^{\,\phi_{\textsl{start}}}\rightarrow{\textsl{X}_{1}}_{\beta_{1}}^{\alpha_{1}}\ldots{\textsl{X}_{h}}_{\beta_{h}}^{\alpha_{h}}\bot)$. We also know then that $f_{1}$ is defined on $\phi_{\textsl{start}}$, and that $\alpha_{1}=f_{1}(\phi_{\textsl{start}})$. For the parameterized item $x=(\mathfrak{S}_{f_{k+1}}\rightarrow\makebox[7.0pt]{\textbullet}\textsl{X}_{1}^{f_{1}}\ldots\textsl{X}_{k}^{f_{k}},0,0,\phi_{\textsl{start}}\,f_{1}(\phi_{\textsl{start}}))$ this implies that $x\in\operatorname{Init}$, and that $(\mathfrak{S}^{\phi_{\textsl{start}}}_{\beta}\rightarrow\makebox[7.0pt]{\textbullet}w,0,0)\in\overline{x}\subseteq\overline{\operatorname{Init}}$.

We now prove $\overline{\operatorname{Init}}\subseteq\operatorname{Norm}\left(\operatorname{Predict}^{\prime}0\,\operatorname{Init}^{\prime}\right)$. So assume $x^{\prime}\in\overline{\operatorname{Init}}$. Then there must be $x\in\operatorname{Init}$ such that $x^{\prime}\in\overline{x}$. We know that

[TABLE]

for some $\textsl{X}_{1},\ldots,\textsl{X}_{u}$ and some $f_{1},\ldots,f_{u}$. From this $x^{\prime}\in\operatorname{Norm}\left(\operatorname{Predict}^{\prime}0\,\operatorname{Init}^{\prime}\right)$ immediately follows. ∎

Theorem 4.4**.**

Let $x$ be a parameterized item such that

[TABLE]

(and $v\geq d+1$). Then for each $\gamma\in\Phi$ there is $x^{\prime}\in\overline{x}$ with

[TABLE]

for some $\beta\in\Phi$ and some $w\in(\overline{\mathfrak{N}}\cup\overline{\mathfrak{T}})^{*}$.

Proof.

The proof is basically the same as the proof of Theorem 4.1, only that instead of extending $\rho$ we extend $\rho\,\gamma$ this time. ∎

Theorem 4.5**.**

Assume $(\textsl{N}^{\,\alpha}_{\beta}\rightarrow w)\in\overline{\mathfrak{R}}$. If $w$ ends with $\bot$ then this implies $|w|\geq 2$. Furthermore, for any $d$ with

[TABLE]

and for any $0\leq i\leq j\leq|D|$ there is a parameterized item

[TABLE]

such that $(\textsl{N}^{\,\alpha}_{\beta}\rightarrow w,d,i,j)\in\overline{x}$.

Proof.

Assume $w$ does not end with $\bot$. Then there is a parameterized rule $r=\textsl{N}_{f_{|w|+1}}\rightarrow\textsl{X}_{1}^{f_{1}}\ldots\textsl{X}_{|w|}^{f_{|w|}}\in\mathfrak{R}$ such that $(\textsl{N}^{\alpha}_{\beta}\rightarrow w)\in\overline{r}$, and there are $\alpha_{1},\beta_{1},\ldots,\alpha_{|w|},\beta_{|w|}$ such that $w={\textsl{X}_{1}}_{\beta_{1}}^{\alpha_{1}}\ldots{\textsl{X}_{|w|}}_{\beta_{|w|}}^{\alpha_{|w|}}$ and $\alpha\,\alpha_{1}\,\beta_{1}\ldots\alpha_{|w|}\,\beta_{|w|}\,\beta\in\langle{f_{1},\ldots,f_{|w|+1}}\rangle$. Setting $x=(r,d,i,j,\rho)$ where $\rho=\operatorname{take}_{2(d+1)}\,(\alpha\,\alpha_{1}\,\beta_{1}\ldots\alpha_{|w|}\,\beta_{|w|}\,\beta)$ yields the desired result.

On the other hand, assume $w$ ends with $\bot$. Then there is a parameterized rule $r=\textsl{N}_{f_{k+1}}\rightarrow\textsl{X}_{1}^{f_{1}}\ldots\textsl{X}_{k}^{f_{k}}\in\mathfrak{R}$ such that $(\textsl{N}^{\alpha}_{\beta}\rightarrow w)\in\overline{r}$ and $1\leq|w|-1\leq k$. In particular there are $\alpha_{1},\beta_{1},\ldots,\alpha_{|w|-1},\beta_{|w|-1}$ such that $w=\textsl{X}_{\beta_{1}}^{\alpha_{1}}\ldots\textsl{X}_{\beta_{|w|-1}}^{\alpha_{|w|-1}}\,\bot$ and $\alpha\,\alpha_{1}\,\beta_{1}\ldots\alpha_{|w|-1}\in\langle{f_{1},\ldots,f_{|w|-1}}\rangle$. Setting $x=(r,d,i,j,\rho)$ where $\rho=\operatorname{take}_{2(d+1)}\,(\alpha\,\alpha_{1}\,\beta_{1}\ldots\alpha_{|w|-1})$ yields the desired result in this case as well. ∎

Theorem 4.6**.**

Assume $I\sim I^{\prime}$. Then

[TABLE]

Proof.

We first prove $\overline{\operatorname{Predict}k\,I}\subseteq\operatorname{Norm}\left(\operatorname{Predict}^{\prime}k\,I^{\prime}\right)$, so assume $x^{\prime}\in\overline{\operatorname{Predict}k\,I}$. Then there must be $x\in\operatorname{Predict}k\,I$ such that $x^{\prime}\in\overline{x}$. If $x\in I$ then because of $I\sim I^{\prime}$ it automatically follows that $x^{\prime}\in\operatorname{Norm}\left(I^{\prime}\right)\subseteq\operatorname{Norm}\left(\operatorname{Predict}^{\prime}k\,I^{\prime}\right)$. So assume $x\notin I$. This means that

[TABLE]

and there is a parameterized item $y$ where

[TABLE]

such that $\textsl{X}_{d+1}=\textsl{M}$. From $x^{\prime}\in\overline{x}$ it follows that

[TABLE]

for some $\gamma\in\Phi$ and some $a\in(\overline{\mathfrak{N}}\cup\overline{\mathfrak{T}})^{*}$. From Theorem 4.4 we obtain an item $y^{\prime}$ with

[TABLE]

for some $\beta\in\Phi$ and some $w\in(\overline{\mathfrak{N}}\cup\overline{\mathfrak{T}})^{*}$. Because $I\sim I^{\prime}$ implies $y^{\prime}\in I^{\prime}$ it follows immediately that $x^{\prime}\in\operatorname{Predict}^{\prime}k\,I^{\prime}$. As $x^{\prime}$ is an induced item, this implies $x^{\prime}\in\operatorname{Norm}\left(\operatorname{Predict}^{\prime}k\,I^{\prime}\right)$.

Now we prove $\operatorname{Norm}\left(\operatorname{Predict}^{\prime}k\,I^{\prime}\right)\subseteq\overline{\operatorname{Predict}k\,I}$. Assume $x^{\prime}\in\operatorname{Norm}\left(\operatorname{Predict}^{\prime}k\,I^{\prime}\right)$. If $x^{\prime}\in I^{\prime}$ then $x^{\prime}\in\overline{I}$ and we are done, so assume $x^{\prime}\notin I^{\prime}$. This means that $x^{\prime}=(\textsl{M}^{\alpha}_{\gamma}\rightarrow\makebox[7.0pt]{\textbullet}a,k,k)$ for some $\textsl{M}^{\alpha}_{\gamma}\rightarrow a\in\overline{\mathfrak{R}}$, and there is $y^{\prime}=(\textsl{N}^{\beta}_{\delta}\rightarrow b\makebox[7.0pt]{\textbullet}\textsl{M}^{\alpha}_{\gamma},i,k)\in I^{\prime}$. This means that there is $y\in I$ with $y^{\prime}\in\overline{y}$. From Theorem 4.5 we obtain an $x$ with $x^{\prime}\in\overline{x}$ and it follows straight from the definitions that $x\in\operatorname{Predict}k\,\{y\}$. ∎

Theorem 4.7**.**

Assume $I\sim I^{\prime}$. Then

[TABLE]

Proof.

We first prove $\overline{\operatorname{Complete}k\,I}\subseteq\operatorname{Norm}\left(\operatorname{Complete}^{\prime}k\,I^{\prime}\right)$, so assume $x^{\prime}\in\overline{\operatorname{Complete}k\,I}$. Then there must be $x\in\operatorname{Complete}k\,I$ such that $x^{\prime}\in\overline{x}$. We can assume $x\notin I$ as otherwise the result follows immediately. This means that there are parameterized items $y$ and $z$ such that $x$, $y$ and $z$ have the shape

[TABLE]

such that $\textsl{X}_{d+1}=M$ and $\rho_{2d+1}=\xi_{0}$ and $\rho^{\prime}=\rho\,\xi_{2u+1}$. Moving the dot in $x^{\prime}$ one position to the left results in an item $y^{\prime}$, and obviously $y^{\prime}\in\overline{y}$. From Theorem 4.1 we obtain $z^{\prime}\in\overline{z}$. Because of $I\sim I^{\prime}$ we have $\{y^{\prime},z^{\prime}\}\subseteq\operatorname{Norm}\left(I^{\prime}\right)$. Furthermore it is easy to see that $x^{\prime}\in\operatorname{Complete}^{\prime}k\,\{y^{\prime},z^{\prime}\}$. This concludes this direction of the proof.

For the other direction assume $x^{\prime}\in\operatorname{Norm}\left(\operatorname{Complete}^{\prime}k\,I^{\prime}\right)$. We need to show that $x^{\prime}\in\overline{\operatorname{Complete}k\,I}$. We can assume $x^{\prime}\notin I^{\prime}$ as otherwise $x^{\prime}\in\overline{I}$ follows immediately. Then there exist $y^{\prime},z^{\prime}\in I^{\prime}$ such that $x^{\prime}$, $y^{\prime}$ and $z^{\prime}$ have the shape

[TABLE]

where $a\neq\bot$ as $x^{\prime}\in\operatorname{Norm}\left(\ldots\right)$. Because of $I\sim I^{\prime}$ there exist $y,z\in I$ with $y^{\prime}\in\overline{y}$, $z^{\prime}\in\overline{z}$ and

[TABLE]

Because of $a\neq\bot$ we know that $f_{d+2}$ is defined on $\rho^{\prime}=\rho\,\beta_{d+1}$ and thus $x\in\operatorname{Complete}k\,\{y,z\}$ where

[TABLE]

It is clear that $x^{\prime}\in\overline{x}$, which concludes the proof. ∎

Theorem 4.8**.**

Assume $I\sim I^{\prime}$. Then

[TABLE]

Proof.

Let us first introduce two abbreviations $V$ and $V^{\prime}$:

[TABLE]

Unfolding the definitions of $\operatorname{Tokens}$ and $\operatorname{Tokens}^{\prime}$ shows that the theorem statement is equivalent to

[TABLE]

which according to the definition of $\overline{\textsl{Sel}}$ is equivalent to

[TABLE]

This means that if we can prove

[TABLE]

we have proven the theorem.

We first prove $\mathcal{U}(V)\subseteq V^{\prime}$, so assume $(t^{\alpha}_{\beta},c)\in\mathcal{U}(V)$, or equivalently $(t,\alpha,\beta,c)\in V$. This means that there is a parameterized item

[TABLE]

with $\textsl{X}_{d+1}=t$, $\rho_{2d+1}=\alpha$ and $(t,\alpha,\beta,c)\in\textsl{Lex}(t,\alpha,D,k)$. Theorem 4.4 yields an item $x^{\prime}\in\overline{x}\subseteq\overline{I}\subseteq I^{\prime}$ such that

[TABLE]

for some $\delta$ and some $w$. This proves $(t^{\alpha}_{\beta},c)\in V^{\prime}$.

To prove $V^{\prime}\subseteq\mathcal{U}(V)$, assume $(t^{\alpha}_{\beta},c)\in V^{\prime}$. Then there must be an item

[TABLE]

such that $(t^{\alpha}_{\beta},c)\in\overline{\textsl{Lex}}(t^{\alpha}_{\beta})(D,k)$, or equivalently

[TABLE]

Because the dot in $x^{\prime}$ appears before a terminal symbol we know that $x^{\prime}\in\operatorname{Norm}\left(I^{\prime}\right)$, thus there is an $x\in I$ with

[TABLE]

such that $x^{\prime}\in\overline{x}$. This implies $\textsl{X}_{|a|+1}=t$ and $\rho_{2|a|+1}=\alpha$. This proves $(t,\alpha,\beta,c)\in V$. ∎

Theorem 4.9**.**

Assume $I\sim I^{\prime}$. Then

[TABLE]

Proof.

The proof is straightforward and similar to the proof of Theorem 4.7. ∎

Apart from using parameterized building blocks, PELLA as shown in Figure 2 is identical to ELLA as shown in Figure 4. Given that we now know that all of PELLA’s building blocks simulate those of ELLA as described in Figure 3, it is easy to see that the relationship $\mathfrak{I}\sim\mathfrak{I}^{\prime}$ holds for the result $\mathfrak{I}$ of PELLA and the result $\mathfrak{I}^{\prime}$ of ELLA. We show this in the following through a sequence of simple theorems.

Theorem 4.10**.**

Assume $I_{u}\sim I^{\prime}_{u}$ for all $u\in\{0,1,2,\ldots\}$. Then

[TABLE]

Proof.

[TABLE]

∎

We say that a function $f$ simulates a function $g$ iff $I\sim I^{\prime}$ implies $f\,I\sim g\,I^{\prime}$ for any $I$ and $I^{\prime}$.

Theorem 4.11**.**

If $f$ simulates $f^{\prime}$ and $g$ simulates $g^{\prime}$ then $g\circ f$ simulates $g^{\prime}\circ f^{\prime}$.

Proof.

From $I\sim I^{\prime}$ follows $f\,I\sim f^{\prime}\,I^{\prime}$, and from that $g\,(f\,I)\sim g^{\prime}\,(f^{\prime}\,I^{\prime})$ follows. ∎

Theorem 4.12**.**

Assume that $f$ simulates $g$. Then for any $n\in\{0,1,2,\ldots\}$ we have that $f^{n}$ simulates $g^{n}$.

Proof.

This is an immediate consequence of Theorem 4.11.∎

Theorem 4.13**.**

Assume that $f$ simulates $g$. Then $\operatorname{limit}\,f$ simulates $\operatorname{limit}\,g$.

Proof.

We need to show that from $I\sim I^{\prime}$ it follows that

[TABLE]

which follows immediately from Theorems 4.10 and 4.12. ∎

Theorem 4.14**.**

$\pi_{k}\,T$* simulates $\pi^{\prime}_{k}\ \mathcal{U}(T)$.*

Proof.

We know that $\operatorname{Predict}\,k$ simulates $\operatorname{Predict}^{\prime}\,k$ (Theorem 4.6), $\operatorname{Complete}\,k$ simulates $\operatorname{Complete}^{\prime}\,k$ (Theorem 4.7) and $\operatorname{Scan}\,T\,k$ simulates $\operatorname{Scan}^{\prime}\,\mathcal{U}(T)\,k$ (Theorem 4.9). From this and Theorems 4.11 and  4.13 the result follows immediately. ∎

Theorem 4.15**.**

$\mathcal{J}_{0}^{0}\sim{\mathcal{J}^{\prime}}_{0}^{\,0}$**

Proof.

We have $\pi^{\prime}_{0}\,\emptyset\,\operatorname{Init}^{\prime}=\pi^{\prime}_{0}\,\emptyset\,(\operatorname{Predict}^{\prime}0\,\operatorname{Init}^{\prime})$, which together with Theorems 4.3 and 4.14 implies $\mathcal{J}_{0}^{0}\sim{\mathcal{J}^{\prime}}_{0}^{\,0}$. ∎

Theorem 4.16**.**

Assume $\mathcal{J}_{k}^{0}\sim{\mathcal{J}^{\prime}}_{k}^{\,0}$. Then

[TABLE]

Proof.

We first prove $\mathcal{J}_{k}^{u}\sim{\mathcal{J}^{\prime}}_{k}^{\,u}$ and $\mathcal{U}(\mathcal{T}_{k}^{\,u})={\mathcal{T}^{\prime}}_{k}^{\,u}$ by induction over $u$. The base case $u=0$ follows trivially from our assumption $\mathcal{J}_{k}^{0}\sim{\mathcal{J}^{\prime}}_{k}^{\,0}$ and the fact that $\mathcal{U}(\emptyset)=\emptyset$. For the induction step $u\rightarrow u+1$ we apply Theorem 4.8 and the induction hypothesis and obtain $\mathcal{U}(\mathcal{T}_{k}^{\,u+1})={\mathcal{T}^{\prime}}_{k}^{\,u+1}$. From this, together with Theorem 4.14 and the induction hypothesis, we obtain $\mathcal{J}_{k}^{u+1}\sim{\mathcal{J}^{\prime}}_{k}^{\,u+1}.$

From \mathcal{J}_{k}^{u}\sim{\mathcal{J}^{\prime}}_{k}^{\,u}\quad\text{for all u\in{0,1,2,\ldots}} and Theorem 4.10 follows then immediately $\mathcal{I}_{k}\sim{\mathcal{I}}^{\prime}_{k}$. ∎

Theorem 4.17**.**

[TABLE]

Proof.

The first three formulas follow immediately by induction over $k$ and application of Theorem 4.15 and Theorem 4.16 for the base case, and Theorem 4.14 and Theorem 4.16 for the induction step, respectively.

We then deduce $\mathfrak{I}=\mathcal{I}_{|D|}\sim{\mathcal{I}}^{\prime}_{|D|}=\mathfrak{I}^{\prime}$. ∎

We are now in a position to prove the correctness of PELLA.

Proof of Theorem 4.2.

We first introduce the abbreviation

[TABLE]

Then our goal is to prove $\sigma({D})=P$.

To prove $\sigma({D})\subseteq P$, assume $\beta\in\sigma({D})$. Then there is a path $p\in\ell\ell(D)$ such that $\top\Rightarrow\mathfrak{S}^{\phi_{\textsl{start}}}_{\beta}\overset{*\ }{\Rightarrow}[p]$. This means that there is an item $x^{\prime}=(\mathfrak{S}^{\phi_{\textsl{start}}}_{\beta}\rightarrow w,0,|D|)$ which is $p$-valid, i.e. $x^{\prime}\in\langle{\mathfrak{P}}\rangle$. From the correctness proof of ELLA we know that $\langle{\mathfrak{P}}\rangle=\mathfrak{I}^{\prime}$ and thus $x^{\prime}\in\mathfrak{I}^{\prime}$, and the shape of $x^{\prime}$ implies even $x^{\prime}\in\operatorname{Norm}\left(\mathfrak{I}^{\prime}\right)$. Therefore Theorem 4.17 allows us to deduce $x^{\prime}\in\overline{\mathfrak{I}}$, and this means that there is an $x\in\mathfrak{I}$ such that $x^{\prime}\in\overline{x}$ and such that $x$ has the shape

[TABLE]

From $x^{\prime}\in\overline{x}$ follows immediately that $\rho_{0}=\phi_{\textsl{start}}$ and $\rho_{2u+1}=\beta$, and therefore $\beta\in P$.

To prove the other direction, $P\subseteq\sigma({D})$, assume we have an $x\in\mathfrak{I}$ such that $x=(\mathfrak{S}_{f_{u+1}}\rightarrow\textsl{X}_{1}^{f_{1}}\ldots\textsl{X}_{u}^{f_{u}}\makebox[7.0pt]{\textbullet},0,|D|,\rho)$ and $\rho_{0}=\phi_{\textsl{start}}$. We need to prove $\rho_{2u+1}\in\sigma({D})$. Theorem 4.1 tells us that there is an $x^{\prime}\in\overline{x}$, and this $x^{\prime}$ has necessarily the form

[TABLE]

From Theorem 4.17 and the correctness of ELLA follows $x^{\prime}\in\overline{x}\subseteq\overline{\mathfrak{I}}\subseteq\mathfrak{I}^{\prime}=\langle{\mathfrak{P}}\rangle$. Thus there is a path $p\in\mathfrak{P}$ such that $x^{\prime}$ is $p$-valid, i.e. there is $v\in\{0,\ldots,|p|\}$ such that

[TABLE]

As part of the correctness proof of ELLA we have previously seen that if we drop the first $v$ empty tokens of $p$, the result $q=p_{v}\ldots p_{|p|-1}$ will still be in $\mathfrak{P}$ (Theorem 5.2 in locallexing ). We deduce

[TABLE]

and $q\in\ell\ell(D)$, and thus $\rho_{2u+1}\in\sigma({D})$. ∎