Relational parsing: a clean, fast parsing strategy for all context-free languages
Grzegorz Herman
TL;DR
This paper introduces a new, mathematically elegant parsing algorithm for all context-free languages that is efficient, easy to implement with immutable data structures, and can outperform existing algorithms in practical scenarios.
Contribution
The paper presents a novel, relation-based parsing algorithm with a clean mathematical formulation applicable to all context-free languages, improving efficiency and implementation simplicity.
Findings
Parsing complexity matches state-of-the-art: cubic, quadratic, or linear.
Implementation with immutable data structures enables effective memoization.
Proof-of-concept outperforms common algorithms, sometimes significantly.
Abstract
We present a novel parsing algorithm for all context-free languages, based on computing the relation between configurations and reaching transitions in a recursive transition network. Parsing complexity w.r.t. input length matches the state of the art: it is worst-case cubic, quadratic for unambiguous grammars, and linear for LR-regular ones. What distinguishes our algorithm is its clean mathematical formulation: parsing is expressed as a composition of simple operations on languages and relations, and can therefore be implemented using only immutable data structures. With a proper choice of these structures, a vast majority of operations performed during parsing typical programming languages can be memoized, which allows our proof-of-concept implementation to outperform common generalized parsing algorithms, in some cases by orders of magnitude.
Peer Reviews
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.
Taxonomy
TopicsAlgorithms and Data Compression · semigroups and automata theory · DNA and Biological Computing
\TabPositions
.55
Relational parsing: a clean, fast parsing strategy for all context-free languages
††thanks: This manuscript is a work in progress: a few proofs still need to be written down, and there are many rough edges. We also hope to provide more experimental results and extend the discussion in the final section. Thus, please contact us first if you would like to cite this work. We also welcome comments and suggestions of improvements, regarding both the algorithm itself and the way it is presented here.
Grzegorz Herman
Theoretical Computer Science, Jagiellonian University
Abstract
We present a novel parsing algorithm for all context-free languages, based on computing the relation between configurations and reaching transitions in a recursive transition network. Parsing complexity w.r.t. input length matches the state of the art: it is worst-case cubic, quadratic for unambiguous grammars, and linear for LR-regular ones. What distinguishes our algorithm is its clean mathematical formulation: parsing is expressed as a composition of simple operations on languages and relations, and can therefore be implemented using only immutable data structures. With a proper choice of these structures, a vast majority of operations performed during parsing typical programming languages can be memoized, which allows our proof-of-concept implementation to outperform common generalized parsing algorithms, in some cases by orders of magnitude.
1 Introduction
Parsing is a well-studied and yet still active topic in computer science. Multiple highly efficient deterministic parsers can handle large families of unambiguous context-free grammars, and oftentimes more. However, grammars of many programming languages do not naturally fit within the limitations required by these parsers, and need tedious manual adaptation (e.g., replacing left recursion with right recursion). Worse, such adaptation needs to be “undone” on parse trees, in order to make them reflect the desired structure of the language. Further, in many cases the “natural” grammar of a language allows some ambiguity, which is easier resolved at a later compilation step. With the growing need for rapid development of new languages, generalized parsers—able to handle all, even ambiguous, context-free grammars—are gaining wider adoption.
Most generalized parsing techniques are based on clever parallel simulation of nondeterministic choices of a pushdown automaton. Some of these algorithms offer good complexity guarantees: worst-case cubic, quadratic on unambiguous grammars, and in some cases linear on “nice” language fragments. Nondeterminism is handled by means of (some variant of) a data structure called GSS (graph-structured stack). This makes the constant factors involved significantly larger than in deterministic parsers, which use a simple stack. Moreover, in order to handle the full class of context-free grammars, the graph-like data structures in all these algorithms need to be mutable and allow cycles. Even where it does not significantly complicate the implementation, it makes reasoning about the algorithm more difficult.
We present a new generalized context-free parsing algorithm which we call relational parsing. Similarly to existing approaches, it simulates possible runs of a pushdown automaton (specifically, a recursive transition network). However, its formulation is based on precise mathematical semantics, given in Section 2: it inductively computes the languages of configurations reachable after reading consecutive input symbols. We show that each such language can be obtained from the previous one by a constant number of simple, well-known language-theoretic operations. The way of representing these languages (and their grammar-dependent atomic building blocks) is left abstract at this point.
Our recognition algorithm generalizes cleanly to a full-fledged parser, capable of producing a compact representation of all possible parse trees. To achieve that, instead of languages of reachable configurations, we compute the relations between configurations and the ways in which they can be reached (hence the algorithm name). This generalization is presented in Section 3. Again, the representation of relations is hidden behind an abstract API.
We give possible concrete realizations of all required abstract data types in Section 4. For the relations computed during parsing, we use a DAG structure akin to the graph-structured stack. However, with our approach, all cyclicity is embedded in the atomic relations, and thus we never need to add edges to existing DAG nodes. The atomic languages and relations are shown to be regular, and thus can be represented by nondeterministic finite automata. We also discuss some possible representations of transition languages.
Instead of computing the language of all accepting transition sequences, our parsing algorithm can work with any semiring induced by individual transitions. However, as presented, it introduces artificial ambiguity into the objects computed, and thus requires such semiring to be idempotent. In Section 5 we pinpoint the reasons for this ambiguity, and show how it can be eliminated by a simple yet subtle adjustment of the atomic relations.
The input-related complexity of our algorithm, discussed in Section 6, matches the state of the art: our parser is worst-case cubic, quadratic on unambiguous grammars, and linear on LR-regular grammars.
There are multiple benefits of our clean, semantic approach. The automata representing atomic languages can be optimized. More importantly, due to immutability, partial results can be memoized and reused. In Section 7 we outline how to achieve such reuse by using a more complex representation of languages. On real-world inputs (Java 8 grammar and a large collection of source files) it allows a vast majority of phases to be performed on a plain stack, which makes our (unoptimized) proof-of-concept C♯ implementation significantly outperform (our, unoptimized implementation of) GLL. In recognition mode the speed-up is close to two orders of magnitude—the running times are on par with those of the hand-coded deterministic parser used by the Java compiler. This experimental evaluation is presented in Section 8.
Finally, in Section 9 we discuss how our approach fits into the generalized parsing landscape. We show how the bits and pieces of our algorithm relate to the seminal work of Lang, Earley, and Tomita, as well as to GLL, GLR, GLC (generalized left-corner), reduction-incorporated parsers, and Adaptive LL(*) employed by ANTLR4. Within the discussion we also hint at some places where our algorithm could be improved, or our approach extended.
Our proof-of-concept implementation can be accessed at
https://gitlab.com/alt-lang/research/relational-parsing.
2 Recognition
There are many equivalent formalisms capturing context-free languages. In this work, we use recursive transition networks [25], a restricted class of nondeterministic pushdown automata. They directly model the computational behavior of (nondeterministic) recursive descent parsers, and at the same time can be trivially obtained from context-free grammars.111This includes popular variants of context-free grammars in which regular expressions can be used at right-hand sides of production rules. Importantly, the states obtained in such translation are exactly the “items” used by GLL, (G)LC, and (G)LR parsers. Let us begin with a quick review of the chosen model.
Definition 1**.**
A recursive transition network over a terminal alphabet and set of production labels222The labels are never looked at by our algorithm. However, they can be attached to internal parse tree nodes—a role usually served by grammar productions, hence the name. consists of:
- •
a finite set of states, with a distinguished start state ,
- •
a finite set of transitions, each being one of:
- –
* with and ,*
- –
* with , or*
- –
* with and .*
Throughout the paper, we assume to be working with a single network, and thus consider , , and to be fixed. For convenience, we let denote the set of shifts for each particular symbol , and —the set of all non-shift transitions.
Recognition by an RTN begins in the state . At each moment, the network may nondeterministically choose any legal transition from its current state . A consumes the symbol from the input and changes state to , recursively invokes recognition from state and moves to once the recursive call returns, and returns from a single level of recursion. An input belongs to the language of the RTN if there is a sequence of legal transitions which consumes the whole , and ends by returning from the top recursion level. If a parse tree is to be constructed, its shape follows exactly the nesting of recursive calls made, with from used to label the resulting node.
Making explicit the recursion stack, the recognition process can be formalized as follows:
Definition 2**.**
A configuration of a recursive transition network is a stack of its states, i.e. a member of (the top—current—state is the first in such sequence). Each transition induces the following reachability relation \mathrel{\leavevmode\hbox to7.16pt{\vbox to12.28pt{\pgfpicture\makeatletter\hbox{\hskip 3.57956pt\lower-8.60823pt\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{ }\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ } {{}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}{}{{ {}{}}}{ {}{}} {{}{{}}}{{}{}}{}{{}{}} { }{{{{}}\pgfsys@beginscope\pgfsys@invoke{ }\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{-1.45735pt}{-1.95294pt}\pgfsys@invoke{ }\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{ }\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{{\vbox{\halign{\hfil#\hfil\cr\cr\vskip 0.017pt\cr\hbox{{\scriptstyle d}}\cr}}}} }}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} { {}{}{}}{{{}}{{}}}{{}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}{}{{ {}{}}}{ {}{}} {{}{{}}}{{}{}}{}{{}{}} { }{{{{}}\pgfsys@beginscope\pgfsys@invoke{ }\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{0.0pt}{-5.94182pt}\pgfsys@invoke{ }\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{ }\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{} }}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} {{}{{}}{}{{}}{}{ {}} {}{}}{{}{}}{}{}{}{{}}{{}}{{}{}}{{}{}} {{{{}{}{{}} }}{{}}}{{{{}{}{{}} }}{{}}{{}}} {{{{}{}{{}} }}{{}} {}{}{} {}{}{} {}{}{} {}{}{} }{{{{}{}{{}} }}{{}} {}{}{} {}{}{} {}{}{} {}{}{} }{{{{}{}{{}} }}{{}} {}{}{} {}{}{} }{{{{}{}{{}} }}{{}}}{{{{}{}{{}} }}{{}} {{}} } {{{{}{}{{}} }}{{}} }{{{{}{}{{}} }}{{}}{{}}}{}{{ {\pgfsys@beginscope \pgfsys@setdash{}{0.0pt}\pgfsys@roundcap\pgfsys@roundjoin{} {}{}{} {}{}{} \pgfsys@moveto{-2.07999pt}{1.17778pt}\pgfsys@curveto{-1.69998pt}{0.4711pt}{-0.85318pt}{0.1374pt}{0.0pt}{0.0pt}\pgfsys@curveto{-0.85318pt}{-0.1374pt}{-1.69998pt}{-0.4711pt}{-2.07999pt}{-1.17778pt}\pgfsys@stroke\pgfsys@endscope}} }{}{}{{}}\pgfsys@moveto{-3.37956pt}{-3.87515pt}\pgfsys@lineto{-3.37956pt}{-3.87515pt}\pgfsys@curveto{-3.23605pt}{-3.684pt}{-3.09254pt}{-3.53072pt}{-2.94904pt}{-3.53072pt}\pgfsys@curveto{-2.80553pt}{-3.53072pt}{-2.66202pt}{-3.684pt}{-2.51851pt}{-3.87515pt}\pgfsys@curveto{-2.375pt}{-4.0663pt}{-2.23149pt}{-4.21959pt}{-2.08798pt}{-4.21959pt}\pgfsys@curveto{-1.94447pt}{-4.21959pt}{-1.80096pt}{-4.0663pt}{-1.65746pt}{-3.87515pt}\pgfsys@curveto{-1.51384pt}{-3.684pt}{-1.37033pt}{-3.53072pt}{-1.22682pt}{-3.53072pt}\pgfsys@curveto{-1.08331pt}{-3.53072pt}{-0.9398pt}{-3.684pt}{-0.7963pt}{-3.87515pt}\pgfsys@curveto{-0.65279pt}{-4.0663pt}{-0.50928pt}{-4.21959pt}{-0.36577pt}{-4.21959pt}\pgfsys@curveto{-0.22226pt}{-4.21959pt}{-0.07875pt}{-4.0663pt}{0.06476pt}{-3.87515pt}\pgfsys@curveto{0.20837pt}{-3.684pt}{0.35188pt}{-3.53072pt}{0.49539pt}{-3.53072pt}\pgfsys@curveto{0.6389pt}{-3.53072pt}{0.78241pt}{-3.684pt}{0.92592pt}{-3.87515pt}\pgfsys@lineto{0.92598pt}{-3.87515pt}\pgfsys@lineto{2.97957pt}{-3.87515pt}\pgfsys@stroke\pgfsys@invoke{ }{{}{{}}{}{}{{}}{{{}}{{{}}{\pgfsys@beginscope\pgfsys@invoke{ }\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{3.17957pt}{-3.87515pt}\pgfsys@invoke{ }\pgfsys@invoke{ \lxSVG@closescope }\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}{{}}}} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope{{ {}{}{}}}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}} between configurations:
[TABLE]
Reachability generalizes to sequences of transitions (by composing relations for consecutive transitions), and then to languages of transitions (by taking union of relations for individual transition sequences). A sequence of transitions is viable if it induces a nonempty reachability relation.
Our recognition algorithm will simulate the nondeterministic choices made by the RTN by computing the sets of configurations reachable after consuming consecutive symbols from the input. To avoid dealing with empty configurations, we augment the set of states by a fresh state (with no outgoing transitions) and use it as a guard marking the bottom of each configuration.
Definition 3**.**
For an input , the parsing language consists of configurations (augmented with ) reachable from the initial configuration when parsing :
[TABLE]
The question of whether an input belongs to the language recognized by the network is now the same as whether its parsing language contains the configuration . The following definition allows constructing this language inductively, symbol by symbol:
Definition 4**.**
The call-reduce closure and shift by a symbol of a language are the sets of configurations reachable from without shifts and by shifting , respectively:
[TABLE]
Based on the obvious observation that and , we propose Algorithm 1 as a generic blueprint for context-free recognition. Assume for the moment that we already have the closures of individual states. The main line of development of this paper is showing how line 3, called a phase, can be performed efficiently.
Algorithm 1**.**
Checking whether belongs to the language of the RTN
1* *
2* foreach *(in order):
3* *
4* return whether *
Algorithm 2**.**
Calculating
1* *
2* foreach :*
3* foreach :*
4* *
5* if t\mathrel{\leavevmode\hbox to10.34pt{\vbox to13.65pt{\pgfpicture\makeatletter\hbox{\hskip 5.16759pt\lower-9.29378pt\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{ }\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ } {{}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}{}{{ {}{}}}{ {}{}} {{}{{}}}{{}{}}{}{{}{}} { }{{{{}}\pgfsys@beginscope\pgfsys@invoke{ }\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{-3.04538pt}{-2.63849pt}\pgfsys@invoke{ }\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{ }\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{{\vbox{\halign{\hfil#\hfil\cr\cr\vskip 0.017pt\cr\hbox{{\scriptstyle D_{\epsilon}^{*}}}\cr}}}} }}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} { {}{}{}}{{{}}{{}}}{{}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}{}{{ {}{}}}{ {}{}} {{}{{}}}{{}{}}{}{{}{}} { }{{{{}}\pgfsys@beginscope\pgfsys@invoke{ }\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{0.0pt}{-6.62737pt}\pgfsys@invoke{ }\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{ }\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{} }}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} {{}{{}}{}{{}}{}{ {}} {}{}}{{}{}}{}{}{}{{}}{{}}{{}{}}{{}{}} {{{{}{}{{}} }}{{}}}{{{{}{}{{}} }}{{}}{{}}} {{{{}{}{{}} }}{{}} {}{}{} {}{}{} {}{}{} {}{}{} }{{{{}{}{{}} }}{{}} {}{}{} {}{}{} {}{}{} {}{}{} }{{{{}{}{{}} }}{{}} {}{}{} {}{}{} {}{}{} {}{}{} }{{{{}{}{{}} }}{{}} {}{}{} {}{}{} {}{}{} {}{}{} }{{{{}{}{{}} }}{{}} {}{}{} {}{}{} }{{{{}{}{{}} }}{{}}}{{{{}{}{{}} }}{{}} {{}} } {{{{}{}{{}} }}{{}} }{{{{}{}{{}} }}{{}}{{}}}{}{}{}{}{{}}\pgfsys@moveto{-4.96759pt}{-4.5607pt}\pgfsys@lineto{-4.96759pt}{-4.5607pt}\pgfsys@curveto{-4.82408pt}{-4.36955pt}{-4.68057pt}{-4.21626pt}{-4.53706pt}{-4.21626pt}\pgfsys@curveto{-4.39355pt}{-4.21626pt}{-4.25005pt}{-4.36955pt}{-4.10654pt}{-4.5607pt}\pgfsys@curveto{-3.96303pt}{-4.75185pt}{-3.81952pt}{-4.90514pt}{-3.67601pt}{-4.90514pt}\pgfsys@curveto{-3.5325pt}{-4.90514pt}{-3.38899pt}{-4.75185pt}{-3.24548pt}{-4.5607pt}\pgfsys@curveto{-3.10187pt}{-4.36955pt}{-2.95836pt}{-4.21626pt}{-2.81485pt}{-4.21626pt}\pgfsys@curveto{-2.67134pt}{-4.21626pt}{-2.52783pt}{-4.36955pt}{-2.38432pt}{-4.5607pt}\pgfsys@curveto{-2.24081pt}{-4.75185pt}{-2.0973pt}{-4.90514pt}{-1.9538pt}{-4.90514pt}\pgfsys@curveto{-1.81029pt}{-4.90514pt}{-1.66678pt}{-4.75185pt}{-1.52327pt}{-4.5607pt}\pgfsys@curveto{-1.37965pt}{-4.36955pt}{-1.23615pt}{-4.21626pt}{-1.09264pt}{-4.21626pt}\pgfsys@curveto{-0.94913pt}{-4.21626pt}{-0.80562pt}{-4.36955pt}{-0.66211pt}{-4.5607pt}\pgfsys@curveto{-0.5186pt}{-4.75185pt}{-0.37509pt}{-4.90514pt}{-0.23158pt}{-4.90514pt}\pgfsys@curveto{-0.08807pt}{-4.90514pt}{0.05544pt}{-4.75185pt}{0.19894pt}{-4.5607pt}\pgfsys@curveto{0.34256pt}{-4.36955pt}{0.48607pt}{-4.21626pt}{0.62958pt}{-4.21626pt}\pgfsys@curveto{0.77309pt}{-4.21626pt}{0.9166pt}{-4.36955pt}{1.0601pt}{-4.5607pt}\pgfsys@curveto{1.20361pt}{-4.75185pt}{1.34712pt}{-4.90514pt}{1.49063pt}{-4.90514pt}\pgfsys@curveto{1.63414pt}{-4.90514pt}{1.77765pt}{-4.75185pt}{1.92116pt}{-4.5607pt}\pgfsys@curveto{2.06477pt}{-4.36955pt}{2.20828pt}{-4.21626pt}{2.35179pt}{-4.21626pt}\pgfsys@curveto{2.4953pt}{-4.21626pt}{2.63881pt}{-4.36955pt}{2.78232pt}{-4.5607pt}\pgfsys@lineto{2.78238pt}{-4.5607pt}\pgfsys@lineto{4.5676pt}{-4.5607pt}\pgfsys@stroke\pgfsys@invoke{ }{{}{{}}{}{}{{}}{{{}}{{{}}{\pgfsys@beginscope\pgfsys@invoke{ }\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{4.7676pt}{-4.5607pt}\pgfsys@invoke{ }\pgfsys@invoke{ \lxSVG@closescope }\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}{{}}}} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope{{ {}{}{}}}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}}\epsilon:*
6* *
7* if s_{1}\mathrel{\leavevmode\hbox to10.34pt{\vbox to13.65pt{\pgfpicture\makeatletter\hbox{\hskip 5.16759pt\lower-9.29378pt\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{ }\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ } {{}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}{}{{ {}{}}}{ {}{}} {{}{{}}}{{}{}}{}{{}{}} { }{{{{}}\pgfsys@beginscope\pgfsys@invoke{ }\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{-3.04538pt}{-2.63849pt}\pgfsys@invoke{ }\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{ }\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{{\vbox{\halign{\hfil#\hfil\cr\cr\vskip 0.017pt\cr\hbox{{\scriptstyle D_{\epsilon}^{*}}}\cr}}}} }}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} { {}{}{}}{{{}}{{}}}{{}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}{}{{ {}{}}}{ {}{}} {{}{{}}}{{}{}}{}{{}{}} { }{{{{}}\pgfsys@beginscope\pgfsys@invoke{ }\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{0.0pt}{-6.62737pt}\pgfsys@invoke{ }\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{ }\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{} }}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} {{}{{}}{}{{}}{}{ {}} {}{}}{{}{}}{}{}{}{{}}{{}}{{}{}}{{}{}} {{{{}{}{{}} }}{{}}}{{{{}{}{{}} }}{{}}{{}}} {{{{}{}{{}} }}{{}} {}{}{} {}{}{} {}{}{} {}{}{} }{{{{}{}{{}} }}{{}} {}{}{} {}{}{} {}{}{} {}{}{} }{{{{}{}{{}} }}{{}} {}{}{} {}{}{} {}{}{} {}{}{} }{{{{}{}{{}} }}{{}} {}{}{} {}{}{} {}{}{} {}{}{} }{{{{}{}{{}} }}{{}} {}{}{} {}{}{} }{{{{}{}{{}} }}{{}}}{{{{}{}{{}} }}{{}} {{}} } {{{{}{}{{}} }}{{}} }{{{{}{}{{}} }}{{}}{{}}}{}{}{}{}{{}}\pgfsys@moveto{-4.96759pt}{-4.5607pt}\pgfsys@lineto{-4.96759pt}{-4.5607pt}\pgfsys@curveto{-4.82408pt}{-4.36955pt}{-4.68057pt}{-4.21626pt}{-4.53706pt}{-4.21626pt}\pgfsys@curveto{-4.39355pt}{-4.21626pt}{-4.25005pt}{-4.36955pt}{-4.10654pt}{-4.5607pt}\pgfsys@curveto{-3.96303pt}{-4.75185pt}{-3.81952pt}{-4.90514pt}{-3.67601pt}{-4.90514pt}\pgfsys@curveto{-3.5325pt}{-4.90514pt}{-3.38899pt}{-4.75185pt}{-3.24548pt}{-4.5607pt}\pgfsys@curveto{-3.10187pt}{-4.36955pt}{-2.95836pt}{-4.21626pt}{-2.81485pt}{-4.21626pt}\pgfsys@curveto{-2.67134pt}{-4.21626pt}{-2.52783pt}{-4.36955pt}{-2.38432pt}{-4.5607pt}\pgfsys@curveto{-2.24081pt}{-4.75185pt}{-2.0973pt}{-4.90514pt}{-1.9538pt}{-4.90514pt}\pgfsys@curveto{-1.81029pt}{-4.90514pt}{-1.66678pt}{-4.75185pt}{-1.52327pt}{-4.5607pt}\pgfsys@curveto{-1.37965pt}{-4.36955pt}{-1.23615pt}{-4.21626pt}{-1.09264pt}{-4.21626pt}\pgfsys@curveto{-0.94913pt}{-4.21626pt}{-0.80562pt}{-4.36955pt}{-0.66211pt}{-4.5607pt}\pgfsys@curveto{-0.5186pt}{-4.75185pt}{-0.37509pt}{-4.90514pt}{-0.23158pt}{-4.90514pt}\pgfsys@curveto{-0.08807pt}{-4.90514pt}{0.05544pt}{-4.75185pt}{0.19894pt}{-4.5607pt}\pgfsys@curveto{0.34256pt}{-4.36955pt}{0.48607pt}{-4.21626pt}{0.62958pt}{-4.21626pt}\pgfsys@curveto{0.77309pt}{-4.21626pt}{0.9166pt}{-4.36955pt}{1.0601pt}{-4.5607pt}\pgfsys@curveto{1.20361pt}{-4.75185pt}{1.34712pt}{-4.90514pt}{1.49063pt}{-4.90514pt}\pgfsys@curveto{1.63414pt}{-4.90514pt}{1.77765pt}{-4.75185pt}{1.92116pt}{-4.5607pt}\pgfsys@curveto{2.06477pt}{-4.36955pt}{2.20828pt}{-4.21626pt}{2.35179pt}{-4.21626pt}\pgfsys@curveto{2.4953pt}{-4.21626pt}{2.63881pt}{-4.36955pt}{2.78232pt}{-4.5607pt}\pgfsys@lineto{2.78238pt}{-4.5607pt}\pgfsys@lineto{4.5676pt}{-4.5607pt}\pgfsys@stroke\pgfsys@invoke{ }{{}{{}}{}{}{{}}{{{}}{{{}}{\pgfsys@beginscope\pgfsys@invoke{ }\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{4.7676pt}{-4.5607pt}\pgfsys@invoke{ }\pgfsys@invoke{ \lxSVG@closescope }\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}{{}}}} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope{{ {}{}{}}}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}}\epsilon:*
8* *
9* *
10* return *
Let us begin with a naïve implementation, presented as Algorithm 2. While obviously correct, it is not directly usable, as the loop in line 2 ranges over potentially infinite . To deal with this issue, we rephrase it in terms of language derivatives.
Definition 5**.**
A derivative of degree of a language by a symbol is any collection of languages such that for each we have333On the right-hand side of the equivalence, is completely redundant. We keep it for consistency with later generalizations of this definition.
[TABLE]
A language is -regular if it belongs to some family of size , closed under derivatives of degree . It is -regular if it is -regular for some (finite) , and regular if it is -regular for some .
This definition of regular languages is equivalent to the standard one. The parameter measures the size of an automaton recognizing such language, while —the degree of its nondeterminism. In particular, derivatives of degree one are exactly those of Brzozowski [3].
Derivatives let us look at the first (top) state in a configuration, keeping everything that lies below it encapsulated. This leads to Algorithm 3 which, while still operating on potentially infinite objects, no longer needs to explicitly examine their contents. As we will show in Section 4, all languages encountered during recognition are regular, and thus have a finite representation on which the necessary operations can be performed efficiently.
Algorithm 3**.**
Calculating using derivatives
1* *
2* foreach :*
3* foreach :*
4* *
5* if t\mathrel{\leavevmode\hbox to10.34pt{\vbox to13.65pt{\pgfpicture\makeatletter\hbox{\hskip 5.16759pt\lower-9.29378pt\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{ }\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ } {{}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}{}{{ {}{}}}{ {}{}} {{}{{}}}{{}{}}{}{{}{}} { }{{{{}}\pgfsys@beginscope\pgfsys@invoke{ }\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{-3.04538pt}{-2.63849pt}\pgfsys@invoke{ }\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{ }\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{{\vbox{\halign{\hfil#\hfil\cr\cr\vskip 0.017pt\cr\hbox{{\scriptstyle D_{\epsilon}^{*}}}\cr}}}} }}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} { {}{}{}}{{{}}{{}}}{{}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}{}{{ {}{}}}{ {}{}} {{}{{}}}{{}{}}{}{{}{}} { }{{{{}}\pgfsys@beginscope\pgfsys@invoke{ }\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{0.0pt}{-6.62737pt}\pgfsys@invoke{ }\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{ }\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{} }}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} {{}{{}}{}{{}}{}{ {}} {}{}}{{}{}}{}{}{}{{}}{{}}{{}{}}{{}{}} {{{{}{}{{}} }}{{}}}{{{{}{}{{}} }}{{}}{{}}} {{{{}{}{{}} }}{{}} {}{}{} {}{}{} {}{}{} {}{}{} }{{{{}{}{{}} }}{{}} {}{}{} {}{}{} {}{}{} {}{}{} }{{{{}{}{{}} }}{{}} {}{}{} {}{}{} {}{}{} {}{}{} }{{{{}{}{{}} }}{{}} {}{}{} {}{}{} {}{}{} {}{}{} }{{{{}{}{{}} }}{{}} {}{}{} {}{}{} }{{{{}{}{{}} }}{{}}}{{{{}{}{{}} }}{{}} {{}} } {{{{}{}{{}} }}{{}} }{{{{}{}{{}} }}{{}}{{}}}{}{}{}{}{{}}\pgfsys@moveto{-4.96759pt}{-4.5607pt}\pgfsys@lineto{-4.96759pt}{-4.5607pt}\pgfsys@curveto{-4.82408pt}{-4.36955pt}{-4.68057pt}{-4.21626pt}{-4.53706pt}{-4.21626pt}\pgfsys@curveto{-4.39355pt}{-4.21626pt}{-4.25005pt}{-4.36955pt}{-4.10654pt}{-4.5607pt}\pgfsys@curveto{-3.96303pt}{-4.75185pt}{-3.81952pt}{-4.90514pt}{-3.67601pt}{-4.90514pt}\pgfsys@curveto{-3.5325pt}{-4.90514pt}{-3.38899pt}{-4.75185pt}{-3.24548pt}{-4.5607pt}\pgfsys@curveto{-3.10187pt}{-4.36955pt}{-2.95836pt}{-4.21626pt}{-2.81485pt}{-4.21626pt}\pgfsys@curveto{-2.67134pt}{-4.21626pt}{-2.52783pt}{-4.36955pt}{-2.38432pt}{-4.5607pt}\pgfsys@curveto{-2.24081pt}{-4.75185pt}{-2.0973pt}{-4.90514pt}{-1.9538pt}{-4.90514pt}\pgfsys@curveto{-1.81029pt}{-4.90514pt}{-1.66678pt}{-4.75185pt}{-1.52327pt}{-4.5607pt}\pgfsys@curveto{-1.37965pt}{-4.36955pt}{-1.23615pt}{-4.21626pt}{-1.09264pt}{-4.21626pt}\pgfsys@curveto{-0.94913pt}{-4.21626pt}{-0.80562pt}{-4.36955pt}{-0.66211pt}{-4.5607pt}\pgfsys@curveto{-0.5186pt}{-4.75185pt}{-0.37509pt}{-4.90514pt}{-0.23158pt}{-4.90514pt}\pgfsys@curveto{-0.08807pt}{-4.90514pt}{0.05544pt}{-4.75185pt}{0.19894pt}{-4.5607pt}\pgfsys@curveto{0.34256pt}{-4.36955pt}{0.48607pt}{-4.21626pt}{0.62958pt}{-4.21626pt}\pgfsys@curveto{0.77309pt}{-4.21626pt}{0.9166pt}{-4.36955pt}{1.0601pt}{-4.5607pt}\pgfsys@curveto{1.20361pt}{-4.75185pt}{1.34712pt}{-4.90514pt}{1.49063pt}{-4.90514pt}\pgfsys@curveto{1.63414pt}{-4.90514pt}{1.77765pt}{-4.75185pt}{1.92116pt}{-4.5607pt}\pgfsys@curveto{2.06477pt}{-4.36955pt}{2.20828pt}{-4.21626pt}{2.35179pt}{-4.21626pt}\pgfsys@curveto{2.4953pt}{-4.21626pt}{2.63881pt}{-4.36955pt}{2.78232pt}{-4.5607pt}\pgfsys@lineto{2.78238pt}{-4.5607pt}\pgfsys@lineto{4.5676pt}{-4.5607pt}\pgfsys@stroke\pgfsys@invoke{ }{{}{{}}{}{}{{}}{{{}}{{{}}{\pgfsys@beginscope\pgfsys@invoke{ }\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{4.7676pt}{-4.5607pt}\pgfsys@invoke{ }\pgfsys@invoke{ \lxSVG@closescope }\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}{{}}}} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope{{ {}{}{}}}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}}\epsilon,** foreach :*
6* foreach :*
7* *
8* if s_{1}\mathrel{\leavevmode\hbox to10.34pt{\vbox to13.65pt{\pgfpicture\makeatletter\hbox{\hskip 5.16759pt\lower-9.29378pt\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{ }\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ } {{}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}{}{{ {}{}}}{ {}{}} {{}{{}}}{{}{}}{}{{}{}} { }{{{{}}\pgfsys@beginscope\pgfsys@invoke{ }\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{-3.04538pt}{-2.63849pt}\pgfsys@invoke{ }\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{ }\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{{\vbox{\halign{\hfil#\hfil\cr\cr\vskip 0.017pt\cr\hbox{{\scriptstyle D_{\epsilon}^{*}}}\cr}}}} }}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} { {}{}{}}{{{}}{{}}}{{}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}{}{{ {}{}}}{ {}{}} {{}{{}}}{{}{}}{}{{}{}} { }{{{{}}\pgfsys@beginscope\pgfsys@invoke{ }\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{0.0pt}{-6.62737pt}\pgfsys@invoke{ }\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{ }\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{} }}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} {{}{{}}{}{{}}{}{ {}} {}{}}{{}{}}{}{}{}{{}}{{}}{{}{}}{{}{}} {{{{}{}{{}} }}{{}}}{{{{}{}{{}} }}{{}}{{}}} {{{{}{}{{}} }}{{}} {}{}{} {}{}{} {}{}{} {}{}{} }{{{{}{}{{}} }}{{}} {}{}{} {}{}{} {}{}{} {}{}{} }{{{{}{}{{}} }}{{}} {}{}{} {}{}{} {}{}{} {}{}{} }{{{{}{}{{}} }}{{}} {}{}{} {}{}{} {}{}{} {}{}{} }{{{{}{}{{}} }}{{}} {}{}{} {}{}{} }{{{{}{}{{}} }}{{}}}{{{{}{}{{}} }}{{}} {{}} } {{{{}{}{{}} }}{{}} }{{{{}{}{{}} }}{{}}{{}}}{}{}{}{}{{}}\pgfsys@moveto{-4.96759pt}{-4.5607pt}\pgfsys@lineto{-4.96759pt}{-4.5607pt}\pgfsys@curveto{-4.82408pt}{-4.36955pt}{-4.68057pt}{-4.21626pt}{-4.53706pt}{-4.21626pt}\pgfsys@curveto{-4.39355pt}{-4.21626pt}{-4.25005pt}{-4.36955pt}{-4.10654pt}{-4.5607pt}\pgfsys@curveto{-3.96303pt}{-4.75185pt}{-3.81952pt}{-4.90514pt}{-3.67601pt}{-4.90514pt}\pgfsys@curveto{-3.5325pt}{-4.90514pt}{-3.38899pt}{-4.75185pt}{-3.24548pt}{-4.5607pt}\pgfsys@curveto{-3.10187pt}{-4.36955pt}{-2.95836pt}{-4.21626pt}{-2.81485pt}{-4.21626pt}\pgfsys@curveto{-2.67134pt}{-4.21626pt}{-2.52783pt}{-4.36955pt}{-2.38432pt}{-4.5607pt}\pgfsys@curveto{-2.24081pt}{-4.75185pt}{-2.0973pt}{-4.90514pt}{-1.9538pt}{-4.90514pt}\pgfsys@curveto{-1.81029pt}{-4.90514pt}{-1.66678pt}{-4.75185pt}{-1.52327pt}{-4.5607pt}\pgfsys@curveto{-1.37965pt}{-4.36955pt}{-1.23615pt}{-4.21626pt}{-1.09264pt}{-4.21626pt}\pgfsys@curveto{-0.94913pt}{-4.21626pt}{-0.80562pt}{-4.36955pt}{-0.66211pt}{-4.5607pt}\pgfsys@curveto{-0.5186pt}{-4.75185pt}{-0.37509pt}{-4.90514pt}{-0.23158pt}{-4.90514pt}\pgfsys@curveto{-0.08807pt}{-4.90514pt}{0.05544pt}{-4.75185pt}{0.19894pt}{-4.5607pt}\pgfsys@curveto{0.34256pt}{-4.36955pt}{0.48607pt}{-4.21626pt}{0.62958pt}{-4.21626pt}\pgfsys@curveto{0.77309pt}{-4.21626pt}{0.9166pt}{-4.36955pt}{1.0601pt}{-4.5607pt}\pgfsys@curveto{1.20361pt}{-4.75185pt}{1.34712pt}{-4.90514pt}{1.49063pt}{-4.90514pt}\pgfsys@curveto{1.63414pt}{-4.90514pt}{1.77765pt}{-4.75185pt}{1.92116pt}{-4.5607pt}\pgfsys@curveto{2.06477pt}{-4.36955pt}{2.20828pt}{-4.21626pt}{2.35179pt}{-4.21626pt}\pgfsys@curveto{2.4953pt}{-4.21626pt}{2.63881pt}{-4.36955pt}{2.78232pt}{-4.5607pt}\pgfsys@lineto{2.78238pt}{-4.5607pt}\pgfsys@lineto{4.5676pt}{-4.5607pt}\pgfsys@stroke\pgfsys@invoke{ }{{}{{}}{}{}{{}}{{{}}{{{}}{\pgfsys@beginscope\pgfsys@invoke{ }\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{4.7676pt}{-4.5607pt}\pgfsys@invoke{ }\pgfsys@invoke{ \lxSVG@closescope }\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}{{}}}} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope{{ {}{}{}}}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}}\epsilon,** foreach :*
9* foreach :*
10* *
11* *
12* return *
Nested iteration in Algorithm 3 could be implemented using bounded recursion. However, the only reason for the nesting is taking derivatives by successive nullable states (a state is nullable if s\mathrel{\leavevmode\hbox to10.34pt{\vbox to13.65pt{\pgfpicture\makeatletter\hbox{\hskip 5.16759pt\lower-9.29378pt\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{ }\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ } {{}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}{}{{ {}{}}}{ {}{}} {{}{{}}}{{}{}}{}{{}{}} { }{{{{}}\pgfsys@beginscope\pgfsys@invoke{ }\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{-3.04538pt}{-2.63849pt}\pgfsys@invoke{ }\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{ }\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{{\vbox{\halign{\hfil#\hfil\cr\cr\vskip 0.017pt\cr\hbox{{\scriptstyle D_{\epsilon}^{*}}}\cr}}}} }}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} { {}{}{}}{{{}}{{}}}{{}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}{}{{ {}{}}}{ {}{}} {{}{{}}}{{}{}}{}{{}{}} { }{{{{}}\pgfsys@beginscope\pgfsys@invoke{ }\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{0.0pt}{-6.62737pt}\pgfsys@invoke{ }\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{ }\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{} }}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} {{}{{}}{}{{}}{}{ {}} {}{}}{{}{}}{}{}{}{{}}{{}}{{}{}}{{}{}} {{{{}{}{{}} }}{{}}}{{{{}{}{{}} }}{{}}{{}}} {{{{}{}{{}} }}{{}} {}{}{} {}{}{} {}{}{} {}{}{} }{{{{}{}{{}} }}{{}} {}{}{} {}{}{} {}{}{} {}{}{} }{{{{}{}{{}} }}{{}} {}{}{} {}{}{} {}{}{} {}{}{} }{{{{}{}{{}} }}{{}} {}{}{} {}{}{} {}{}{} {}{}{} }{{{{}{}{{}} }}{{}} {}{}{} {}{}{} }{{{{}{}{{}} }}{{}}}{{{{}{}{{}} }}{{}} {{}} } {{{{}{}{{}} }}{{}} }{{{{}{}{{}} }}{{}}{{}}}{}{}{}{}{{}}\pgfsys@moveto{-4.96759pt}{-4.5607pt}\pgfsys@lineto{-4.96759pt}{-4.5607pt}\pgfsys@curveto{-4.82408pt}{-4.36955pt}{-4.68057pt}{-4.21626pt}{-4.53706pt}{-4.21626pt}\pgfsys@curveto{-4.39355pt}{-4.21626pt}{-4.25005pt}{-4.36955pt}{-4.10654pt}{-4.5607pt}\pgfsys@curveto{-3.96303pt}{-4.75185pt}{-3.81952pt}{-4.90514pt}{-3.67601pt}{-4.90514pt}\pgfsys@curveto{-3.5325pt}{-4.90514pt}{-3.38899pt}{-4.75185pt}{-3.24548pt}{-4.5607pt}\pgfsys@curveto{-3.10187pt}{-4.36955pt}{-2.95836pt}{-4.21626pt}{-2.81485pt}{-4.21626pt}\pgfsys@curveto{-2.67134pt}{-4.21626pt}{-2.52783pt}{-4.36955pt}{-2.38432pt}{-4.5607pt}\pgfsys@curveto{-2.24081pt}{-4.75185pt}{-2.0973pt}{-4.90514pt}{-1.9538pt}{-4.90514pt}\pgfsys@curveto{-1.81029pt}{-4.90514pt}{-1.66678pt}{-4.75185pt}{-1.52327pt}{-4.5607pt}\pgfsys@curveto{-1.37965pt}{-4.36955pt}{-1.23615pt}{-4.21626pt}{-1.09264pt}{-4.21626pt}\pgfsys@curveto{-0.94913pt}{-4.21626pt}{-0.80562pt}{-4.36955pt}{-0.66211pt}{-4.5607pt}\pgfsys@curveto{-0.5186pt}{-4.75185pt}{-0.37509pt}{-4.90514pt}{-0.23158pt}{-4.90514pt}\pgfsys@curveto{-0.08807pt}{-4.90514pt}{0.05544pt}{-4.75185pt}{0.19894pt}{-4.5607pt}\pgfsys@curveto{0.34256pt}{-4.36955pt}{0.48607pt}{-4.21626pt}{0.62958pt}{-4.21626pt}\pgfsys@curveto{0.77309pt}{-4.21626pt}{0.9166pt}{-4.36955pt}{1.0601pt}{-4.5607pt}\pgfsys@curveto{1.20361pt}{-4.75185pt}{1.34712pt}{-4.90514pt}{1.49063pt}{-4.90514pt}\pgfsys@curveto{1.63414pt}{-4.90514pt}{1.77765pt}{-4.75185pt}{1.92116pt}{-4.5607pt}\pgfsys@curveto{2.06477pt}{-4.36955pt}{2.20828pt}{-4.21626pt}{2.35179pt}{-4.21626pt}\pgfsys@curveto{2.4953pt}{-4.21626pt}{2.63881pt}{-4.36955pt}{2.78232pt}{-4.5607pt}\pgfsys@lineto{2.78238pt}{-4.5607pt}\pgfsys@lineto{4.5676pt}{-4.5607pt}\pgfsys@stroke\pgfsys@invoke{ }{{}{{}}{}{}{{}}{{{}}{{{}}{\pgfsys@beginscope\pgfsys@invoke{ }\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{4.7676pt}{-4.5607pt}\pgfsys@invoke{ }\pgfsys@invoke{ \lxSVG@closescope }\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}{{}}}} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope{{ {}{}{}}}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}}\epsilon). Let us therefore introduce a condition on languages, requiring all nullable states to be (optionally) skipped:
Definition 6**.**
A language is null-closed if for each S\ni s\mathrel{\leavevmode\hbox to10.34pt{\vbox to13.65pt{\pgfpicture\makeatletter\hbox{\hskip 5.16759pt\lower-9.29378pt\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{ }\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ } {{}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}{}{{ {}{}}}{ {}{}} {{}{{}}}{{}{}}{}{{}{}} { }{{{{}}\pgfsys@beginscope\pgfsys@invoke{ }\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{-3.04538pt}{-2.63849pt}\pgfsys@invoke{ }\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{ }\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{{\vbox{\halign{\hfil#\hfil\cr\cr\vskip 0.017pt\cr\hbox{{\scriptstyle D_{\epsilon}^{}}}\cr}}}} }}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} { {}{}{}}{{{}}{{}}}{{}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}{}{{ {}{}}}{ {}{}} {{}{{}}}{{}{}}{}{{}{}} { }{{{{}}\pgfsys@beginscope\pgfsys@invoke{ }\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{0.0pt}{-6.62737pt}\pgfsys@invoke{ }\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{ }\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{} }}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} {{}{{}}{}{{}}{}{ {}} {}{}}{{}{}}{}{}{}{{}}{{}}{{}{}}{{}{}} {{{{}{}{{}} }}{{}}}{{{{}{}{{}} }}{{}}{{}}} {{{{}{}{{}} }}{{}} {}{}{} {}{}{} {}{}{} {}{}{} }{{{{}{}{{}} }}{{}} {}{}{} {}{}{} {}{}{} {}{}{} }{{{{}{}{{}} }}{{}} {}{}{} {}{}{} {}{}{} {}{}{} }{{{{}{}{{}} }}{{}} {}{}{} {}{}{} {}{}{} {}{}{} }{{{{}{}{{}} }}{{}} {}{}{} {}{}{} }{{{{}{}{{}} }}{{}}}{{{{}{}{{}} }}{{}} {{}} } {{{{}{}{{}} }}{{}} }{{{{}{}{{}} }}{{}}{{}}}{}{}{}{}{{}}\pgfsys@moveto{-4.96759pt}{-4.5607pt}\pgfsys@lineto{-4.96759pt}{-4.5607pt}\pgfsys@curveto{-4.82408pt}{-4.36955pt}{-4.68057pt}{-4.21626pt}{-4.53706pt}{-4.21626pt}\pgfsys@curveto{-4.39355pt}{-4.21626pt}{-4.25005pt}{-4.36955pt}{-4.10654pt}{-4.5607pt}\pgfsys@curveto{-3.96303pt}{-4.75185pt}{-3.81952pt}{-4.90514pt}{-3.67601pt}{-4.90514pt}\pgfsys@curveto{-3.5325pt}{-4.90514pt}{-3.38899pt}{-4.75185pt}{-3.24548pt}{-4.5607pt}\pgfsys@curveto{-3.10187pt}{-4.36955pt}{-2.95836pt}{-4.21626pt}{-2.81485pt}{-4.21626pt}\pgfsys@curveto{-2.67134pt}{-4.21626pt}{-2.52783pt}{-4.36955pt}{-2.38432pt}{-4.5607pt}\pgfsys@curveto{-2.24081pt}{-4.75185pt}{-2.0973pt}{-4.90514pt}{-1.9538pt}{-4.90514pt}\pgfsys@curveto{-1.81029pt}{-4.90514pt}{-1.66678pt}{-4.75185pt}{-1.52327pt}{-4.5607pt}\pgfsys@curveto{-1.37965pt}{-4.36955pt}{-1.23615pt}{-4.21626pt}{-1.09264pt}{-4.21626pt}\pgfsys@curveto{-0.94913pt}{-4.21626pt}{-0.80562pt}{-4.36955pt}{-0.66211pt}{-4.5607pt}\pgfsys@curveto{-0.5186pt}{-4.75185pt}{-0.37509pt}{-4.90514pt}{-0.23158pt}{-4.90514pt}\pgfsys@curveto{-0.08807pt}{-4.90514pt}{0.05544pt}{-4.75185pt}{0.19894pt}{-4.5607pt}\pgfsys@curveto{0.34256pt}{-4.36955pt}{0.48607pt}{-4.21626pt}{0.62958pt}{-4.21626pt}\pgfsys@curveto{0.77309pt}{-4.21626pt}{0.9166pt}{-4.36955pt}{1.0601pt}{-4.5607pt}\pgfsys@curveto{1.20361pt}{-4.75185pt}{1.34712pt}{-4.90514pt}{1.49063pt}{-4.90514pt}\pgfsys@curveto{1.63414pt}{-4.90514pt}{1.77765pt}{-4.75185pt}{1.92116pt}{-4.5607pt}\pgfsys@curveto{2.06477pt}{-4.36955pt}{2.20828pt}{-4.21626pt}{2.35179pt}{-4.21626pt}\pgfsys@curveto{2.4953pt}{-4.21626pt}{2.63881pt}{-4.36955pt}{2.78232pt}{-4.5607pt}\pgfsys@lineto{2.78238pt}{-4.5607pt}\pgfsys@lineto{4.5676pt}{-4.5607pt}\pgfsys@stroke\pgfsys@invoke{ }{{}{{}}{}{}{{}}{{{}}{{{}}{\pgfsys@beginscope\pgfsys@invoke{ }\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{4.7676pt}{-4.5607pt}\pgfsys@invoke{ }\pgfsys@invoke{ \lxSVG@closescope }\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}{{}}}} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope{{ {}{}{}}}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}}\epsilon and we have*
[TABLE]
The null closure of a language is the smallest null-closed language .
Now, for null-closed , the phase algorithm can be rewritten as Algorithm 4. Lines 5–7 are necessary because the state could have entered the language “in the middle” of a call-reduce closure, and thus might itself not have been call-reduce closed.
Algorithm 4**.**
Calculating for null-closed
1* *
2* foreach :*
3* foreach :*
4* *
5* if t\mathrel{\leavevmode\hbox to10.34pt{\vbox to13.65pt{\pgfpicture\makeatletter\hbox{\hskip 5.16759pt\lower-9.29378pt\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{ }\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ } {{}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}{}{{ {}{}}}{ {}{}} {{}{{}}}{{}{}}{}{{}{}} { }{{{{}}\pgfsys@beginscope\pgfsys@invoke{ }\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{-3.04538pt}{-2.63849pt}\pgfsys@invoke{ }\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{ }\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{{\vbox{\halign{\hfil#\hfil\cr\cr\vskip 0.017pt\cr\hbox{{\scriptstyle D_{\epsilon}^{*}}}\cr}}}} }}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} { {}{}{}}{{{}}{{}}}{{}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}{}{{ {}{}}}{ {}{}} {{}{{}}}{{}{}}{}{{}{}} { }{{{{}}\pgfsys@beginscope\pgfsys@invoke{ }\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{0.0pt}{-6.62737pt}\pgfsys@invoke{ }\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{ }\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{} }}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} {{}{{}}{}{{}}{}{ {}} {}{}}{{}{}}{}{}{}{{}}{{}}{{}{}}{{}{}} {{{{}{}{{}} }}{{}}}{{{{}{}{{}} }}{{}}{{}}} {{{{}{}{{}} }}{{}} {}{}{} {}{}{} {}{}{} {}{}{} }{{{{}{}{{}} }}{{}} {}{}{} {}{}{} {}{}{} {}{}{} }{{{{}{}{{}} }}{{}} {}{}{} {}{}{} {}{}{} {}{}{} }{{{{}{}{{}} }}{{}} {}{}{} {}{}{} {}{}{} {}{}{} }{{{{}{}{{}} }}{{}} {}{}{} {}{}{} }{{{{}{}{{}} }}{{}}}{{{{}{}{{}} }}{{}} {{}} } {{{{}{}{{}} }}{{}} }{{{{}{}{{}} }}{{}}{{}}}{}{}{}{}{{}}\pgfsys@moveto{-4.96759pt}{-4.5607pt}\pgfsys@lineto{-4.96759pt}{-4.5607pt}\pgfsys@curveto{-4.82408pt}{-4.36955pt}{-4.68057pt}{-4.21626pt}{-4.53706pt}{-4.21626pt}\pgfsys@curveto{-4.39355pt}{-4.21626pt}{-4.25005pt}{-4.36955pt}{-4.10654pt}{-4.5607pt}\pgfsys@curveto{-3.96303pt}{-4.75185pt}{-3.81952pt}{-4.90514pt}{-3.67601pt}{-4.90514pt}\pgfsys@curveto{-3.5325pt}{-4.90514pt}{-3.38899pt}{-4.75185pt}{-3.24548pt}{-4.5607pt}\pgfsys@curveto{-3.10187pt}{-4.36955pt}{-2.95836pt}{-4.21626pt}{-2.81485pt}{-4.21626pt}\pgfsys@curveto{-2.67134pt}{-4.21626pt}{-2.52783pt}{-4.36955pt}{-2.38432pt}{-4.5607pt}\pgfsys@curveto{-2.24081pt}{-4.75185pt}{-2.0973pt}{-4.90514pt}{-1.9538pt}{-4.90514pt}\pgfsys@curveto{-1.81029pt}{-4.90514pt}{-1.66678pt}{-4.75185pt}{-1.52327pt}{-4.5607pt}\pgfsys@curveto{-1.37965pt}{-4.36955pt}{-1.23615pt}{-4.21626pt}{-1.09264pt}{-4.21626pt}\pgfsys@curveto{-0.94913pt}{-4.21626pt}{-0.80562pt}{-4.36955pt}{-0.66211pt}{-4.5607pt}\pgfsys@curveto{-0.5186pt}{-4.75185pt}{-0.37509pt}{-4.90514pt}{-0.23158pt}{-4.90514pt}\pgfsys@curveto{-0.08807pt}{-4.90514pt}{0.05544pt}{-4.75185pt}{0.19894pt}{-4.5607pt}\pgfsys@curveto{0.34256pt}{-4.36955pt}{0.48607pt}{-4.21626pt}{0.62958pt}{-4.21626pt}\pgfsys@curveto{0.77309pt}{-4.21626pt}{0.9166pt}{-4.36955pt}{1.0601pt}{-4.5607pt}\pgfsys@curveto{1.20361pt}{-4.75185pt}{1.34712pt}{-4.90514pt}{1.49063pt}{-4.90514pt}\pgfsys@curveto{1.63414pt}{-4.90514pt}{1.77765pt}{-4.75185pt}{1.92116pt}{-4.5607pt}\pgfsys@curveto{2.06477pt}{-4.36955pt}{2.20828pt}{-4.21626pt}{2.35179pt}{-4.21626pt}\pgfsys@curveto{2.4953pt}{-4.21626pt}{2.63881pt}{-4.36955pt}{2.78232pt}{-4.5607pt}\pgfsys@lineto{2.78238pt}{-4.5607pt}\pgfsys@lineto{4.5676pt}{-4.5607pt}\pgfsys@stroke\pgfsys@invoke{ }{{}{{}}{}{}{{}}{{{}}{{{}}{\pgfsys@beginscope\pgfsys@invoke{ }\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{4.7676pt}{-4.5607pt}\pgfsys@invoke{ }\pgfsys@invoke{ \lxSVG@closescope }\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}{{}}}} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope{{ {}{}{}}}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}}\epsilon,** foreach :*
6* foreach :*
7* *
8* return *
We would now like to take Algorithm 1 and replace all call-reduce closures by their null closures. The correctness of such change needs to be justified—we do so by the following reasoning.
Lemma 1** (Canonical decomposition).**
Every viable sequence of non-shift transitions can be uniquely decomposed into two parts:
- •
reductive* , which nulls some configuration, i.e., S^{*}\ni\sigma_{\scriptscriptstyle-}\mathrel{\leavevmode\hbox to8.09pt{\vbox to11.89pt{\pgfpicture\makeatletter\hbox{\hskip 4.04582pt\lower-8.41377pt\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{ }\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ } {{}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}{}{{ {}{}}}{ {}{}} {{}{{}}}{{}{}}{}{{}{}} { }{{{{}}\pgfsys@beginscope\pgfsys@invoke{ }\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{-1.92361pt}{-1.75848pt}\pgfsys@invoke{ }\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{ }\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{{\vbox{\halign{\hfil#\hfil\cr\cr\vskip 0.017pt\cr\hbox{{\scriptstyle\eta_{\scriptscriptstyle-}}}\cr}}}} }}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} { {}{}{}}{{{}}{{}}}{{}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}{}{{ {}{}}}{ {}{}} {{}{{}}}{{}{}}{}{{}{}} { }{{{{}}\pgfsys@beginscope\pgfsys@invoke{ }\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{0.0pt}{-5.74736pt}\pgfsys@invoke{ }\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{ }\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{} }}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} {{}{{}}{}{{}}{}{ {}} {}{}}{{}{}}{}{}{}{{}}{{}}{{}{}}{{}{}} {{{{}{}{{}} }}{{}}}{{{{}{}{{}} }}{{}}{{}}} {{{{}{}{{}} }}{{}} {}{}{} {}{}{} {}{}{} {}{}{} }{{{{}{}{{}} }}{{}} {}{}{} {}{}{} {}{}{} {}{}{} }{{{{}{}{{}} }}{{}} {}{}{} {}{}{} {}{}{} {}{}{} }{{{{}{}{{}} }}{{}} {}{}{} {}{}{} }{{{{}{}{{}} }}{{}}}{{{{}{}{{}} }}{{}} {{}} } {{{{}{}{{}} }}{{}} }{{{{}{}{{}} }}{{}}{{}}}{}{}{}{}{{}}\pgfsys@moveto{-3.84583pt}{-3.6807pt}\pgfsys@lineto{-3.84583pt}{-3.6807pt}\pgfsys@curveto{-3.70232pt}{-3.48955pt}{-3.5588pt}{-3.33626pt}{-3.4153pt}{-3.33626pt}\pgfsys@curveto{-3.27179pt}{-3.33626pt}{-3.12828pt}{-3.48955pt}{-2.98477pt}{-3.6807pt}\pgfsys@curveto{-2.84126pt}{-3.87184pt}{-2.69775pt}{-4.02513pt}{-2.55424pt}{-4.02513pt}\pgfsys@curveto{-2.41074pt}{-4.02513pt}{-2.26723pt}{-3.87184pt}{-2.12372pt}{-3.6807pt}\pgfsys@curveto{-1.9801pt}{-3.48955pt}{-1.8366pt}{-3.33626pt}{-1.69308pt}{-3.33626pt}\pgfsys@curveto{-1.54958pt}{-3.33626pt}{-1.40607pt}{-3.48955pt}{-1.26256pt}{-3.6807pt}\pgfsys@curveto{-1.11905pt}{-3.87184pt}{-0.97554pt}{-4.02513pt}{-0.83203pt}{-4.02513pt}\pgfsys@curveto{-0.68852pt}{-4.02513pt}{-0.54501pt}{-3.87184pt}{-0.4015pt}{-3.6807pt}\pgfsys@curveto{-0.25789pt}{-3.48955pt}{-0.11438pt}{-3.33626pt}{0.02913pt}{-3.33626pt}\pgfsys@curveto{0.17264pt}{-3.33626pt}{0.31615pt}{-3.48955pt}{0.45966pt}{-3.6807pt}\pgfsys@curveto{0.60316pt}{-3.87184pt}{0.74667pt}{-4.02513pt}{0.89018pt}{-4.02513pt}\pgfsys@curveto{1.03369pt}{-4.02513pt}{1.1772pt}{-3.87184pt}{1.32071pt}{-3.6807pt}\pgfsys@curveto{1.46432pt}{-3.48955pt}{1.60783pt}{-3.33626pt}{1.75134pt}{-3.33626pt}\pgfsys@curveto{1.89485pt}{-3.33626pt}{2.03836pt}{-3.48955pt}{2.18187pt}{-3.6807pt}\pgfsys@lineto{2.18193pt}{-3.6807pt}\pgfsys@lineto{3.44583pt}{-3.6807pt}\pgfsys@stroke\pgfsys@invoke{ }{{}{{}}{}{}{{}}{{{}}{{{}}{\pgfsys@beginscope\pgfsys@invoke{ }\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{3.64583pt}{-3.6807pt}\pgfsys@invoke{ }\pgfsys@invoke{ \lxSVG@closescope }\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}{{}}}} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope{{ {}{}{}}}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}}\epsilon, and*
- •
nonreductive* , which does not null some configuration consisting of a single state, i.e., S\ni s_{\scriptscriptstyle+}\mathrel{\leavevmode\hbox to9.51pt{\vbox to12.01pt{\pgfpicture\makeatletter\hbox{\hskip 4.75693pt\lower-8.46933pt\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{ }\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ } {{}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}{}{{ {}{}}}{ {}{}} {{}{{}}}{{}{}}{}{{}{}} { }{{{{}}\pgfsys@beginscope\pgfsys@invoke{ }\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{-2.63472pt}{-1.81404pt}\pgfsys@invoke{ }\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{ }\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{{\vbox{\halign{\hfil#\hfil\cr\cr\vskip 0.017pt\cr\hbox{{\scriptstyle\eta_{\scriptscriptstyle+}}}\cr}}}} }}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} { {}{}{}}{{{}}{{}}}{{}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}{}{{ {}{}}}{ {}{}} {{}{{}}}{{}{}}{}{{}{}} { }{{{{}}\pgfsys@beginscope\pgfsys@invoke{ }\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{0.0pt}{-5.80292pt}\pgfsys@invoke{ }\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{ }\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{} }}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} {{}{{}}{}{{}}{}{ {}} {}{}}{{}{}}{}{}{}{{}}{{}}{{}{}}{{}{}} {{{{}{}{{}} }}{{}}}{{{{}{}{{}} }}{{}}{{}}} {{{{}{}{{}} }}{{}} {}{}{} {}{}{} {}{}{} {}{}{} }{{{{}{}{{}} }}{{}} {}{}{} {}{}{} {}{}{} {}{}{} }{{{{}{}{{}} }}{{}} {}{}{} {}{}{} {}{}{} {}{}{} }{{{{}{}{{}} }}{{}} {}{}{} {}{}{} }{{{{}{}{{}} }}{{}}}{{{{}{}{{}} }}{{}} {{}} } {{{{}{}{{}} }}{{}} }{{{{}{}{{}} }}{{}}{{}}}{}{}{}{}{{}}\pgfsys@moveto{-4.55693pt}{-3.73625pt}\pgfsys@lineto{-4.55693pt}{-3.73625pt}\pgfsys@curveto{-4.41342pt}{-3.5451pt}{-4.26991pt}{-3.39182pt}{-4.1264pt}{-3.39182pt}\pgfsys@curveto{-3.9829pt}{-3.39182pt}{-3.83939pt}{-3.5451pt}{-3.69588pt}{-3.73625pt}\pgfsys@curveto{-3.55237pt}{-3.9274pt}{-3.40886pt}{-4.08069pt}{-3.26535pt}{-4.08069pt}\pgfsys@curveto{-3.12184pt}{-4.08069pt}{-2.97833pt}{-3.9274pt}{-2.83482pt}{-3.73625pt}\pgfsys@curveto{-2.69121pt}{-3.5451pt}{-2.5477pt}{-3.39182pt}{-2.40419pt}{-3.39182pt}\pgfsys@curveto{-2.26068pt}{-3.39182pt}{-2.11717pt}{-3.5451pt}{-1.97366pt}{-3.73625pt}\pgfsys@curveto{-1.83015pt}{-3.9274pt}{-1.68665pt}{-4.08069pt}{-1.54314pt}{-4.08069pt}\pgfsys@curveto{-1.39963pt}{-4.08069pt}{-1.25612pt}{-3.9274pt}{-1.11261pt}{-3.73625pt}\pgfsys@curveto{-0.969pt}{-3.5451pt}{-0.82549pt}{-3.39182pt}{-0.68198pt}{-3.39182pt}\pgfsys@curveto{-0.53847pt}{-3.39182pt}{-0.39496pt}{-3.5451pt}{-0.25145pt}{-3.73625pt}\pgfsys@curveto{-0.10794pt}{-3.9274pt}{0.03557pt}{-4.08069pt}{0.17908pt}{-4.08069pt}\pgfsys@curveto{0.32259pt}{-4.08069pt}{0.4661pt}{-3.9274pt}{0.6096pt}{-3.73625pt}\pgfsys@curveto{0.75322pt}{-3.5451pt}{0.89673pt}{-3.39182pt}{1.04024pt}{-3.39182pt}\pgfsys@curveto{1.18375pt}{-3.39182pt}{1.32726pt}{-3.5451pt}{1.47076pt}{-3.73625pt}\pgfsys@lineto{1.47083pt}{-3.73625pt}\pgfsys@lineto{4.15694pt}{-3.73625pt}\pgfsys@stroke\pgfsys@invoke{ }{{}{{}}{}{}{{}}{{{}}{{{}}{\pgfsys@beginscope\pgfsys@invoke{ }\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{4.35693pt}{-3.73625pt}\pgfsys@invoke{ }\pgfsys@invoke{ \lxSVG@closescope }\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}{{}}}} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope{{ {}{}{}}}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}}\sigma_{\scriptscriptstyle+}\in S^{+}.*
Proof.
The proof is by induction on the length of . If , the decomposition is (with ) and (with being any state in ).
Otherwise, let be the source state of the first transition in . If s_{0}\mathrel{\leavevmode\hbox to7.02pt{\vbox to11.89pt{\pgfpicture\makeatletter\hbox{\hskip 3.51248pt\lower-8.41377pt\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{ }\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ } {{}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}{}{{ {}{}}}{ {}{}} {{}{{}}}{{}{}}{}{{}{}} { }{{{{}}\pgfsys@beginscope\pgfsys@invoke{ }\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{-1.39027pt}{-1.75848pt}\pgfsys@invoke{ }\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{ }\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{{\vbox{\halign{\hfil#\hfil\cr\cr\vskip 0.017pt\cr\hbox{{\scriptstyle\eta}}\cr}}}} }}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} { {}{}{}}{{{}}{{}}}{{}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}{}{{ {}{}}}{ {}{}} {{}{{}}}{{}{}}{}{{}{}} { }{{{{}}\pgfsys@beginscope\pgfsys@invoke{ }\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{0.0pt}{-5.74736pt}\pgfsys@invoke{ }\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{ }\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{} }}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} {{}{{}}{}{{}}{}{ {}} {}{}}{{}{}}{}{}{}{{}}{{}}{{}{}}{{}{}} {{{{}{}{{}} }}{{}}}{{{{}{}{{}} }}{{}}{{}}} {{{{}{}{{}} }}{{}} {}{}{} {}{}{} {}{}{} {}{}{} }{{{{}{}{{}} }}{{}} {}{}{} {}{}{} {}{}{} {}{}{} }{{{{}{}{{}} }}{{}} {}{}{} {}{}{} }{{{{}{}{{}} }}{{}}}{{{{}{}{{}} }}{{}} {{}} } {{{{}{}{{}} }}{{}} }{{{{}{}{{}} }}{{}}{{}}}{}{}{}{}{{}}\pgfsys@moveto{-3.31248pt}{-3.6807pt}\pgfsys@lineto{-3.31248pt}{-3.6807pt}\pgfsys@curveto{-3.16898pt}{-3.48955pt}{-3.02547pt}{-3.33626pt}{-2.88196pt}{-3.33626pt}\pgfsys@curveto{-2.73845pt}{-3.33626pt}{-2.59494pt}{-3.48955pt}{-2.45143pt}{-3.6807pt}\pgfsys@curveto{-2.30792pt}{-3.87184pt}{-2.16441pt}{-4.02513pt}{-2.0209pt}{-4.02513pt}\pgfsys@curveto{-1.8774pt}{-4.02513pt}{-1.73389pt}{-3.87184pt}{-1.59038pt}{-3.6807pt}\pgfsys@curveto{-1.44676pt}{-3.48955pt}{-1.30325pt}{-3.33626pt}{-1.15974pt}{-3.33626pt}\pgfsys@curveto{-1.01624pt}{-3.33626pt}{-0.87273pt}{-3.48955pt}{-0.72922pt}{-3.6807pt}\pgfsys@curveto{-0.58571pt}{-3.87184pt}{-0.4422pt}{-4.02513pt}{-0.29869pt}{-4.02513pt}\pgfsys@curveto{-0.15518pt}{-4.02513pt}{-0.01167pt}{-3.87184pt}{0.13184pt}{-3.6807pt}\pgfsys@curveto{0.27545pt}{-3.48955pt}{0.41896pt}{-3.33626pt}{0.56247pt}{-3.33626pt}\pgfsys@curveto{0.70598pt}{-3.33626pt}{0.84949pt}{-3.48955pt}{0.993pt}{-3.6807pt}\pgfsys@lineto{0.99306pt}{-3.6807pt}\pgfsys@lineto{2.91249pt}{-3.6807pt}\pgfsys@stroke\pgfsys@invoke{ }{{}{{}}{}{}{{}}{{{}}{{{}}{\pgfsys@beginscope\pgfsys@invoke{ }\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{3.11249pt}{-3.6807pt}\pgfsys@invoke{ }\pgfsys@invoke{ \lxSVG@closescope }\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}{{}}}} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope{{ {}{}{}}}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}}\sigma_{\scriptscriptstyle+} for some , the decomposition is and (with ). Otherwise, let with being the longest prefix of valid from . It must be that s_{0}\mathrel{\leavevmode\hbox to8.62pt{\vbox to11.89pt{\pgfpicture\makeatletter\hbox{\hskip 4.31248pt\lower-8.41377pt\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{ }\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ } {{}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}{}{{ {}{}}}{ {}{}} {{}{{}}}{{}{}}{}{{}{}} { }{{{{}}\pgfsys@beginscope\pgfsys@invoke{ }\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{-2.19028pt}{-1.75848pt}\pgfsys@invoke{ }\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{ }\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{{\vbox{\halign{\hfil#\hfil\cr\cr\vskip 0.017pt\cr\hbox{{\scriptstyle\eta_{0}}}\cr}}}} }}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} { {}{}{}}{{{}}{{}}}{{}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}{}{{ {}{}}}{ {}{}} {{}{{}}}{{}{}}{}{{}{}} { }{{{{}}\pgfsys@beginscope\pgfsys@invoke{ }\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{0.0pt}{-5.74736pt}\pgfsys@invoke{ }\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{ }\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{} }}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} {{}{{}}{}{{}}{}{ {}} {}{}}{{}{}}{}{}{}{{}}{{}}{{}{}}{{}{}} {{{{}{}{{}} }}{{}}}{{{{}{}{{}} }}{{}}{{}}} {{{{}{}{{}} }}{{}} {}{}{} {}{}{} {}{}{} {}{}{} }{{{{}{}{{}} }}{{}} {}{}{} {}{}{} {}{}{} {}{}{} }{{{{}{}{{}} }}{{}} {}{}{} {}{}{} {}{}{} {}{}{} }{{{{}{}{{}} }}{{}} {}{}{} {}{}{} }{{{{}{}{{}} }}{{}}}{{{{}{}{{}} }}{{}} {{}} } {{{{}{}{{}} }}{{}} }{{{{}{}{{}} }}{{}}{{}}}{}{}{}{}{{}}\pgfsys@moveto{-4.11249pt}{-3.6807pt}\pgfsys@lineto{-4.11249pt}{-3.6807pt}\pgfsys@curveto{-3.96898pt}{-3.48955pt}{-3.82547pt}{-3.33626pt}{-3.68196pt}{-3.33626pt}\pgfsys@curveto{-3.53845pt}{-3.33626pt}{-3.39494pt}{-3.48955pt}{-3.25143pt}{-3.6807pt}\pgfsys@curveto{-3.10793pt}{-3.87184pt}{-2.96442pt}{-4.02513pt}{-2.8209pt}{-4.02513pt}\pgfsys@curveto{-2.6774pt}{-4.02513pt}{-2.53389pt}{-3.87184pt}{-2.39038pt}{-3.6807pt}\pgfsys@curveto{-2.24677pt}{-3.48955pt}{-2.10326pt}{-3.33626pt}{-1.95975pt}{-3.33626pt}\pgfsys@curveto{-1.81624pt}{-3.33626pt}{-1.67273pt}{-3.48955pt}{-1.52922pt}{-3.6807pt}\pgfsys@curveto{-1.38571pt}{-3.87184pt}{-1.2422pt}{-4.02513pt}{-1.0987pt}{-4.02513pt}\pgfsys@curveto{-0.95518pt}{-4.02513pt}{-0.81168pt}{-3.87184pt}{-0.66817pt}{-3.6807pt}\pgfsys@curveto{-0.52455pt}{-3.48955pt}{-0.38104pt}{-3.33626pt}{-0.23753pt}{-3.33626pt}\pgfsys@curveto{-0.09402pt}{-3.33626pt}{0.04948pt}{-3.48955pt}{0.193pt}{-3.6807pt}\pgfsys@curveto{0.3365pt}{-3.87184pt}{0.48001pt}{-4.02513pt}{0.62352pt}{-4.02513pt}\pgfsys@curveto{0.76703pt}{-4.02513pt}{0.91054pt}{-3.87184pt}{1.05405pt}{-3.6807pt}\pgfsys@curveto{1.19766pt}{-3.48955pt}{1.34117pt}{-3.33626pt}{1.48468pt}{-3.33626pt}\pgfsys@curveto{1.62819pt}{-3.33626pt}{1.7717pt}{-3.48955pt}{1.9152pt}{-3.6807pt}\pgfsys@lineto{1.91527pt}{-3.6807pt}\pgfsys@lineto{3.7125pt}{-3.6807pt}\pgfsys@stroke\pgfsys@invoke{ }{{}{{}}{}{}{{}}{{{}}{{{}}{\pgfsys@beginscope\pgfsys@invoke{ }\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{3.91249pt}{-3.6807pt}\pgfsys@invoke{ }\pgfsys@invoke{ \lxSVG@closescope }\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}{{}}}} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope{{ {}{}{}}}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}}\epsilon. Use the induction hypothesis to decompose (witnessed by , and ), and set (with ) and (with and ).
Uniqueness follows by the same induction from the fact that no proper prefix of nulls . ∎
Lemma 2**.**
* for every call-reduce-closed language .*
Proof.
Every configuration in comes from
[TABLE]
Then there must exist with and . As is call-reduce-closed, we have , from which and as desired. ∎
Lemma 3**.**
* for every language .*
Proof.
Every configuration in comes from
[TABLE]
Let be the canonical decomposition of , witnessed by , and . If , then with and for some . Then \sigma_{1}\mathrel{\leavevmode\hbox to10.34pt{\vbox to13.65pt{\pgfpicture\makeatletter\hbox{\hskip 5.16759pt\lower-9.29378pt\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{ }\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ } {{}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}{}{{ {}{}}}{ {}{}} {{}{{}}}{{}{}}{}{{}{}} { }{{{{}}\pgfsys@beginscope\pgfsys@invoke{ }\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{-3.04538pt}{-2.63849pt}\pgfsys@invoke{ }\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{ }\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{{\vbox{\halign{\hfil#\hfil\cr\cr\vskip 0.017pt\cr\hbox{{\scriptstyle D_{\epsilon}^{*}}}\cr}}}} }}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} { {}{}{}}{{{}}{{}}}{{}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}{}{{ {}{}}}{ {}{}} {{}{{}}}{{}{}}{}{{}{}} { }{{{{}}\pgfsys@beginscope\pgfsys@invoke{ }\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{0.0pt}{-6.62737pt}\pgfsys@invoke{ }\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{ }\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{} }}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} {{}{{}}{}{{}}{}{ {}} {}{}}{{}{}}{}{}{}{{}}{{}}{{}{}}{{}{}} {{{{}{}{{}} }}{{}}}{{{{}{}{{}} }}{{}}{{}}} {{{{}{}{{}} }}{{}} {}{}{} {}{}{} {}{}{} {}{}{} }{{{{}{}{{}} }}{{}} {}{}{} {}{}{} {}{}{} {}{}{} }{{{{}{}{{}} }}{{}} {}{}{} {}{}{} {}{}{} {}{}{} }{{{{}{}{{}} }}{{}} {}{}{} {}{}{} {}{}{} {}{}{} }{{{{}{}{{}} }}{{}} {}{}{} {}{}{} }{{{{}{}{{}} }}{{}}}{{{{}{}{{}} }}{{}} {{}} } {{{{}{}{{}} }}{{}} }{{{{}{}{{}} }}{{}}{{}}}{}{}{}{}{{}}\pgfsys@moveto{-4.96759pt}{-4.5607pt}\pgfsys@lineto{-4.96759pt}{-4.5607pt}\pgfsys@curveto{-4.82408pt}{-4.36955pt}{-4.68057pt}{-4.21626pt}{-4.53706pt}{-4.21626pt}\pgfsys@curveto{-4.39355pt}{-4.21626pt}{-4.25005pt}{-4.36955pt}{-4.10654pt}{-4.5607pt}\pgfsys@curveto{-3.96303pt}{-4.75185pt}{-3.81952pt}{-4.90514pt}{-3.67601pt}{-4.90514pt}\pgfsys@curveto{-3.5325pt}{-4.90514pt}{-3.38899pt}{-4.75185pt}{-3.24548pt}{-4.5607pt}\pgfsys@curveto{-3.10187pt}{-4.36955pt}{-2.95836pt}{-4.21626pt}{-2.81485pt}{-4.21626pt}\pgfsys@curveto{-2.67134pt}{-4.21626pt}{-2.52783pt}{-4.36955pt}{-2.38432pt}{-4.5607pt}\pgfsys@curveto{-2.24081pt}{-4.75185pt}{-2.0973pt}{-4.90514pt}{-1.9538pt}{-4.90514pt}\pgfsys@curveto{-1.81029pt}{-4.90514pt}{-1.66678pt}{-4.75185pt}{-1.52327pt}{-4.5607pt}\pgfsys@curveto{-1.37965pt}{-4.36955pt}{-1.23615pt}{-4.21626pt}{-1.09264pt}{-4.21626pt}\pgfsys@curveto{-0.94913pt}{-4.21626pt}{-0.80562pt}{-4.36955pt}{-0.66211pt}{-4.5607pt}\pgfsys@curveto{-0.5186pt}{-4.75185pt}{-0.37509pt}{-4.90514pt}{-0.23158pt}{-4.90514pt}\pgfsys@curveto{-0.08807pt}{-4.90514pt}{0.05544pt}{-4.75185pt}{0.19894pt}{-4.5607pt}\pgfsys@curveto{0.34256pt}{-4.36955pt}{0.48607pt}{-4.21626pt}{0.62958pt}{-4.21626pt}\pgfsys@curveto{0.77309pt}{-4.21626pt}{0.9166pt}{-4.36955pt}{1.0601pt}{-4.5607pt}\pgfsys@curveto{1.20361pt}{-4.75185pt}{1.34712pt}{-4.90514pt}{1.49063pt}{-4.90514pt}\pgfsys@curveto{1.63414pt}{-4.90514pt}{1.77765pt}{-4.75185pt}{1.92116pt}{-4.5607pt}\pgfsys@curveto{2.06477pt}{-4.36955pt}{2.20828pt}{-4.21626pt}{2.35179pt}{-4.21626pt}\pgfsys@curveto{2.4953pt}{-4.21626pt}{2.63881pt}{-4.36955pt}{2.78232pt}{-4.5607pt}\pgfsys@lineto{2.78238pt}{-4.5607pt}\pgfsys@lineto{4.5676pt}{-4.5607pt}\pgfsys@stroke\pgfsys@invoke{ }{{}{{}}{}{}{{}}{{{}}{{{}}{\pgfsys@beginscope\pgfsys@invoke{ }\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{4.7676pt}{-4.5607pt}\pgfsys@invoke{ }\pgfsys@invoke{ \lxSVG@closescope }\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}{{}}}} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope{{ {}{}{}}}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}}\epsilon, implying that and .
Otherwise, for some we must have
[TABLE]
Also, there must exist with and . We then have
[TABLE]
from which and as desired. ∎
Proposition 4**.**
* and .*
Proof.
The first equality follows directly from the definition of . The second can be obtained by combining Lemmas 2 and 3, idempotency of null closure, and monotonicity of null closure, shift and call-reduce closure into the following:
[TABLE]
∎
As a consequence, plugging Algorithm 4 into Algorithm 1 (with all call-reduce closures replaced by their null closures) we obtain a procedure for context-free recognition, realizable using any data type representing languages over , implementing API 5.
API 5**.**
Operations required for recognition.
- •
* \tab,*
- •
* \tab,*
- •
* \tab,*
- •
* \tabwhether ,*
- •
* \tab.*
3 Parsing
We now augment our algorithm to perform generalized parsing and not just mere recognition. The exposition here mirrors closely the one from the previous section. All definitions and algorithms are adjusted so that instead of asking whether some configuration is reachable, we ask about the language of transitions by which it can be reached. In particular, instead of computing (a representation of) all possible parse trees, we are going to output the language of all legal transition sequences.
Definition 7**.**
For an input , the parsing relation associates configurations reachable when parsing with reversed444Tracking how an RTN configuration evolves under a sequence of transitions, one can see that the states at the beginning (top) of the ultimate configuration depend primarily on the transitions at the end of the sequence. Thus, to keep the direction of concatenation consistent, we record the transition history in reverse. sequences of transitions by which they can be reached from the initial configuration:
[TABLE]
In particular, accepting transition sequences for an input string are exactly (reversed) those which associates with the configuration .
Definition 8**.**
The call-reduce closure and shift by a symbol of a relation are defined as:
[TABLE]
Parsing relations for a particular input can be calculated inductively analogously to parsing languages, because and . To efficiently perform a single phase according to the latter equality, we need a suitable notion of derivatives:
Definition 9**.**
A derivative of degree of a relation by a symbol is any collection of pairs with and , such that for each and we have
[TABLE]
A relation is -regular if it belongs to some family of size , closed under derivatives of degree . It is -regular if it is -regular for some , and regular if it is -regular for some .
Regular relations, as defined here, are similar to rational relations—a well-studied generalization of regular languages [5]. The fundamental difference is that the latter require the components to be “jointly regular”, whereas we put no restriction on the transition languages . We are only concerned about finiteness (and bounded nondeterminism) of the automaton with respect to . Note however, that despite this flexibility, such automata are not always determinizable.
Algorithm 6**.**
Calculating
1* *
2* foreach :*
3* foreach :*
4* *
5* if ,** foreach :*
6* foreach :*
7* *
8* if ,** foreach :*
9* foreach :*
10* *
11* *
12* return *
For convenience, let us denote
[TABLE]
Algorithm 6 (completely analogous to Algorithm 3) can now be used to calculate . Adapting it to have constant depth is however not as easy as before, because skipping nullable states requires additional transitions to be performed. To handle this, we enrich the alphabet of configurations to
[TABLE]
allowing them to intersperse states with (non-shift) transitions. Such transitions will “guide” the simulation of the RTN—if present on top of a configuration, they will need to be executed (en bloc) before the states below them can be accessed. To express that, reachability is enriched by
[TABLE]
Note, that guiding transitions will be introduced into configurations only artificially, replacing states which we commit to null later on—reachability may only remove them, fulfilling that commitment.
We now consider guided languages (languages of guided configurations, i.e., subsets of ) and guided relations (subsets of ), and (re)define null closure to optionally replace states by their nulling transitions:
Definition 10**.**
A guided language (respectively, guided relation ) is null-closed if for each S\ni s\mathrel{\leavevmode\hbox to21.29pt{\vbox to14.05pt{\pgfpicture\makeatletter\hbox{\hskip 10.64674pt\lower-9.49377pt\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{ }\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ } {{}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}{}{{ {}{}}}{ {}{}} {{}{{}}}{{}{}}{}{{}{}} { }{{{{}}\pgfsys@beginscope\pgfsys@invoke{ }\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{-8.52454pt}{-2.83849pt}\pgfsys@invoke{ }\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{ }\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{{\vbox{\halign{\hfil#\hfil\cr\cr\vskip 0.017pt\cr\hbox{{\scriptstyle\eta\in D_{\epsilon}^{}}}\cr}}}} }}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} { {}{}{}}{{{}}{{}}}{{}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}{}{{ {}{}}}{ {}{}} {{}{{}}}{{}{}}{}{{}{}} { }{{{{}}\pgfsys@beginscope\pgfsys@invoke{ }\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{0.0pt}{-6.82736pt}\pgfsys@invoke{ }\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{ }\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{} }}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} {{}{{}}{}{{}}{}{ {}} {}{}}{{}{}}{}{}{}{{}}{{}}{{}{}}{{}{}} {{{{}{}{{}} }}{{}}}{{{{}{}{{}} }}{{}}{{}}} {{{{}{}{{}} }}{{}} {}{}{} {}{}{} {}{}{} {}{}{} }{{{{}{}{{}} }}{{}} {}{}{} {}{}{} {}{}{} {}{}{} }{{{{}{}{{}} }}{{}} {}{}{} {}{}{} {}{}{} {}{}{} }{{{{}{}{{}} }}{{}} {}{}{} {}{}{} {}{}{} {}{}{} }{{{{}{}{{}} }}{{}} {}{}{} {}{}{} {}{}{} {}{}{} }{{{{}{}{{}} }}{{}} {}{}{} {}{}{} {}{}{} {}{}{} }{{{{}{}{{}} }}{{}} {}{}{} {}{}{} {}{}{} {}{}{} }{{{{}{}{{}} }}{{}} {}{}{} {}{}{} {}{}{} {}{}{} }{{{{}{}{{}} }}{{}} {}{}{} {}{}{} {}{}{} {}{}{} }{{{{}{}{{}} }}{{}} {}{}{} {}{}{} {}{}{} {}{}{} }{{{{}{}{{}} }}{{}} {}{}{} {}{}{} }{{{{}{}{{}} }}{{}}}{{{{}{}{{}} }}{{}} {{}} } {{{{}{}{{}} }}{{}} }{{{{}{}{{}} }}{{}}{{}}}{}{}{}{}{{}}\pgfsys@moveto{-10.44675pt}{-4.7607pt}\pgfsys@lineto{-10.44675pt}{-4.7607pt}\pgfsys@curveto{-10.30324pt}{-4.56955pt}{-10.15973pt}{-4.41626pt}{-10.01622pt}{-4.41626pt}\pgfsys@curveto{-9.87271pt}{-4.41626pt}{-9.7292pt}{-4.56955pt}{-9.5857pt}{-4.7607pt}\pgfsys@curveto{-9.44218pt}{-4.95184pt}{-9.29868pt}{-5.10513pt}{-9.15517pt}{-5.10513pt}\pgfsys@curveto{-9.01166pt}{-5.10513pt}{-8.86815pt}{-4.95184pt}{-8.72464pt}{-4.7607pt}\pgfsys@curveto{-8.58102pt}{-4.56955pt}{-8.43752pt}{-4.41626pt}{-8.294pt}{-4.41626pt}\pgfsys@curveto{-8.1505pt}{-4.41626pt}{-8.00699pt}{-4.56955pt}{-7.86348pt}{-4.7607pt}\pgfsys@curveto{-7.71997pt}{-4.95184pt}{-7.57646pt}{-5.10513pt}{-7.43295pt}{-5.10513pt}\pgfsys@curveto{-7.28944pt}{-5.10513pt}{-7.14594pt}{-4.95184pt}{-7.00243pt}{-4.7607pt}\pgfsys@curveto{-6.85881pt}{-4.56955pt}{-6.7153pt}{-4.41626pt}{-6.5718pt}{-4.41626pt}\pgfsys@curveto{-6.42828pt}{-4.41626pt}{-6.28477pt}{-4.56955pt}{-6.14127pt}{-4.7607pt}\pgfsys@curveto{-5.99776pt}{-4.95184pt}{-5.85425pt}{-5.10513pt}{-5.71074pt}{-5.10513pt}\pgfsys@curveto{-5.56723pt}{-5.10513pt}{-5.42372pt}{-4.95184pt}{-5.28021pt}{-4.7607pt}\pgfsys@curveto{-5.1366pt}{-4.56955pt}{-4.99309pt}{-4.41626pt}{-4.84958pt}{-4.41626pt}\pgfsys@curveto{-4.70607pt}{-4.41626pt}{-4.56256pt}{-4.56955pt}{-4.41905pt}{-4.7607pt}\pgfsys@curveto{-4.27554pt}{-4.95184pt}{-4.13203pt}{-5.10513pt}{-3.98853pt}{-5.10513pt}\pgfsys@curveto{-3.84502pt}{-5.10513pt}{-3.7015pt}{-4.95184pt}{-3.558pt}{-4.7607pt}\pgfsys@curveto{-3.41438pt}{-4.56955pt}{-3.27087pt}{-4.41626pt}{-3.12737pt}{-4.41626pt}\pgfsys@curveto{-2.98386pt}{-4.41626pt}{-2.84035pt}{-4.56955pt}{-2.69684pt}{-4.7607pt}\pgfsys@curveto{-2.55333pt}{-4.95184pt}{-2.40982pt}{-5.10513pt}{-2.26631pt}{-5.10513pt}\pgfsys@curveto{-2.1228pt}{-5.10513pt}{-1.9793pt}{-4.95184pt}{-1.83578pt}{-4.7607pt}\pgfsys@curveto{-1.69217pt}{-4.56955pt}{-1.54866pt}{-4.41626pt}{-1.40515pt}{-4.41626pt}\pgfsys@curveto{-1.26164pt}{-4.41626pt}{-1.11813pt}{-4.56955pt}{-0.97462pt}{-4.7607pt}\pgfsys@curveto{-0.83112pt}{-4.95184pt}{-0.6876pt}{-5.10513pt}{-0.5441pt}{-5.10513pt}\pgfsys@curveto{-0.40059pt}{-5.10513pt}{-0.25708pt}{-4.95184pt}{-0.11357pt}{-4.7607pt}\pgfsys@curveto{0.03004pt}{-4.56955pt}{0.17355pt}{-4.41626pt}{0.31706pt}{-4.41626pt}\pgfsys@curveto{0.46057pt}{-4.41626pt}{0.60408pt}{-4.56955pt}{0.74759pt}{-4.7607pt}\pgfsys@curveto{0.8911pt}{-4.95184pt}{1.0346pt}{-5.10513pt}{1.17812pt}{-5.10513pt}\pgfsys@curveto{1.32162pt}{-5.10513pt}{1.46513pt}{-4.95184pt}{1.60864pt}{-4.7607pt}\pgfsys@curveto{1.75226pt}{-4.56955pt}{1.89577pt}{-4.41626pt}{2.03928pt}{-4.41626pt}\pgfsys@curveto{2.18279pt}{-4.41626pt}{2.3263pt}{-4.56955pt}{2.4698pt}{-4.7607pt}\pgfsys@curveto{2.61331pt}{-4.95184pt}{2.75682pt}{-5.10513pt}{2.90033pt}{-5.10513pt}\pgfsys@curveto{3.04384pt}{-5.10513pt}{3.18735pt}{-4.95184pt}{3.33086pt}{-4.7607pt}\pgfsys@curveto{3.47447pt}{-4.56955pt}{3.61798pt}{-4.41626pt}{3.76149pt}{-4.41626pt}\pgfsys@curveto{3.905pt}{-4.41626pt}{4.04851pt}{-4.56955pt}{4.19202pt}{-4.7607pt}\pgfsys@curveto{4.33553pt}{-4.95184pt}{4.47903pt}{-5.10513pt}{4.62254pt}{-5.10513pt}\pgfsys@curveto{4.76605pt}{-5.10513pt}{4.90956pt}{-4.95184pt}{5.05307pt}{-4.7607pt}\pgfsys@curveto{5.19669pt}{-4.56955pt}{5.3402pt}{-4.41626pt}{5.4837pt}{-4.41626pt}\pgfsys@curveto{5.62721pt}{-4.41626pt}{5.77072pt}{-4.56955pt}{5.91423pt}{-4.7607pt}\pgfsys@curveto{6.05774pt}{-4.95184pt}{6.20125pt}{-5.10513pt}{6.34476pt}{-5.10513pt}\pgfsys@curveto{6.48827pt}{-5.10513pt}{6.63177pt}{-4.95184pt}{6.77528pt}{-4.7607pt}\pgfsys@curveto{6.9189pt}{-4.56955pt}{7.06241pt}{-4.41626pt}{7.20592pt}{-4.41626pt}\pgfsys@curveto{7.34943pt}{-4.41626pt}{7.49294pt}{-4.56955pt}{7.63644pt}{-4.7607pt}\pgfsys@lineto{7.6365pt}{-4.7607pt}\pgfsys@lineto{10.04675pt}{-4.7607pt}\pgfsys@stroke\pgfsys@invoke{ }{{}{{}}{}{}{{}}{{{}}{{{}}{\pgfsys@beginscope\pgfsys@invoke{ }\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{10.24675pt}{-4.7607pt}\pgfsys@invoke{ }\pgfsys@invoke{ \lxSVG@closescope }\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}{{}}}} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope{{ {}{}{}}}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}}\epsilon, (and ) we have*
[TABLE]
The null closure of a language (relation ) is the smallest null-closed guided language (guided relation ).
We now revisit and augment the reasoning from the previous section to show that an inductive procedure can be used to compute the null closures of parsing relations. First, we make a convenient observation about the interplay between performing transitions and null closure:
Lemma 5**.**
Consider and . Then any sequence of transitions \gamma^{\prime}\mathrel{\leavevmode\hbox to21.3pt{\vbox to13.18pt{\pgfpicture\makeatletter\hbox{\hskip 10.65146pt\lower-9.0588pt\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{ }\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ } {{}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}{}{{ {}{}}}{ {}{}} {{}{{}}}{{}{}}{}{{}{}} { }{{{{}}\pgfsys@beginscope\pgfsys@invoke{ }\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{-8.52925pt}{-2.40352pt}\pgfsys@invoke{ }\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{ }\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{{\vbox{\halign{\hfil#\hfil\cr\cr\vskip 0.017pt\cr\hbox{{\scriptstyle\delta\in D^{}}}\cr}}}} }}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} { {}{}{}}{{{}}{{}}}{{}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}{}{{ {}{}}}{ {}{}} {{}{{}}}{{}{}}{}{{}{}} { }{{{{}}\pgfsys@beginscope\pgfsys@invoke{ }\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{0.0pt}{-6.3924pt}\pgfsys@invoke{ }\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{ }\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{} }}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} {{}{{}}{}{{}}{}{ {}} {}{}}{{}{}}{}{}{}{{}}{{}}{{}{}}{{}{}} {{{{}{}{{}} }}{{}}}{{{{}{}{{}} }}{{}}{{}}} {{{{}{}{{}} }}{{}} {}{}{} {}{}{} {}{}{} {}{}{} }{{{{}{}{{}} }}{{}} {}{}{} {}{}{} {}{}{} {}{}{} }{{{{}{}{{}} }}{{}} {}{}{} {}{}{} {}{}{} {}{}{} }{{{{}{}{{}} }}{{}} {}{}{} {}{}{} {}{}{} {}{}{} }{{{{}{}{{}} }}{{}} {}{}{} {}{}{} {}{}{} {}{}{} }{{{{}{}{{}} }}{{}} {}{}{} {}{}{} {}{}{} {}{}{} }{{{{}{}{{}} }}{{}} {}{}{} {}{}{} {}{}{} {}{}{} }{{{{}{}{{}} }}{{}} {}{}{} {}{}{} {}{}{} {}{}{} }{{{{}{}{{}} }}{{}} {}{}{} {}{}{} {}{}{} {}{}{} }{{{{}{}{{}} }}{{}} {}{}{} {}{}{} {}{}{} {}{}{} }{{{{}{}{{}} }}{{}} {}{}{} {}{}{} }{{{{}{}{{}} }}{{}}}{{{{}{}{{}} }}{{}} {{}} } {{{{}{}{{}} }}{{}} }{{{{}{}{{}} }}{{}}{{}}}{}{}{}{}{{}}\pgfsys@moveto{-10.45146pt}{-4.32573pt}\pgfsys@lineto{-10.45146pt}{-4.32573pt}\pgfsys@curveto{-10.30795pt}{-4.13458pt}{-10.16444pt}{-3.9813pt}{-10.02094pt}{-3.9813pt}\pgfsys@curveto{-9.87743pt}{-3.9813pt}{-9.73392pt}{-4.13458pt}{-9.59041pt}{-4.32573pt}\pgfsys@curveto{-9.4469pt}{-4.51688pt}{-9.30339pt}{-4.67017pt}{-9.15988pt}{-4.67017pt}\pgfsys@curveto{-9.01637pt}{-4.67017pt}{-8.87286pt}{-4.51688pt}{-8.72935pt}{-4.32573pt}\pgfsys@curveto{-8.58574pt}{-4.13458pt}{-8.44223pt}{-3.9813pt}{-8.29872pt}{-3.9813pt}\pgfsys@curveto{-8.15521pt}{-3.9813pt}{-8.0117pt}{-4.13458pt}{-7.8682pt}{-4.32573pt}\pgfsys@curveto{-7.72469pt}{-4.51688pt}{-7.58118pt}{-4.67017pt}{-7.43767pt}{-4.67017pt}\pgfsys@curveto{-7.29416pt}{-4.67017pt}{-7.15065pt}{-4.51688pt}{-7.00714pt}{-4.32573pt}\pgfsys@curveto{-6.86353pt}{-4.13458pt}{-6.72002pt}{-3.9813pt}{-6.5765pt}{-3.9813pt}\pgfsys@curveto{-6.433pt}{-3.9813pt}{-6.28949pt}{-4.13458pt}{-6.14598pt}{-4.32573pt}\pgfsys@curveto{-6.00247pt}{-4.51688pt}{-5.85896pt}{-4.67017pt}{-5.71545pt}{-4.67017pt}\pgfsys@curveto{-5.57195pt}{-4.67017pt}{-5.42844pt}{-4.51688pt}{-5.28493pt}{-4.32573pt}\pgfsys@curveto{-5.14131pt}{-4.13458pt}{-4.9978pt}{-3.9813pt}{-4.8543pt}{-3.9813pt}\pgfsys@curveto{-4.71078pt}{-3.9813pt}{-4.56728pt}{-4.13458pt}{-4.42377pt}{-4.32573pt}\pgfsys@curveto{-4.28026pt}{-4.51688pt}{-4.13675pt}{-4.67017pt}{-3.99324pt}{-4.67017pt}\pgfsys@curveto{-3.84973pt}{-4.67017pt}{-3.70622pt}{-4.51688pt}{-3.56271pt}{-4.32573pt}\pgfsys@curveto{-3.4191pt}{-4.13458pt}{-3.27559pt}{-3.9813pt}{-3.13208pt}{-3.9813pt}\pgfsys@curveto{-2.98857pt}{-3.9813pt}{-2.84506pt}{-4.13458pt}{-2.70155pt}{-4.32573pt}\pgfsys@curveto{-2.55804pt}{-4.51688pt}{-2.41454pt}{-4.67017pt}{-2.27103pt}{-4.67017pt}\pgfsys@curveto{-2.12752pt}{-4.67017pt}{-1.98401pt}{-4.51688pt}{-1.8405pt}{-4.32573pt}\pgfsys@curveto{-1.69688pt}{-4.13458pt}{-1.55338pt}{-3.9813pt}{-1.40987pt}{-3.9813pt}\pgfsys@curveto{-1.26636pt}{-3.9813pt}{-1.12285pt}{-4.13458pt}{-0.97934pt}{-4.32573pt}\pgfsys@curveto{-0.83583pt}{-4.51688pt}{-0.69232pt}{-4.67017pt}{-0.54881pt}{-4.67017pt}\pgfsys@curveto{-0.4053pt}{-4.67017pt}{-0.2618pt}{-4.51688pt}{-0.11829pt}{-4.32573pt}\pgfsys@curveto{0.02533pt}{-4.13458pt}{0.16884pt}{-3.9813pt}{0.31235pt}{-3.9813pt}\pgfsys@curveto{0.45586pt}{-3.9813pt}{0.59937pt}{-4.13458pt}{0.74287pt}{-4.32573pt}\pgfsys@curveto{0.88638pt}{-4.51688pt}{1.02989pt}{-4.67017pt}{1.1734pt}{-4.67017pt}\pgfsys@curveto{1.31691pt}{-4.67017pt}{1.46042pt}{-4.51688pt}{1.60393pt}{-4.32573pt}\pgfsys@curveto{1.74754pt}{-4.13458pt}{1.89105pt}{-3.9813pt}{2.03456pt}{-3.9813pt}\pgfsys@curveto{2.17807pt}{-3.9813pt}{2.32158pt}{-4.13458pt}{2.46509pt}{-4.32573pt}\pgfsys@curveto{2.6086pt}{-4.51688pt}{2.7521pt}{-4.67017pt}{2.89561pt}{-4.67017pt}\pgfsys@curveto{3.03912pt}{-4.67017pt}{3.18263pt}{-4.51688pt}{3.32614pt}{-4.32573pt}\pgfsys@curveto{3.46976pt}{-4.13458pt}{3.61327pt}{-3.9813pt}{3.75677pt}{-3.9813pt}\pgfsys@curveto{3.90028pt}{-3.9813pt}{4.0438pt}{-4.13458pt}{4.1873pt}{-4.32573pt}\pgfsys@curveto{4.33081pt}{-4.51688pt}{4.47432pt}{-4.67017pt}{4.61783pt}{-4.67017pt}\pgfsys@curveto{4.76134pt}{-4.67017pt}{4.90485pt}{-4.51688pt}{5.04836pt}{-4.32573pt}\pgfsys@curveto{5.19197pt}{-4.13458pt}{5.33548pt}{-3.9813pt}{5.47899pt}{-3.9813pt}\pgfsys@curveto{5.6225pt}{-3.9813pt}{5.766pt}{-4.13458pt}{5.90952pt}{-4.32573pt}\pgfsys@curveto{6.05302pt}{-4.51688pt}{6.19653pt}{-4.67017pt}{6.34004pt}{-4.67017pt}\pgfsys@curveto{6.48355pt}{-4.67017pt}{6.62706pt}{-4.51688pt}{6.77057pt}{-4.32573pt}\pgfsys@curveto{6.91418pt}{-4.13458pt}{7.0577pt}{-3.9813pt}{7.2012pt}{-3.9813pt}\pgfsys@curveto{7.34471pt}{-3.9813pt}{7.48822pt}{-4.13458pt}{7.63173pt}{-4.32573pt}\pgfsys@lineto{7.63179pt}{-4.32573pt}\pgfsys@lineto{10.05147pt}{-4.32573pt}\pgfsys@stroke\pgfsys@invoke{ }{{}{{}}{}{}{{}}{{{}}{{{}}{\pgfsys@beginscope\pgfsys@invoke{ }\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{10.25146pt}{-4.32573pt}\pgfsys@invoke{ }\pgfsys@invoke{ \lxSVG@closescope }\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}{{}}}} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope{{ {}{}{}}}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}}\gamma^{\prime}_{2} can be “tracked back” to \gamma\mathrel{\leavevmode\hbox to6.73pt{\vbox to12.28pt{\pgfpicture\makeatletter\hbox{\hskip 3.36664pt\lower-8.60823pt\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{ }\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ } {{}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}{}{{ {}{}}}{ {}{}} {{}{{}}}{{}{}}{}{{}{}} { }{{{{}}\pgfsys@beginscope\pgfsys@invoke{ }\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{-1.24443pt}{-1.95294pt}\pgfsys@invoke{ }\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{ }\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{{\vbox{\halign{\hfil#\hfil\cr\cr\vskip 0.017pt\cr\hbox{{\scriptstyle\delta}}\cr}}}} }}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} { {}{}{}}{{{}}{{}}}{{}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}{}{{ {}{}}}{ {}{}} {{}{{}}}{{}{}}{}{{}{}} { }{{{{}}\pgfsys@beginscope\pgfsys@invoke{ }\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{0.0pt}{-5.94182pt}\pgfsys@invoke{ }\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{ }\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{} }}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} {{}{{}}{}{{}}{}{ {}} {}{}}{{}{}}{}{}{}{{}}{{}}{{}{}}{{}{}} {{{{}{}{{}} }}{{}}}{{{{}{}{{}} }}{{}}{{}}} {{{{}{}{{}} }}{{}} {}{}{} {}{}{} {}{}{} {}{}{} }{{{{}{}{{}} }}{{}} {}{}{} {}{}{} {}{}{} {}{}{} }{{{{}{}{{}} }}{{}} {}{}{} {}{}{} }{{{{}{}{{}} }}{{}}}{{{{}{}{{}} }}{{}} {{}} } {{{{}{}{{}} }}{{}} }{{{{}{}{{}} }}{{}}{{}}}{}{}{}{}{{}}\pgfsys@moveto{-3.16664pt}{-3.87515pt}\pgfsys@lineto{-3.16664pt}{-3.87515pt}\pgfsys@curveto{-3.02313pt}{-3.684pt}{-2.87962pt}{-3.53072pt}{-2.73611pt}{-3.53072pt}\pgfsys@curveto{-2.5926pt}{-3.53072pt}{-2.4491pt}{-3.684pt}{-2.30559pt}{-3.87515pt}\pgfsys@curveto{-2.16208pt}{-4.0663pt}{-2.01857pt}{-4.21959pt}{-1.87506pt}{-4.21959pt}\pgfsys@curveto{-1.73155pt}{-4.21959pt}{-1.58804pt}{-4.0663pt}{-1.44453pt}{-3.87515pt}\pgfsys@curveto{-1.30092pt}{-3.684pt}{-1.15741pt}{-3.53072pt}{-1.0139pt}{-3.53072pt}\pgfsys@curveto{-0.87039pt}{-3.53072pt}{-0.72688pt}{-3.684pt}{-0.58337pt}{-3.87515pt}\pgfsys@curveto{-0.43987pt}{-4.0663pt}{-0.29636pt}{-4.21959pt}{-0.15285pt}{-4.21959pt}\pgfsys@curveto{-0.00934pt}{-4.21959pt}{0.13417pt}{-4.0663pt}{0.27768pt}{-3.87515pt}\pgfsys@curveto{0.4213pt}{-3.684pt}{0.5648pt}{-3.53072pt}{0.70831pt}{-3.53072pt}\pgfsys@curveto{0.85182pt}{-3.53072pt}{0.99533pt}{-3.684pt}{1.13884pt}{-3.87515pt}\pgfsys@lineto{1.1389pt}{-3.87515pt}\pgfsys@lineto{2.76665pt}{-3.87515pt}\pgfsys@stroke\pgfsys@invoke{ }{{}{{}}{}{}{{}}{{{}}{{{}}{\pgfsys@beginscope\pgfsys@invoke{ }\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{2.96664pt}{-3.87515pt}\pgfsys@invoke{ }\pgfsys@invoke{ \lxSVG@closescope }\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}{{}}}} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope{{ {}{}{}}}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}}\gamma_{2} with .*
Proof.
The proof is by induction on the length of . The case when is trivial. Otherwise, and must be nonempty. We distinguish three cases.
If for some and , we have
[TABLE]
and the result follows from applying the induction hypothesis to \overline{\gamma_{1}}\ni\gamma^{\prime}_{1}\mathrel{\leavevmode\hbox to8.33pt{\vbox to13.31pt{\pgfpicture\makeatletter\hbox{\hskip 4.16664pt\lower-9.12378pt\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{ }\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ } {{}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}{}{{ {}{}}}{ {}{}} {{}{{}}}{{}{}}{}{{}{}} { }{{{{}}\pgfsys@beginscope\pgfsys@invoke{ }\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{-2.04443pt}{-2.46849pt}\pgfsys@invoke{ }\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{ }\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{{\vbox{\halign{\hfil#\hfil\cr\cr\vskip 0.017pt\cr\hbox{{\scriptstyle\delta_{1}}}\cr}}}} }}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} { {}{}{}}{{{}}{{}}}{{}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}{}{{ {}{}}}{ {}{}} {{}{{}}}{{}{}}{}{{}{}} { }{{{{}}\pgfsys@beginscope\pgfsys@invoke{ }\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{0.0pt}{-6.45737pt}\pgfsys@invoke{ }\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{ }\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{} }}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} {{}{{}}{}{{}}{}{ {}} {}{}}{{}{}}{}{}{}{{}}{{}}{{}{}}{{}{}} {{{{}{}{{}} }}{{}}}{{{{}{}{{}} }}{{}}{{}}} {{{{}{}{{}} }}{{}} {}{}{} {}{}{} {}{}{} {}{}{} }{{{{}{}{{}} }}{{}} {}{}{} {}{}{} {}{}{} {}{}{} }{{{{}{}{{}} }}{{}} {}{}{} {}{}{} {}{}{} {}{}{} }{{{{}{}{{}} }}{{}} {}{}{} {}{}{} }{{{{}{}{{}} }}{{}}}{{{{}{}{{}} }}{{}} {{}} } {{{{}{}{{}} }}{{}} }{{{{}{}{{}} }}{{}}{{}}}{}{}{}{}{{}}\pgfsys@moveto{-3.96664pt}{-4.3907pt}\pgfsys@lineto{-3.96664pt}{-4.3907pt}\pgfsys@curveto{-3.82314pt}{-4.19955pt}{-3.67963pt}{-4.04626pt}{-3.53612pt}{-4.04626pt}\pgfsys@curveto{-3.39261pt}{-4.04626pt}{-3.2491pt}{-4.19955pt}{-3.10559pt}{-4.3907pt}\pgfsys@curveto{-2.96208pt}{-4.58185pt}{-2.81857pt}{-4.73514pt}{-2.67506pt}{-4.73514pt}\pgfsys@curveto{-2.53156pt}{-4.73514pt}{-2.38805pt}{-4.58185pt}{-2.24454pt}{-4.3907pt}\pgfsys@curveto{-2.10092pt}{-4.19955pt}{-1.95741pt}{-4.04626pt}{-1.8139pt}{-4.04626pt}\pgfsys@curveto{-1.6704pt}{-4.04626pt}{-1.52689pt}{-4.19955pt}{-1.38338pt}{-4.3907pt}\pgfsys@curveto{-1.23987pt}{-4.58185pt}{-1.09636pt}{-4.73514pt}{-0.95285pt}{-4.73514pt}\pgfsys@curveto{-0.80934pt}{-4.73514pt}{-0.66583pt}{-4.58185pt}{-0.52232pt}{-4.3907pt}\pgfsys@curveto{-0.37871pt}{-4.19955pt}{-0.2352pt}{-4.04626pt}{-0.09169pt}{-4.04626pt}\pgfsys@curveto{0.05182pt}{-4.04626pt}{0.19533pt}{-4.19955pt}{0.33884pt}{-4.3907pt}\pgfsys@curveto{0.48235pt}{-4.58185pt}{0.62585pt}{-4.73514pt}{0.76936pt}{-4.73514pt}\pgfsys@curveto{0.91287pt}{-4.73514pt}{1.05638pt}{-4.58185pt}{1.19989pt}{-4.3907pt}\pgfsys@curveto{1.3435pt}{-4.19955pt}{1.48701pt}{-4.04626pt}{1.63052pt}{-4.04626pt}\pgfsys@curveto{1.77403pt}{-4.04626pt}{1.91754pt}{-4.19955pt}{2.06105pt}{-4.3907pt}\pgfsys@lineto{2.06111pt}{-4.3907pt}\pgfsys@lineto{3.56665pt}{-4.3907pt}\pgfsys@stroke\pgfsys@invoke{ }{{}{{}}{}{}{{}}{{{}}{{{}}{\pgfsys@beginscope\pgfsys@invoke{ }\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{3.76665pt}{-4.3907pt}\pgfsys@invoke{ }\pgfsys@invoke{ \lxSVG@closescope }\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}{{}}}} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope{{ {}{}{}}}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}}\gamma^{\prime}_{2}.
If for some and also begins with a state, it must be the same state . Then the first transition in must be valid from , giving
[TABLE]
so we can succeed by applying the induction hypothesis to \overline{\sigma{\cdot}\gamma_{1}}\ni\sigma{\cdot}\gamma^{\prime}_{1}\mathrel{\leavevmode\hbox to8.33pt{\vbox to13.31pt{\pgfpicture\makeatletter\hbox{\hskip 4.16664pt\lower-9.12378pt\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{ }\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ } {{}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}{}{{ {}{}}}{ {}{}} {{}{{}}}{{}{}}{}{{}{}} { }{{{{}}\pgfsys@beginscope\pgfsys@invoke{ }\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{-2.04443pt}{-2.46849pt}\pgfsys@invoke{ }\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{ }\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{{\vbox{\halign{\hfil#\hfil\cr\cr\vskip 0.017pt\cr\hbox{{\scriptstyle\delta_{1}}}\cr}}}} }}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} { {}{}{}}{{{}}{{}}}{{}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}{}{{ {}{}}}{ {}{}} {{}{{}}}{{}{}}{}{{}{}} { }{{{{}}\pgfsys@beginscope\pgfsys@invoke{ }\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{0.0pt}{-6.45737pt}\pgfsys@invoke{ }\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{ }\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{} }}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} {{}{{}}{}{{}}{}{ {}} {}{}}{{}{}}{}{}{}{{}}{{}}{{}{}}{{}{}} {{{{}{}{{}} }}{{}}}{{{{}{}{{}} }}{{}}{{}}} {{{{}{}{{}} }}{{}} {}{}{} {}{}{} {}{}{} {}{}{} }{{{{}{}{{}} }}{{}} {}{}{} {}{}{} {}{}{} {}{}{} }{{{{}{}{{}} }}{{}} {}{}{} {}{}{} {}{}{} {}{}{} }{{{{}{}{{}} }}{{}} {}{}{} {}{}{} }{{{{}{}{{}} }}{{}}}{{{{}{}{{}} }}{{}} {{}} } {{{{}{}{{}} }}{{}} }{{{{}{}{{}} }}{{}}{{}}}{}{}{}{}{{}}\pgfsys@moveto{-3.96664pt}{-4.3907pt}\pgfsys@lineto{-3.96664pt}{-4.3907pt}\pgfsys@curveto{-3.82314pt}{-4.19955pt}{-3.67963pt}{-4.04626pt}{-3.53612pt}{-4.04626pt}\pgfsys@curveto{-3.39261pt}{-4.04626pt}{-3.2491pt}{-4.19955pt}{-3.10559pt}{-4.3907pt}\pgfsys@curveto{-2.96208pt}{-4.58185pt}{-2.81857pt}{-4.73514pt}{-2.67506pt}{-4.73514pt}\pgfsys@curveto{-2.53156pt}{-4.73514pt}{-2.38805pt}{-4.58185pt}{-2.24454pt}{-4.3907pt}\pgfsys@curveto{-2.10092pt}{-4.19955pt}{-1.95741pt}{-4.04626pt}{-1.8139pt}{-4.04626pt}\pgfsys@curveto{-1.6704pt}{-4.04626pt}{-1.52689pt}{-4.19955pt}{-1.38338pt}{-4.3907pt}\pgfsys@curveto{-1.23987pt}{-4.58185pt}{-1.09636pt}{-4.73514pt}{-0.95285pt}{-4.73514pt}\pgfsys@curveto{-0.80934pt}{-4.73514pt}{-0.66583pt}{-4.58185pt}{-0.52232pt}{-4.3907pt}\pgfsys@curveto{-0.37871pt}{-4.19955pt}{-0.2352pt}{-4.04626pt}{-0.09169pt}{-4.04626pt}\pgfsys@curveto{0.05182pt}{-4.04626pt}{0.19533pt}{-4.19955pt}{0.33884pt}{-4.3907pt}\pgfsys@curveto{0.48235pt}{-4.58185pt}{0.62585pt}{-4.73514pt}{0.76936pt}{-4.73514pt}\pgfsys@curveto{0.91287pt}{-4.73514pt}{1.05638pt}{-4.58185pt}{1.19989pt}{-4.3907pt}\pgfsys@curveto{1.3435pt}{-4.19955pt}{1.48701pt}{-4.04626pt}{1.63052pt}{-4.04626pt}\pgfsys@curveto{1.77403pt}{-4.04626pt}{1.91754pt}{-4.19955pt}{2.06105pt}{-4.3907pt}\pgfsys@lineto{2.06111pt}{-4.3907pt}\pgfsys@lineto{3.56665pt}{-4.3907pt}\pgfsys@stroke\pgfsys@invoke{ }{{}{{}}{}{}{{}}{{{}}{{{}}{\pgfsys@beginscope\pgfsys@invoke{ }\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{3.76665pt}{-4.3907pt}\pgfsys@invoke{ }\pgfsys@invoke{ \lxSVG@closescope }\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}{{}}}} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope{{ {}{}{}}}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}}\gamma^{\prime}_{2}.
Finally, we might have and with and s\mathrel{\leavevmode\hbox to7.02pt{\vbox to11.89pt{\pgfpicture\makeatletter\hbox{\hskip 3.51248pt\lower-8.41377pt\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{ }\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ } {{}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}{}{{ {}{}}}{ {}{}} {{}{{}}}{{}{}}{}{{}{}} { }{{{{}}\pgfsys@beginscope\pgfsys@invoke{ }\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{-1.39027pt}{-1.75848pt}\pgfsys@invoke{ }\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{ }\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{{\vbox{\halign{\hfil#\hfil\cr\cr\vskip 0.017pt\cr\hbox{{\scriptstyle\eta}}\cr}}}} }}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} { {}{}{}}{{{}}{{}}}{{}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}{}{{ {}{}}}{ {}{}} {{}{{}}}{{}{}}{}{{}{}} { }{{{{}}\pgfsys@beginscope\pgfsys@invoke{ }\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{0.0pt}{-5.74736pt}\pgfsys@invoke{ }\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{ }\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{} }}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} {{}{{}}{}{{}}{}{ {}} {}{}}{{}{}}{}{}{}{{}}{{}}{{}{}}{{}{}} {{{{}{}{{}} }}{{}}}{{{{}{}{{}} }}{{}}{{}}} {{{{}{}{{}} }}{{}} {}{}{} {}{}{} {}{}{} {}{}{} }{{{{}{}{{}} }}{{}} {}{}{} {}{}{} {}{}{} {}{}{} }{{{{}{}{{}} }}{{}} {}{}{} {}{}{} }{{{{}{}{{}} }}{{}}}{{{{}{}{{}} }}{{}} {{}} } {{{{}{}{{}} }}{{}} }{{{{}{}{{}} }}{{}}{{}}}{}{}{}{}{{}}\pgfsys@moveto{-3.31248pt}{-3.6807pt}\pgfsys@lineto{-3.31248pt}{-3.6807pt}\pgfsys@curveto{-3.16898pt}{-3.48955pt}{-3.02547pt}{-3.33626pt}{-2.88196pt}{-3.33626pt}\pgfsys@curveto{-2.73845pt}{-3.33626pt}{-2.59494pt}{-3.48955pt}{-2.45143pt}{-3.6807pt}\pgfsys@curveto{-2.30792pt}{-3.87184pt}{-2.16441pt}{-4.02513pt}{-2.0209pt}{-4.02513pt}\pgfsys@curveto{-1.8774pt}{-4.02513pt}{-1.73389pt}{-3.87184pt}{-1.59038pt}{-3.6807pt}\pgfsys@curveto{-1.44676pt}{-3.48955pt}{-1.30325pt}{-3.33626pt}{-1.15974pt}{-3.33626pt}\pgfsys@curveto{-1.01624pt}{-3.33626pt}{-0.87273pt}{-3.48955pt}{-0.72922pt}{-3.6807pt}\pgfsys@curveto{-0.58571pt}{-3.87184pt}{-0.4422pt}{-4.02513pt}{-0.29869pt}{-4.02513pt}\pgfsys@curveto{-0.15518pt}{-4.02513pt}{-0.01167pt}{-3.87184pt}{0.13184pt}{-3.6807pt}\pgfsys@curveto{0.27545pt}{-3.48955pt}{0.41896pt}{-3.33626pt}{0.56247pt}{-3.33626pt}\pgfsys@curveto{0.70598pt}{-3.33626pt}{0.84949pt}{-3.48955pt}{0.993pt}{-3.6807pt}\pgfsys@lineto{0.99306pt}{-3.6807pt}\pgfsys@lineto{2.91249pt}{-3.6807pt}\pgfsys@stroke\pgfsys@invoke{ }{{}{{}}{}{}{{}}{{{}}{{{}}{\pgfsys@beginscope\pgfsys@invoke{ }\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{3.11249pt}{-3.6807pt}\pgfsys@invoke{ }\pgfsys@invoke{ \lxSVG@closescope }\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}{{}}}} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope{{ {}{}{}}}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}}\epsilon. Then (it cannot be shorter than , because guiding transitions can only be executed en bloc), resulting in
[TABLE]
We finish by invoking the inductive hypothesis on \overline{\gamma_{1}}\ni\gamma^{\prime}_{1}\mathrel{\leavevmode\hbox to8.33pt{\vbox to13.31pt{\pgfpicture\makeatletter\hbox{\hskip 4.16664pt\lower-9.12378pt\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{ }\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ } {{}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}{}{{ {}{}}}{ {}{}} {{}{{}}}{{}{}}{}{{}{}} { }{{{{}}\pgfsys@beginscope\pgfsys@invoke{ }\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{-2.04443pt}{-2.46849pt}\pgfsys@invoke{ }\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{ }\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{{\vbox{\halign{\hfil#\hfil\cr\cr\vskip 0.017pt\cr\hbox{{\scriptstyle\delta_{1}}}\cr}}}} }}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} { {}{}{}}{{{}}{{}}}{{}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}{}{{ {}{}}}{ {}{}} {{}{{}}}{{}{}}{}{{}{}} { }{{{{}}\pgfsys@beginscope\pgfsys@invoke{ }\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{0.0pt}{-6.45737pt}\pgfsys@invoke{ }\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{ }\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{} }}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} {{}{{}}{}{{}}{}{ {}} {}{}}{{}{}}{}{}{}{{}}{{}}{{}{}}{{}{}} {{{{}{}{{}} }}{{}}}{{{{}{}{{}} }}{{}}{{}}} {{{{}{}{{}} }}{{}} {}{}{} {}{}{} {}{}{} {}{}{} }{{{{}{}{{}} }}{{}} {}{}{} {}{}{} {}{}{} {}{}{} }{{{{}{}{{}} }}{{}} {}{}{} {}{}{} {}{}{} {}{}{} }{{{{}{}{{}} }}{{}} {}{}{} {}{}{} }{{{{}{}{{}} }}{{}}}{{{{}{}{{}} }}{{}} {{}} } {{{{}{}{{}} }}{{}} }{{{{}{}{{}} }}{{}}{{}}}{}{}{}{}{{}}\pgfsys@moveto{-3.96664pt}{-4.3907pt}\pgfsys@lineto{-3.96664pt}{-4.3907pt}\pgfsys@curveto{-3.82314pt}{-4.19955pt}{-3.67963pt}{-4.04626pt}{-3.53612pt}{-4.04626pt}\pgfsys@curveto{-3.39261pt}{-4.04626pt}{-3.2491pt}{-4.19955pt}{-3.10559pt}{-4.3907pt}\pgfsys@curveto{-2.96208pt}{-4.58185pt}{-2.81857pt}{-4.73514pt}{-2.67506pt}{-4.73514pt}\pgfsys@curveto{-2.53156pt}{-4.73514pt}{-2.38805pt}{-4.58185pt}{-2.24454pt}{-4.3907pt}\pgfsys@curveto{-2.10092pt}{-4.19955pt}{-1.95741pt}{-4.04626pt}{-1.8139pt}{-4.04626pt}\pgfsys@curveto{-1.6704pt}{-4.04626pt}{-1.52689pt}{-4.19955pt}{-1.38338pt}{-4.3907pt}\pgfsys@curveto{-1.23987pt}{-4.58185pt}{-1.09636pt}{-4.73514pt}{-0.95285pt}{-4.73514pt}\pgfsys@curveto{-0.80934pt}{-4.73514pt}{-0.66583pt}{-4.58185pt}{-0.52232pt}{-4.3907pt}\pgfsys@curveto{-0.37871pt}{-4.19955pt}{-0.2352pt}{-4.04626pt}{-0.09169pt}{-4.04626pt}\pgfsys@curveto{0.05182pt}{-4.04626pt}{0.19533pt}{-4.19955pt}{0.33884pt}{-4.3907pt}\pgfsys@curveto{0.48235pt}{-4.58185pt}{0.62585pt}{-4.73514pt}{0.76936pt}{-4.73514pt}\pgfsys@curveto{0.91287pt}{-4.73514pt}{1.05638pt}{-4.58185pt}{1.19989pt}{-4.3907pt}\pgfsys@curveto{1.3435pt}{-4.19955pt}{1.48701pt}{-4.04626pt}{1.63052pt}{-4.04626pt}\pgfsys@curveto{1.77403pt}{-4.04626pt}{1.91754pt}{-4.19955pt}{2.06105pt}{-4.3907pt}\pgfsys@lineto{2.06111pt}{-4.3907pt}\pgfsys@lineto{3.56665pt}{-4.3907pt}\pgfsys@stroke\pgfsys@invoke{ }{{}{{}}{}{}{{}}{{{}}{{{}}{\pgfsys@beginscope\pgfsys@invoke{ }\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{3.76665pt}{-4.3907pt}\pgfsys@invoke{ }\pgfsys@invoke{ \lxSVG@closescope }\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}{{}}}} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope{{ {}{}{}}}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}}\gamma^{\prime}_{2}. ∎
Corollary 6**.**
* for every guided relation .*
Corollary 7**.**
* for every guided relation .*
Corollary 8**.**
Null closure preserves being call-reduce-closed:
[TABLE]
Proof.
. ∎
Proposition 9**.**
* and .*
Proof.
Redo the proof of Proposition 4, using Corollaries 6 and 7 instead of Lemmas 2 and 3. ∎
To proceed to phase computation, we define two variants of derivatives for guided relations: the first one, analogous to Definition 9, separates the guiding transitions, while the second, weaker, concatenates them to the remaining relation:
Definition 11**.**
A derivative of degree of a guided relation by a symbol is any collection of pairs with and , such that for each and we have
[TABLE]
A guided relation is -regular if it belongs to some family of size , closed under derivatives of degree . It is -regular if it is -regular for some , and regular if it is -regular for some .
Definition 12**.**
A flat derivative of degree of a guided relation by a symbol is any collection of guided relations with , such that for each :
[TABLE]
Algorithm 7**.**
Calculating for call-reduce-closed, proper
1* *
2* foreach :*
3* foreach :*
4* *
5* if ,** foreach :*
6* foreach :*
7* *
8* return *
When transitions are forgotten, both above definitions degenerate to Brzozowski derivatives. The distinction is necessary for clean separation of concerns in our algorithms, and for their complexity analysis. In particular, only the weaker notion of derivatives is needed to calculate null closures of parsing relations, as shown in Algorithm 7. We only prove its correctness for guided relations which are proper, i.e., can be obtained as null closures of non-guided relations.
Proposition 10**.**
For a call-reduce-closed, proper in which every configuration has the state at its bottom, Algorithm 7 correctly returns .
Proof.
Claim 1: . Every pair in must come from
[TABLE]
Let be the canonical decomposition of , witnessed by , and . If , we have and , from where
[TABLE]
.
Otherwise, for some , we have and (the state surely exists, as every configuration has non-nullable at its bottom). Because begins with , we might split \sigma_{\scriptscriptstyle-}\mathrel{\leavevmode\hbox to8.09pt{\vbox to11.89pt{\pgfpicture\makeatletter\hbox{\hskip 4.04582pt\lower-8.41377pt\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{ }\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ } {{}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}{}{{ {}{}}}{ {}{}} {{}{{}}}{{}{}}{}{{}{}} { }{{{{}}\pgfsys@beginscope\pgfsys@invoke{ }\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{-1.92361pt}{-1.75848pt}\pgfsys@invoke{ }\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{ }\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{{\vbox{\halign{\hfil#\hfil\cr\cr\vskip 0.017pt\cr\hbox{{\scriptstyle\eta_{\scriptscriptstyle-}}}\cr}}}} }}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} { {}{}{}}{{{}}{{}}}{{}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}{}{{ {}{}}}{ {}{}} {{}{{}}}{{}{}}{}{{}{}} { }{{{{}}\pgfsys@beginscope\pgfsys@invoke{ }\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{0.0pt}{-5.74736pt}\pgfsys@invoke{ }\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{ }\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{} }}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} {{}{{}}{}{{}}{}{ {}} {}{}}{{}{}}{}{}{}{{}}{{}}{{}{}}{{}{}} {{{{}{}{{}} }}{{}}}{{{{}{}{{}} }}{{}}{{}}} {{{{}{}{{}} }}{{}} {}{}{} {}{}{} {}{}{} {}{}{} }{{{{}{}{{}} }}{{}} {}{}{} {}{}{} {}{}{} {}{}{} }{{{{}{}{{}} }}{{}} {}{}{} {}{}{} {}{}{} {}{}{} }{{{{}{}{{}} }}{{}} {}{}{} {}{}{} }{{{{}{}{{}} }}{{}}}{{{{}{}{{}} }}{{}} {{}} } {{{{}{}{{}} }}{{}} }{{{{}{}{{}} }}{{}}{{}}}{}{}{}{}{{}}\pgfsys@moveto{-3.84583pt}{-3.6807pt}\pgfsys@lineto{-3.84583pt}{-3.6807pt}\pgfsys@curveto{-3.70232pt}{-3.48955pt}{-3.5588pt}{-3.33626pt}{-3.4153pt}{-3.33626pt}\pgfsys@curveto{-3.27179pt}{-3.33626pt}{-3.12828pt}{-3.48955pt}{-2.98477pt}{-3.6807pt}\pgfsys@curveto{-2.84126pt}{-3.87184pt}{-2.69775pt}{-4.02513pt}{-2.55424pt}{-4.02513pt}\pgfsys@curveto{-2.41074pt}{-4.02513pt}{-2.26723pt}{-3.87184pt}{-2.12372pt}{-3.6807pt}\pgfsys@curveto{-1.9801pt}{-3.48955pt}{-1.8366pt}{-3.33626pt}{-1.69308pt}{-3.33626pt}\pgfsys@curveto{-1.54958pt}{-3.33626pt}{-1.40607pt}{-3.48955pt}{-1.26256pt}{-3.6807pt}\pgfsys@curveto{-1.11905pt}{-3.87184pt}{-0.97554pt}{-4.02513pt}{-0.83203pt}{-4.02513pt}\pgfsys@curveto{-0.68852pt}{-4.02513pt}{-0.54501pt}{-3.87184pt}{-0.4015pt}{-3.6807pt}\pgfsys@curveto{-0.25789pt}{-3.48955pt}{-0.11438pt}{-3.33626pt}{0.02913pt}{-3.33626pt}\pgfsys@curveto{0.17264pt}{-3.33626pt}{0.31615pt}{-3.48955pt}{0.45966pt}{-3.6807pt}\pgfsys@curveto{0.60316pt}{-3.87184pt}{0.74667pt}{-4.02513pt}{0.89018pt}{-4.02513pt}\pgfsys@curveto{1.03369pt}{-4.02513pt}{1.1772pt}{-3.87184pt}{1.32071pt}{-3.6807pt}\pgfsys@curveto{1.46432pt}{-3.48955pt}{1.60783pt}{-3.33626pt}{1.75134pt}{-3.33626pt}\pgfsys@curveto{1.89485pt}{-3.33626pt}{2.03836pt}{-3.48955pt}{2.18187pt}{-3.6807pt}\pgfsys@lineto{2.18193pt}{-3.6807pt}\pgfsys@lineto{3.44583pt}{-3.6807pt}\pgfsys@stroke\pgfsys@invoke{ }{{}{{}}{}{}{{}}{{{}}{{{}}{\pgfsys@beginscope\pgfsys@invoke{ }\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{3.64583pt}{-3.6807pt}\pgfsys@invoke{ }\pgfsys@invoke{ \lxSVG@closescope }\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}{{}}}} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope{{ {}{}{}}}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}}\epsilon as \sigma_{\scriptscriptstyle-}=t{\cdot}\sigma_{*}\mathrel{\leavevmode\hbox to8.18pt{\vbox to11.89pt{\pgfpicture\makeatletter\hbox{\hskip 4.09026pt\lower-8.41377pt\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{ }\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ } {{}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}{}{{ {}{}}}{ {}{}} {{}{{}}}{{}{}}{}{{}{}} { }{{{{}}\pgfsys@beginscope\pgfsys@invoke{ }\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{-1.96805pt}{-1.75848pt}\pgfsys@invoke{ }\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{ }\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{{\vbox{\halign{\hfil#\hfil\cr\cr\vskip 0.017pt\cr\hbox{{\scriptstyle\eta_{t}}}\cr}}}} }}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} { {}{}{}}{{{}}{{}}}{{}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}{}{{ {}{}}}{ {}{}} {{}{{}}}{{}{}}{}{{}{}} { }{{{{}}\pgfsys@beginscope\pgfsys@invoke{ }\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{0.0pt}{-5.74736pt}\pgfsys@invoke{ }\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{ }\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{} }}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} {{}{{}}{}{{}}{}{ {}} {}{}}{{}{}}{}{}{}{{}}{{}}{{}{}}{{}{}} {{{{}{}{{}} }}{{}}}{{{{}{}{{}} }}{{}}{{}}} {{{{}{}{{}} }}{{}} {}{}{} {}{}{} {}{}{} {}{}{} }{{{{}{}{{}} }}{{}} {}{}{} {}{}{} {}{}{} {}{}{} }{{{{}{}{{}} }}{{}} {}{}{} {}{}{} {}{}{} {}{}{} }{{{{}{}{{}} }}{{}} {}{}{} {}{}{} }{{{{}{}{{}} }}{{}}}{{{{}{}{{}} }}{{}} {{}} } {{{{}{}{{}} }}{{}} }{{{{}{}{{}} }}{{}}{{}}}{}{}{}{}{{}}\pgfsys@moveto{-3.89026pt}{-3.6807pt}\pgfsys@lineto{-3.89026pt}{-3.6807pt}\pgfsys@curveto{-3.74675pt}{-3.48955pt}{-3.60324pt}{-3.33626pt}{-3.45973pt}{-3.33626pt}\pgfsys@curveto{-3.31622pt}{-3.33626pt}{-3.17271pt}{-3.48955pt}{-3.0292pt}{-3.6807pt}\pgfsys@curveto{-2.8857pt}{-3.87184pt}{-2.74219pt}{-4.02513pt}{-2.59868pt}{-4.02513pt}\pgfsys@curveto{-2.45517pt}{-4.02513pt}{-2.31166pt}{-3.87184pt}{-2.16815pt}{-3.6807pt}\pgfsys@curveto{-2.02454pt}{-3.48955pt}{-1.88103pt}{-3.33626pt}{-1.73752pt}{-3.33626pt}\pgfsys@curveto{-1.59401pt}{-3.33626pt}{-1.4505pt}{-3.48955pt}{-1.30699pt}{-3.6807pt}\pgfsys@curveto{-1.16348pt}{-3.87184pt}{-1.01997pt}{-4.02513pt}{-0.87646pt}{-4.02513pt}\pgfsys@curveto{-0.73296pt}{-4.02513pt}{-0.58945pt}{-3.87184pt}{-0.44594pt}{-3.6807pt}\pgfsys@curveto{-0.30232pt}{-3.48955pt}{-0.15881pt}{-3.33626pt}{-0.0153pt}{-3.33626pt}\pgfsys@curveto{0.1282pt}{-3.33626pt}{0.27171pt}{-3.48955pt}{0.41522pt}{-3.6807pt}\pgfsys@curveto{0.55873pt}{-3.87184pt}{0.70224pt}{-4.02513pt}{0.84575pt}{-4.02513pt}\pgfsys@curveto{0.98926pt}{-4.02513pt}{1.13277pt}{-3.87184pt}{1.27628pt}{-3.6807pt}\pgfsys@curveto{1.41989pt}{-3.48955pt}{1.5634pt}{-3.33626pt}{1.70691pt}{-3.33626pt}\pgfsys@curveto{1.85042pt}{-3.33626pt}{1.99393pt}{-3.48955pt}{2.13744pt}{-3.6807pt}\pgfsys@lineto{2.1375pt}{-3.6807pt}\pgfsys@lineto{3.49026pt}{-3.6807pt}\pgfsys@stroke\pgfsys@invoke{ }{{}{{}}{}{}{{}}{{{}}{{{}}{\pgfsys@beginscope\pgfsys@invoke{ }\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{3.69026pt}{-3.6807pt}\pgfsys@invoke{ }\pgfsys@invoke{ \lxSVG@closescope }\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}{{}}}} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope{{ {}{}{}}}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}}\sigma_{*}\mathrel{\leavevmode\hbox to8.62pt{\vbox to11.89pt{\pgfpicture\makeatletter\hbox{\hskip 4.31248pt\lower-8.41377pt\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{ }\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ } {{}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}{}{{ {}{}}}{ {}{}} {{}{{}}}{{}{}}{}{{}{}} { }{{{{}}\pgfsys@beginscope\pgfsys@invoke{ }\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{-2.19028pt}{-1.75848pt}\pgfsys@invoke{ }\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{ }\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{{\vbox{\halign{\hfil#\hfil\cr\cr\vskip 0.017pt\cr\hbox{{\scriptstyle\eta_{*}}}\cr}}}} }}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} { {}{}{}}{{{}}{{}}}{{}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}{}{{ {}{}}}{ {}{}} {{}{{}}}{{}{}}{}{{}{}} { }{{{{}}\pgfsys@beginscope\pgfsys@invoke{ }\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{0.0pt}{-5.74736pt}\pgfsys@invoke{ }\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{ }\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{} }}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} {{}{{}}{}{{}}{}{ {}} {}{}}{{}{}}{}{}{}{{}}{{}}{{}{}}{{}{}} {{{{}{}{{}} }}{{}}}{{{{}{}{{}} }}{{}}{{}}} {{{{}{}{{}} }}{{}} {}{}{} {}{}{} {}{}{} {}{}{} }{{{{}{}{{}} }}{{}} {}{}{} {}{}{} {}{}{} {}{}{} }{{{{}{}{{}} }}{{}} {}{}{} {}{}{} {}{}{} {}{}{} }{{{{}{}{{}} }}{{}} {}{}{} {}{}{} }{{{{}{}{{}} }}{{}}}{{{{}{}{{}} }}{{}} {{}} } {{{{}{}{{}} }}{{}} }{{{{}{}{{}} }}{{}}{{}}}{}{}{}{}{{}}\pgfsys@moveto{-4.11249pt}{-3.6807pt}\pgfsys@lineto{-4.11249pt}{-3.6807pt}\pgfsys@curveto{-3.96898pt}{-3.48955pt}{-3.82547pt}{-3.33626pt}{-3.68196pt}{-3.33626pt}\pgfsys@curveto{-3.53845pt}{-3.33626pt}{-3.39494pt}{-3.48955pt}{-3.25143pt}{-3.6807pt}\pgfsys@curveto{-3.10793pt}{-3.87184pt}{-2.96442pt}{-4.02513pt}{-2.8209pt}{-4.02513pt}\pgfsys@curveto{-2.6774pt}{-4.02513pt}{-2.53389pt}{-3.87184pt}{-2.39038pt}{-3.6807pt}\pgfsys@curveto{-2.24677pt}{-3.48955pt}{-2.10326pt}{-3.33626pt}{-1.95975pt}{-3.33626pt}\pgfsys@curveto{-1.81624pt}{-3.33626pt}{-1.67273pt}{-3.48955pt}{-1.52922pt}{-3.6807pt}\pgfsys@curveto{-1.38571pt}{-3.87184pt}{-1.2422pt}{-4.02513pt}{-1.0987pt}{-4.02513pt}\pgfsys@curveto{-0.95518pt}{-4.02513pt}{-0.81168pt}{-3.87184pt}{-0.66817pt}{-3.6807pt}\pgfsys@curveto{-0.52455pt}{-3.48955pt}{-0.38104pt}{-3.33626pt}{-0.23753pt}{-3.33626pt}\pgfsys@curveto{-0.09402pt}{-3.33626pt}{0.04948pt}{-3.48955pt}{0.193pt}{-3.6807pt}\pgfsys@curveto{0.3365pt}{-3.87184pt}{0.48001pt}{-4.02513pt}{0.62352pt}{-4.02513pt}\pgfsys@curveto{0.76703pt}{-4.02513pt}{0.91054pt}{-3.87184pt}{1.05405pt}{-3.6807pt}\pgfsys@curveto{1.19766pt}{-3.48955pt}{1.34117pt}{-3.33626pt}{1.48468pt}{-3.33626pt}\pgfsys@curveto{1.62819pt}{-3.33626pt}{1.7717pt}{-3.48955pt}{1.9152pt}{-3.6807pt}\pgfsys@lineto{1.91527pt}{-3.6807pt}\pgfsys@lineto{3.7125pt}{-3.6807pt}\pgfsys@stroke\pgfsys@invoke{ }{{}{{}}{}{}{{}}{{{}}{{{}}{\pgfsys@beginscope\pgfsys@invoke{ }\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{3.91249pt}{-3.6807pt}\pgfsys@invoke{ }\pgfsys@invoke{ \lxSVG@closescope }\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}{{}}}} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope{{ {}{}{}}}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}}\epsilon, obtaining
[TABLE]
Claim 2: is null-closed. This is because it is obtained from null-closed pieces ( and are by definition, while and consist only of transitions) by operations which preserve being null-closed (concatenation, union, and derivatives).
Claim 3: . Consider any pair added to . If it was added in line 4, it must be of the form
[TABLE]
for (\gamma_{1},{\leavevmode\hbox to6.61pt{\vbox to8.1pt{\pgfpicture\makeatletter\hbox{\hskip 3.30612pt\lower-2.5pt\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{ }\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ } {{}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}{}{{ {}{}}}{ {}{}} {{}{{}}}{{}{}}{}{{}{}} { }{{{{}}\pgfsys@beginscope\pgfsys@invoke{ }\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{-3.10612pt}{-0.94444pt}\pgfsys@invoke{ }\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{ }\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{{\eta_{1}}} }}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} {{}}{{{}}{{}}}{}{{}}{}{ {}}{{{}}{{}}} {}{}{}{}{}{}{{}}\pgfsys@moveto{3.10612pt}{4.22221pt}\pgfsys@lineto{-2.70613pt}{4.22221pt}\pgfsys@stroke\pgfsys@invoke{ }{{}{{}}{}{}{{}}{{{}}{{{}}{\pgfsys@beginscope\pgfsys@invoke{ }\pgfsys@transformcm{-1.0}{0.0}{0.0}{-1.0}{-2.90613pt}{4.22221pt}\pgfsys@invoke{ }\pgfsys@invoke{ \lxSVG@closescope }\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}{{}}}} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope{{ {}{}{}}}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}})\in\overline{\mathcal{C}(t)}, and (\gamma_{2},{\leavevmode\hbox to6.2pt{\vbox to10.1pt{\pgfpicture\makeatletter\hbox{\hskip 3.09778pt\lower-3.49956pt\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{ }\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ } {{}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}{}{{ {}{}}}{ {}{}} {{}{{}}}{{}{}}{}{{}{}} { }{{{{}}\pgfsys@beginscope\pgfsys@invoke{ }\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{-2.89778pt}{-2.056pt}\pgfsys@invoke{ }\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{ }\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{{\delta_{2}}} }}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} {{}}{{{}}{{}}}{}{{}}{}{ {}}{{{}}{{}}} {}{}{}{}{}{}{{}}\pgfsys@moveto{2.89778pt}{5.22177pt}\pgfsys@lineto{-2.49779pt}{5.22177pt}\pgfsys@stroke\pgfsys@invoke{ }{{}{{}}{}{}{{}}{{{}}{{{}}{\pgfsys@beginscope\pgfsys@invoke{ }\pgfsys@transformcm{-1.0}{0.0}{0.0}{-1.0}{-2.69778pt}{5.22177pt}\pgfsys@invoke{ }\pgfsys@invoke{ \lxSVG@closescope }\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}{{}}}} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope{{ {}{}{}}}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}})\in\Psi_{0}. We now have:
[TABLE]
Pairs added in line 7 must be of the form
[TABLE]
for (\gamma_{1},{\leavevmode\hbox to6.61pt{\vbox to8.1pt{\pgfpicture\makeatletter\hbox{\hskip 3.30612pt\lower-2.5pt\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{ }\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ } {{}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}{}{{ {}{}}}{ {}{}} {{}{{}}}{{}{}}{}{{}{}} { }{{{{}}\pgfsys@beginscope\pgfsys@invoke{ }\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{-3.10612pt}{-0.94444pt}\pgfsys@invoke{ }\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{ }\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{{\eta_{1}}} }}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} {{}}{{{}}{{}}}{}{{}}{}{ {}}{{{}}{{}}} {}{}{}{}{}{}{{}}\pgfsys@moveto{3.10612pt}{4.22221pt}\pgfsys@lineto{-2.70613pt}{4.22221pt}\pgfsys@stroke\pgfsys@invoke{ }{{}{{}}{}{}{{}}{{{}}{{{}}{\pgfsys@beginscope\pgfsys@invoke{ }\pgfsys@transformcm{-1.0}{0.0}{0.0}{-1.0}{-2.90613pt}{4.22221pt}\pgfsys@invoke{ }\pgfsys@invoke{ \lxSVG@closescope }\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}{{}}}} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope{{ {}{}{}}}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}})\in\overline{\mathcal{C}(s^{\prime})} and (\gamma_{2},{\leavevmode\hbox to6.2pt{\vbox to10.1pt{\pgfpicture\makeatletter\hbox{\hskip 3.09778pt\lower-3.49956pt\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{ }\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ } {{}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}{}{{ {}{}}}{ {}{}} {{}{{}}}{{}{}}{}{{}{}} { }{{{{}}\pgfsys@beginscope\pgfsys@invoke{ }\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{-2.89778pt}{-2.056pt}\pgfsys@invoke{ }\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{ }\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{{\delta_{2}}} }}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} {{}}{{{}}{{}}}{}{{}}{}{ {}}{{{}}{{}}} {}{}{}{}{}{}{{}}\pgfsys@moveto{2.89778pt}{5.22177pt}\pgfsys@lineto{-2.49779pt}{5.22177pt}\pgfsys@stroke\pgfsys@invoke{ }{{}{{}}{}{}{{}}{{{}}{{{}}{\pgfsys@beginscope\pgfsys@invoke{ }\pgfsys@transformcm{-1.0}{0.0}{0.0}{-1.0}{-2.69778pt}{5.22177pt}\pgfsys@invoke{ }\pgfsys@invoke{ \lxSVG@closescope }\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}{{}}}} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope{{ {}{}{}}}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}})\in\Psi_{1}. In this case we have:
[TABLE]
Finale: Combine the above claims with Corollaries 6 and 7 to obtain
[TABLE]
∎
Algorithm 8**.**
Calculating for call-reduce-closed, proper (final)
1* *
2* foreach :*
3* foreach :*
4* *
5* if :*
6* *
7* foreach :*
8* foreach :*
9* *
10* return *
One last observation we apply is that derivatives distribute over union, and thus the inner loops in lines 5 and 6 can be pulled out to the top level, resulting in Algorithm 8.
Algorithm 9**.**
Parsing
1* *
2* foreach *(in order):
3* *
4* *
5* foreach :*
6* *\Delta_{\textup{out}}\mathrel{\mathop{:}}=\Delta_{\textup{out}}\ \cup\ \{\delta{\cdot}\eta:\ (\eta,{\leavevmode\hbox to3.96pt{\vbox to8.66pt{\pgfpicture\makeatletter\hbox{\hskip 1.97777pt\lower-2.77777pt\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{ }\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ } {{}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}{}{{ {}{}}}{ {}{}} {{}{{}}}{{}{}}{}{{}{}} { }{{{{}}\pgfsys@beginscope\pgfsys@invoke{ }\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{-1.77777pt}{-2.77777pt}\pgfsys@invoke{ }\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{ }\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{{\delta}} }}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} {{}}{{{}}{{}}}{}{{}}{}{ {}}{{{}}{{}}} {}{}{}{}{}{}{{}}\pgfsys@moveto{1.77777pt}{4.49998pt}\pgfsys@lineto{-1.37778pt}{4.49998pt}\pgfsys@stroke\pgfsys@invoke{ }{{}{{}}{}{}{{}}{{{}}{{{}}{\pgfsys@beginscope\pgfsys@invoke{ }\pgfsys@transformcm{-1.0}{0.0}{0.0}{-1.0}{-1.57777pt}{4.49998pt}\pgfsys@invoke{ }\pgfsys@invoke{ \lxSVG@closescope }\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}{{}}}} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope{{ {}{}{}}}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}})\in\Psi^{\prime},\eta\in D_{\epsilon}^{*}\}
7* return *
Extracting the language of accepting transition sequences from the parsing relation for the whole input is also a bit more complicated, because any remaining guiding transitions need to be executed. Thus we replace our main Algorithm 1 with Algorithm 9. Overall, we realize generalized context-free parsing, using any representation of guided relations supporting API 10.
API 10**.**
Operations on relations required for full parsing.
- •
* \tab,*
- •
* \tab,*
- •
* \tab,*
- •
* \tab,*
- •
* \tab\{\delta{\cdot}\eta:(\eta,{\leavevmode\hbox to3.96pt{\vbox to8.66pt{\pgfpicture\makeatletter\hbox{\hskip 1.97777pt\lower-2.77777pt\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{ }\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ } {{}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}{}{{ {}{}}}{ {}{}} {{}{{}}}{{}{}}{}{{}{}} { }{{{{}}\pgfsys@beginscope\pgfsys@invoke{ }\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{-1.77777pt}{-2.77777pt}\pgfsys@invoke{ }\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{ }\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{{\delta}} }}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} {{}}{{{}}{{}}}{}{{}}{}{ {}}{{{}}{{}}} {}{}{}{}{}{}{{}}\pgfsys@moveto{1.77777pt}{4.49998pt}\pgfsys@lineto{-1.37778pt}{4.49998pt}\pgfsys@stroke\pgfsys@invoke{ }{{}{{}}{}{}{{}}{{{}}{{{}}{\pgfsys@beginscope\pgfsys@invoke{ }\pgfsys@transformcm{-1.0}{0.0}{0.0}{-1.0}{-1.57777pt}{4.49998pt}\pgfsys@invoke{ }\pgfsys@invoke{ \lxSVG@closescope }\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}{{}}}} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope{{ {}{}{}}}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}})\in\Psi\},*
- •
* \tab.*
4 Representations
We now make concrete the key observation underlying this paper: that although the sets of reachable parser configurations are sometimes infinite, their regularity makes it possible to manipulate them efficiently.
4.1 Parsing languages and relations
API 11**.**
Required operations on atomic languages.
- •
* \tab,*
- •
* \tabwhether ,*
- •
* \tab.*
We begin top-down, by presenting a data structure implementing API 5. To make it independent of the grammar, let us parameterize it with a data type , representing a finite family of languages over , realizing API 11. We allow the first argument of prepend to be any element of .
Denote by the -free part of (i.e., ). Our implementation is based on the following observation:
Proposition 11**.**
Let be a sequence of languages over , in which each is obtained by applying one of the operations of API 5 to some with . Then there exists a finite collection of pairs with and , such that
[TABLE]
Proof.
We argue by induction on . For languages returned by derivative, the inductive step follows by
[TABLE]
and applying the inductive hypothesis to the latter part of the sum. All other cases are trivial. ∎
Our proposed data structure keeps, for each , the set of pairs warranted above, and an additional bit denoting whether . All operations have natural implementations, with derivative following the above proof. Their complexity will be analyzed in Section 6. Here, we note only that, as language union is idempotent, any duplicate pairs encountered can and should be merged. Thus, each is represented by at most pairs.
The whole structure can be viewed as a DAG, whose vertices correspond to the languages . Edges, labeled with elements of , follow the references from Proposition 11: an edge with label is present iff the decomposition of contains the pair . Each vertex is additionally labeled with the bit—vertices at which this bit is set will be called final.
API 12**.**
Required operations on atomic relations ( represents relations over , i.e., subsets of ).
- •
* \tab,*
- •
* \tab,*
- •
* \tab.*
In order to adapt this data structure to represent parsing relations, we need to additionally keep track of transitions. Instead of the underlying type , let us parameterize it with a type , representing a finite family of guided relations, realizing API 12. Our implementation is supposed to compute flat derivatives, let us then introduce an auxiliary flattening operation, defined for any as
[TABLE]
With denoting the -free part of (i.e., ), we can now show the following generalization of Proposition 11:
Proposition 12**.**
Let be a sequence of guided relations over , in which each is obtained by applying one of the operations of API 10 to some with . Then there exists a finite collection of triples with , and , such that
[TABLE]
Proof.
Again, the only nontrivial operation to be considered in the inductive proof is derivative. This time the inductive step follows from
[TABLE]
∎
Applying this result to our DAG structure requires labeling edges with pairs , with and . Instead of the single bit, vertices need to be labeled with relations over (subsets of )—final vertices are now those with a nonempty label.
As we can see, for edge and vertex labels we need an additional data type, denoted , representing relations over . For efficiency reasons, we allow it to be different from the type returned from derivative and epsilon calls on atomic relations. Realizing our API requires elements of to be merged using set union, flattened. We also require concatenatenation on the left with an atomic or with whatever our prepend method is called. To simplify further reasoning, we combine them into a single operation. Concatenation on the right with elements of is always immediately followed by flattening, and is therefore redundant, as . The requirements are summarized by API 13.
API 13**.**
Required operations on transition relations (subsets of ). represents languages of transitions (i.e., subsets of ).
- •
* \tab,*
- •
* \tab,*
- •
* \tab,*
- •
* \tab.*
It is also clear that if the Boolean type is used in place of (and thus also and ), we are left with the simpler DAG useful for recognition.
4.2 Atomic closures
We now turn to the call-reduce closures of individual states, realizing APIs 11 and 12. The constructive proof of the proposition below presents a possible direct representation using nondeterministic finite automata. The non-relational variant could of course be determinized and minimized, but it might not be advantageous to do so—the price for less nondeterminism is a larger automaton size, and the grammar-related complexity of our complete algorithm depends on both.
Let us denote
[TABLE]
In particular, . By definition, the derivatives of any can be expressed as
[TABLE]
This, however, does not directly lead to a finite family closed under derivatives. Instead, we show the following.
Lemma 13**.**
For every , the derivatives of are
[TABLE]
Proof.
The configurations in are those for which s\mathrel{\leavevmode\hbox to10.34pt{\vbox to13.65pt{\pgfpicture\makeatletter\hbox{\hskip 5.16759pt\lower-9.29378pt\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{ }\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ } {{}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}{}{{ {}{}}}{ {}{}} {{}{{}}}{{}{}}{}{{}{}} { }{{{{}}\pgfsys@beginscope\pgfsys@invoke{ }\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{-3.04538pt}{-2.63849pt}\pgfsys@invoke{ }\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{ }\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{{\vbox{\halign{\hfil#\hfil\cr\cr\vskip 0.017pt\cr\hbox{{\scriptstyle D_{\epsilon}^{*}}}\cr}}}} }}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} { {}{}{}}{{{}}{{}}}{{}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}{}{{ {}{}}}{ {}{}} {{}{{}}}{{}{}}{}{{}{}} { }{{{{}}\pgfsys@beginscope\pgfsys@invoke{ }\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{0.0pt}{-6.62737pt}\pgfsys@invoke{ }\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{ }\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{} }}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} {{}{{}}{}{{}}{}{ {}} {}{}}{{}{}}{}{}{}{{}}{{}}{{}{}}{{}{}} {{{{}{}{{}} }}{{}}}{{{{}{}{{}} }}{{}}{{}}} {{{{}{}{{}} }}{{}} {}{}{} {}{}{} {}{}{} {}{}{} }{{{{}{}{{}} }}{{}} {}{}{} {}{}{} {}{}{} {}{}{} }{{{{}{}{{}} }}{{}} {}{}{} {}{}{} {}{}{} {}{}{} }{{{{}{}{{}} }}{{}} {}{}{} {}{}{} {}{}{} {}{}{} }{{{{}{}{{}} }}{{}} {}{}{} {}{}{} }{{{{}{}{{}} }}{{}}}{{{{}{}{{}} }}{{}} {{}} } {{{{}{}{{}} }}{{}} }{{{{}{}{{}} }}{{}}{{}}}{}{}{}{}{{}}\pgfsys@moveto{-4.96759pt}{-4.5607pt}\pgfsys@lineto{-4.96759pt}{-4.5607pt}\pgfsys@curveto{-4.82408pt}{-4.36955pt}{-4.68057pt}{-4.21626pt}{-4.53706pt}{-4.21626pt}\pgfsys@curveto{-4.39355pt}{-4.21626pt}{-4.25005pt}{-4.36955pt}{-4.10654pt}{-4.5607pt}\pgfsys@curveto{-3.96303pt}{-4.75185pt}{-3.81952pt}{-4.90514pt}{-3.67601pt}{-4.90514pt}\pgfsys@curveto{-3.5325pt}{-4.90514pt}{-3.38899pt}{-4.75185pt}{-3.24548pt}{-4.5607pt}\pgfsys@curveto{-3.10187pt}{-4.36955pt}{-2.95836pt}{-4.21626pt}{-2.81485pt}{-4.21626pt}\pgfsys@curveto{-2.67134pt}{-4.21626pt}{-2.52783pt}{-4.36955pt}{-2.38432pt}{-4.5607pt}\pgfsys@curveto{-2.24081pt}{-4.75185pt}{-2.0973pt}{-4.90514pt}{-1.9538pt}{-4.90514pt}\pgfsys@curveto{-1.81029pt}{-4.90514pt}{-1.66678pt}{-4.75185pt}{-1.52327pt}{-4.5607pt}\pgfsys@curveto{-1.37965pt}{-4.36955pt}{-1.23615pt}{-4.21626pt}{-1.09264pt}{-4.21626pt}\pgfsys@curveto{-0.94913pt}{-4.21626pt}{-0.80562pt}{-4.36955pt}{-0.66211pt}{-4.5607pt}\pgfsys@curveto{-0.5186pt}{-4.75185pt}{-0.37509pt}{-4.90514pt}{-0.23158pt}{-4.90514pt}\pgfsys@curveto{-0.08807pt}{-4.90514pt}{0.05544pt}{-4.75185pt}{0.19894pt}{-4.5607pt}\pgfsys@curveto{0.34256pt}{-4.36955pt}{0.48607pt}{-4.21626pt}{0.62958pt}{-4.21626pt}\pgfsys@curveto{0.77309pt}{-4.21626pt}{0.9166pt}{-4.36955pt}{1.0601pt}{-4.5607pt}\pgfsys@curveto{1.20361pt}{-4.75185pt}{1.34712pt}{-4.90514pt}{1.49063pt}{-4.90514pt}\pgfsys@curveto{1.63414pt}{-4.90514pt}{1.77765pt}{-4.75185pt}{1.92116pt}{-4.5607pt}\pgfsys@curveto{2.06477pt}{-4.36955pt}{2.20828pt}{-4.21626pt}{2.35179pt}{-4.21626pt}\pgfsys@curveto{2.4953pt}{-4.21626pt}{2.63881pt}{-4.36955pt}{2.78232pt}{-4.5607pt}\pgfsys@lineto{2.78238pt}{-4.5607pt}\pgfsys@lineto{4.5676pt}{-4.5607pt}\pgfsys@stroke\pgfsys@invoke{ }{{}{{}}{}{}{{}}{{{}}{{{}}{\pgfsys@beginscope\pgfsys@invoke{ }\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{4.7676pt}{-4.5607pt}\pgfsys@invoke{ }\pgfsys@invoke{ \lxSVG@closescope }\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}{{}}}} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope{{ {}{}{}}}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}}t{\cdot}\sigma. Taking derivative by , we are interested in for some . Therefore, consider a sequence of transitions which realizes s\mathrel{\leavevmode\hbox to7.02pt{\vbox to11.89pt{\pgfpicture\makeatletter\hbox{\hskip 3.51248pt\lower-8.41377pt\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{ }\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ } {{}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}{}{{ {}{}}}{ {}{}} {{}{{}}}{{}{}}{}{{}{}} { }{{{{}}\pgfsys@beginscope\pgfsys@invoke{ }\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{-1.39027pt}{-1.75848pt}\pgfsys@invoke{ }\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{ }\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{{\vbox{\halign{\hfil#\hfil\cr\cr\vskip 0.017pt\cr\hbox{{\scriptstyle\eta}}\cr}}}} }}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} { {}{}{}}{{{}}{{}}}{{}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}{}{{ {}{}}}{ {}{}} {{}{{}}}{{}{}}{}{{}{}} { }{{{{}}\pgfsys@beginscope\pgfsys@invoke{ }\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{0.0pt}{-5.74736pt}\pgfsys@invoke{ }\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{ }\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{} }}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} {{}{{}}{}{{}}{}{ {}} {}{}}{{}{}}{}{}{}{{}}{{}}{{}{}}{{}{}} {{{{}{}{{}} }}{{}}}{{{{}{}{{}} }}{{}}{{}}} {{{{}{}{{}} }}{{}} {}{}{} {}{}{} {}{}{} {}{}{} }{{{{}{}{{}} }}{{}} {}{}{} {}{}{} {}{}{} {}{}{} }{{{{}{}{{}} }}{{}} {}{}{} {}{}{} }{{{{}{}{{}} }}{{}}}{{{{}{}{{}} }}{{}} {{}} } {{{{}{}{{}} }}{{}} }{{{{}{}{{}} }}{{}}{{}}}{}{}{}{}{{}}\pgfsys@moveto{-3.31248pt}{-3.6807pt}\pgfsys@lineto{-3.31248pt}{-3.6807pt}\pgfsys@curveto{-3.16898pt}{-3.48955pt}{-3.02547pt}{-3.33626pt}{-2.88196pt}{-3.33626pt}\pgfsys@curveto{-2.73845pt}{-3.33626pt}{-2.59494pt}{-3.48955pt}{-2.45143pt}{-3.6807pt}\pgfsys@curveto{-2.30792pt}{-3.87184pt}{-2.16441pt}{-4.02513pt}{-2.0209pt}{-4.02513pt}\pgfsys@curveto{-1.8774pt}{-4.02513pt}{-1.73389pt}{-3.87184pt}{-1.59038pt}{-3.6807pt}\pgfsys@curveto{-1.44676pt}{-3.48955pt}{-1.30325pt}{-3.33626pt}{-1.15974pt}{-3.33626pt}\pgfsys@curveto{-1.01624pt}{-3.33626pt}{-0.87273pt}{-3.48955pt}{-0.72922pt}{-3.6807pt}\pgfsys@curveto{-0.58571pt}{-3.87184pt}{-0.4422pt}{-4.02513pt}{-0.29869pt}{-4.02513pt}\pgfsys@curveto{-0.15518pt}{-4.02513pt}{-0.01167pt}{-3.87184pt}{0.13184pt}{-3.6807pt}\pgfsys@curveto{0.27545pt}{-3.48955pt}{0.41896pt}{-3.33626pt}{0.56247pt}{-3.33626pt}\pgfsys@curveto{0.70598pt}{-3.33626pt}{0.84949pt}{-3.48955pt}{0.993pt}{-3.6807pt}\pgfsys@lineto{0.99306pt}{-3.6807pt}\pgfsys@lineto{2.91249pt}{-3.6807pt}\pgfsys@stroke\pgfsys@invoke{ }{{}{{}}{}{}{{}}{{{}}{{{}}{\pgfsys@beginscope\pgfsys@invoke{ }\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{3.11249pt}{-3.6807pt}\pgfsys@invoke{ }\pgfsys@invoke{ \lxSVG@closescope }\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}{{}}}} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope{{ {}{}{}}}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}}t{\cdot}u{\cdot}\sigma^{\prime} and split it at the point where becomes the suffix of the configuration, not to be touched later.
What lies above cannot be empty (as then would get touched), which means that must be the lower state placed on the configration by some call. Thus the sequence looks as follows:
[TABLE]
with {\leavevmode\hbox to6.61pt{\vbox to8.1pt{\pgfpicture\makeatletter\hbox{\hskip 3.30612pt\lower-2.5pt\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{ }\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ } {{}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}{}{{ {}{}}}{ {}{}} {{}{{}}}{{}{}}{}{{}{}} { }{{{{}}\pgfsys@beginscope\pgfsys@invoke{ }\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{-3.10612pt}{-0.94444pt}\pgfsys@invoke{ }\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{ }\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{{\eta_{2}}} }}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} {{}}{{{}}{{}}}{}{{}}{}{ {}}{{{}}{{}}} {}{}{}{}{}{}{{}}\pgfsys@moveto{3.10612pt}{4.22221pt}\pgfsys@lineto{-2.70613pt}{4.22221pt}\pgfsys@stroke\pgfsys@invoke{ }{{}{{}}{}{}{{}}{{{}}{{{}}{\pgfsys@beginscope\pgfsys@invoke{ }\pgfsys@transformcm{-1.0}{0.0}{0.0}{-1.0}{-2.90613pt}{4.22221pt}\pgfsys@invoke{ }\pgfsys@invoke{ \lxSVG@closescope }\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}{{}}}} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope{{ {}{}{}}}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}}\in\Delta_{t^{\prime\prime}\rightsquigarrow t} and (\sigma^{\prime},{\leavevmode\hbox to6.61pt{\vbox to8.1pt{\pgfpicture\makeatletter\hbox{\hskip 3.30612pt\lower-2.5pt\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{ }\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ } {{}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}{}{{ {}{}}}{ {}{}} {{}{{}}}{{}{}}{}{{}{}} { }{{{{}}\pgfsys@beginscope\pgfsys@invoke{ }\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{-3.10612pt}{-0.94444pt}\pgfsys@invoke{ }\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{ }\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{{\eta_{1}}} }}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} {{}}{{{}}{{}}}{}{{}}{}{ {}}{{{}}{{}}} {}{}{}{}{}{}{{}}\pgfsys@moveto{3.10612pt}{4.22221pt}\pgfsys@lineto{-2.70613pt}{4.22221pt}\pgfsys@stroke\pgfsys@invoke{ }{{}{{}}{}{}{{}}{{{}}{{{}}{\pgfsys@beginscope\pgfsys@invoke{ }\pgfsys@transformcm{-1.0}{0.0}{0.0}{-1.0}{-2.90613pt}{4.22221pt}\pgfsys@invoke{ }\pgfsys@invoke{ \lxSVG@closescope }\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}{{}}}} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope{{ {}{}{}}}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}})\in\Phi_{s\rightsquigarrow t^{\prime}}, as required. ∎
Corollary 14**.**
For each , the language and relation are -regular.
Proof.
The definitions of , derivatives, and regularity for relations degenerate cleanly to those for languages when specific transitions are forgotten. Therefore we only need to prove the statement about relations. Indeed, by the above lemma, for each , the family containing and for every is closed under derivatives of degree . ∎
This result can be translated to the null closures of atomic languages and relations: when taking derivatives, nullable states might need to be skipped over (with their nulling transitions given in the first component of the ), which in the language of finite automata corresponds to taking -closure, possibly for the price of increased nondeterminism.
Proposition 15**.**
For each , the guided language and relation are -regular.
Proof.
Again, only the statement about relations needs to be proven.
The required family closed under derivatives are simply the null closures of those given above, i.e., and . We would like to show that for some we have
[TABLE]
To express the transition relations which are to be split off when taking derivatives, let us first give a name to the transition languages from Lemma 13, denoting
[TABLE]
Now consider calculating , fix some and imagine a pair (\gamma,{\leavevmode\hbox to4.37pt{\vbox to8.1pt{\pgfpicture\makeatletter\hbox{\hskip 2.18611pt\lower-2.5pt\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{ }\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ } {{}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}{}{{ {}{}}}{ {}{}} {{}{{}}}{{}{}}{}{{}{}} { }{{{{}}\pgfsys@beginscope\pgfsys@invoke{ }\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{-1.98611pt}{-0.94444pt}\pgfsys@invoke{ }\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{ }\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{{\eta}} }}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} {{}}{{{}}{{}}}{}{{}}{}{ {}}{{{}}{{}}} {}{}{}{}{}{}{{}}\pgfsys@moveto{1.98611pt}{4.22221pt}\pgfsys@lineto{-1.58612pt}{4.22221pt}\pgfsys@stroke\pgfsys@invoke{ }{{}{{}}{}{}{{}}{{{}}{{{}}{\pgfsys@beginscope\pgfsys@invoke{ }\pgfsys@transformcm{-1.0}{0.0}{0.0}{-1.0}{-1.78612pt}{4.22221pt}\pgfsys@invoke{ }\pgfsys@invoke{ \lxSVG@closescope }\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}{{}}}} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope{{ {}{}{}}}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}})\in\overline{\Phi_{s\rightsquigarrow t}} which will participate in this component of the derivative.
The configuration might begin with the state . In this case, we can simply take the derivative and null-close the result. Therefore, must contain .
If does not start with , it must begin by a sequence of guiding transitions which nulls some state . The state must have been present on top of the configuration in to whose null closure belongs. Therefore, we might take , moving to (note that the state might be different than ), and then recursively calculate the derivative . Therefore, must also contain {\leavevmode\hbox to16.63pt{\vbox to9.89pt{\pgfpicture\makeatletter\hbox{\hskip 8.31686pt\lower-3.39333pt\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{ }\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ } {{}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}{}{{ {}{}}}{ {}{}} {{}{{}}}{{}{}}{}{{}{}} { }{{{{}}\pgfsys@beginscope\pgfsys@invoke{ }\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{-8.11687pt}{-2.07333pt}\pgfsys@invoke{ }\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{ }\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{{\Delta_{u^{\prime}\rightsquigarrow\epsilon}}} }}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} {{}}{{{}}{{}}}{}{{}}{}{ {}}{{{}}{{}}} {}{}{}{}{}{}{{}}\pgfsys@moveto{8.11687pt}{5.11554pt}\pgfsys@lineto{-7.71687pt}{5.11554pt}\pgfsys@stroke\pgfsys@invoke{ }{{}{{}}{}{}{{}}{{{}}{{{}}{\pgfsys@beginscope\pgfsys@invoke{ }\pgfsys@transformcm{-1.0}{0.0}{0.0}{-1.0}{-7.91687pt}{5.11554pt}\pgfsys@invoke{ }\pgfsys@invoke{ \lxSVG@closescope }\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}{{}}}} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope{{ {}{}{}}}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}}{\times}\Delta_{u^{\prime},t,t^{\prime\prime}}\ {\cdot}\ \Lambda_{u,t^{\prime\prime},t^{\prime}}.
As there are no other possibilities, we conclude that the relations must be the least (wrt. inclusion) solutions to the equations
[TABLE]
For the derivative , the reasoning is similar: either we go directly to the target relation , splitting off nothing (as was the case in Lemma 13), or we skip over a nullable state by taking derivative by it (this time this can only move us to ) and recursively calculate . We conclude that
[TABLE]
where the singleton case on the left might be incorporated into the family on the right by including the pair in the transition relation for . ∎
As a consequence, once the necessary transition relations and languages have been pre-computed (this might happen at parser generation time), the closures of grammar states, together with all their derivatives, might be represented during parsing simply by pairs of states.
We also need to extract the transition languages corresponging to the empty configuration—or, for guided relations, to the configurations containing only guiding transitions and no states. The first task is simple, because by definition
[TABLE]
In the guided case, we might again need to skip over some nullable states. Denoting
[TABLE]
by an argument analogous to the one above we can conclude that
[TABLE]
The equations given for and follow directly from the above reasoning, but using them as they stand would make our algorithm potentially exponential in the RTN size. Therefore, we rewrite them into an equivalent form.
Let us begin with the original equation, with indices renamed:
[TABLE]
We unwind the recursion to an arbitrary depth , obtaining
[TABLE]
then split the cases for and , and in the latter regroup the final terms and repack the rest using the equation above:
[TABLE]
Analogously, the equations for are replaced by the equivalent
[TABLE]
4.3 Transition relations and languages
Moving down the ladder of abstraction, it is time to find the representations and for transition relations and languages.
For , note that the only way its values, formed from by chains of calls to prepend and union, can ever be examined is by calls to flatten. Consider first a value formed using only prepend, i.e., of the form
[TABLE]
The flattening of such value can be expressed as
[TABLE]
To perform this computation, it is enough to require the type to support a strengthened version of flattening, which we call wrapping:
- •
\tab.
If forming the in question involved some calls to union, we will make use of the fact that flattening distributes over union. The whole expression for can be seen as a DAG with a single distinguished sink node, and edges labeled with calls to prepend. Each path through this DAG represents a union-free expression as discussed above. The relation represented by a node will be the union over all paths from this node to the sink. Shall flatten be requested for a node representing some , the value can be computed following a topological traversal from , in time linear in the size of the DAG, and thus in the number of operations used to form .
For the atomic relations (i.e., the type ), we “represent” them directly by the implementation of their wrap operation. We only need to express how the result of wrap (for an arbitrary ) will look like for the primitives returned by API 12, namely
[TABLE]
This can be given by the following set of recursive equations:
[TABLE]
Of course, it makes sense to permanently remove from the calculation of the above unions those components which are never going to be relevant, i.e., those for which or is empty.
API 14**.**
Required operations on transition languages (subsets of )
- •
* \tab,*
- •
* \tab,*
- •
* \tab,*
- •
* \tabwhether ,*
- •
* \tab(see text)*
As the final piece of data representation, we turn to the type encoding transition languages. The basic operations performed on its elements during parsing are union, concatenation, and checking (non)emptyness (cf. API 14). However, one also needs a rather rich set of “primitives” (which could best be pre-computed during parser generation): singletons of individual shift transitions, , and , and, moreover, the ability to solve equations of the shape given in the above discussion concerning . We employ the equation solver (to be discussed shortly) to compute the primitives by expressing
[TABLE]
This way, we are only left with individual transitions, concatenation, union, and equations expressible in terms of these.
To assess the required capabilities of the equation solver, we will analyze the dependency graph between variables. In particular, when this graph turns out to be acyclic, the solutions might be calculated simply by evaluation. This time, we start with the variables at the end of the dependency chain.
. Every seems to induce a dependency between and each of and . However, this dependency is only real if (respectively, ) is nonempty, which is exactly when (respectively, ) is nullable. Let us then assume that nullability has been computed by some other means (see, e.g., [10], Section 4.2), and announce a right dependency if for some nullable , and a left-right dependency if for some nullable . The direction(s) of dependencies record on which side of their targets a nonempty sequence of transitions might occur.
. Dependencies on are irrelevant, as they will never introduce cycles. The only internal dependencies in this layer are a right dependency if for some nullable . Note that it occurs in accord with an identical dependency .
. The dependency graph between these variables is independent of (unless , in which case the solution is trivially ) and also of , let us then omit them from node descriptions. We have a left-right dependency if and only if is nullable and , which in turns happens if we have a with . Note, that a left-right dependency , witnessed by a nullable as discussed above, implies .
Other variables introduce no potentially cyclic dependencies. This means there are only two ways in which a cycle can appear, making solution-by-evaluation impossible:
There is a cycle of left-right dependencies between the nodes denoted . Consider such a cycle , and imagine a successful run of the RTN in which the state appears. The history of any such run must look as follows:
[TABLE]
(note that this time , and might contain shifts). Now, for each , the dependency is witnessed by t_{i}\mathrel{\leavevmode\hbox to8.13pt{\vbox to11.89pt{\pgfpicture\makeatletter\hbox{\hskip 4.0637pt\lower-8.41377pt\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{ }\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{ }\nullfont\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ } {{}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}{}{{ {}{}}}{ {}{}} {{}{{}}}{{}{}}{}{{}{}} { }{{{{}}\pgfsys@beginscope\pgfsys@invoke{ }\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{-1.9415pt}{-1.75848pt}\pgfsys@invoke{ }\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{ }\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{{\vbox{\halign{\hfil#\hfil\cr\cr\vskip 0.017pt\cr\hbox{{\scriptstyle\eta_{i}}}\cr}}}} }}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} { {}{}{}}{{{}}{{}}}{{}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}{}{{ {}{}}}{ {}{}} {{}{{}}}{{}{}}{}{{}{}} { }{{{{}}\pgfsys@beginscope\pgfsys@invoke{ }\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{0.0pt}{-5.74736pt}\pgfsys@invoke{ }\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{ }\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{} }}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} {{}{{}}{}{{}}{}{ {}} {}{}}{{}{}}{}{}{}{{}}{{}}{{}{}}{{}{}} {{{{}{}{{}} }}{{}}}{{{{}{}{{}} }}{{}}{{}}} {{{{}{}{{}} }}{{}} {}{}{} {}{}{} {}{}{} {}{}{} }{{{{}{}{{}} }}{{}} {}{}{} {}{}{} {}{}{} {}{}{} }{{{{}{}{{}} }}{{}} {}{}{} {}{}{} {}{}{} {}{}{} }{{{{}{}{{}} }}{{}} {}{}{} {}{}{} }{{{{}{}{{}} }}{{}}}{{{{}{}{{}} }}{{}} {{}} } {{{{}{}{{}} }}{{}} }{{{{}{}{{}} }}{{}}{{}}}{}{}{}{}{{}}\pgfsys@moveto{-3.86371pt}{-3.6807pt}\pgfsys@lineto{-3.86371pt}{-3.6807pt}\pgfsys@curveto{-3.7202pt}{-3.48955pt}{-3.57669pt}{-3.33626pt}{-3.43318pt}{-3.33626pt}\pgfsys@curveto{-3.28967pt}{-3.33626pt}{-3.14616pt}{-3.48955pt}{-3.00266pt}{-3.6807pt}\pgfsys@curveto{-2.85915pt}{-3.87184pt}{-2.71564pt}{-4.02513pt}{-2.57213pt}{-4.02513pt}\pgfsys@curveto{-2.42862pt}{-4.02513pt}{-2.28511pt}{-3.87184pt}{-2.1416pt}{-3.6807pt}\pgfsys@curveto{-1.99799pt}{-3.48955pt}{-1.85448pt}{-3.33626pt}{-1.71097pt}{-3.33626pt}\pgfsys@curveto{-1.56746pt}{-3.33626pt}{-1.42395pt}{-3.48955pt}{-1.28044pt}{-3.6807pt}\pgfsys@curveto{-1.13693pt}{-3.87184pt}{-0.99342pt}{-4.02513pt}{-0.84991pt}{-4.02513pt}\pgfsys@curveto{-0.7064pt}{-4.02513pt}{-0.5629pt}{-3.87184pt}{-0.41939pt}{-3.6807pt}\pgfsys@curveto{-0.27577pt}{-3.48955pt}{-0.13226pt}{-3.33626pt}{0.01125pt}{-3.33626pt}\pgfsys@curveto{0.15475pt}{-3.33626pt}{0.29826pt}{-3.48955pt}{0.44177pt}{-3.6807pt}\pgfsys@curveto{0.58528pt}{-3.87184pt}{0.72879pt}{-4.02513pt}{0.8723pt}{-4.02513pt}\pgfsys@curveto{1.01581pt}{-4.02513pt}{1.15932pt}{-3.87184pt}{1.30283pt}{-3.6807pt}\pgfsys@curveto{1.44644pt}{-3.48955pt}{1.58995pt}{-3.33626pt}{1.73346pt}{-3.33626pt}\pgfsys@curveto{1.87697pt}{-3.33626pt}{2.02048pt}{-3.48955pt}{2.16399pt}{-3.6807pt}\pgfsys@lineto{2.16405pt}{-3.6807pt}\pgfsys@lineto{3.46371pt}{-3.6807pt}\pgfsys@stroke\pgfsys@invoke{ }{{}{{}}{}{}{{}}{{{}}{{{}}{\pgfsys@beginscope\pgfsys@invoke{ }\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{3.66371pt}{-3.6807pt}\pgfsys@invoke{ }\pgfsys@invoke{ \lxSVG@closescope }\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}{{}}}} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope{{ {}{}{}}}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}}t_{i+1}{\cdot}u_{i}. At the same time, each is guaranteed to be nullable, which implies that the original run could be replaced with an equally successful
[TABLE]
Iterating this trick, one obtains an infinite set of accepting transition sequences for the same input. Moreover, as the insertions on the left and right of need to be balanced (this is the reason we call such dependencies left-right), the language of those accepting runs is not regular (it is obviously context-free).
Together, either every state on such cycle is useless and could be removed, or the RTN is nonregularly infinitely ambiguous. One could argue that such grammars could be immediately rejected during parser generation555That is what our proof-of-concept implementation does. (the check for this situation is fairly simple). If one decides to handle them, the type needs to be equipped with some mechanism for handling context-free (nonregular) structures. 2. 2.
There is a cycle of joint right and left-right dependencies between the nodes . Again, one could argue that either the whole such cycle is useless, or the RTN is infinitely ambiguous. However, if all such cycles consist of right dependencies only, the situation is somewhat less complicated: mutual dependencies exist only between the variables , and all those dependencies are left-linear. In such case, the languages in question are regular (albeit still infinite) and the only additional feature required of the type is the Kleene star operator.
From the discussion above we can see that, unless one needs to handle infinitely ambiguous grammars, the requirements on are quite small: the primitive operaton in API 14 only needs to handle individual transitions.
This leaves a wide spectrum of implementation possibilities. As mentioned previously, one can instantiate to , obtaining a recognition algorithm. On the other extreme, one can use a free algebra over concatenate and union—the result will be an encoding of all parse trees, very similar in spirit to the SPPF structure employed by polynomial-time generalized parsers. Both of the above require time per operation on .
There are, however, other options. In particular, one may keep singleton languages only, replacing larger ones by a unique ambiguity marker. The result is a de-generalized parser, finding the unique parse tree for its input (or reporting ambiguity). If the languages are remembered up to (and including) the first ambiguity, the location and nature of the ambiguity can be reported to the user.
Further, one can introduce a partial ordering of transitions, and “prune” each intermediate language to contain only lexicographically-maximal transition sequences. This achieves transition prioritization, useful among others for expressing operator associativity and precedence, and eager/lazy versions of repetition constructs. All of this happens without any modification to the parsing algorithm itself!
5 Arbitrary semiring parsing
If we restrict our attention to finitely ambiguous RTNs, the API we require of transition languages is simply the one of a semiring. In fact, the alternatives we sketched in Section 4.3 are just special semirings. Substituting with an arbitrary semiring encounters, however, a hidden limitation—the algorithm, as presented above, requires semiring addition to be idempotent. Lifting this limitation would allow faster calculation of other useful features (cf. [6]), e.g., the number of distinct parse trees. We will now show how it can be achieved.
Let us then assume that is an arbitrary semiring, and that a valuation function assigns values to individual transitions. Valuation can be naturally extended to a semiring homomorphism between the set of languages over (i.e., subsets of ) and the semiring :
[TABLE]
We would like our parsing algorithm to return, for an input , the value
[TABLE]
Valuation can be pre-computed for the “building blocks” of the languages of transitions (individual transitions, nullings of individual states, and whatever is needed for the derivatives of ), and then, being a homomorphism, pushed through the algorithm to its final result. It might happen, however, that at some point of the computation, the same sequence of transitions appears as a member of both arguments of a union operation—we will say that such computation is redundant. If is idempotent (as set union is), this does not hurt. If it is not, such a sequence will be “counted twice”. Therefore, to make the algorithm work correctly over an arbitrary semiring, we must assure that such a situation never takes place.
Redundancy may be potentially introduced wherever a union of transition languages appears in the algorithm, namely when:
- •
(pre)computing the valuation of transition relations and languages needed by the derivatives of ,
- •
computing derivatives of degree —if the same pair appears in more than one of the components, or
- •
composing or in Algorithm 8.
The first case we have already avoided—in the equations considered in Section 4.3, the sets of transition sequences in each member of each union are guaranteed to be disjoint. The second is an additional requirement to be put on the API for guided relations—a requirement which the representation proposed in Section 4.1 also already satisfies. The remaining part of this section addresses the third case.
As it stands, Algorithm 7 (and thus the equivalent Algorithm 8) is redundant in two ways. Firstly, some sequences of transitions (and their corresponding configurations) may be added to both in lines 4 and 7. Secondly, when it is used iteratively by Algorithm 9, some sequences of transitions have multiple ways in which they can be split between successive iterations.
It turns out that a careful adjustment of the nulled atomic closure relations is enough to completely get rid of redundancy—neither the top-level parsing algorithm, nor the API (or implementation) of guided relations needs to be modified. Formally, we change the meaning of call-reduce closure never to include the empty configuration:
[TABLE]
and restrict null closure not to touch the top of the configuration:
[TABLE]
This modification silently alters the semantics of both the main algorithm and phase calculation. We should then prove that they remain correct.
inlineinlinetodo: inlineTODO: Re-prove Propositions 9 and 10
Finally, we need to show that the atomic closure relations remain regular. However, the only change we have effectively made to them is requiring each guided configuration to begin with a state. Therefore, the nondeterministic automaton witnessing regularity can be obtained by:
- •
making the initial state non-accepting:
[TABLE]
- •
using the non-guided derivatives from the initial state:
[TABLE]
- •
leaving everything else as in the guided variant.
Thus, getting rid of redundancy not only generalizes relational parsing to arbitrary semirings, but has also an additional positive effect of making the implementation simpler and more effective, as fewer edges are created in the dag structure for .
6 Complexity
We will now show that the input-related complexity of our algorithm from Sections 2 and 3, run using the representations of languages given in Section 4, matches that of Earley parser [4] with Leo’s improvement [11]. To our best knowledge this is the best among state-of-the-art generalized parsers.
Proposition 16**.**
With the proposed implementation, a sequence of “constructive” operations from API 10 and a single call to epsilon takes time .
Proof.
As noted before, each language (relation) in such a sequence can be represented by at most pairs. When computing derivative, one possibly needs to examine (and combine) the representations of all “directly referenced” by the current . This takes time . Running times of union and prepend are linear in the size of their arguments. Summing over the sequence of operations gives the desired . Returning epsilon involves flattening a single label, and thus contributes only a constant additional factor to the total time. ∎
Corollary 17**.**
Parsing an input of length takes time .
To be able to give better complexity bounds for restricted classes of grammars, we will make the standard natural assumption that each state in the grammar is productive, i.e., yields some (possibly empty) terminal word. Detecting and removing non-productive states can be easily done during parser generation.
The consequence of this assumption is that every reachable configuration is also productive. This allows us to prove the following:
Proposition 18**.**
When the recursive transition network is unambiguous, parsing an input of length takes time .
Proof.
Each way a configuration can “enter” into a parsing language corresponds to some viable sequence of RTN transitions. In particular, should any configuration have more than one such way, the grammar would be ambiguous. This implies that, for unambiguous grammars, all unions—those requested explicitly and those performed internally by derivative, are in fact disjoint. This makes each operation run in time proportional to the size of its result (i.e., the number of edges of the vertex created). Consequently, the complexity of the whole sequence of operations is linear in the size of the complete DAG constructed. The result follows. ∎
It turns out that for LR-regular grammars (this class contains LR(k) for all k, and thus most deterministic grammars), the size of the DAG is always linear in the input length:
Proposition 19**.**
When parsing according to a recursive transition network which is LR-regular, the outdegree of each DAG vertex created is bounded by a constant.
Proof.
Let us classify each vertex of the DAG depending on the kind of operation which has created it. Note that prepend with an -free language always creates a single edge to its argument, while union and derivative only copy existing edges, with labels possibly altered. Analyzing our phase computation (Algorithm 4), one can see that only derivative vertices will ever have incoming edges, and that only edges going out of such vertices need to be considered—prepend vertices always have outdegree 1, while union vertices combine a constant number of prepend vertices.
Denote by the union vertex representing the parsing language computed in the -th phase of the algorithm. Consider a vertex whose first incoming edge is created by one of the members of such union, and let be the label of this edge. This implies that .
Now track the progress of new incoming edges being added to , resulting with it being linked from either or for some and . The labels must have been obtained by taking successive derivatives of the original one. Let denote this sequence of derivatives.
In the first of the cases above, it implies that . As our DAG contains no useless edges, this inclusion must not be trivial: there must exist and for which . Looking at the sequence of transitions witnessing the first of these three conditions, and splitting it immediately before enters the configuration, one can find and such that generates the part of the input between positions and . Yet, by an argument of Leo ([11], Lemma 4.7), for LR-regular grammars each allows only a constant number of different ’s where this is possible.
A similar reasoning can be carried over for the vertices . Together with the fact that vertices are created for each input position, one obtains the desired constant bound on the out-degree of every DAG vertex. ∎
Corollary 20**.**
When the recursive transition network is LR-regular, parsing an input of length takes time .
7 Memoization
We find the mathematical clarity of our algorithm to be a virtue on its own. In particular, it opens a clear way of investigating potentially more effective data representations, and making use of language-theoretic algorithms, like optimization of nondeterministic automata. However, an aspect we find especially beneficial is the immutability of the intermediate objects computed during parsing. This is because it allows memoizing and reusing the results of computation. We report on this aspect in this section, beginning with recognition and moving on to arbitrary semiring parsing. Experimental evaluation of all these techniques is given in Section 8.
7.1 Trivial memoization
The most obvious way in which one can reuse the results of previous phases of computation is the following: if then . To build an intuition on when configuration languages at different input positions can be equal, imagine the structure of a standard, “hierarchical” programming language, in which syntactic structures (like classes, functions, code blocks, parenthesized expressions, etc.) nest within one another. A grammar of such a language will most likely contain productions corresponding to particular structures. In turn, a parser configuration at an input position where some structures are “currently open” will contain a sequence of states from those productions. Of course, even for deterministic grammars, there can be more than one reachable configuration at a given point. However, the general intuition holds: input locations with identical “nesting structure” will often share configuration languages. This happens both within a single input, and across multiple inputs.
7.2 Dominator-based memoization
To further develop our inuition on configuration languages, imagine a syntactic language structure requiring a specific closing terminal (e.g., }). Looking at the parsing stack, the state (say, ) corresponding to such structure being “currently open” cannot be reduced until the closing terminal is encountered. During this period, every configuration will have the form , with varying but identical . Our parser will not even look at until it is uncovered by taking a derivative by . This means that computation results for one can be “transplanted” on top of another, as long as they have at least one state “covering” this bottom part of the stack.
To make use of this observation we need to significantly complicate our representation of languages. A language will now be represented as a stack of DAG vertices, its semantics being the concatenation (top-to-bottom) of languages corresponding to individual vertices. To keep the languages deeper in the stack “covered”, we require all but the bottom vertices not to be final (i.e., to denote -free languages). Should we ever attempt to push a final vertex on a nonempty stack, we instead merge it with the current top, computing the concatenation of their corresponding languages.
During each phase, we keep track of how long a prefix of the stack we have seen. Note, that uncovering deeper vertices requires taking derivatives by at least states, and a single phase takes derivatives by at most two of them. Together with the potential merge to keep the -free invariant, this means that a phase will examine at most three top stack entries. When a phase is done, its result (a single DAG vertex , about to be placed on top of the part of the stack which has not been touched) is first factorized: the fragment of the DAG between and all final vertices reachable from it is split at all their common dominators. The resulting factors are represented by individual vertices, and these are pushed on the stack instead of .
Such partial phase computations are held in a trie, which maps a terminal and a prefix (with at most three elements) of the stack into a prefix it should get replaced with. Whenever the top of the stack is found in the trie, phase computation requires only a handful of simple stack operations.
7.3 Memoizing arbitrary semirings
We have shown how to effectively use memoization in our recognizer. It is possible to use the same techniques for parsing (over an arbitrary semiring). However, the quality of memoization drops rapidly as the semiring domain grows. It is best exemplified in the “reachest”, free semiring, distinguishing all transition languages. In this case, each transition sequence occurring in the parsing relation encodes the parsed input (the input can be read off the shift transitions). This means that complete parsing relations never repeat while parsing a single input. The situation is not that bad with dominator-based memoization, but the efficiency is still unsatisfactory.
Effective memoization of full-fledged relations is made possible by combining two observations. First, the shapes of the DAGs constructed while parsing are exactly the same as during recognition666This assumes identical “shapes” of atomic closures. When the grammar or atomic automata are optimized, these shapes might depend on the chosen semiring. Still, shape repeatability is in practice very high regardless of that choice. and thus do repeat very often—it is the labels that do not. Second, the semiring API allows label values to be combined, but not examined: the only exception is is-empty, but this information is also present in the shape of the DAG.
Imagine an instance of our labeled DAG structure in which all labels have been replaced with variables of unknown (non-zero) values. Our phase computation algorithm will happily accept such a DAG, creating some new labeled vertices and edges. The values of these fresh labels can be specified using expressions in the above variables, and such expressions depend only on the shape of the original DAG. Thus, one may view the phase computation as a combination of two parts: the first specifies how the shape of the output DAG depends on the shape of the input one, while the second prescribes a substitution, allowing to compute output labels from input labels.
With the trivial memoization, most of the substitution will be trivial, as a single phase only touches the fragment of the DAG close to its current top. Here, the dominator-based approach not only improves memoization rates, but also helps to avoid the trivial substitutions.
The complete representation of relations now looks as follows. It is still a stack of DAG vertices, but instead of semiring values, the labels are given as expressions with variables standing for labels of (up to three) stack nodes from which the current node has been obtained. An additional pointer to this “origin” node makes it possible to perform the substitution when needed. The trie used for memoizing actions is practically the same, but only the shapes of the vertices (without labels) are taken into consideration.
Instead of a single semiring value, the final result of parsing becomes now a fairly involved data structure, describing an expression for this value as a hierarchy of small substitutions. These substitutions have to be performed if actual value is to be returned, and this computation often takes significantly longer than parsing per se! What have we saved then? We claim that in order to arrive at the final value, more or less the same semiring operations (possibly in a different order) would have to be performed by any semiring-agnostic parser. Our final substitution is then in some way optimal, as it ends up computing exactly those intermediate values which are actually relevant for the result.
It is also interesting to see how the resulting substitution structure looks like for unambiguous languages. If there is no legal parse of the input, the result is a single constant: the semiring zero. Otherwise, all union operations in all substitutions must be degenerate, i.e., have exactly one operand. Thus, the whole expression is a (complex) concatenation of individual transitions. Each small expression given at each level of substitutions is then a sequence of transitions, with “holes” to be filled with the values of referenced variables. Viewed as a description of a parse tree, it is akin to a tree with “holes”, to be filled with subtrees obtained from referenced variables. This suggests that for some applications one might not need to actually compute the final value, but instead operate directly on the “compressed” substitution structure. It is thus an interesting open question whether this way of encoding parse forests might be advantageous over SPPFs returned by virtually all generalized parsers.
8 Evaluation
To evaluate the effects of memoization on practical programming languages, we have chosen a grammar for Java 8 from the ANTLR4 grammar repository (https://github.com/antlr/grammars-v4/blob/master/java8/Java8.g4; this grammar is ambiguous, but extremely close to the Java language specification) and a large, popular Java project (elasticsearch-6.5.3, with 9596 .java files totalling over 10 million terminals).
The grammar, originally with 3132 RTN states, has been left-factored and then optimized by simple partition refinement, analogous to Moore’s method of minimizing finite automata. At parser generation time, the automata representing atomic relations have been optimized in the same way. All these optimizations depend on the semiring in which the parser is supposed to operate— Figure 1 reports the numbers of states in all the cases.
We have performed the evaluation on a modest laptop, with 3 GHz Intel Core i7 CPU, running 64-bit Linux system. To take into account the time required for garbage collection (and for a more fair comparison with the javac compiler), we have restricted the whole processes (including .NET Core or Java VM) to run on a single CPU core. About 5 GB of RAM were available to the process at each run.
Figure 2 compares the effectiveness of different methods of memoization. Each entry in this table gives the percentage of phases whose result was taken from the cache. The mark ! denotes situations in which the algorithm would require too much RAM to complete—the value in such cases is approximate, since it only accounts for the phases performed before exhausting all available memory.
As expected according to the discussion in Section 7, trivial memoization quickly becomes ineffective as the semiring grows richer. For dominator-based memoization using actual semiring values, the trend is similar, although not that rapid. Memoization using substitutions may only depend on the semiring indirectly, through the shape of the optimized atomic automata. In our tests, they had almost no influence on its effectiveness.
With over 10 million parsing phases to be performed, it is not by accident that only the variants with high () memoization rate were able to complete—attempting to store millions of configurations is simply impractical. Furthermore, with trivial memoization, performing the 5.9% non-memoized phases took 96% of total recognition time—this shows how expensive the DAG operations are compared to a simple dictionary lookup. With dominator-based memoization, due to yet increased complexity of the data structures, the 0.3% non-memoized phases took about 40% of total recognition time. This shows that variants for which memoization is anything below excellent would remain impractical even if given unlimited memory.
We will now share some raw performance comparison, not only between variants of our algorithm, but also with our implementation of GLL, and the hand-coded deterministic parser built into the Java 8 compiler javac. While our proof-of-concept implementation has not been created with speed in mind,777It has multiple additional layers of abstraction, useful for experimenting with different representations. In C, the overhead of these layers cannot be eliminated at compile-time and must be paid during parsing. It seems that a well-structured C++ implementation could do significantly better. the results are already a strong evidence of its practicality.
Figure 3 gives time and memory usage of different recognizers. Note that, while other timings are for parsing alone, the one for javac includes tokenizing the input and building parse trees. However, in a hand-coded, deterministic parser, we would not expect these two tasks to take significantly more than half of total execution time. The comparison suggests that, with our method, an unoptimized recognizer, automatically generated from an ambiguous language specification can rival optimized, dedicated, hand-written, deterministic code!
The table includes two rows marked as “non-optimized”. The timings given there are for the appropriate algorithms run on the grammar which has only been left-factored, and has not undergone partition refinement optimization. As evident, while such optimization has clearly helped our approach (by reducing the cardinality of from 5503 to 2949), it has made GLL perform significantly worse (by making its GSS denser). Not also, that if both algorithms are given the same, optimized grammar, our recognizer outperforms GLL by a factor of over 300. Even though our implementation of GLL is most probably suboptimal, relational parsing remains in clear advantage.
We now turn to the evaluation of parsing. As we have not yet implemented a variant of GLL able to work with an arbitrary semiring, we only report here on the different variants of our method.
The timings are given by Figure 4. The comparison only contains variants with dominator-based memoization. The column named “no evaluation” is for the substitution-based algorithm, but without the final evaluation of substitutions to actual semiring value. In other words, it simulates what happens if we allow the results of parsing to be returned in “compressed” form.
Comparing the numbers here with those from Figure 3, one can see our full parsing algorithm to take the same time as the GLL recognizer (and this only if we choose the “better” variant of the grammar for each of them; on the same, optimized grammar, the speedup is about 5 times). Shall the latter need to construct an SPPF, our method would again be in greater advantage.
Moreover, computing the final value takes more than 90% of parsing time. We are almost certain that this is too much, and that a better representation of substitutions (or a more clever way of evaluating them) would make our algorithm even better.
9 Related work
Parsing is a vast subject (see [7] for a not-so-recent survey, with over 1500 references!), thus here we only touch on what we find to be most relevant to our proposed algorithm.
Simulating nondeterministic pushdown automata
Effective simultaneous simulation of possible runs of a PDA has been proposed by Lang [9]. In [23, 24], Tomita presented the graph-structured stack as a convenient structure for capturing such nondeterminism. This has led to a multitude of generalized parsers, differing primarily by the automaton being simulated: this includes the GLR family (e.g., [22]), GLC [13, 12], and GLL [20, 21].
As Lang’s, our method could be adjusted to simulate other versions of pushdown automata. It is even conceivable that an appropriate “phase function” could be obtained automatically for an arbitrary PDA, and still require only a constant number of primitive language operations. We have not investigated this path.
The Adaptive LL(*) algorithm [15], underlying the popular ANTLR4 parser generator, uses simulation to predict valid transitions. It represents configuration sets explicitly, and thus fails to handle left-recursive grammars, where these sets can be infinite. Our approach, originally aimed to remove this restriction, abstracts away the specific representation. In fact, we have first used a “standard” GSS instead of the proposed DAG structure—however, in such case we failed to attain linear complexity on some LR-regular grammars.
Left- and right-recursive productions
For top-down (predictive) parsers, left-recursive productions are inherently problematic, because it is difficult to know up front how many times a call loop should be followed. Thus, most algorithms in the LL family refuse to handle such grammars. GLL captures all possible runs through left recursion by introducing cycles into its graph-structured stack, and so does Earley’s algorithm (cyclicity here takes the form of an item referencing its own layer).
Right recursion requires special attention when reduction possibilities are considered, because it may happen that a new way of reaching some state in discovered after it has been “processed”. All nondeterminism-simulating parsers handle this using work queues or other mutable data structures. Similar care (and mutability) is needed in Earley-style parsers.
With simultaneous left and right recursion, the grammar is infinitely ambiguous, and thus the final result of parsing must be cyclic. Relational parsing integrates both left and right recursion into the atomic languages, thus completely avoiding the need for cyclic structures and mutation during parsing. To our best knowledge it is the first algorithm with this property.
Right recursion influences also the complexity of generalized parsers, as it can make linearly long sequences of reductions available at each input position. Some parsers, including Earley’s, use lookahead to avoid incurring quadratic complexity on LR(k) grammars. Another approach, used in Leo’s modification [11] and applicable to all LR-regular grammars without using lookahead, is to create shortcuts through such long reduction paths. This is precisely what we achieve by the decomposition proposed in Proposition 11.
Nullables
Nullable states (nonterminals) seem to be a nuisance for every parsing algorithm. Although theoretically one could avoid dealing with them by rewriting the grammar, it is impractical to do so: binary grammars can grow quadratically, and arbitrary ones—exponentially. Right-nulled GLR [19, 17] avoids the exponential blow-up by only eliminating trailing nullables in each production. Most other algorithms attempt to handle all nullables “on the fly”. In our case, this amounts to making the atomic languages null-closed. While it does not cause the automata to have more states, additional edges are introduced and traversed.
In an analogous situation, the version of CYK presented in [10] does not precompute the extra edges. Instead it avoids higher grammar-related complexity by grouping together multiple walks on its “automata”. It is interesting whether this idea could somehow be adapted to our setting.
Atomic closures vs. left corners
The slightly less popular GLC parser builds a bridge between top-down and bottom-up parsing by using the left corner relation, containing a pair of nonterminals whenever one of them can appear leftmost in some derivation from the other. Our proposed implementation of atomic closures is indexed by pairs of states related in exactly the same way, and the appropriate rules of GLC mirror the transitions in our atomic automata.
The authors of GLC propose to make the algorithm more effective by grouping some of the cases heuristically. With our approach, it is clear that one could use any automaton recognizing the same language. This opens the way for well-understood optimizations.
Memoization
Memoization has been put to great use in the Adaptive LL(*) parsing algorithm, even though it is only used there when predicting the right nondeterministic choice. To make memoized computations applicable in more situations, the algorithm pretends to forget all but the top state of the RTN. If such “blind” computation succeeds, it can then be applied on top of any stack. However, should it fail, the algorithm resorts to non-memoized computation with full stack information. Our dominator-based memoization handles such situations better, and in a way optimally: we always look at exactly such stack depth as is necessary.
Limiting stack activity
It is well known that the primary source of inefficiency in generalized parsers is handling large graph-like structures (i.e., the GSS), offering poor cache locality. Reduction-incorporated parsers (cf. [18]) attempt to limit the size of these graphs by handling most of the grammar using finite automata, and using the stack only when necessary. Appropriate pushdown automata can be constructed in multiple ways, and thus in [8] the authors suggest selecting the best one by profiling the parser on sample inputs.
In our algorithm, all activity between successive terminals is handled by the automata for atomic languages. Furthermore, instead of limiting the depth of the (multiple) stacks, we perform most—even locally ambiguous—operations on a single stack. With dominator-based memoization, the algorithm “learns” the right stack actions while parsing, though one could also possibly “train” it beforehand on some sample inputs.
Semantics
As far as we know, no previous generalized parsing algorithm explicitly computes the languages of reachable configurations. However, these languages are implicitly present in all of them, and often could be easily read off their data structures after processing each terminal: in GLL for example, reachable configurations are precisely all the paths through the GSS.
We believe that our semantics-based approach opens the way not only to cleaner and more performant parsers for all context-free languages, but possibly also to handling larger useful grammar classes, beginning with conjunctive grammars [14] or even grammars with one- or two-sided contexts [2, 1, 16].
The reference list from the paper itself. Each links out to its DOI / PubMed record.
- 1[1] Mikhail Barash and Alexander Okhotin. Two-sided context specifications in formal grammars. Theor. Comput. Sci. , 591(C):134–153, August 2015. URL: http://dx.doi.org/10.1016/j.tcs.2015.05.004 , doi:10.1016/j.tcs.2015.05.004 . · doi ↗
- 2[2] Mikhail Barash and Alexander Okhotin. Generalized lr parsing algorithm for grammars with one-sided contexts. Theor. Comp. Sys. , 61(2):581–605, August 2017. URL: https://doi.org/10.1007/s 00224-016-9683-3 , doi:10.1007/s 00224-016-9683-3 . · doi ↗
- 3[3] Janusz A. Brzozowski. Derivatives of regular expressions. J. ACM , 11(4):481–494, October 1964. URL: http://doi.acm.org/10.1145/321239.321249 , doi:10.1145/321239.321249 . · doi ↗
- 4[4] Jay Earley. An efficient context-free parsing algorithm. Commun. ACM , 13(2):94–102, February 1970. URL: http://doi.acm.org/10.1145/362007.362035 , doi:10.1145/362007.362035 . · doi ↗
- 5[5] Samuel Eilenberg. Automata, Languages, and Machines . Academic Press, Inc., Orlando, FL, USA, 1974.
- 6[6] Joshua Goodman. Semiring parsing. Comput. Linguist. , 25(4):573–605, December 1999. URL: http://dl.acm.org/citation.cfm?id=973226.973230 .
- 7[7] Dick Grune. Parsing Techniques: A Practical Guide . Springer Publishing Company, Incorporated, 2nd edition, 2010.
- 8[8] Adrian Johnstone and Elizabeth Scott. Automatic recursion engineering of reduction incorporated parsers. Sci. Comput. Program. , 68(2):95–110, September 2007. URL: http://dx.doi.org/10.1016/j.scico.2006.04.011 , doi:10.1016/j.scico.2006.04.011 . · doi ↗