From: Ulya Trofimovich Date: Mon, 8 Jul 2019 10:55:34 +0000 (+0100) Subject: Paper: updated and fixed all the proofs. X-Git-Tag: 1.2~50 X-Git-Url: https://granicus.if.org/sourcecode?a=commitdiff_plain;h=597e67d779c904315edbb10bf886036c148fa26c;p=re2c Paper: updated and fixed all the proofs. --- diff --git a/doc/tdfa_v2/img/pe.tex b/doc/tdfa_v2/img/pe.tex index 58e33e63..929b0f75 100644 --- a/doc/tdfa_v2/img/pe.tex +++ b/doc/tdfa_v2/img/pe.tex @@ -6,7 +6,45 @@ \usepackage[utf8]{inputenc} \usepackage{amsmath, amssymb, amsfonts, accents} \usetikzlibrary{graphdrawing, graphs, arrows, shapes, automata, calc} + +% workaround for https://github.com/u-fischer/luaotfload/issues/6 +\usepackage{luacode} +\begin{luacode} + function pgf_lookup_and_require(name) + local sep = '/' + if string.find(os.getenv('PATH'),';') then + sep = '\string\\' + end + local function lookup(name) + local sub = name:gsub('%.',sep) + local find_func = function (name, suffix) + if resolvers then + local n = resolvers.findfile (name.."."..suffix, suffix) -- changed + return (not (n == '')) and n or nil + else + return kpse.find_file(name,suffix) + end + end + if find_func(sub, 'lua') then + require(name) + elseif find_func(sub, 'clua') then + collectgarbage('stop') + require(name) + collectgarbage('restart') + else + return false + end + return true + end + return + lookup('pgf.gd.' .. name .. '.library') or + lookup('pgf.gd.' .. name) or + lookup(name .. '.library') or + lookup(name) + end +\end{luacode} \usegdlibrary{trees, layered} + \usepackage{stix} @@ -162,8 +200,8 @@ \;\Rightarrow\; \alpha \sqsubset \beta \;\Rightarrow\; \alpha < \beta \\ - \|s\|^{Sub}_1 = 2 &> 1 = \|t\|^{Sub}_1 \wedge \|s\|^{Sub}_p = \|t\|^{Sub}_p \;\forall p < 1 - \;\Rightarrow\; s <_1 t + \|s\|^{sub}_1 = 2 &> 1 = \|t\|^{sub}_1 \wedge \|s\|^{sub}_p = \|t\|^{sub}_p \;\forall p < 1 + \;\Rightarrow\; s \prec_1 t \end{aligned}$ }; \end{scope} @@ -267,8 +305,8 @@ \;\Rightarrow\; \alpha \sim \beta \;\wedge\; \alpha \subset \beta \;\Rightarrow\; \alpha < \beta \\ - &\|s\|^{Sub}_1 = 1 > -1 = \|t\|^{Sub}_1 \wedge \|s\|^{Sub}_p = \|t\|^{Sub}_p \;\forall p < 1 - \;\Rightarrow\; s <_1 t + &\|s\|^{sub}_1 = 1 > -1 = \|t\|^{sub}_1 \wedge \|s\|^{sub}_p = \|t\|^{sub}_p \;\forall p < 1 + \;\Rightarrow\; s \prec_1 t \end{aligned}$ }; \end{scope} @@ -394,8 +432,8 @@ \;\Rightarrow\; \alpha \sim \beta \;\wedge\; \alpha \subset \beta \;\Rightarrow\; \alpha < \beta \\ - &\|s\|^{Sub}_2 = \infty > 0 = \|t\|^{Sub}_2 \wedge \|s\|^{Sub}_p = \|t\|^{Sub}_p \;\forall p < 2 - \;\Rightarrow\; s <_2 t + &\|s\|^{sub}_2 = \infty > 0 = \|t\|^{sub}_2 \wedge \|s\|^{sub}_p = \|t\|^{sub}_p \;\forall p < 2 + \;\Rightarrow\; s \prec_2 t \end{aligned}$ }; \end{scope} @@ -492,8 +530,8 @@ \;\Rightarrow\; \alpha \sim \beta \;\wedge\; \beta \subset \alpha \;\Rightarrow\; \beta < \alpha \\ - &\|s\|^{Sub}_2 = 0 > -1 = \|s\|^{Sub}_2 \wedge \|s\|^{Sub}_p = \|t\|^{Sub}_p \;\forall p < 2 - \;\Rightarrow\; t <_2 s + &\|s\|^{sub}_2 = 0 > -1 = \|s\|^{sub}_2 \wedge \|s\|^{sub}_p = \|t\|^{sub}_p \;\forall p < 2 + \;\Rightarrow\; t \prec_2 s \end{aligned}$ }; \end{scope} @@ -619,7 +657,7 @@ &\Phi_0(t_9) = \overbracket {\Xl_1 \Xl_2 \Xl_3 \Xl_4} a \overbracket {\Xr_3 \Xr_2 \Xr_1 \Xl_2 \Xl_3 \Xl_4} a \overbracket {\Xr_3 \Xr_2 \Xr_1 \Xl_2 \Xl_3 \Xl_4} a \overbracket {\Xr_3 \Xr_2 \Xr_1 \Xr_0} \end{aligned} \\ - & \quad\quad t_1 < t_2 < t_3 < t_4 < t_5 < t_7 < t_6 < t_8 < t_9 + & \quad\quad t_1 \prec t_2 \prec t_3 \prec t_4 \prec t_5 \prec t_7 \prec t_6 \prec t_8 \prec t_9 \end{aligned}$ }; \end{scope} diff --git a/doc/tdfa_v2/part_1_tnfa.tex b/doc/tdfa_v2/part_1_tnfa.tex index 212e98bb..1afabf86 100644 --- a/doc/tdfa_v2/part_1_tnfa.tex +++ b/doc/tdfa_v2/part_1_tnfa.tex @@ -44,7 +44,7 @@ %\IncMargin{-\parindent} \usepackage[utf8]{inputenc} -\usepackage{amsmath,amssymb,amsfonts} +\usepackage{amsmath, amssymb, amsthm, amsfonts} \usepackage{accents} \usepackage{mathtools} \usepackage{graphicx} @@ -53,6 +53,7 @@ \usepackage{url} \usepackage{vwcol} \usepackage[section]{placeins} +\usepackage{proof-at-the-end} \newcommand{\Xl}{\langle} \newcommand{\Xr}{\rangle} @@ -96,8 +97,8 @@ \newcommand{\Xstirling}[2]{\genfrac{\{}{\}}{0pt}{}{#1}{#2}} \newcommand*{\Xbar}[1]{\overline{#1}} -\newcommand{\pnorm}[2]{\|{#1}\|^{Pos}_{#2}} -\newcommand{\snorm}[2]{\|{#1}\|^{Sub}_{#2}} +\newcommand{\pnorm}[2]{\|{#1}\|^{pos}_{#2}} +\newcommand{\snorm}[2]{\|{#1}\|^{sub}_{#2}} \DeclarePairedDelimiter\ceil{\lceil}{\rceil} \DeclarePairedDelimiter\floor{\lfloor}{\rfloor} @@ -115,12 +116,6 @@ \setlength{\parindent}{0pt} \setlength{\belowcaptionskip}{-1em} -%\theoremstyle{definition} -\newtheorem{Xdef}{Definition} -\newtheorem{XThe}{Theorem} -\newtheorem{XLem}{Lemma} -\newtheorem{Xobs}{Observation} - \begin{document} @@ -406,7 +401,7 @@ which allows us to compare ambiguous paths using the definition of order on pare Below are the four basic definitions and the skeleton of the algorithm. In the following sections we formalize the relation between different representations and fill in all the details. - \begin{Xdef} + \begin{definition} \emph{Regular expressions (RE)} over finite alphabet $\Sigma$, denoted $\XR_\Sigma$: \begin{enumerate} \item @@ -419,10 +414,10 @@ In the following sections we formalize the relation between different representa submatch group $(e_1)$ are in $\XR_\Sigma$. \end{enumerate} - \end{Xdef} + \end{definition} - \begin{Xdef} + \begin{definition} \emph{Parse trees (PT)} over finite alphabet $\Sigma$, denoted $\XT_\Sigma$: \begin{enumerate} \item @@ -434,10 +429,10 @@ In the following sections we formalize the relation between different representa ${T}^i(t_1, \dots, t_n)$ is in $\XT_\Sigma$. \end{enumerate} - \end{Xdef} + \end{definition} - \begin{Xdef} + \begin{definition} \emph{Parenthesized expressions (PE)} over finite alphabet $\Sigma$, denoted $\XP_\Sigma$: \begin{enumerate} \item @@ -450,10 +445,10 @@ In the following sections we formalize the relation between different representa $\Xl e_1 \Xr$ are in $\XP_\Sigma$. \end{enumerate} - \end{Xdef} + \end{definition} - \begin{Xdef} + \begin{definition} \emph{Tagged Nondeterministic Finite Automaton (TNFA)} is a structure $(\Sigma, Q, T, \Delta, q_0, q_f)$, where: \begin{itemize} @@ -470,7 +465,7 @@ In the following sections we formalize the relation between different representa \item[] $q_0 \in Q$ is the \emph{initial} state \item[] $q_f \in Q$ is the \emph{final} state \end{itemize} - \end{Xdef} + \end{definition} As the reader might notice, our definitions are subtly different from the usual ones in literature. Regular expressions are extended with submatch operator @@ -555,6 +550,8 @@ unfortunately we do not know in advance which configurations will spawn ambiguou \section{Formalization}\label{section_formalization} In this section we establish the relation between all intermediate representations. +For readability all proofs are moved to appendix. +% First of all, we rewrite REs in a form that makes submatch information explicit: to each subexpression we assign an \emph{implicit} and \emph{explicit} submatch index, where explicit indices enumerate submatch groups (for all other subexpressions they are zero), @@ -564,7 +561,7 @@ This form reflects POSIX standard, which states that submatch extraction applies only to parenthesized subexpressions, but the longest-match rule applies to all subexpressions regardless of parentheses. - \begin{Xdef} + \begin{definition} \emph{Indexed regular expressions (IRE)} over finite alphabet $\Sigma$, denoted $\XIR_\Sigma$: \begin{enumerate} \item @@ -578,7 +575,7 @@ but the longest-match rule applies to all subexpressions regardless of parenthes repetition $(i, j, r_1^{n, m})$, where $0 \leq n \leq m \leq \infty$, are in $\XIR_\Sigma$. \end{enumerate} - \end{Xdef} + \end{definition} Function $\IRE$ transforms RE into IRE. It is defined via a composition of two functions, @@ -662,10 +659,10 @@ and $\PT(r, w)$ denotes the set $\big\{ t \in \PT(\IRE(r)) \mid str(t) = w \big\ \end{align*} \medskip - \begin{Xdef}\label{ambiguity_of_parse_trees} + \begin{definition}\label{ambiguity_of_parse_trees} \emph{Ambiguity of parse trees.} PTs $s$ and $t$ are \emph{ambiguous} iff $s \neq t$ and $s, t \in PT(r, w)$ for some RE $r$ and string $w$. - \end{Xdef} + \end{definition} Following \ref{OS13}, we assign \emph{positions} to the nodes of RE and PT. The root position is $\Lambda$, and position of the $i$-th subtree of a tree with position $p$ is $p.i$ @@ -700,7 +697,7 @@ S-norm is marked with $\#$. %\FloatBarrier - \begin{Xdef}\label{tnorm_of_PTs} + \begin{definition}\label{tnorm_of_PTs} The \emph{p-norm} and \emph{s-norm} of a PT $t$ at position $p$ are: \begin{align*} \pnorm{t}{p} = @@ -717,7 +714,7 @@ S-norm is marked with $\#$. \infty &\text{if } p \not\in Sub(t) \end{cases} \end{align*} - \end{Xdef} + \end{definition} Generally the norm of a subtree means the number of alphabet symbols in its leaves, with two exceptions. First, for nil subtrees the norm is $-1$: intuitively, they have the lowest ``ranking'' among all possible subtrees. @@ -729,70 +726,204 @@ and another tree $t$ has no subtree at position $p$, then the infinite norm $\|t\|_p$ ``outranks'' $\|s\|_p$. We define two orders on PTs: - \begin{Xdef}\label{total_order_on_PTs} - \emph{P-order on PTs.} - Given parse trees $t, s \in PT(e, w)$, we say that $t <_p s$ w.r.t. \emph{desision position} $p$ + \begin{definition}[P-order on PTs] + \label{total_order_on_PTs} + Given parse trees $t, s \in PT(r, w)$, we say that $t <_p s$ w.r.t. \emph{desision position} $p$ iff $\pnorm{t}{p} > \pnorm{s}{p}$ and $\pnorm{t}{q} = \pnorm{s}{q} \; \forall q < p$. We say that $t < s$ iff $t <_p s$ for some $p$. - \end{Xdef} + \end{definition} - \begin{Xdef}\label{partial_order_on_PTs} - \emph{S-order on PTs.} - Given parse trees $t, s \in PT(e, w)$, we say that $t \prec_p s$ w.r.t. \emph{desision position} $p$ % $p \in Sub(t) \cup Sub(s)$ + \begin{definition}[S-order on PTs] + \label{partial_order_on_PTs} + Given parse trees $t, s \in PT(r, w)$, we say that $t \prec_p s$ w.r.t. \emph{desision position} $p$ % $p \in Sub(t) \cup Sub(s)$ iff $\snorm{t}{p} > \snorm{s}{p}$ and $\snorm{t}{q} = \snorm{s}{q} \; \forall q < p$. We say that $t \prec s$ iff $t \prec_p s$ for some $p$. - \end{Xdef} + \end{definition} - \begin{Xdef}\label{incomparable_IPTs} - IPTs $t$ and $s$ are \emph{incomparable}, denoted $t \sim s$, + \begin{definition}\label{incomparable_PTs} + PTs $t$ and $s$ are \emph{incomparable}, denoted $t \sim s$, iff neither $t \prec s$, nor $s \prec t$. - \end{Xdef} - - \begin{XThe}\label{theorem_porder_on_PTs} - P-order $<$ is a strict total order on IPTs. - (Proof given in appendix [??].) - \end{XThe} - - \begin{XThe}\label{theorem_sorder_on_PTs} - S-order $\prec$ is a strict weak order on IPTs. - (Proof given in appendix [??].) - \end{XThe} - -P-order is total --- the $<$-minimal tree is unique. -S-order is partial: -there might be two distinct PTs that coincide in all submatch positions, yet differ in some non-submatch positions. -Such trees are called \emph{incomparable}, -and from disambiguation perspective they are indistinguishable. -% -Incomparability is an equivalence relation: it is -reflexive (obviously $s \sim s$), -symmetric (obviously $s \sim t$ implies $t \sim s$) and -transitive (see lemma \ref{lemma_ptorder_transitivity_of_incomparability} in appendix). -Consequently there is a whole class of $\prec$-minimal trees. -%$\PT_{min}(r,w) = \{ t \in \PT(r,w) \mid \forall u \in \PT(r,w) : t \sim u \vee t < u \}$. -% -One might ask, what is the relation between p-order $<$ and s-order $\prec$? -We show by the means of a counterexample that p-order is not an extension of s-order. -Consider trees $t$ and $u$ on figure \ref{fig_mark_enum}: + \end{definition} + +\begin{theoremEnd}[restate, no link to proof, no link to theorem, category=theorem_porder_on_PTs]{theorem} + \label{theorem_porder_on_PTs} + P-order $<$ is a strict total order on $PT(e, w)$ for any RE $r$ and string $w$. +\end{theoremEnd} +\begin{proofEnd} + We need to show that $<$ is transitive and trichotomous. + + \begin{itemize}[itemsep=0.5em] + \item[(1)] + Transitivity: we need to show that $\forall t, s, u \in PT(e,w): (t < s \wedge s < u) \implies t < u$. + \\[0.5em] + Let $t <_p s$ and $s <_q u$ for some positions $p$, $q$, and let $r = min (p, q)$. + \\[0.5em] + First, we show that $\pnorm{t}{r} > \pnorm{u}{r}$. + If $p \leq q$, we have $\pnorm{t}{p} > \pnorm{s}{p}$ (implied by $t <_p s$) + and $\pnorm{s}{p} \geq \pnorm{u}{p}$ (implied by $s <_q u \wedge p \leq q$), + therefore $\pnorm{t}{p} > \pnorm{u}{p}$. + Otherwise $p > q$, we have $\pnorm{t}{q} > \pnorm{u}{q}$ (implied by $s <_q u$) + and $\pnorm{t}{q} = \pnorm{s}{q}$ (implied by $t <_p s \wedge q < p$), + therefore $\pnorm{t}{q} > \pnorm{u}{q}$. + \\[0.5em] + Second, we show that $\forall r' < r : \pnorm{t}{r'} = \pnorm{u}{r'}$. + We have $\pnorm{t}{r'} = \pnorm{s}{r'}$ (implied by $t <_p s \wedge r' < p$) + and $\pnorm{s}{r'} = \pnorm{u}{r'}$ (implied by $s <_q u \wedge r' < q$), + therefore $\pnorm{t}{r'} = \pnorm{u}{r'}$. + + \item[(2)] + Trichotomy: we need to show that $\forall t, s \in PT(e,w)$ + exactly one of $t < s$, $s < t$ or $t = s$ holds. + Consider the set of positions where norms of $t$ and $s$ disagree + $P = \{p \in Pos(t) \cup Pos(s) : \pnorm{t}{p} \neq \pnorm{s}{p}\}$. + + \begin{itemize}[itemsep=0.5em] + \item[(2.1)] First case: $P \neq \emptyset$. + We show that in this case exactly one of $t < s$ or $s < t$ is true + ($t \neq s$ is obvious). + \\[0.5em] + First, we show that at least one of $t < s$ or $s < t$ is true. + % + Let $p = min(P)$; it is well-defined since $P$ is non-empty, finite and lexicographically ordered. + % + For all $q < p$ we have $\pnorm{t}{q} = \pnorm{s}{q}$ (by definition of $p$ + and because $\pnorm{t}{q} = \infty = \pnorm{s}{q}$ if $q \not\in Pos(t) \cup Pos(s)$). + % + Since $\pnorm{t}{p} \neq \pnorm{s}{p}$, we have either $t <_p s$ or $t <_p s$. + \\[0.5em] + Second, we show that at most one of $t < s$ or $s < t$ is true, + i.e. $<$ is asymmetric: $\forall t, s \in PT(e,w) : t < s \implies s \not< t$. + % + Suppose, on the contrary, that $t <_p s$ and $s <_q t$ for some $p$, $q$. + Without loss of generality let $p \leq q$. + On one hand $t <_p s$ implies $\pnorm{t}{p} > \pnorm{s}{p}$. + But on the other hand $s <_q t \wedge p \leq q$ implies $\pnorm{t}{p} \leq \pnorm{s}{p}$. + Contradiction. + + \item[(2.2)] Second case: $P = \emptyset$. + We show that in this case $t = s$. + \\[0.5em] + We have $Pos(t) = Pos(s)$ --- otherwise there is a position with norm $\infty$ in only one of the trees. + Therefore $t$ and $s$ have identical node structure. + % + By lemma \ref{lemma_positions} any position in $t$ and $s$ corresponds to the same position in $\IRE(e)$. + % + Since any position in $\IRE(e)$ coresponds to a unique explicit submatch index, + it must be that submatch indices of all nodes in $t$ and $s$ coincide. + % + Consider some position $p \in Pos(t)$. + If $p$ corresponds to an inner node, then both $t|_p$ and $s|_p$ are of the form $T^i(\hdots)$. + Otherwise, $p$ corresponds to a leaf node, which can be either $\varnothing$ or $\epsilon$ or $\alpha$. + Since all three have different norms ($-1$, $0$ and $1$ respectively), + and since $\pnorm{t}{p} = \pnorm{s}{p}$, it must be that $t|_p$ and $s|_p$ are identical. + \end{itemize} + \end{itemize} +\end{proofEnd} +\vspace{-0.5em} + +\begin{theoremEnd}[restate, no link to proof, no link to theorem, category=theorem_sorder_on_PTs]{theorem} + \label{theorem_sorder_on_PTs} + S-order $\prec$ is a strict weak order on $PT(e, w)$ for any RE $r$ and string $w$. +\end{theoremEnd} +\begin{proofEnd} + We need to show that $\prec$ is asymmetric and transitive, and incomparability relation $\sim$ is transitive. + + \begin{itemize}[itemsep=0.5em] + \item[(1)] + Asymmetry: we need to show that $\forall t, s \in PT(e,w): t \prec s \implies s \not\prec t$. + \\[0.5em] + Suppose, on the contrary, that $t \prec_p s$ and $s \prec_q t$ for some $p$, $q$. + Without loss of generality let $p \leq q$. + On one hand $t \prec_p s$ implies $\snorm{t}{p} > \snorm{s}{p}$. + But on the other hand $s \prec_q t \wedge p \leq q$ implies $\snorm{t}{p} \leq \snorm{s}{p}$. + Contradiction. + + \item[(2)] + Transitivity: we need to show that $\forall t, s, u \in PT(e,w): (t \prec s \wedge s \prec u) \implies t \prec u$. + \\[0.5em] + Let $t \prec_p s$ and $s \prec_q u$ for some positions $p$, $q$, and let $r = min (p, q)$. + \\[0.5em] + First, we show that $\snorm{t}{r} > \snorm{u}{r}$. + If $p \leq q$, we have $\snorm{t}{p} > \snorm{s}{p}$ (implied by $t \prec_p s$) + and $\snorm{s}{p} \geq \snorm{u}{p}$ (implied by $s \prec_q u \wedge p \leq q$), + therefore $\snorm{t}{p} > \snorm{u}{p}$. + Otherwise $p > q$, we have $\snorm{t}{q} > \snorm{u}{q}$ (implied by $s \prec_q u$) + and $\snorm{t}{q} = \snorm{s}{q}$ (implied by $t \prec_p s \wedge q < p$), + therefore $\snorm{t}{q} > \snorm{u}{q}$. + \\[0.5em] + Second, we show that $\forall r' < r : \snorm{t}{r'} = \snorm{u}{r'}$. + We have $\snorm{t}{r'} = \snorm{s}{r'}$ (implied by $t \prec_p s \wedge r' < p$) + and $\snorm{s}{r'} = \snorm{u}{r'}$ (implied by $s \prec_q u \wedge r' < q$), + therefore $\snorm{t}{r'} = \snorm{u}{r'}$. + + \item[(3)] + Transitivity of incomparability: we need to show that $\forall t, s \in PT(e,w): (t \sim s \wedge s \sim u) \implies t \sim u$. + \\[0.5em] + By forward implication of lemma \ref{lemma_incomparability_equivdef} + $t \sim s \Rightarrow \forall p : \snorm{t}{p} = \snorm{s}{p}$ and + $s \sim u \Rightarrow \forall p : \snorm{s}{p} = \snorm{u}{p}$, therefore + $(t \sim s \wedge s \sim u) \Rightarrow \forall p : \snorm{t}{p} = \snorm{u}{p} \Rightarrow t \sim u$ + by backward implication of lemma \ref{lemma_incomparability_equivdef}. + \end{itemize} +\end{proofEnd} + +The following theorem \ref{theorem_order_compat} establishes an important relation between P-order and S-order. +P-order is total, and there is a unique $<$-minimal tree $t_{min}$. +S-order is partial, it partitions all trees into equivalence classes +and there is a whole class of $\prec$-minimal trees $T_{min}$ +(such trees coincide in submatch positions, but differ in some non-submatch positions). +Theorem \ref{theorem_order_compat} shows that $t_{min} \in T_{min}$. +This means that P-order and S-order ``agree'' on the notion of minimal tree: +we can continuously narrow down $T_{min}$ until we are left with $t_{min}$. +In practice, this means that adding more parentheses in RE does not drastically change submatch results. +% +Note that this doesn't mean that P-order is an extension of S-order: +the two orders may disagree. +For example, consider trees $t$ and $u$ on figure \ref{fig_mark_enum}: on one hand $t \prec_{2.2} u$, because $\snorm{t}{2.2} = \infty > 0 = \snorm{u}{2.2}$ and s-norms at all preceding submatch positions agree; on the other hand $u <_{1.1} t$, because $\pnorm{t}{1.1} = -1 < 0 = \pnorm{u}{1.1}$ and p-norms at all preceding positions agree. -So the two orders may disagree. -However, as theorem \ref{theorem_order_compat} shows, -the two orders agree on the notion of minimal tree. -% -This is important, as it means that adding a few parentheses in RE will not drastically change submatch results: -we will continuously narrow down the class of $\prec$-minimal trees -until we are left with a unique $<$-minimal tree. -In the rest of the paper the words ``order'' and ``norm`` refer to s-order and s-norm. - - \begin{XThe}\label{theorem_order_compat} - For an IRE $r$ and string $w$, - let $t_{min}$ be the $<$-minimal tree in $\PT(r,w)$ - and let $T_{min} = \PT_{min}(r,w)$ be the class of the $\prec$-minimal trees in $\PT(r,w)$. + +\begin{theoremEnd}[restate, no link to proof, no link to theorem, category=theorem_order_compat]{theorem} + \label{theorem_order_compat} + For a RE $e$ and string $w$, + let $t_{min}$ be the $<$-minimal tree in $\PT(e,w)$ + and let $T_{min}$ be the class of the $\prec$-minimal trees in $\PT(e,w)$. Then $t_{min} \in T_{min}$. - (Proof given in appendix [??].) - \end{XThe} +\end{theoremEnd} +\begin{proofEnd} + Consider any $t \in T_{min}$. + From $t$ we can construct another tree $t'$ in the following way. + Consider all positions $p \in Sub(t)$ which are not proper prefixes of another position in $Sub(t)$. + For each such position, $t|_p$ is itself a PT for some sub-IRE $r'$ and substring $w'$: $t|_p \in \PT(r', w')$. + Let $t'_{min}$ be the $<$-minimal tree in $\PT(r', w')$ and substitute $t|_p$ with $t'_{min}$. + Let $t'$ be the tree resulting from all such substitutions + (note that they are independent of the order in which we consider positions $p$). + Since substitutions preserve s-norm at submatch positions, we have $t' \in T_{min}$. + We will show that $t' = t_{min}$. + \\[0.5em] + Suppose, on the contrary, that $t' \neq t_{min}$. + % + Then $t_{min} <_p t'$ for some decision position $p$. + % + It must be that $p \not\in Sub(t') \cup Sub(t_{min})$, because + otherwise $\snorm{t_{min}}{p} = \pnorm{t_{min}}{p} > \pnorm{t'}{p} = \snorm{t'}{p}$ + and $\pnorm{t_{min}}{p} = \pnorm{t'}{p} \; \forall q < p$ implies $\snorm{t_{min}}{p} = \snorm{t'}{p} \; \forall q < p$, + which means that $t_{min} \prec_p t'$, which contradicts to $t' \in T_{min}$. + Thus $p$ is a non-submatch position. + % + Let $p = p'.p''$, where $p'$ is the longest proper prefix of $p$ in $Sub(u) \cup Sub(t_{min})$. + % + For all $q \leq p'$ it must be that $\snorm{u}{q} = \snorm{t_{min}}{q}$, + otherwise $\snorm{u}{q} \neq \snorm{t_{min}}{q}$ implies $\pnorm{u}{q} \neq \pnorm{t_{min}}{q}$, + which contradicts to $t_{min} <_p t'$ because $q \leq p' < p$. + % + By lemma \ref{lemma_subtrees} subtrees $t'_{p'}$ and $t_{min}|_{p'}$ are comparable: + $\exists r', w' : t'|_{p'}, t_{min}|_{p'} \in \PT(r', w')$. + By construction of $t'$ subtree $t'_{p'}$ is $<$-minimal in $\PT(r', w')$, + but at the same time $t_{min} <_{p'.p''} u$ implies $t_{min}|_{p'} <_{p''} u|_{p'}$. + Contradiction. +\end{proofEnd} Following the idea of Okui and Suzuki, we go from comparison of parse trees to comparison of their linearized representation --- parenthesized expressions. @@ -825,15 +956,15 @@ and the set of all prefixes in $\PE(r, w)$ is denoted $\PR(r, w)$. Each PE $\alpha$ can be represented as $\alpha_0 a_1 \alpha_1 \dots a_n \alpha_n$, where $\alpha_i$ is the $i$-th \emph{frame} --- a possibly empty sequence of parentheses between subsequent alphabet symbols $a_i$ and $a_{i+1}$ (or the beginning and end of $\alpha$). -We say that PE prefixes $\alpha$ and $\beta$ are \emph{comparable} -if they contain the same number of frames and $\alpha, \beta \in \PR(r, w)$ for some $r$ and $w$. +PE fragments $\alpha$ and $\beta$ are \emph{comparable} +if they have the same number of frames and $\alpha, \beta \in \PR(r, w)$ for some $r$ and $w$. % -For PE fragments $\alpha$ and $\beta$, -$\alpha \sqcap \beta$ denotes the longest common prefix of $\alpha$ and $\beta$, +For fragments $\alpha$ and $\beta$, +$\alpha \sqcap \beta$ denotes their longest common prefix, $\alpha \backslash \beta$ denotes the suffix of $\alpha$ after removing $\alpha \sqcap \beta$, -$lasth(\alpha)$ denotes the height of the last parenthesis in $\alpha$ (or $\infty$ if $\alpha$ is empty or begins with a letter), -$minh(\alpha)$ denotes the minimal height of parenthesis in $\alpha$ (or $\infty$ if $\alpha$ is empty or begins with a letter), -$first(\alpha)$ denotes the first parenthesis in $\alpha$ (or $\bot$ if $\alpha$ is empty or begins with a letter). +$lasth(\alpha)$ denotes the height of the last parenthesis in $\alpha$ (or $\infty$ if $\alpha$ is empty or begins with an alphabet symbol), +$minh(\alpha)$ denotes the minimal height of parenthesis in $\alpha$ (or $\infty$ if $\alpha$ is empty or begins with an alphabet symbol), +$f\!irst(\alpha)$ denotes the first parenthesis in $\alpha$ (or $\bot$ if $\alpha$ is empty or begins with an alphabet symbol). For comparable PE fragments $\alpha$ and $\beta$ the index of the first distinct pair of frames is called \emph{fork}. \begin{figure}\label{fig_pe} @@ -847,88 +978,84 @@ Examples: (a) -- (d): four main rules of POSIX comparison, %\FloatBarrier - \begin{Xdef} + \begin{definition} + \label{def_traces} Let $\alpha$, $\beta$ be comparable PE prefixes, such that $\alpha = \alpha_0 a_1 \alpha_1 \dots a_n \alpha_n$, $\beta = \beta_0 a_1 \beta_1 \dots a_n \beta_n$ and $k$ is the fork. We define $trace (\alpha, \beta)$ as the sequence $(\rho_0, \dots, \rho_n)$, where: - $$ + % + \begin{align*} \rho_i = \begin{cases} -1 &\text{if } i < k \\[-0.2em] min (lasth (\alpha_i \sqcap \beta_i), minh(\alpha_i \backslash \beta_i)) &\text{if } i = k \\[-0.2em] min (\rho_{i-1}, minh(\alpha_i)) &\text{if } i > k \end{cases} - $$ + \end{align*} + We write $traces(\alpha, \beta)$ to denote $\big( trace (\alpha, \beta), trace (\beta, \alpha) \big)$. - \end{Xdef} + \end{definition} - \begin{Xdef}\label{prec1} + \begin{definition}\label{prec1} + (Longest precedence.) Let $\alpha$, $\beta$ be comparable PE prefixes and $traces(\alpha, \beta) = \big( (\rho_0, \dots, \rho_n), (\rho'_0, \dots, \rho'_n) \big)$. - The \emph{longest-precedence} relation $\sqsubset$ is defined as - $\alpha \sqsubset \beta \Leftrightarrow \exists i \leq n: + Then $\alpha \sqsubset \beta \Leftrightarrow \exists i \leq n: \big( \rho_i > \rho'_i \big) \wedge \big( \rho_j = \rho'_j \; \forall j > i \big)$. If neither $\alpha \sqsubset \beta$, nor $\beta \sqsubset \alpha$, then $\alpha$, $\beta$ are \emph{longest-equivalent}: $\alpha \sim \beta$ (note that in this case $\rho_i = \rho'_i \; \forall i = \overline {1, n}$). - \end{Xdef} + \end{definition} - \begin{Xdef}\label{prec2} + \begin{definition}\label{prec2} + (Leftmost precedence.) Let $\alpha$, $\beta$ be comparable PE prefixes, and let $x = first (\alpha \backslash \beta)$, $y = first (\beta \backslash \alpha)$. - The \emph{leftmost-precedence} relation $\subset$ is defined as - $\alpha \subset \beta \Leftrightarrow x < y$, where + Then $\alpha \subset \beta \Leftrightarrow x < y$, where the set of possible values of $x$ and $y$ is ordered as follows: $\bot < \Xr < \Xl < \Xm$. - \end{Xdef} + \end{definition} - \begin{Xdef}\label{pe_order} - The \emph{longest-leftmost-precedence} relation $<$ on comparable PE prefixes is defined as + \begin{definition}\label{pe_order} + (Longest-leftmost precedence.) + Let $\alpha$, $\beta$ be comparable PE prefixes, then $\alpha < \beta \Leftrightarrow \big( \alpha \sqsubset \beta \big) \vee \big( \alpha \sim \beta \wedge \alpha \subset \beta \big)$. - \end{Xdef} - - \begin{XThe}\label{theorem_order_on_pe_same_as_on_pt} - Let $s, t \in PT(r, w)$, then - $s <_p t \Leftrightarrow \Phi_{h}(s) < \Phi_{h}(t) \; \forall h$. - (Proof in apendix [??].) - \end{XThe} - -Now we have a convenient definition of comparison on parenthesized expressions, -and theorem \ref{theorem_order_on_pe_same_as_on_pt} states that it is equivalent to comparison of parse trees. -What remains is to show that PEs can be compared \emph{incrementally}. -This is necessary for an efficient matching algorithm, -because otherwise we would need to accumulate full-length PEs before comparing them, -which means unbounded memory consumption --- PEs grow with the length of input. -Justification of incremental comparison consists of two parts. -First, lemma \ref{lemma_incr_cmp_frames} states that PEs can be compared frame by frame --- -this justifies the use of precedence tables. - - \begin{XLem}\label{lemma_incr_cmp_frames} - \emph{Frame-by-frame comparison of PEs.} - Let $\alpha = \alpha_0 a_1 \dots a_n \alpha_n$ and - $\beta = \beta_0 a_1 \dots a_n \beta_n$ be comparable PE prefixes, where $n \geq 1$. - If $\alpha_0 \dots \alpha_{n-1} < \beta_0 \dots \beta_{n-1}$, - then $\alpha < \beta$. - (Proof in apendix [??].) - \end{XLem} - -Second, in order to construct efficient $\epsilon$-closure algorithm -we need to show that PEs can be compared incrementally inside of each frame, -if the corresponding TNFA paths meet at an intermediate state. -This is necessary to avoid exploring potentially exponential number of paths in closure. + \end{definition} + +\begin{theoremEnd}[restate, no link to proof, no link to theorem, category=theorem_order_on_pe_same_as_on_pt]{theorem} + \label{theorem_order_on_pe_same_as_on_pt} + For a given RE $e$ and string $w$, + if $s, t \in PT(e, w)$ then + $s \prec t \Leftrightarrow \Phi_{h}(s) < \Phi_{h}(t) \; \forall h$. +\end{theoremEnd} +\begin{proofEnd} + Forward implication is given by lemma \ref{lemma_pe_less}. + Backward implication: + suppose, on the contrary, that $\Phi_{h}(s) < \Phi_{h}(t) \; \forall h$, but $s \not\prec t$. + Since $\prec$ is a strict weak order (by theorem \ref{theorem_sorder_on_PTs}), + it must be that either $s \sim t$ + (then $\Phi_{h}(s) = \Phi_{h}(t) \; \forall h$ by lemma \ref{lemma_pe_equiv}), + or $t \prec s$ + (then $\Phi_{h}(t) < \Phi_{h}(s) \; \forall h$ by lemma \ref{lemma_pe_less}). + Both cases contradict $\Phi_{h}(s) < \Phi_{h}(t) \; \forall h$, + therefore assumption $s \not\prec t$ is incorrect. +\end{proofEnd} + +Next, we go from comparison of PEs to comparison of TNFA paths. % A \emph{path} in TNFA $(\Sigma, Q, T, \Delta, q_0, q_f)$ is a sequence of states $\{q_1, \hdots, q_n\} \subseteq Q$ connected by transitions $\{(q_i, a_i, b_i, q_{i + 1})\}_{i=1}^{n-1} \subseteq \Delta$, where $n \in \YN$. % Every path induces a string of alphabet symbols -and a mixed string of symbols and tags which corresponds to a fragment of PE -(positive opening tags map to $\Xl$, positive closing tags map to $\Xr$, -and every contiguous sequence of negative tags maps to $\Xm$). +and a mixed string of symbols and tags which corresponds to a fragment of PE: +positive opening tags map to $\Xl$, +positive closing tags map to $\Xr$, +and negative tags map to $\Xm$. We write $q_1 \overset {s|\alpha} {\rightsquigarrow} q_2$ to denote the fact that a path from $q_1$ to $q_2$ induces alphabet string $s$ and PE fragment $\alpha$. % @@ -937,88 +1064,126 @@ $\pi_1 = q_1 \overset {s|\alpha} {\rightsquigarrow} q_2$ and $\pi_2 = q_1 \overset {s|\beta} {\rightsquigarrow} q_3$ we say that $\pi_1 < \pi_2$ if $\alpha < \beta$. % -For a given RE $r$ we say that a path is \emph{minimal} if it induces -$\alpha = \PE(t)$ for some minimal tree $t \in \PT(r)$. +For a given RE $e$ we say that a path in TNFA for $e$ is \emph{minimal} if it induces +$\alpha = \PE(t)$ for some minimal tree $t \in \PT(e)$. % Two paths are \emph{ambiguous} if their start and end states coincide and they induce the same alphabet string. Two paths have a \emph{join point} if they have ambiguous prefixes. % -%We state two facts that are later used to show that closure algorithm finds a minimal path. -%First, we show that minimal paths do not contain tagged $\epsilon$-loops (lemma \ref{lemma_closure_minpaths}). -%Second, we show that for paths without tagged $\epsilon$-loops -%comparison of path prefixes at the join point gives the same result as comparison of extended paths (lemma \ref{lemma_closure_rightdist}). -%In section \ref{section_closure} we give a specific closure algorithm and show that it discards paths with tagged $\epsilon$-loops. - -\newcommand \lemmaclosureminpaths { -\emph{Paths with tagged $\epsilon$-loops are not minimal.} - For any path $\pi_1 \pi_2 \pi_3$ where $\pi_2$ is a tagged $\epsilon$-loop - there is path $\pi_1 \pi_3$ - such that $\pi_1 \pi_3 < \pi_1 \pi_2 \pi_3$. -} -\begin{XLem}\label{lemma_closure_minpaths} -\lemmaclosureminpaths -(Proof in apendix [??].) -\end{XLem} - -\newcommand \lemmaclosurerightdist { - \emph{Right distributivity of path comparison over path concatenation for paths with at most one tagged $\epsilon$-loop.} - Let - $\pi_\alpha = q_0 \overset {u | \alpha} {\rightsquigarrow} q_1$ and - $\pi_\beta = q_0 \overset {u | \beta} {\rightsquigarrow} q_1$ - be ambiguous paths - and $\pi_\gamma = q_1 \overset {\epsilon | \gamma} {\rightsquigarrow} q_2$ - their common $\epsilon$-suffix, - such that paths $\pi_\alpha$ and $\pi_\beta$ are loop-free, - at most one of $\pi_\alpha \pi_\gamma$ and $\pi_\beta \pi_\gamma$ contains a tagged $\epsilon$-loop. - Then $\alpha < \beta \implies \alpha \gamma < \beta \gamma$. -} -\begin{XLem}\label{lemma_closure_rightdist} -\lemmaclosurerightdist -(Proof in apendix [??].) -\end{XLem} +In order to justify our TNFA simulation algorithm, +we need to show that PEs induced by TNFA paths can be compared incrementally +(otherwise we would have to keep full-length PEs, which requires the amount of memory proportional to the lenght of input). +Justification of incremental comparison consists of two parts: +the following lemma \ref{lemma_incr_cmp_frames} justifies comparison between frames, +and lemmata \ref{lemma_closure_minpaths}, \ref{lemma_closure_noloop}, \ref{lemma_closure_rightdist} +in section \ref{section_closure} justify comparison at join points inside of one frame +(this is necessary as the number of paths in closure may be exponential in the number of states). + +\begin{theoremEnd}[restate, no link to proof, no link to theorem, category=lemma_frames]{lemma} +[Frame-by-frame comparison of PEs] + \label{lemma_incr_cmp_frames} + If $\alpha$, $\beta$ are comparable PE prefixes, + $c$ is an alphabet symbol and + $\gamma$ is a single-frame PE fragment, + then $\alpha < \beta$ implies $\alpha c \gamma < \beta c \gamma$. +\end{theoremEnd} +\begin{proofEnd} + Let $\big((\rho_1, \dots, \rho_n), (\rho'_1, \dots, \rho'_n)\big) = traces(\alpha, \beta)$ where $n \geq 1$. + Since $\alpha c \gamma$, $\beta c \gamma$ have one more frame than $\alpha$, $\beta$ + and the first $n$ frames are identical to frames of $\alpha$, $\beta$, + we can represent $traces(\alpha c \gamma, \beta c \gamma)$ + as $\big((\rho_1, \dots, \rho_n, \rho_{n+1}), (\rho'_1, \dots, \rho'_n, \rho'_{n+1})\big)$. + %Consider two possible cases: + % + \begin{itemize}[itemsep=0.5em, topsep=0.5em] + \item[(1)] + Case $\alpha \sim \beta \wedge \alpha \subset \beta$. + In this case $\rho_i = \rho'_i \;\forall i \leq n$, + therefore $\rho_{n+1} = min(\rho_n, minh(\gamma)) = min(\rho'_n, minh(\gamma)) = \rho'_{n+1}$ + and $\alpha c \gamma \sim \beta c \gamma$. + Furthermore, + $first (\alpha c \gamma \backslash \beta c \gamma) = first (\alpha \backslash \beta)$ and + $first (\beta c \gamma \backslash \alpha c \gamma) = first (\beta \backslash \alpha)$, + therefore $\alpha \subset \beta \implies \alpha c \gamma \subset \beta c \gamma$. + \item[(2)] + Case $\alpha \sqsubset \beta$. + In this case $\exists j \leq n$ such that $\rho_j > \rho'_j$ and $\rho_i = \rho'_i \;\forall j < i \leq n$. + We show that $\exists l \leq n + 1$ such that $\rho_l > \rho'_l$ and $\rho_i = \rho'_i \;\forall l < i \leq n + 1$, + which by definition means that $\alpha c \gamma \sqsubset \beta c \gamma$. + \begin{itemize} + \item[(2a)] + Case $j < n$. + In this case $\rho_n = \rho'_n$ and + $\rho_{n+1} = min(\rho_n, minh(\gamma)) = min(\rho'_n, minh(\gamma)) = \rho'_{n+1}$, + therefore $l = j$. + \item[(2b)] + Case $j = n$ and $minh(\gamma) > \rho'_n$. + In this case $\rho_n > \rho'_n$ and we have + $\rho_{n+1} = min(\rho_n, minh(\gamma)) > \rho'_n$ and + $\rho'_{n+1} = min(\rho'_n, minh(\gamma)) = \rho'_n$, + therefore $\rho_{n+1} > \rho'_{n+1}$ + and $l = n + 1$. + \item[(2c)] + Case $j = n$ and $minh(\gamma) \leq \rho'_n$. + In this case $\rho_n > \rho'_n$ and we have + $\rho_{n+1} = min(\rho_n, minh(\gamma)) = minh(\gamma)$ and + $\rho'_{n+1} = min(\rho'_n, minh(\gamma)) = minh(\gamma)$, + therefore $\rho_{n+1} = \rho'_{n+1}$ + and $l = n$. + \end{itemize} + \end{itemize} + In both cases $\alpha c \gamma < \beta c \gamma$. +\end{proofEnd} -%\vfill \section{$\epsilon$-closure}\label{section_closure} The problem of constructing $\epsilon$-closure with POSIX disambiguation can be formulated as a shortest path problem on directed graph with weighted arcs. -%In our case \emph{weight} corresponds to PE fragment induced by the path. +In our case weight is not a number --- it is the PE fragment induced by the path. % -Cormen [Cor??] gives a framework for shortest-path algorithms based on \emph{closed semirings}. +We give two algorithms for closure construction: GOR1, named after the well-known Goldberg-Radzik algorithm [GRC??], +and GTOP, named after ``global topological order''. % -A \emph{semiring} is a structure $(\YK, \oplus, \otimes, \Xbar{0}, \Xbar{1})$, where -$\YK$ is a set, -$\oplus \!\!:\!\! \YK \times \YK \rightarrow \YK$ is an associative and commutative operation with identity element $\Xbar{0}$, -$\otimes \!\!:\!\! \YK \times \YK \rightarrow \YK$ is an associative operation with identity element $\Xbar{1}$, -$\otimes$ distributes over $\oplus$ -and $\Xbar{0}$ is annihilator for $\otimes$. +Both have the usual structure of shortest-path finding algorithms. +The algorithm starts with a set of initial configurations, empty queue and empty set of resulting configurations. +Initial configurations are enqueued and the algorithm loops until the queue becomes empty. +At each iteration it dequeues configuration $(q, o, u, r)$ and scans $\epsilon$-transitions from state $q$. +For transition $(q, \Xund, \gamma, p)$ it constructs a new configuration $(p, o, v, r)$ +that combines $u$ and $\gamma$ in an extended path $v$. +If the resulting set contains another configuration for state $p$, +then the algorithm choses configuration which has a better path from POSIX perspective. +Otherwise it adds the new configuration to the resulting set. +If the resulting set was changed, the new configuration is enqueued for further scanning. +Eventually all states in $\epsilon$-closure are explored, no improvements can be made, and the algorithm terminates. % -Additionally, \emph{closed} semiring requires that -$\oplus$ is idempotent, -any countable $\oplus$-sum of $\YK$ elements is in $\YK$, -and associativity, commutativity, distributivity and idempotence apply to countable $\oplus$-sums. -Mohri [Moh02] generalizes this definition and notes that either left or right distributivity is sufficient. +%Lemma \ref{lemma_closure_rightdist} allows us to skip comparison in non-join states (with in-degree 1), because +%any path to such state is formed by concatenation of the unique transition and the shortest known path to the previous state. +\\ + +The difference between GOR1 and GTOP is in the order they inspect configurations. % -In our case we have semiring $(\YP, min, \cdot, \varnothing, \epsilon)$, where -$\YP$ is the set of closure paths with at most one loop, -$min$ is POSIX comparison of ambiguous paths, -$\cdot$ is concatenation of paths (within TNFA bounds), -$\varnothing$ corresponds to an infinitely long path, -and $\epsilon$ is the empty path. +Both algorithms are based on the idea of topologcal ordering. +Unlike other shortest-path algorithms, their queuing discipline is based on graph structure, not on the distance estimates. +This is crucial, because we do not have any distance estimates: +paths can be compared, but there is no absolute ``POSIX-ness'' value that we can attribute to each path. % -It is easy to show that -$min$ is commutative and associative (theorem \ref{theorem_order_on_pe_same_as_on_pt} and \ref{theorem_sorder_on_PTs}), -$min(\pi, \varnothing) = min(\varnothing, \pi) = \pi$, -$\cdot$ is associative, $\pi \cdot \epsilon = \epsilon \cdot \pi = \pi$, -$\pi \cdot \varnothing = \varnothing \cdot \pi = \varnothing$, -and right distributivity of $\cdot$ over $min$ for paths with at most one $\epsilon$-loop is given by lemma \ref{lemma_closure_rightdist}. +GOR1 is described in [CGR93]. +It uses two stacks and makes a number of passes; +each pass consists of a depth-first search on admissible subgraph +followed by a linear scan of states that are topologically ordered by depth-first search. +The algorithm is one of the most efficient shortest-path algorithms [CGR96] [CGR99]. +$n$-Pass structure guarantees worst-case complexity $O(n \, m)$ of the Bellman-Ford algorithm, +where $n$ is the number of states and $m$ is the number of transitions in $\epsilon$-closure +(both can be approximated by TNFA size). % -Idempotence holds because $min(\pi, \pi) = \pi$. +GTOP is a simple algorithm that maintains one global priority queue (e.g. a binary heap) +ordered by the topological index of states (for graphs with cycles, we assume reverse depth-first post-order). +Since GTOP does not have $n$-pass structure, its worst-case complexity is not clear. +However, it is much simpler to implement +and in practice it performs almost identically to GOR1 on graphs induced by TNFA $\epsilon$-closures. % -Since $\YP$ is limited to paths with at most one $\epsilon$-loop, -countable subsets of $\YP$ are finite -and the properties for $\oplus$-sums over countable subsets are satisfied. +On acyclic graphs, both GOR1 and GTOP have linear $O(n + m)$ complexity. \\ \begin{algorithm}[] \DontPrintSemicolon \SetKwProg{Fn}{}{}{} \SetAlgoInsideSkip{medskip} @@ -1221,66 +1386,339 @@ Definitions of $compare ()$ and $extend \Xund path ()$ are given in sections \re $\YC$ is the set of all configurations.} \end{algorithm} -We give two algorithms for closure construction: GOR1, named after the well-known Goldberg-Radzik algorithm [GRC??], -and GTOP, named after ``global topological order''. +The general proof of correctness of shortest-path algorithms is out of the scope of this paper. +However, we need to justify the application of these algorithms to our setting. % -Both have the usual structure of shortest-path finding algorithms. -The algorithm starts with a set of initial configurations, empty queue and empty set of resulting configurations. -Initial configurations are enqueued and the algorithm loops until the queue becomes empty. -At each iteration it dequeues configuration $(q, o, u, r)$ and scans $\epsilon$-transitions from state $q$. -For transition $(q, \Xund, \gamma, p)$ it constructs a new configuration $(p, o, v, r)$ -that combines $u$ and $\gamma$ in an extended path $v$. -If the resulting set contains another configuration for state $p$, -then the algorithm choses configuration which has a better path from POSIX perspective. -Otherwise it adds the new configuration to the resulting set. -If the resulting set was changed, the new configuration is enqueued for further scanning. -Eventually all states in $\epsilon$-closure are explored, no improvements can be made, and the algorithm terminates. -\\ - -Importantly, the algorithm finds non-looping paths before looping ones. -Given that, and using lemma \ref{lemma_closure_minpaths}, -we can show by induction on path length that the paths constructed at each step of the algorithm do not contain $\epsilon$-loops. -This means that for any two paths explored by the algorithm, -at most one path may contain tagged $\epsilon$-loop (and only one loop), -which justifies the application of lemma \ref{lemma_closure_rightdist}. -% -(Note that for paths with multiple $\epsilon$-loops right distributivity may not hold: -we may have paths -$\pi_\alpha = q_0 \overset {u | \alpha} {\rightsquigarrow} q_1$, -$\pi_\beta = q_1 \overset {\epsilon | \beta} {\rightsquigarrow} q_1$ and -$\pi_\gamma = q_1 \overset {\epsilon | \gamma} {\rightsquigarrow} q_1$, -such that $\pi_\beta$ and $\pi_\gamma$ are two different $\epsilon$-loops through the same subautomaton -and $\pi_\alpha \pi_\beta < \pi_\alpha \pi_\gamma$: -in this case $\pi_\alpha \pi_\beta \pi_\gamma < \pi_\alpha \pi_\gamma$, -but $\pi_\alpha \pi_\beta > \pi_\alpha$, because the first is a proper prefix of the second.) -% -Lemma \ref{lemma_closure_rightdist} allows us to skip comparison in non-join states (with in-degree 1), because -any path to such state is formed by concatenation of the unique transition and the shortest known path to the previous state. -\\ - -The difference between GOR1 and GTOP is in the order they inspect configurations. +In order to do that, we recall the framework for solving shortest-path algorithms based on \emph{closed semirings} +described in [Cor??] (section 26.4) +and show that our problem fits into this framework. % -Both algorithms are based on the idea of topologcal ordering. -Unlike other shortest-path algorithms, their queuing discipline is based on graph structure, not on the distance estimates. -This is crucial, because we do not have any distance estimates: -paths can be compared, but there is no absolute ``POSIX-ness'' value that we can attribute to each path. +A \emph{semiring} is a structure $(\YK, \oplus, \otimes, \Xbar{0}, \Xbar{1})$, where +$\YK$ is a set, +$\oplus \!\!:\!\! \YK \times \YK \rightarrow \YK$ is an associative and commutative operation with identity element $\Xbar{0}$, +$\otimes \!\!:\!\! \YK \times \YK \rightarrow \YK$ is an associative operation with identity element $\Xbar{1}$, +$\otimes$ distributes over $\oplus$ +and $\Xbar{0}$ is annihilator for $\otimes$. % -GOR1 is described in [CGR93]. -It uses two stacks and makes a number of passes; -each pass consists of a depth-first search on admissible subgraph -followed by a linear scan of states that are topologically ordered by depth-first search. -The algorithm is one of the most efficient shortest-path algorithms [CGR96] [CGR99]. -$n$-Pass structure guarantees worst-case complexity $O(n \, m)$ of the Bellman-Ford algorithm, -where $n$ is the number of states and $m$ is the number of transitions in $\epsilon$-closure -(both can be approximated by TNFA size). +Additionally, \emph{closed} semiring requires that +$\oplus$ is idempotent, +any countable $\oplus$-sum of $\YK$ elements is in $\YK$, +and associativity, commutativity, distributivity and idempotence apply to countable $\oplus$-sums. +Mohri generalizes this definition and notes that either left or right distributivity is sufficient [Moh02]. % -GTOP is a simple algorithm that maintains one global priority queue (e.g. a binary heap) -ordered by the topological index of states (for graphs with cycles, we assume reverse depth-first post-order). -Since GTOP does not have $n$-pass structure, its worst-case complexity is not clear. -However, it is much simpler to implement -and in practice it performs almost identically to GOR1 on graphs induced by TNFA $\epsilon$-closures. +In our case $\YK$ is the set of closure paths without tagged $\epsilon$-loops: +the following lemma \ref{lemma_closure_minpaths} and \ref{lemma_closure_noloop} +show that, on one hand, paths with tagged $\epsilon$-loops are not minimal, +and on the other hand such paths are discarded by the algorithm, +so they can be removed from consideration. % -On acyclic graphs, both GOR1 and GTOP have linear $O(n + m)$ complexity. +Consequently $\YK$ is finite. +We have semiring $(\YK, min, \cdot, \varnothing, \epsilon)$, where +$min$ is POSIX comparison of ambiguous paths, +$\cdot$ is concatenation of paths at the join points +(subject to restriction that paths do not contain tagged $\epsilon$-loops +and remain within TNFA bounds --- concatenation of arbitrary paths is not in $\YK$), +$\varnothing$ corresponds to artificial infinitely long path, +and $\epsilon$ is the empty path. +% +It is easy to show that +$min$ is commutative and associative, +$\varnothing$ is identity for $min$ ($min(\pi, \varnothing) = min(\varnothing, \pi) = \pi$), +$\cdot$ is associative, +$\epsilon$ is identity for $\cdot$ ($\pi \cdot \epsilon = \epsilon \cdot \pi = \pi$), +$\varnothing$ is annihilator for $\cdot$ ($\pi \cdot \varnothing = \varnothing \cdot \pi = \varnothing$), +and right distributivity of $\cdot$ over $min$ for paths with at most one $\epsilon$-loop is given by lemma \ref{lemma_closure_rightdist}. +% +Idempotence holds because $min(\pi, \pi) = \pi$. +% +Since $\YK$ is finite, the properties for $\oplus$-sums over countable subsets are satisfied. + +\begin{theoremEnd}[restate, no link to proof, no link to theorem, category=lemmata_closure]{lemma} + \label{lemma_closure_minpaths} + Minimal paths do not contain tagged $\epsilon$-loops. +\end{theoremEnd} +\begin{proofEnd} + % Proof in terms of REs and correspondence between subexpression and loop + % is a bit hard because of unrolling of repetition in TNFA construction + % (there is no direct correspondence between sub-RE and sub-TNFA). + % + Suppose, on the contrary, that $\pi$ is a minimal path in some TNFA + and that $\pi$ contains at least one tagged $\epsilon$-loop. + We show that it is possible to construct another path $\pi'$ such that $\pi' < \pi$. + % + Path $\pi$ can be represented as + $\pi = \pi_1 \pi_2 \pi_3$, where + $\pi_1 = q_0 \overset {u | \alpha} {\rightsquigarrow} q$, + $\pi_2 = q \overset {\epsilon | \beta} {\rightsquigarrow} q$ is the last tagged $\epsilon$-loop on $\pi$ and + $\pi_3 = q \overset {v | \gamma} {\rightsquigarrow} q_f$. + Let $\pi' = \pi_1 \pi_3$ be the path that is obtained from $\pi$ by removing the loop $\pi_2$. + Paths $\pi$ and $\pi'$ consume the same input string $uv$ + and induce comparable PE $\alpha \beta \gamma$ and $\alpha \gamma$. + Let $\big( (\rho_1, \hdots, \rho_n), (\rho'_1, \hdots, \rho'_n) \big) = traces (\alpha \beta \gamma, \alpha \gamma)$ + and let $k$ be the index of the fork frame. + % + By construction of TNFA the loop $\pi_2$ must be contained in a sub-TNFA $f$ + for sub-IRE of the form $e = (\Xund, \Xund, e_1^{1,\infty})$, + as this is the only looping TNFA construct --- see algorithm \ref{alg_tnfa}. + %Since the $\pi_2$ is tagged, $\Phi_h(e_1)$ is of the form $\Xl_h \dots \Xr_h$. + Let $f_1$ be the sub-TNFA for $e_1$. + Path $\pi$ enters $f$ and iterates through $f_1$ at least twice before leaving $f$ + (single iteration is not enough to create a loop by TNFA construction). + Let $j$ be the total number of iterations through $f_1$, + and let $i$ be the index of the last $\epsilon$-loop iteration + (note that not all iterations are necessarily $\epsilon$-loops). + Consider two possible cases: + % + \begin{enumerate}[itemsep=0.5em, topsep=0.5em] + \item[(1)] + Case $i = j$. + In this case fork of $\alpha \beta \gamma$ and $\alpha \gamma$ happens immediately after $(i-1)$-th iteration: + % + \begin{alignat*}{10} + \alpha \beta \gamma &= x_0 \Xl_{h-1} \;&&\; \Xl_h x_1 \Xr_h \hdots \Xl_h x_{i-1} \Xr_h \;&&\big|\; \Xl_h x_{i} \Xr_h \;&&\; \Xr_{h-1} x_{j+1} \\[-0.5em] + \alpha \gamma &= x_0 \Xl_{h-1} \;&&\; \Xl_h x_1 \Xr_h \hdots \Xl_h x_{i-1} \Xr_h \;&&\big|\; \;&&\; \Xr_{h-1} x_{j+1} + \end{alignat*} + % + Since $x_i$ is an $\epsilon$-loop, it is contained in the fork frame of $\alpha \beta \gamma$. + We have $minh (\beta) = h$ and $minh (\gamma) \leq h - 1$, therefore $\rho_k = \rho'_k \leq h - 1$. + Subsequent frames $l > k$ (if any) are identical and thus $\rho_l = \rho'_l$. + Furthermore, $first (\gamma) = \Xr < \Xl = first (\beta)$. + Therefore $\alpha \beta \gamma \sim \alpha \gamma$ and $\alpha \gamma \subset \alpha \beta \gamma$. + + \item[(2)] + Case $i < j$. + In this case $(i + 1)$-th iteration cannot be an $\epsilon$-loop + (because we assumed that $i$-th iteration is the last $\epsilon$-loop), + therefore the fork of $\alpha \beta \gamma$ and $\alpha \gamma$ happens + inside of $i$-th iteration of $\alpha \beta \gamma$ + and $(i + 1)$-th iteration of $\alpha \gamma$: + % + \begin{alignat*}{10} + \alpha \beta \gamma &= x_0 \Xl_{h-1} \;&&\; \Xl_h x_1 \Xr_h \hdots \Xl_h x_{i-1} \Xr_h \Xl_h y_1 \;&&\big|\; y_2 \Xr_h \Xl_h x_{i+1} && \Xr_h \Xl_h x_{i+2} \Xr_h \hdots \Xl_h x_j \Xr_h \;&&\; \Xr_{h-1} x_{j+1} \\[-0.5em] + \alpha \gamma &= x_0 \Xl_{h-1} \;&&\; \Xl_h x_1 \Xr_h \hdots \Xl_h x_{i-1} \Xr_h \Xl_h y_1 \;&&\big|\; y_3 && \Xr_h \Xl_h x_{i+2} \Xr_h \hdots \Xl_h x_j \Xr_h \;&&\; \Xr_{h-1} x_{j+1} + \end{alignat*} + % + Here $y_1 y_2 = x_i$ and $y_1 y_3 = x_{i+1}$ ($i$-th iteration is missing from $\alpha \gamma$ by construction of $\pi'$). + Fragment $y_2$ is part of the $\epsilon$-loop, + therefore fork frame of $\alpha \beta \gamma$ contains parenthesis $\Xr_h$ and we have $\rho_k = h$. + On the other hand, $y_3$ contains alphabet symbols, + because $x_{i+1}$ is not an $\epsilon$-loop and $y_1$ is a part of the $\epsilon$-loop. + Therefore fork frame of $\alpha \gamma$ ends in $y_3$ and we have $\rho'_k > h$. + % + %In this case + %fork frame of $\alpha \beta \gamma$ contains $y_2 \Xr_h \Xl_h$ fragment, because $y_2$ is part of the $\epsilon$-loop. + %But the fork frame of $\alpha \gamma$ ends inside of $y_3$, because $(i+1)$-th repetiton is not an $\epsilon$-loop and must contain alphabet symbols. + %Therefore at the fork frame $k$ we have $\rho_k = h$ and $\rho'_k > h$. + % + All subsequent frames $l > k$ are identical: + if they contain parentheses of height less than $h$, then $\rho_l = \rho'_l < h$; + otherwise $\rho_l \leq h$ and $\rho'_l > h$. + Therefore $\alpha \gamma \sqsubset \alpha \beta \gamma$. + \end{enumerate} + % + In both cases $\alpha \gamma < \alpha \beta \gamma$, + which contradicts the fact that $\pi$ is a minimal path. +\end{proofEnd} +\vspace{-0.5em} + +\begin{theoremEnd}[restate, no link to proof, no link to theorem, category=lemmata_closure]{lemma} + \label{lemma_closure_noloop} + GOR1 and GTOP discard paths with tagged $\epsilon$-loops. +\end{theoremEnd} +\begin{proofEnd} + Suppose that GOR1/GTOP finds path $\pi_1 \pi_2$ + where $\pi_1 = q_0 \overset {s | \alpha} {\rightsquigarrow} q_1$ + and $\pi_2 = q_1 \overset {\epsilon | \gamma} {\rightsquigarrow} q_1$ is a tagged $\epsilon$-loop. + Both algorithms construct new paths by exploring transitions from the end state of existing paths, + so they can only find $\pi_1 \pi_2$ after they find $\pi_1$. + Therefore when GOR1/GTOP finds $\pi_1 \pi_2$, + it already has some shortest-path candidate $\pi'_1 = q_0 \overset {s | \alpha'} {\rightsquigarrow} q_1$ + and must compare ambiguous paths $\pi_1 \pi_2$ and $\pi'_1$. + There are two possibilities: either $\alpha' = \alpha$ + or $\alpha' < \alpha$ (the latter means that the algorithm has found + a shorter path to $q_1$ in between finding $\pi_1$ and $\pi_1 \pi_2$). + Let $\big( (\rho_1, \hdots, \rho_k), (\rho'_1, \hdots, \rho'_k) \big) = traces (\alpha', \alpha \gamma)$. + % + \begin{itemize}[itemsep=0.5em, topsep=0.5em] + \item[(1)] + Case $\alpha' = \alpha$. + Because $\alpha$ is a proper prefix of $\alpha \gamma$, + fork happens at the last frame and we have + $\rho_k = lasth(\alpha)$ and + $\rho'_k = min (lasth(\alpha), minh(\gamma))$. + If $lasth(\alpha) > minh(\gamma)$, then $\rho_k > \rho'_k$ and $\alpha \sqsubset \alpha \gamma$. + Otherwise $\rho_k = \rho'_k$ and $\alpha \sim \alpha \gamma$, + and we have $first(\alpha \backslash \alpha \gamma) = \bot$ and $first(\alpha \gamma \backslash \alpha) \neq \bot$, + therefore $\alpha \subset \alpha \gamma$. + In both cases $\alpha < \alpha \gamma$. + + \item[(2)] + Case $\alpha' < \alpha$. + Let $\big( (\sigma_1, \hdots, \sigma_k), (\sigma'_1, \hdots, \sigma'_k) \big) = traces (\alpha', \alpha)$. + We have $\rho_k = \sigma_k$ and $\rho'_k = min (\sigma'_k, minh(\gamma)) \leq \sigma_k$. + If $minh(\gamma) < \sigma'_k$ then $\rho_k > \rho'_k$ and $\alpha' \sqsubset \alpha \gamma$. + Otherwise $\rho'_k = \sigma'_k$. + If $\alpha' \sqsubset \alpha$ then $\alpha' \sqsubset \alpha \gamma$. + Otherwise $\alpha' \sim \alpha$ and $\alpha' \subset \alpha$. + None of $\alpha$ and $\alpha'$ is a proper prefix of the other, + because otherwise the longer path has an $\epsilon$-loop through $q_1$, which contradicts our assumption about $\pi_1$ and $\pi'_1$. + Therefore $first (\alpha' \backslash \alpha) = first (\alpha' \backslash \alpha \gamma)$ + and $first (\alpha \backslash \alpha') = first (\alpha \gamma \backslash \alpha')$. + Consequently $\alpha' \subset \alpha \implies \alpha' \subset \alpha \gamma$. + Thus $\alpha' < \alpha \gamma$. + \end{itemize} + % + In both cases $\alpha' < \alpha \gamma$, therefore path $\pi_1 \pi_2$ is discarded. +\end{proofEnd} +\vspace{-0.5em} + +\begin{theoremEnd}[restate, no link to proof, no link to theorem, category=lemmata_closure]{lemma} +[Right distributivity of comparison over concatenation for paths without tagged $\epsilon$-loops] + \label{lemma_closure_rightdist} + Let + $\pi_\alpha = q_0 \overset {u | \alpha} {\rightsquigarrow} q_1$ and + $\pi_\beta = q_0 \overset {u | \beta} {\rightsquigarrow} q_1$ + be ambiguous paths in TNFA $f$ for IRE $e$, + and let $\pi_\gamma = q_1 \overset {\epsilon | \gamma} {\rightsquigarrow} q_2$ + be their common $\epsilon$-suffix, + such that $\pi_\alpha \pi_\gamma$ and $\pi_\beta \pi_\gamma$ do not contain tagged $\epsilon$-loops. + If $\alpha < \beta$ then $\alpha \gamma < \beta \gamma$. +\end{theoremEnd} +\begin{proofEnd} + Let + $\big( (\rho_1, \hdots, \rho_k),$ $(\rho'_1, \hdots, \rho'_k) \big) = traces (\alpha, \beta)$ and + $\big( (\sigma_1, \hdots, \sigma_k),$ $(\sigma'_1, \hdots, \sigma'_k) \big) = traces (\alpha \gamma, \beta \gamma)$. + Appending $\gamma$ to $\alpha$ and $\beta$ changes only the last frame, therefore + for frames $i < k$ we have $\rho_i = \sigma_i$ and $\rho'_i = \sigma'_i$. + %For the last $k$-th frame we have + %$\sigma_k = min (\rho_k, minh (\gamma))$ and + %$\sigma'_k = min (\rho'_k, minh (\gamma))$. + Consider two possible cases. + % + \begin{itemize}[itemsep=0.5em, topsep=0.5em] + \item[(1)] + Case $\alpha \sim \beta \wedge \alpha \subset \beta$. + % + We show that $\alpha \gamma \sim \beta \gamma \wedge \alpha \gamma \subset \beta \gamma$. + % + We have $\rho_i = \rho'_i \; \forall i$ (implied by $\alpha \sim \beta$), therefore + $\sigma_i = \sigma'_i \; \forall i$ and consequently $\alpha \gamma \sim \beta \gamma$. + Let + $x = first (\alpha \backslash \beta)$, + $y = first (\beta \backslash \alpha)$, + $x' = first (\alpha \gamma \backslash \beta \gamma)$ and + $y' = first (\beta \gamma \backslash \alpha \gamma)$. + If one of $\pi_\alpha$ and $\pi_\beta$ is a proper prefix of another, + then the longer path contains tagged $\epsilon$-loop through $q_1$, + which contradicts lemma conditions + (the suffix of the longer path must be an $\epsilon$-path, + because $\alpha$ and $\beta$ have the same number of frames + and the suffix is contained in the last frame). + Therefore none of $\pi_\alpha$ and $\pi_\beta$ is a proper prefix of another. + Consequently $x = x'$ and $y = y'$, and we have + $\alpha \subset \beta$ + $\implies$ + $x < y$ + $\implies$ + $x' < y'$ + $\implies$ + $\alpha \gamma \subset \beta \gamma$. + + \item[(2)] + Case $\alpha \sqsubset \beta$: + by definition this means that $\exists j \leq k$ such that $\rho_j > \rho'_j$ and $\rho_i = \rho'_i \;\forall i > j$. + We show that $\alpha \gamma \sqsubset \beta \gamma$. + % + \begin{itemize} + \item[(2a)] + Case $j < k$. In this case $\rho_k = \rho'_k$ + and appending $\gamma$ does not change relation on the last frame: + $\sigma_k = min (\rho_k, minh (\gamma)) = min (\rho'_k, minh (\gamma)) = \sigma'_k$. + Since $\sigma_i = \rho_i$ and $\sigma'_i = \rho'_i$ for all preceding frames $i < k$, + we have $\alpha \gamma \sqsubset \beta \gamma$. + + \item[(2b)] + Case $j = k$ and $minh (\gamma) > \rho'_k$. + In this case $\rho_k > \rho'_k$ + and again appending $\gamma$ does not change relation on the last frame: + $\sigma_k = min (\rho_k, minh (\gamma)) > \rho'_k$ and + $\sigma'_k = min (\rho'_k, minh (\gamma)) = \rho'_k$, therefore + $\sigma_k > \sigma'_k$. + Therefore $\alpha \gamma \sqsubset \beta \gamma$. + + \item[(2c)] + Case $j = k$ and $minh (\gamma) \leq \rho'_k$ + and $\exists l < k$ such that $\rho_l > \rho'_l$ and $\rho_i = \rho'_i$ for $l < i < k$. + %and $k > 1 \wedge \rho_{k-1} > \rho'_{k-1}$. + In this case $\gamma$ contains parentheses of low height + and appending it makes height on the last frame equal: + $\sigma_k = \sigma'_k = minh (\gamma)$. + However, the relation on the last preceding differing frame is the same: + $\sigma_l = \rho_l > \rho'_l = \sigma'_l$. + %However, this doesn't change comparison result because + %the relation on preceding frame is the same: $\sigma_{k-1} = \rho_{k-1} > \rho'_{k-1} = \sigma'_{k-1}$. + Therefore $\alpha \gamma \sqsubset \beta \gamma$. + + \item[(2d)] + Case $j = k$ %is $\rho_k > \rho'_k$ + and $minh (\gamma) \leq \rho'_k$ + and $\nexists l < k$ such that $\rho_l > \rho'_l$ and $\rho_i = \rho'_i$ for $l < i < k$. + %and $k = 1 \vee \rho_{k-1} \leq \rho'_{k-1}$. + In this case $\gamma$ contains parentheses of low height, + appending it makes height on the last frame equal: + $\sigma_k = \sigma'_k = minh (\gamma)$, + and this may change comparison result + as the relation on the last preceding differing frame may be different. + % +% In other words, the only possible case when $\gamma$ can change comparison result is +% when at the last frame we have $\rho_k > \rho'_k$, +% the appended suffix $\gamma$ contains parentheses with low height $minh (\gamma) \leq \rho'_k$ +% (so that $\sigma_k = \sigma'_k$), +% and the previous frame doesn't exist +% or compares differently from the last frame: $k = 1$ or $\rho_{k-1} \leq \rho'_{k-1}$. + We show that in this case the extended path $\pi_\beta \pi_\gamma$ contains a tagged $\epsilon$-loop. + % + Consider the fragments of paths $\pi_\alpha$ and $\pi_\beta$ from fork to join, + including (if it exists) the common $\epsilon$-transition to the fork state: + $\pi_\alpha'$ and $\pi_\beta'$. + %$\pi_\alpha' = q_2 \overset {u | \alpha'} {\rightsquigarrow} q_1$ and + %$\pi_\beta' = q_2 \overset {u | \beta'} {\rightsquigarrow} q_1$. + % + Minimal parenthesis height on $\pi_\alpha'$ is $\rho_k$. % $minh (\alpha') = \rho_k$. + By TNFA construction this means that $\pi_\alpha'$ is contained + in a sub-TNFA $f'$ for $e|_p$ at some position $p$ with length $|p| = \rho_k$. + % + As for $\pi_\beta'$, its start state coincides with $\pi_\alpha'$ and thus is in $f'$. + The minimal height of all but the last frames of $\pi_\beta'$ is at least $\rho_k$: + by conditions of (2d) either $k = 1$ and there are no such frames, + or $\rho'_{k-1} \geq \rho_{k-1}$ which implies $\rho'_{k-1} \geq \rho_k$ + (because by definition $\rho_k = min(\rho_{k-1}, minh(\alpha_k)) \leq \rho_{k-1}$). + On the last frame of $\pi_\beta'$ minimal height is $\rho'_k < \rho_k$. + Therefore all but the last frames of $\pi_\beta'$ are contained in $f'$, + but the the last frame is not. + % + Now consider $\pi_\gamma$: by conditions of (2d) its minimal height is less than $\rho_k$, + therefore it is not contained in $f'$, + % + but its start state is the join point of $\pi_\alpha'$ and $\pi_\beta'$ and thus in $f'$. + % + Taken together, above facts imply that the last frame of $\pi_\beta \pi_\gamma$ + starts in $f'$, then leaves $f'$, then returns to $f'$ and joins with $\pi_\alpha \pi_\gamma$, + and then leaves $f'$ second time. + Since the end state of $f'$ is unique (by TNFA construction), + $\pi_\beta \pi_\gamma$ must contain a tagged $\epsilon$-loop through it, + which contradicts lemma conditions. + \end{itemize} + \end{itemize} + % + (Note that in the presence of tagged $\epsilon$-loops right distributivity may not hold: + we may have paths $\pi_1$, $\pi_2$ and $\pi_3$ + such that $\pi_2$ and $\pi_3$ are two different $\epsilon$-loops through the same subautomaton + and $\pi_1 \pi_2 < \pi_1 \pi_3$, + in which case $\pi_1 \pi_2 \pi_3 < \pi_1 \pi_3$, + but $\pi_1 < \pi_1 \pi_2$ because the first is a proper prefix of the second.) + % +\end{proofEnd} \section{Tree representation of paths}\label{section_pathtree} @@ -1305,30 +1743,7 @@ This technique was used by many researches, e.g. Laurikari mentions a \emph{func and Karper describes it as the \emph{flyweight pattern} [Kar15]. \\ -A convenient represention of tag tree is an indexed sequence of nodes. -Each node is a triple $(p, s, t)$ where -$p$ is the index of predecessor node, -$s$ is a set of indices of successor nodes -and $t$ is a tag (positive or negative). -% -Forward links are only necessary if the advanced algorithm for $update \Xund ptables ()$ is used -(section \ref{section_comparison}), otherwise successor component can be omitted. -% -Now we can represent $u$-components of configurations with indices in the $U$-tree: -root index is $0$ (which corresponds to the empty path), -and each $u$-component is a tree index from which we can trace predecessors to the root -(function $unroll \Xund path ()$ demonstrates this). -% -In the implementation, it is important to use numeric indices rather than pointers -because it allows to use the ``two-fingers'' algorithm to find fork of two paths (section \ref{section_comparison}). -% -We assume the existence of functions -$pred(U, n)$ that returns $p$-component of $n$-th node, -$succ(U, n)$ that returns $s$-component of $n$-th node and -$tag(U, n)$ that returns $t$-component of $n$-th node. -\\ - -\begin{algorithm} \DontPrintSemicolon \SetKwProg{Fn}{}{}{} \SetAlgoInsideSkip{medskip} +\begin{algorithm}[H] \DontPrintSemicolon \SetKwProg{Fn}{}{}{} \SetAlgoInsideSkip{medskip} \begin{multicols}{2} \setstretch{0.8} @@ -1348,8 +1763,7 @@ $tag(U, n)$ that returns $t$-component of $n$-th node. \Return $n$ } } - - \vfill + \BlankLine \columnbreak @@ -1370,6 +1784,29 @@ $tag(U, n)$ that returns $t$-component of $n$-th node. \end{algorithm} \medskip +A convenient represention of tag tree is an indexed sequence of nodes. +Each node is a triple $(p, s, t)$ where +$p$ is the index of predecessor node, +$s$ is a set of indices of successor nodes +and $t$ is a tag (positive or negative). +% +Forward links are only necessary if the advanced algorithm for $update \Xund ptables ()$ is used +(section \ref{section_comparison}), otherwise successor component can be omitted. +% +Now we can represent $u$-components of configurations with indices in the $U$-tree: +root index is $0$ (which corresponds to the empty path), +and each $u$-component is a tree index from which we can trace predecessors to the root +(function $unroll \Xund path ()$ demonstrates this). +% +In the implementation, it is important to use numeric indices rather than pointers +because it allows to use the ``two-fingers'' algorithm to find fork of two paths (section \ref{section_comparison}). +% +We assume the existence of functions +$pred(U, n)$ that returns $p$-component of $n$-th node, +$succ(U, n)$ that returns $s$-component of $n$-th node and +$tag(U, n)$ that returns $t$-component of $n$-th node. +\\ + \section{Representation of match results}\label{section_results} @@ -1403,11 +1840,13 @@ but this is more complex and the partial trees may require even more space than \Return uninitialized array of pairs $(rm \Xund so, rm \Xund eo)$\; } \BlankLine + \BlankLine \Fn {$\underline{update \Xund result (T, X, U, k, \Xund)} \smallskip$} { \Return $\big\{ (q, o, u, apply (T, U, u, r, k)) \mid (q, o, u, r) \in X \big\}$ \; } \BlankLine + \BlankLine \Fn {$\underline{f\!inal \Xund result (T, U, u, r, k)} \smallskip$} { $pmatch = apply (T, U, u, r, k)$ \; @@ -1415,11 +1854,12 @@ but this is more complex and the partial trees may require even more space than \Return $pmatch$ \; } \BlankLine + \BlankLine \Fn {$\underline{apply (T, U, n, pmatch, k)} \smallskip$} { $done(\Xund) \equiv f\!alse$ \; \While {$n \neq 0$} { - $t = tag(U, n), \; s = sub(T, |t|), \; n = pred(U, n)$ \; + $t = tag(U, n) \; s = sub(T, |t|)$ \; \If {$t < 0 \wedge \big( s = 0 \vee \neg done(s) \big)$} { \For {$t' = \overline{low(T, |t|), upp(T, |t|)}$} { $s' = sub(T, t')$ \; @@ -1433,15 +1873,18 @@ but this is more complex and the partial trees may require even more space than $done(s) = true$ \; $set \Xund tag (pmatch, t, s, k)$ \; } + $n = pred(U, n)$ \; } \Return $pmatch$ \; } \BlankLine + \BlankLine \Fn {$\underline{set \Xund tag (pmatch, t, s, pos)} \smallskip$} { \lIf {$t \, mod \, 2 \equiv 1$} {$pmatch[s].rm \Xund so = pos$} \lElse {$pmatch[s].rm \Xund eo = pos$} } + \BlankLine \vfill @@ -1451,17 +1894,20 @@ but this is more complex and the partial trees may require even more space than \Return $\epsilon$ \; } \BlankLine + \BlankLine \Fn {$\underline{update \Xund result (\Xund, X, U, \Xund, \alpha)} \smallskip$} { \Return $\big\{ (q, o, u, r \cdot unroll \Xund path (U, u) \cdot \alpha)$ \; \Indp\Indp\Indp\Indp\Indp\Indp\Indp\Indp $\mid (q, o, u, r) \in X \big\}$ \; \Indm\Indm\Indm\Indm\Indm\Indm\Indm\Indm } \BlankLine + \BlankLine \Fn {$\underline{f\!inal \Xund result (\Xund, U, u, r, \Xund)} \smallskip$} { \Return $parse \Xund tree (r \cdot unroll \Xund path (U, u), 1)$ \; } \BlankLine + \BlankLine \Fn {$\underline{parse \Xund tree (u, i)} \smallskip$} { \If {$u = (2i \!-\! 1) \cdot (2i)$} { @@ -1846,7 +2292,6 @@ Below is the modified lazy version of $compare()$, the only part of the algorith \end{algorithm} \medskip - The problem with this approach is that we need to keep full-length history of each active path: at the point of ambiguity we may need to look an arbitrary number of steps back in order to find the fork of ambiguous paths. @@ -2122,7 +2567,7 @@ Our set of benchmarks consists of three subsets: (simplified parsers for IPv4 and date). \item Artificial benchmarks with high level of ambiguity. - All these REs are restricted to a single alphabet letter + All these REs are restricted to a single alphabet symbol used with various combinations of RE operators (union, product, iteration and bounded repetition). \item A series of pathological examples that demonstrates worst-case behaviour of naive $update \Xund ptables ()$ algorithm. @@ -2264,544 +2709,173 @@ instead of unrolling bounded repetition. \section*{Appendix} -\subsection{Correctness of $\epsilon$-closure construction} -\setcounter{XLem}{0} - -For a given RT $r$, -we say that PE $\alpha$ is \emph{minimal} if $\alpha = PE(t)$ for some minimal $t \in PT(r)$, -and we say that path $\pi$ in TNFA $F(r)$ is \emph{minimal} if $\pi$ induces a minimal PE. - -GOR1 correctness proof consists of two parts. -First, we get rid of $\epsilon$-loops by showing that, -on one hand, minmal paths do not contain $\epsilon$-loops, -and on the other hand, GOR1 cancels all paths which contain $\epsilon$-loops. -Second, for paths without $\epsilon$-loops we show right distributivity of path comparison over path concatenation. -The proofs make use of the TNFA nested structure -and the fact that each sub-TNFA is has a unique entry and exit states. -TNFA construct for all possible types of RT are shown on the fugure below. - - -\iffalse -\begin{figure}\label{fig_gor1} -\includegraphics[width=\linewidth]{img/gor1.pdf} -\caption{ -Sub-TNFA for individual sub-RT with submatch groups: \\ -(a) -- union, (b) -- product, (c), (d) -- bounded repetition, (e), (f) -- unbounded repetition. -} -\end{figure} -\fi - - \begin{XLem}\label{gor1_path_containment} - Let $r$ be a RE, $\pi = q_1 \overset {\alpha} {\rightsquigarrow} q_2$ a tagged path in TNFA $F(r)$, - where $\alpha \neq \epsilon$, - and $h = minh (\alpha)$ the minimal tag height on path $\pi$. - The following statements are true: - \begin{enumerate} - \item There is a position $p$ of length $|p| = h$ - such that $\pi$ fully lies inside of subautomaton $F(r|_p)$. - - \item There no position $p$ of length $|p| > h$ - such that $\pi$ fully lies inside of subautomaton $F(r|_p)$. - \end{enumerate} - Proof. - Obvious from TNFA construction. - $\square$ - \end{XLem} - - -\begin{XLem}\label{gor1_minpaths} -\lemmaclosureminpaths -\\[0.5em] - % Proof in terms of REs and correspondence between subexpression and loop - % is a bit hard because of unrolling of repetition in TNFA construction - % (there is no direct correspondence between sub-RE and sub-TNFA). - Proof. - Suppose, on the contrary, that $\pi$ is a minimal path in TNFA $F(r)$, and that $\pi$ contains at least one $\epsilon$-loop. - Consider the \emph{last} $\epsilon$-loop in $\pi$: - it can only come from sub-TNFA of the form $F\big( (i, \Xund, (i_1, \Xund, r_1)^{n,\infty}) \big)$ where $n \geq 0$, - as this is the only looping TNFA construct. - Let $w_n$ be the final state of sub-TNFA $F\big( (i_1, \Xund, r_1) \big)$ - as shown on figure \ref{fig_gor1} (e) -- (f). - Then $\pi$ can be represented as - $\pi = \pi_1 \pi_2 \pi_3$, where $\pi_2$ is the $\epsilon$-loop: - $\pi_1 = q_0 \overset {u | \alpha} {\rightsquigarrow} w_n$ and - $\pi_2 = w_n \overset {\epsilon | \beta} {\rightsquigarrow} w_n$ and - $\pi_3 = w_n \overset {v | \gamma} {\rightsquigarrow} q_f$. - Consider path $\pi' = \pi_1 \pi_3$ that is obtained from $\pi$ by removing $\pi_2$. - It consumes the same input string $uv$ as $\pi$, - therefore PE transduced by $\pi$ and $\pi'$ are comparable: $\alpha \beta \gamma, \alpha \gamma \in PE(r, uv)$. - Let $j$ be the total number of repetitions through $F\big( (i_1, \Xund, r_1) \big)$, - and let $i$ be the index of the $\epsilon$-loop repetition. - Consider two cases: - - \begin{enumerate}[itemsep=0.5em] - \item[(1)] - $i = j$. - In this case fork of $\alpha \beta \gamma$ and $\alpha \gamma$ happens immediately after $(i-1)$-th repetition: - % - \begin{alignat*}{10} - \alpha \beta \gamma &= x_0 \Xl_{h-1} \;&&\; \Xl_h x_1 \Xr_h \hdots \Xl_h x_{i-1} \Xr_h \;&&\big|\; \Xl_h x_{i} \Xr_h \;&&\; \Xr_{h-1} x_{j+1} \\[-0.5em] - \alpha \gamma &= x_0 \Xl_{h-1} \;&&\; \Xl_h x_1 \Xr_h \hdots \Xl_h x_{i-1} \Xr_h \;&&\big|\; \;&&\; \Xr_{h-1} x_{j+1} - \end{alignat*} - % - Since $x_i$ is an $\epsilon$-loop, it is contained in the fork frame of $\alpha \beta \gamma$. - We have $minh (\beta) = h$ and $minh (\gamma) \leq h - 1$, therefore $\rho_k = \rho'_k \leq h - 1$. - Subsequent frames $l > k$ (if any) are identical and thus $\rho_l = \rho'_l$. - Furthermore, $first (\gamma) = \Xr < \Xl = first (\beta)$. - Therefore $\alpha \beta \gamma \sim \alpha \gamma$ and $\alpha \gamma \subset \alpha \beta \gamma$. - - \item[(2)] - $i < j$. - In this case $(i + 1)$-th repetition cannot be an $\epsilon$-loop - (because we assumed that $i$-th repetition is the \emph{last} $\epsilon$-loop), - therefore - fork of $\alpha \beta \gamma$ and $\alpha \gamma$ happens - inside of $i$-th repetition of $\alpha \beta \gamma$ - and $(i + 1)$-th repetition of $\alpha \gamma$: - % - \begin{alignat*}{10} - \alpha \beta \gamma &= x_0 \Xl_{h-1} \;&&\; \Xl_h x_1 \Xr_h \hdots \Xl_h x_{i-1} \Xr_h \Xl_h y_1 \;&&\big|\; y_2 \Xr_h \Xl_h x_{i+1} && \Xr_h \Xl_h x_{i+2} \Xr_h \hdots \Xl_h x_j \Xr_h \;&&\; \Xr_{h-1} x_{j+1} \\[-0.5em] - \alpha \gamma &= x_0 \Xl_{h-1} \;&&\; \Xl_h x_1 \Xr_h \hdots \Xl_h x_{i-1} \Xr_h \Xl_h y_1 \;&&\big|\; y_3 && \Xr_h \Xl_h x_{i+2} \Xr_h \hdots \Xl_h x_j \Xr_h \;&&\; \Xr_{h-1} x_{j+1} - \end{alignat*} - % - Here $y_1 y_2 = x_i$ and $y_1 y_3 = x_{i+1}$ ($i$-th iteration is missing from $\alpha \gamma$). - Fragment $y_2$ is part of the $\epsilon$-loop, - therefore fork frame of $\alpha \beta \gamma$ contains parenthesis $\Xr_h$ and we have $\rho_k = h$. - On the other hand, $y_3$ contains alphabet symbols, - because $x_{i+1}$ is not an $\epsilon$-loop and $y_1$ is a part of the $\epsilon$-loop. - Therefore fork frame of $\alpha \gamma$ ends in $y_3$ and we have $\rho'_k > h$. - % - %In this case - %fork frame of $\alpha \beta \gamma$ contains $y_2 \Xr_h \Xl_h$ fragment, because $y_2$ is part of the $\epsilon$-loop. - %But the fork frame of $\alpha \gamma$ ends inside of $y_3$, because $(i+1)$-th repetiton is not an $\epsilon$-loop and must contain alphabet symbols. - %Therefore at the fork frame $k$ we have $\rho_k = h$ and $\rho'_k > h$. - % - All subsequent frames $l > k$ are identical: - if they contain parentheses of height less than $h$, then $\rho_l = \rho'_l < h$; - otherwise $\rho_l \leq h$ and $\rho'_l > h$. - Therefore $\alpha \gamma \sqsubset \alpha \beta \gamma$. - - \end{enumerate} - - In both cases $\alpha \gamma < \alpha \beta \gamma$, - which contradicts the fact that $\pi$ is a minimal path. - $\square$ - -\end{XLem} - - -\iffalse - \begin{XLem}\label{gor1_loops} - GOR1 discards paths with tagged $\epsilon$-loops. - \\ - Proof. - - GOR1 finds non-looping paths before their looping counterparts, - as it uses depth-first search to explore new paths and prunes ambiguous paths - immediately after exploring transitions to the join state. - So for each TNFA state, the first path to be found is a path without $\epsilon$-loops. - We will show that once GOR1 has found a path without $\epsilon$-loops, - it will never prefer a path with an $\epsilon$-loop - (though of course it might prefer some other path without $\epsilon$-loops). - - The only TNFA construct that has a loop is unbounded repetition - $F\big( (i, \Xund, (i_1, \Xund, r_1)^{n,\infty}) \big)$ where $n \geq 0$, - shown on figure \ref{fig_gor1} (e) -- (f). - Consider arbitrary path $\pi$ that contains - $\epsilon$-loop through sub-TNFA $F\big( (i_1, \Xund, r_1) \big)$. - % - Let $q_1$ be the first state on $\pi$ that belongs to the $\epsilon$-loop. +\subsection*{Proof of theorem \ref{theorem_porder_on_PTs}} + +\begin{theoremEnd}[normal, no link to proof, no link to theorem]{lemma} +[Unique position mapping from all PTs to IRE] + \label{lemma_positions} + If $t, s \in PT(e)$ for some RE $e$ + and there is a common position $p \in Pos(t) \cap Pos(s)$, + then $p$ corresponds to the same position $p' \in Pos(\IRE(e))$ for both $t$ and $s$. +\end{theoremEnd} +\begin{proofEnd} + The proof is by induction on the length of $p$. + Let $r = \IRE(e)$. + Induction basis: $p = p' = \Lambda$ (the roots of $t$ and $s$ correspond to the root of $e$). + Induction step: suppose that for any position $p$ of length $|p| < h$ the lemma is true. + We will show that if exists $k \in \YN$ such that $p.k \in Pos(t) \cap Pos(s)$, + then $p.k$ corresponds to the same position $p'.k'$ in $r$ for both $t$ and $s$ (for some $k' \in \YN$). + If $r|_{p'}$ is an elementary IRE of the form $(i, j, \epsilon)$ or $(i, j, \alpha)$, + or if at least one of $t|_p$ and $s|_p$ is $\varnothing$, + then $k$ doesn't exist. + Otherwise $r|_{p'}$ is a compound IRE and both $t|_p$ and $s|_p$ are not $\varnothing$. + If $r|_{p'}$ is a union $(i, j, (i_1, j_1, r_1)|(i_2, r_2, j_2))$ + or a product $(i, j, (i_1, j_1, r_1)\cdot(i_2, r_2, j_2))$, + then both $t|_p$ and $s|_p$ have exactly two subtrees, + and positions $p.1$ and $p.2$ in $t$ and $s$ correspond to positions $p'.1$ and $p'.2$ in $r$. + Otherwise, $r|_{p'}$ is a repetition $(i, j, r_1^{n,m})$ + and for any $k \geq 1$ position $p.k$ in $t$ and $s$ corresponds to position $p'.1$ in $r$. +\end{proofEnd} + +\printProofs[theorem_porder_on_PTs] + + +\subsection*{Proof of theorem \ref{theorem_sorder_on_PTs}} + +\begin{theoremEnd}[normal, no link to proof, no link to theorem]{lemma} + \label{lemma_incomparability_equivdef} + If $t, s \in PT(e, w)$ for some RE $e$ and string $w$, + then $t \sim s \Leftrightarrow \; \forall p : \snorm{t}{p} = \snorm{s}{p}$. +\end{theoremEnd} +\begin{proofEnd} + Forward implication: let $t \sim s$ and suppose, on the contrary, that $\exists p = min \{ q \mid \snorm{t}{q} \neq \snorm{s}{q} \}$, + then either $t \prec_p s$ (if $\snorm{t}{p} > \snorm{s}{p}$) or $s \prec_p t$ (if $\snorm{t}{p} < \snorm{s}{p}$), + both cases contradict $t \sim s$. % - Path $\pi$ can be represented as $\pi = \pi_1 \pi_2 \pi_3$, where - $\pi_1 = q_0 \overset {u | \alpha} {\rightsquigarrow} q_1$ and - $\pi_2 = q_1 \overset {\epsilon | \beta} {\rightsquigarrow} q_1$ and - $\pi_3 = q_1 \overset {v | \gamma} {\rightsquigarrow} q_f$. - % - By the time GOR1 finds path $\pi_1 \pi_2$, - it must have already found some other path $\pi'_1 = q_0 \overset {u | \alpha'} {\rightsquigarrow} q_1$ without $\epsilon$-loops. - There are two possible cases: either $\alpha' = \alpha$, or $\alpha' < \alpha$. - We will show that in both cases $\alpha' < \alpha \gamma$ - and consequently, GOR1 prefers the path without the $\epsilon$-loop. - Let $k$ be the index of the last frame - and $\big( (\rho_1, \hdots, \rho_k), (\rho'_1, \hdots, \rho'_k) \big) = traces (\alpha', \alpha \gamma)$. - - First case: $\alpha' = \alpha$. - Because $\alpha$ is a proper prefix of $\alpha \gamma$, - fork happens at the last frame and we have - $\rho_k = lasth(\alpha)$ and - $\rho'_k = min (lasth(\alpha), minh(\gamma))$. - If $lasth(\alpha) > minh(\gamma)$, then $\rho_k > \rho'_k$ and $\alpha \sqsubset \alpha \gamma$. - Otherwise $\rho_k = \rho'_k$ and $\alpha \sim \alpha \gamma$, - and we have $first(\alpha \backslash \alpha \gamma) = \bot$ and $first(\alpha \gamma \backslash \alpha) \neq \bot$, - therefore $\alpha \subset \alpha \gamma$. - In both cases $\alpha < \alpha \gamma$. - - Second case: $\alpha' < \alpha$. - Let $\big( (\sigma_1, \hdots, \sigma_k), (\sigma'_1, \hdots, \sigma'_k) \big) = traces (\alpha', \alpha)$. - We have $\rho_k = \sigma_k$ and $\rho'_k = min (\sigma'_k, minh(\gamma)) \leq \sigma_k$. - If $minh(\gamma) < \sigma'_k$ then $\rho_k > \rho'_k$ and $\alpha' \sqsubset \alpha \gamma$. - Otherwise $\rho'_k = \sigma'_k$. - If $\alpha' \sqsubset \alpha$ then $\alpha' \sqsubset \alpha \gamma$. - Otherwise $\alpha' \sim \alpha$ and $\alpha' \subset \alpha$. - None of $\alpha$ and $\alpha'$ is a proper prefix of the other, - because otherwise the longer path has an $\epsilon$-loop through $q_1$, which contradicts our assumption about $\pi_1$ and $\pi'_1$. - Therefore $first (\alpha' \backslash \alpha) = first (\alpha' \backslash \alpha \gamma)$ - and $first (\alpha \backslash \alpha') = first (\alpha \gamma \backslash \alpha')$. - Consequently $\alpha' \subset \alpha \implies \alpha' \subset \alpha \gamma$. - Thus $\alpha' < \alpha \gamma$. - $\square$ - \end{XLem} -\fi - + Backward implication: $\forall p : \snorm{t}{p} = \snorm{s}{p}$ + implies $\nexists p : t \prec_p s$ and $\nexists q : s \prec_q t$, + which implies $t \sim s$. + \\[0.5em] +\end{proofEnd} +\printProofs[theorem_sorder_on_PTs] - \begin{XLem} - \lemmaclosurerightdist - \\[0.5em] - Proof. - Let $k = |u|$ be the number of frames in $\alpha$ and $\beta$. - Let - $\big( (\rho_1, \hdots, \rho_k),$ $(\rho'_1, \hdots, \rho'_k) \big) = traces (\alpha, \beta)$ and - $\big( (\sigma_1, \hdots, \sigma_k),$ $(\sigma'_1, \hdots, \sigma'_k) \big) = traces (\alpha \gamma, \beta \gamma)$. - Obviously for frames $i < k$ we have $\rho_i = \sigma_i$ and $\rho'_i = \sigma'_i$, - and for the last frame $k$ we have - $\sigma_k = min (\rho_k, minh (\gamma))$ and - $\sigma'_k = min (\rho'_k, minh (\gamma))$. - Consider two possible cases. +\subsection*{Proof of Theorem \ref{theorem_order_compat}} - First case: $\alpha \sim \beta \wedge \alpha \subset \beta$. - % - We show that $\alpha \gamma \sim \beta \gamma \wedge \alpha \gamma \subset \beta \gamma$. - % - We have $\rho_i = \rho'_i \; \forall i$, therefore - $\sigma_i = \sigma'_i \; \forall i$ and consequently $\alpha \gamma \sim \beta \gamma$. - Let - $x = first (\alpha \backslash \beta)$, - $y = first (\beta \backslash \alpha)$, - $x' = first (\alpha \backslash \beta \gamma)$ and - $y' = first (\beta \backslash \alpha \gamma)$. - None of $\pi_\alpha$ and $\pi_\beta$ is a proper prefix of another, - otherwise the longer path must contain $\epsilon$-loop through $q_1$ - (because $\alpha$ and $\beta$ have the same number of frames). - Consequently $x = x'$ and $y = y'$, and we have - $\alpha \subset \beta$ - $\implies$ - $x < y$ - $\implies$ - $x' < y'$ - $\implies$ - $\alpha \gamma \subset \beta \gamma$. - - Second case: $\alpha \sqsubset \beta$. - We show that $\alpha \gamma \sqsubset \beta \gamma$. +\begin{theoremEnd}[normal, no link to proof, no link to theorem]{lemma} +[Comparability of subtrees] + \label{lemma_subtrees} + For a giver RE $e$, string $w$ and position $p$, + if $t, s \in \PT(e, w)$, $p \in Sub(t) \cup Sub(s)$ and $\snorm{t}{q} = \snorm{s}{q} \; \forall q \leq p$, + then $\exists e', w' : t|_p, s|_p \in \PT(e', w')$. +\end{theoremEnd} +\begin{proofEnd} + By induction on the length of $p$. + Induction basis: $p = \Lambda$, let $e' = e$ and $w' = w$. % - If $\rho_k = \rho'_k$ then $\sigma_k = \sigma'_k$ - and obviously $\alpha \gamma \sqsubset \beta \gamma$. - Else it must be $\rho_k > \rho'_k$. - In this case, if $minh (\gamma) > \rho'_k$, then $\sigma_k > \sigma'_k$ and again $\alpha \gamma \sqsubset \beta \gamma$. - Else $minh (\gamma) \leq \rho'_k$ and $\sigma_k = \sigma'_k$. - In this case, if $k > 1$ and $\rho_{k-1} > \rho'_{k-1}$ then again $\alpha \gamma \sqsubset \beta \gamma$. + Induction step: suppose that the lemma is true for any position $p$ of length + $|p| < h$, we will show that it is true for any position $p.k$ of length $h$ + ($k \in \YN$). % - In other words, the only possible case when $\gamma$ can change comparison result is - when at the last frame we have $\rho_k > \rho'_k$, - the appended suffix $\gamma$ contains parentheses with low height $minh (\gamma) \leq \rho'_k$ - (so that $\sigma_k = \sigma'_k$), - and the previous frame doesn't exist - or compares differently from the last frame: $k = 1$ or $\rho_{k-1} \leq \rho'_{k-1}$. - We show that in this case the extended path $\pi_\beta \pi_\gamma$ must contain $\epsilon$-loop, - which contradicts to the lemma condiitons. - - Consider the fragments of paths $\pi_\alpha$ and $\pi_\beta$ from fork to join, - including (if it exists) the $\epsilon$-transition to the fork state: - $\pi_\alpha' = q_2 \overset {u | \alpha'} {\rightsquigarrow} q_1$ and - $\pi_\beta' = q_2 \overset {u | \beta'} {\rightsquigarrow} q_1$. - We know that $minh (\alpha') = \rho_k$. -% (because $\rho_k$ is set to the minimal parenthesis height on the path from fork to join). - Therefore by lemma \ref{gor1_path_containment} - we know that $\pi_\alpha'$ is contained in a subautomaton $f$ of height $\rho_k$. - Likewise we know that $\pi_\beta'$ is not contained in $f$, because $minh (\beta') = \rho'_k < \rho_k$. + Assume that $p.k \in Sub(t) \cap Sub(s)$ + (otherwise either $p.k \not\in Sub(t) \cup Sub(s)$, + or exactly one of $\snorm{t}{p.k}$, $\snorm{s}{p.k}$ is $\infty$ --- in both + cases lemma conditions are not satisfied). + Then both $t|_p$ and $s|_p$ have at least one subtree: let + $t|_{p} = T(t_1, \dots, t_n)$ and + $s|_{p} = T(s_1, \dots, s_m)$, where $n, m \geq k$. % - Let $\pi_\beta''$ be the part of $\pi_\beta'$ containing the last $k$-th frame, - and note the following: - \begin{enumerate} - \item[(a)] the start state of $\pi_\beta''$ must be contained in $f$ - (because by our assumption - either $k = 1$ and then start state of $\pi_\beta''$ is the fork state, - or $\rho_{k-1} \leq \rho'_{k-1}$ which implies $\rho'_{k-1} \geq \rho_k$ - and then all but the last frames of $\pi_\beta'$ must be contained in $f$) - \item[(b)] $\pi$ cannot be contained in $f$ - (because by our assumption $\rho_k > \rho'_k$) - \item[(c)] the end state of $\pi_\beta''$ is contained in $f$ - (because it's the join state $q_1$ of $\pi_\alpha'$ and $\pi_\beta'$) - \item[(d)] $\pi_\gamma$ is not contained in $f$ - (because by our assumption $minh (\gamma) \leq \rho'_k$ and consequently $minh (\gamma) < \rho_k$) - \end{enumerate} + By induction hypothesis $\exists e', w' : t|_p, s|_p \in \PT(e', w')$. + We have $w' = str(t_1) \dots str(t_n) = str(s_1) \dots str(s_m)$. % - Put together, items (a) - (d) mean that the $\epsilon$-path $\pi_\beta'' \pi_\gamma$ - first leaves subautomaton $f$, then re-enters $f$, and then leaves $f$ second time. - Because $f$ has a unique exit state, this means that $\pi_\beta'' \pi_\gamma$ contains $\epsilon$-loop - through the exit state of $f$, which contradicts lemma conditions. - (Effectively it means that $\pi_\beta \pi_\gamma$ is non-minimal and would be discarded by GOR1 anyway.) -% Note that $\pi_\beta'$ itself does not necessarily contain $\epsilon$-loop. + We show that $str(t_k) = str(s_k)$. + Consider positions $p.j$ for $j \leq k$. + By defintion the set of submatch positions contains siblings, + therefore $p.j \in Sub(t) \cap Sub(s)$. + By lemma conditions $\snorm{t}{p.j} = \snorm{s}{p.j}$ (because $p.j \leq p.k$), + therefore $|str(t_1) \dots str(t_{k-1})|$ + $= \sum\nolimits_{j=1}^{k-1}\snorm{t}{j}$ + $= \sum\nolimits_{j=1}^{k-1}\snorm{s}{j}$ + $= |str(s_1) \dots str(s_{k-1})|$ and + $|str(t_k)| = |str(s_k)|$. + Consequently, $str(t_k)$ and $str(s_k)$ start and end at the same character in $w'$ and therefore are equal. % - $\square$ - \end{XLem} - -\subsection*{Proof of Theorem \ref{theorem_order_on_IPTs}} - - \begin{XLem}\label{lemma_ptorder_antisymmetry} - The order on IPTs is antisymmetric: if $t < s$, then $s \not< t$. - \\ - Proof. - - Suppose, on the contrary, that $t <_p s$ and $s <_q t$ for some $p$, $q$. - Without loss of generality let $p \leq q$. - On one hand $t <_p s$ implies $\|t\|_p > \|s\|_p$. - On the other hand $s <_q t$ implies $\|t\|_p \leq \|s\|_p$. - Contradicting the assumption. - $\square$ - \end{XLem} - - \begin{XLem}\label{lemma_ptorder_transitivity} - The order on IPTs is transitive: if $t < s$ and $s < u$, then $t < u$. - \\ - Proof. - - Let $t <_p s$ and $s <_q u$ for some positions $p$, $q$, and let $r = min (p, q)$. - \\[-1em] - - First, we show that $\|t\|_r > \|u\|_r$. - If $p \leq q$, we have $\|t\|_p > \|s\|_p$ (implied by $t <_p s$) - and $\|s\|_p \geq \|u\|_p$ (implied by conjunction $s <_q u \wedge p \leq q$), - therefore $\|t\|_p > \|u\|_p$. - Otherwise $p > q$, we have $\|s\|_q > \|u\|_q$ (implied by $s <_q u$) - and $\|t\|_q = \|s\|_q$ (implied by conjunction $t <_p s \wedge q < p$), - therefore $\|t\|_q > \|u\|_q$. - \\[-1em] - - Second, we show that $\forall r' < r$ it holds that $\|t\|_{r'} = \|u\|_{r'}$. - We have $\|t\|_{r'} = \|s\|_{r'}$ (implied by conjunction $t <_p s \wedge r' < p$) - and $\|s\|_{r'} = \|u\|_{r'}$ (implied by conjunction $s <_q u \wedge r' < q$), - therefore $\|t\|_{r'} = \|u\|_{r'}$. - $\square$ - \end{XLem} - - \begin{XLem}\label{incomparability_equivdef} - $t \sim s \Leftrightarrow \; \forall p : \|t\|_p = \|s\|_p$. - \\ - Proof. - - $\Rightarrow$. %First, we show $t \sim s \Rightarrow \forall p : \|t\|_p = \|s\|_p$. - Suppose, on the contrary, that $\exists p = min \{ q \mid \|t\|_q \neq \|s\|_q \}$, - then either $t <_p s$ (if $\|t\|_p > \|s\|_p$), or $s <_p t$ (if $\|t\|_p < \|s\|_p$). - Both cases contradict $t \sim s$. - \\[-1em] + Finally, have $t|_{p.k}, s|_{p.k} \in PT(r|_{p.k}, str(t_k))$ and induction step is complete. +\end{proofEnd} - $\Leftarrow$. - $\forall p : \|t\|_p = \|s\|_p$ implies - $\nexists p : t <_p s$ and $\nexists q : s <_q t$, - which implies $t \sim s$. - $\square$ - \end{XLem} - - \begin{XLem}\label{lemma_ptorder_transitivity_of_incomparability} - Incomparability relation on parse trees is transitive: if $t \sim s$ and $s \sim u$, then $t \sim u$. - \\ - Proof. - - By lemma \ref{incomparability_equivdef} we have - $t \sim s \Rightarrow \forall p : \|t\|_p = \|s\|_p$ and - $s \sim u \Rightarrow \forall p : \|s\|_p = \|u\|_p$, - therefore by lemma \ref{incomparability_equivdef} $\forall p : \|t\|_p = \|u\|_p \Rightarrow t \sim u$. - $\square$ - \end{XLem} +\printProofs[theorem_order_compat] -The proof of theorem \ref{theorem_order_on_IPTs} -follows from -the lemma \ref{lemma_ptorder_antisymmetry}, -the lemma \ref{lemma_ptorder_transitivity} and -the lemma \ref{lemma_ptorder_transitivity_of_incomparability}. - - -\subsection*{Proof of Theorem \ref{theorem_order_compat}} -First, we prove an auxilary lemma \ref{lemma_subtrees} which -shows that comparison of sub-IPT is justified -if the s-norms at all preceding submatch positions are equal. - - \begin{XLem}\label{lemma_subtrees} - If $t, s \in \IPT(r, w)$ and $\exists p \in Sub(t) \cup Sub(s)$ such that $\snorm{t}{q} = \snorm{s}{q} \; \forall q \leq p$, - then $\exists \widetilde{r}, \widetilde{w} : t|_p, s|_p \in \IPT(\widetilde{r}, \widetilde{w})$. - \\ - Proof. - By induction on position $p$. - \\[-1em] - - Induction basis: the case of $p = \Lambda$ is trivial: let $\widetilde{r} = r$, $\widetilde{w} = w$. - \\[-1em] - - Induction step: we have $|p| > 0$, let $p = p'.i$, where $i \in \YN$. - Let $t' = t|_{p'} = T(t_1, \dots, t_n)$, - $s' = s|_{p'} = T(s_1, \dots, s_m)$. - By induction hypothesis $\exists r', w' : t', s' \in \IPT(r', w')$, - where $w' = str(t_1) \dots str(t_n) = str(s_1) \dots str(s_m)$. - \\[-1em] - - Next, we show that $str(t_i) = str(s_i)$. - It must be that $i \in Sub(s') \cap Sub(t')$, - otherwise only one of $\|t'\|_i$, $\|s'\|_i$ is $\infty$, - which contradicts lemma condiiton $\|t\|_p = \|s\|_p$. - Consider position $j \leq i$. - Because the set of submatch positions contains siblings, we have $j \in Sub(s') \cap Sub(t')$. - Consequently, $\|t'\|_j = |str(t_j)|$ and $\|s\|_j = |str(s_j)|$. - By lemma condition we have $\|t\|_{p'.j} = \|s\|_{p'.j}$, - therefore $\|t'\|_j = \|s'\|_j$, - therefore $|str(t_j)| = |str(s_j)|$. - Because $str(t_1) \dots str(t_n) = str(s_1) \dots str(s_m)$, - we have $str(t_i) = str(s_i)$. - \\[-1em] - - Now, let $\widetilde{w} = str(t_i)$. - If $r' = r_1|r_2$ or $r' = r_1 r_2$, let $\widetilde{r} = r_i$. - Otherwise, $r' = r_1^{k,l}$, let $\widetilde{r} = r_1$. - $\square$ - \end{XLem} - - - Proof of theorem \ref{theorem_order_compat}. - \\[-1em] +\subsection*{Proof of Theorem \ref{theorem_order_on_pe_same_as_on_pt}} - Consider any $t \in T_{min}$. - For each position $p \in Sub(t)$, which is not itself a prefix of another position in $Sub(t)$, - consider subtree $t' = t|_p$. - It is an IPT for some sub-IRE $r'$ and substring $w'$: $t' \in \IPT(r', w')$. - Let $t''$ be the $<$-minimal tree in $\IPT(r', w')$ and substitute $t'$ with $t''$ in $t$. - (Note that substitutions are independent and can be performed in any order.) - Let $u$ be the tree resulting from all such substitutions. - By lemma \ref{incomparability_equivdef} we have $u \sim t$ - (because substitutions preserve the s-norm of subtrees at positions in $Sub(t)$), - and so $u \in T_{min}$. - We will show that $u = t_{min}$. - \\[-1em] - - Suppose, on the contrary, that $u \neq t_{min}$. - % - Then we have $t_{min} <_p u$ for some non-submatch decision position $p$. - Let $p = p'.p''$, where $p'$ is the longest prefix of $p$ that is a submatch position: $p' \in Sub(u) \cup Sub(t_{min})$. - \\[-1em] - - It must be that for all submatch positions $q' < p'$ we have $\snorm{u}{q'} = \snorm{t_{min}}{q'}$, - because $u \in T_{min}$ and thus either $u \sim t_{min}$, - or $u \prec_q t_{min}$ for some $q \in Sub(u) \cup Sub(t_{min})$ - (in which case it must be $q > p$, because $u \prec_q t_{min}$ implies $\snorm{u}{q} > \snorm{t_{min}}{q}$, - which in turn implies $\pnorm{u}{q} > \pnorm{t_{min}}{q}$, - which contradicts $t_{min} <_p u$ if $q \leq p$). - \\[-1em] - - Therefore by lemma \ref{lemma_subtrees} we have $\exists r', w' : u|_{p'}, t_{min}|_{p'} \in \IPT(r', w')$. - On one hand, $t_{min} <_{p'.p''} u$ implies $t_{min}|_{p'} <_{p''} u|_{p'}$. - But on the other hand, $p' \in Sub(u)$ and $p'$ is not itself a prefix of another position in $Sub(u)$, - therefore $u|_{p'}$ is $<$-minimal by construction of $u$. - Contradiction. -% +%\begin{theoremEnd}[normal, no link to proof, no link to theorem]{lemma} +% \label{lemma_pe_order_antisymm} +% The longest-leftmost-precedence relation $<$ is antisymmetric: +% if $\alpha < \beta$, then $\beta \not< \alpha$. +%\end{theoremEnd} +%\begin{proofEnd} +% Suppose, on the contrary, that $\alpha < \beta$ and $\beta < \alpha$. +% Let $\big( (\rho_0, \dots, \rho_n), (\rho'_0, \dots, \rho'_n) \big) = traces(\alpha, \beta)$. % % -% On one hand, $u <_q \widetilde{s}$ for some submatch position $q$ (because $u \in P_{min}$). -% On the other hand, $s \lessdot_p \widetilde{u}$ for some non-submatch position $p < q$ (because $s$ is $\lessdot$-minimal). +% If $\exists i = max \{j \mid \rho_j \neq \rho'_j \}$, then +% $\alpha < \beta \implies \alpha \sqsubset \beta \implies \rho_i > \rho'_i$, but +% $\beta < \alpha \implies \beta \sqsubset \alpha \implies \rho'_i > \rho_i$. Contradiction. % % -% Let $p = p'.p''$, where $p'$ is the longest prefix of $p$ in $Sub(\widetilde{s}) \cup Sub(u)$. -% It must be $\|u\|_{q'} = \|\widetilde{s}\|_{q'} \forall q' \leq p'$ (because $p' < q$ and $u <_q \widetilde{s}$), -% and $p' \in Sub(u)$ (otherwise $\|u\|_{p'} = \infty \neq \|\widetilde{s}\|_{p'}$). -% % -% Now, by lemma \ref{lemma_subtrees} we have $\exists r', w' : u|_{p'}, \widetilde{s}|_{p'} \in PT(r', w')$, -% therefore $s \lessdot_{p'.p''} u$ implies $s|_{p'} \lessdot_{p''} \widetilde{u}|_{p'}$. -% But $p' \in Sub(u)$ and $p'$ is not itself a prefix of another position in $Sub(u)$, -% therefore $\widetilde{u}|_{p'}$ is $\lessdot$-minimal by construction of $u$. -% Contradiction. - $\square$ - - -\subsection*{Proof of Theorem \ref{theorem_order_on_pe_same_as_on_pt}} - - \begin{XLem}\label{lemma_pe_order_antisymm} - The longest-leftmost-precedence relation $<$ is antisymmetric: - if $\alpha < \beta$, then $\beta \not< \alpha$. - \\ - Proof. - Suppose, on the contrary, that $\alpha < \beta$ and $\beta < \alpha$. - Let $\big( (\rho_0, \dots, \rho_n), (\rho'_0, \dots, \rho'_n) \big) = traces(\alpha, \beta)$. - - \medskip - - If $\exists i = max \{j \mid \rho_j \neq \rho'_j \}$, then - $\alpha < \beta \implies \alpha \sqsubset \beta \implies \rho_i > \rho'_i$, but - $\beta < \alpha \implies \beta \sqsubset \alpha \implies \rho'_i > \rho_i$. Contradiction. - - \medskip - - Otherwise $\rho_i = \rho'_i \; \forall i$, then - $\alpha < \beta \implies \alpha \sim \beta \wedge \alpha \subset \beta$ and - $\beta < \alpha \implies \beta \sim \alpha \wedge \beta \subset \alpha$. - Let - $x = first (\alpha \backslash \beta)$, - $y = first (\beta \backslash \alpha)$, then - $\alpha \subset \beta \implies x < y$, but - $\beta \subset \alpha \implies y < x$. Contradiction. - $\square$ - \end{XLem} - - - \begin{XLem}\label{lemma_pe_equiv} - Let $s, t \in PT(r, w)$. +% Otherwise $\rho_i = \rho'_i \; \forall i$, then +% $\alpha < \beta \implies \alpha \sim \beta \wedge \alpha \subset \beta$ and +% $\beta < \alpha \implies \beta \sim \alpha \wedge \beta \subset \alpha$. +% Let +% $x = first (\alpha \backslash \beta)$, +% $y = first (\beta \backslash \alpha)$, then +% $\alpha \subset \beta \implies x < y$, but +% $\beta \subset \alpha \implies y < x$. Contradiction. +%\end{proofEnd} + +\begin{theoremEnd}[normal, no link to proof, no link to theorem]{lemma} + \label{lemma_pe_equiv} + Let $s, t \in PT(e, w)$ for some RE $e$ and string $w$. If $s \sim t$, then $\Phi_{h}(s) = \Phi_{h}(t) \; \forall h$. - \\ - Proof. - By induction on the height of $r$. - - \medskip - - Induction basis. - For RT of height $1$ we have - $| PT(r, w) | \leq 1 \; \forall w$, +\end{theoremEnd} +\begin{proofEnd} + By induction on the height of $e$. + % + Induction basis: or height $1$ we have + $| PT(e, w) | \leq 1 \; \forall w$, therefore $s = t$ and $\Phi_{h}(s) = \Phi_{h}(t)$. - - \medskip - - Induction step. - We have + % + Induction step: + height is greater than 1, therefore $s = T^{d} (s_1, \dots, s_n)$ and $t = T^{d} (t_1, \dots, t_m)$. If $d = 0$, then $\Phi_{h}(s) = str(s) = w = str(t) = \Phi_{h}(t)$. Otherwise $d \neq 0$. - By lemma \ref{incomparability_equivdef} we have $s \sim t \Rightarrow \forall p: \|s\|_p = \|t\|_p$. + By lemma \ref{lemma_incomparability_equivdef} we have $s \sim t \Rightarrow \snorm{s}{p} = \snorm{t}{p} \;\forall p$. This implies $n = m$ (otherwise the norm of subtree at position $min(n,m)+1$ is $\infty$ for only one of $s$, $t$). Therefore $\Phi_{h}(s) = \Xl_{h+1} \Phi_{h+1}(s_1), \dots, \Phi_{h+1}(s_n) \Xr_h$ and $\Phi_{h}(t) = \Xl_{h+1} \Phi_{h+1}(t_1), \dots, \Phi_{h+1}(t_n) \Xr_h$. -% Consider any $i \leq n$. It suffices to show that $\forall i \leq n: \Phi_{h+1}(s_i) = \Phi_{h+1}(t_i)$. - We have $\forall p: \|s_i\|_p = \|t_i\|_p$ (implied by $\forall p: \|s\|_p = \|t\|_p$), - therefore by lemma \ref{incomparability_equivdef} we have $s_i \sim t_i$, - and by lemma \ref{lemma_subtrees} $\exists r', w': s_i, t_i \in PT(r', w')$, - where the height of $r'$ is less than the height of $r$. + We have $\snorm{s_i}{p} = \snorm{t_i}{p} \;\forall p$ (implied by $\snorm{s}{p} = \snorm{t}{p} \;\forall p$), + therefore by lemma \ref{lemma_incomparability_equivdef} $s_i \sim t_i$, + and by lemma \ref{lemma_subtrees} $\exists e', w': s_i, t_i \in PT(e', w')$, + where the height of $e'$ is less than the height of $e$. By induction hypothesis $\Phi_{h+1}(s_i) = \Phi_{h+1}(t_i)$. - $\square$ - \end{XLem} - - - \begin{XLem}\label{lemma_pe_less_1} - Let $s, t \in PT(r, w)$. - If $s <_p t$ and $|p| = 1$, then $\Phi_{h}(s) < \Phi_{h}(t) \; \forall h$. - \\ - Proof. - - By lemma conditions $|p| = 1$, which implies that $s$ and $t$ are compound PT - $s = T^{d} (s_1, \dots, s_n)$ and - $t = T^{d} (t_1, \dots, t_m)$, where - $d \neq 0$ - (because $\Lambda$ is a prefix of decision position $p$). - Therefore $\Phi_{h}(s)$, $\Phi_{h}(t)$ can be represented as follows, - where $k$ is the number of frames and $j$ is the fork: +\end{proofEnd} + +\begin{theoremEnd}[normal, no link to proof, no link to theorem]{lemma} + \label{lemma_pe_less_1} + Let $s, t \in PT(e, w)$. + If $s \prec_p t$ and $|p| = 1$, then $\Phi_{h}(s) < \Phi_{h}(t) \; \forall h$. +\end{theoremEnd} +\begin{proofEnd} + By lemma conditions $|p| = 1$, therefore $p \in \YN$. + At least one of $s|_p$ and $t|_p$ must exist (otherwise $\snorm{s}{p} = \infty = \snorm{t}{p}$ which contradicts $s \prec_p t$), + therefore $e$ is a compound RE and $s$, $t$ can be represented as + $s = T^{d} (s_1, \dots, s_n)$ and + $t = T^{d} (t_1, \dots, t_m)$ + where $d \neq 0$ because $\Lambda$ is a prefix of decision position $p$. + Let $k$ be the number of frames and let $j$ be the fork, then: \begin{alignat*}{7} \Phi_{h}(s) &\;=\; \Xl_{h+1} &&\Phi_{h+1}(s_1) &&\dots &&\Phi_{h+1}(s_n) \Xr_h &&\;=\; \beta_0 a_1 \dots a_j \beta_j &&\;\big|\; && \gamma_j a_{j + 1} \dots a_k \gamma_k \\[-0.5em] @@ -2809,132 +2883,132 @@ if the s-norms at all preceding submatch positions are equal. &&\;=\; \beta_0 a_1 \dots a_j \beta_j &&\;\big|\; && \delta_j a_{j + 1} \dots a_k \delta_k \end{alignat*} % - By lemma conditions $|p| = 1$, therefore $p \in \YN$. - Consider any $i \in \YN$ such that $i < p$. - By lemma conditions $s <_p t$, which means - $\|s\|_p > \|t\|_p \wedge \|s\|_q = \|t\|_q \;\forall q < p$. - In particular $\|s_i\|_q = \|t_i\|_q \;\forall q$, - therefore by lemma \ref{incomparability_equivdef} $s_i \sim t_i$ - and by lemma \ref{lemma_pe_equiv} we have $\Phi(s_i) = \Phi(t_i)$. - Let $traces (\Phi_{h}(s), \Phi_{h}(t)) = \big( (\rho_0, \dots, \rho_k), (\rho'_0, \dots, \rho'_k) \big)$ - and consider the following cases. + Consider any $i < p$ ($i \in \YN$). + By lemma conditions $s \prec_p t$, therefore $\snorm{s}{q} = \snorm{t}{q} \;\forall q < p$, and + in particular $\snorm{s_i}{q} = \snorm{t_i}{q} \;\forall q$, therefore + by lemma \ref{lemma_incomparability_equivdef} $s_i \sim t_i$, + therefore by lemma \ref{lemma_pe_equiv} $\Phi_{h+1}(s_i) = \Phi_{h+1}(t_i)$. + Let $traces (\Phi_{h}(s), \Phi_{h}(t)) = \big( (\rho_0, \dots, \rho_k), (\rho'_0, \dots, \rho'_k) \big)$. - \medskip - - First case: - $\infty = \|s_p\| > \|t_p\|$. - In this case $s|_p$ does not exist - (because $p$ corresponds to a submatch position in $r$, - therefore $p \in Pos(s)$ implies $p \in Sub(s)$, - which contradicts $\|s_p\| = \infty$). - Fork happens immediately after $\Phi_{h+1}(s_{p-1})$, $\Phi_{h+1}(t_{p-1})$: - \begin{alignat*}{7} - \Phi_{h}(s) &\;=\; \Xl_{h+1} &&\Phi_{h+1}(s_1) &&\dots &&\Phi_{h+1}(s_{p-1}) - &&\;\big|\; \Xr_{h} && && \\[-0.5em] - \Phi_{h}(t) &\;=\; \Xl_{h+1} &&\Phi_{h+1}(t_1) &&\dots &&\Phi_{h+1}(t_{p-1}) - &&\;\big|\; \Phi_{h+1}(t_p) &&\dots &&\Phi_{h+1}(t_m) \Xr_{h} - \end{alignat*} - % - In this case fork frame is the last frame: $j = k$, and therefore $\rho_j = \rho'_j = h$ - (because $\gamma_j$ and $\delta_j$ contain the closing parenthesis $\Xr_{h}$). - For all $i < j$ we have $\rho_i = \rho'_i = -1$, therefore $\Phi_{h}(s) \sim \Phi_{h}(t)$. - Furthermore, $first(\gamma_j)$ is $\Xr$ and $first(\delta_j)$ is one of $\Xl$ and $\Xm$, - therefore $\Phi_{h}(s) \subset \Phi_{h}(t)$. - Consequently $\Phi_{h}(s) < \Phi_{h}(t)$. - - \medskip + \begin{itemize}[itemsep=0.5em, topsep=0.5em] + \item[(1)] + Case $\infty = \snorm{s}{p} > \snorm{t}{p}$. + In this case $s_p$ does not exist + and fork happens immediately after $\Phi_{h+1}(s_{p-1})$, $\Phi_{h+1}(t_{p-1})$: + \begin{alignat*}{7} + \Phi_{h}(s) &\;=\; \Xl_{h+1} &&\Phi_{h+1}(s_1) &&\dots &&\Phi_{h+1}(s_{p-1}) + &&\;\big|\; \Xr_{h} && && \\[-0.5em] + \Phi_{h}(t) &\;=\; \Xl_{h+1} &&\Phi_{h+1}(t_1) &&\dots &&\Phi_{h+1}(t_{p-1}) + &&\;\big|\; \Phi_{h+1}(t_p) &&\dots &&\Phi_{h+1}(t_m) \Xr_{h} + \end{alignat*} + % + Fork frame is the last one, + therefore both $\gamma_j$ and $\delta_j$ contain the closing parenthesis $\Xr_{h}$ + and we have $\rho_j = \rho'_j = h$. + For all $i < j$ we have $\rho_i = \rho'_i = -1$. + Therefore $\rho_i = \rho'_i \;\forall i$ and $\Phi_{h}(s) \sim \Phi_{h}(t)$. + Since $first(\gamma_j)$ is $\Xr$ and $first(\delta_j)$ is one of $\Xl$ and $\Xm$, + we have $\Phi_{h}(s) \subset \Phi_{h}(t)$. + Therefore $\Phi_{h}(s) < \Phi_{h}(t)$. - Second case: $\infty > \|s_p\| > \|t_p\| = -1$. - In this case both $s_p$ and $t_p$ exist, - $s_p$ is not $\varnothing$ and $t_p$ is $\varnothing$, - and fork happens immediately after $\Phi_{h+1}(s_{p-1})$, $\Phi_{h+1}(t_{p-1})$: - \begin{alignat*}{8} - \Phi_{h}(s) &\;=\; \Xl_{h+1} &&\Phi_{h+1}(s_1) &&\dots &&\Phi_{h+1}(s_{p-1}) - &&\;\big|\; \Xl_{h+1} \; x \; \Xr_{h+1} \; &&\Phi_{h+1}(s_{p+1}) &&\dots &&\Phi_{h+1}(s_n) \Xr_{h} \\[-0.5em] - \Phi_{h}(t) &\;=\; \Xl_{h+1} &&\Phi_{h+1}(t_1) &&\dots &&\Phi_{h+1}(t_{p-1}) - &&\;\big|\; \Xm_{h+1} \;\;\;\;\;\; &&\Phi_{h+1}(t_{p+1}) &&\dots &&\Phi_{h+1}(t_m) \Xr_{h} - \end{alignat*} - % - If $j$-th frame is the last, we have $\rho_j = \rho'_j = h$ like in the first case. - Otherwise we have $\rho_j = \rho'_j = h + 1$, - because $minh(\gamma_j)$, $minh(\delta_j) \geq h + 1$ - and $lasth (\beta_j) = h + 1$ - (because if $p = 1$ then $\beta_j = \Xl_{h+1}$, otherwise - $s_{p-1}$ exists and the last parenthesis in $\beta_j$ - is last parenthesis of $\Phi_{h+1}(s_{p-1})$, which is either $\Xr_{h+1}$ or $\Xm_{h+1}$). - For subsequent frames $i$ such that $j < i < k$ we have $\rho_i = \rho'_i = h + 1$ - (because $minh(\gamma_j)$, $minh(\delta_j) \geq h + 1$), - and for the last pair of frames we have $\rho_k = \rho'_k = h$. - So in this case again $\Phi_{h}(s) \sim \Phi_{h}(t)$. - Furthermore, $first (\gamma_j) = \Xl < \Xm = first (\delta_j)$, therefore $\Phi_{h}(s) \subset \Phi_{h}(t)$ - and $\Phi_{h}(s) < \Phi_{h}(t)$. + \item[(2)] + Case $\infty > \snorm{s}{p} > \snorm{t}{p} = -1$. + In this case both $s_p$ and $t_p$ exist, + $s_p$ is not $\varnothing$ and $t_p$ is $\varnothing$, + and fork happens immediately after $\Phi_{h+1}(s_{p-1})$, $\Phi_{h+1}(t_{p-1})$: + \begin{alignat*}{8} + \Phi_{h}(s) &\;=\; \Xl_{h+1} &&\Phi_{h+1}(s_1) &&\dots &&\Phi_{h+1}(s_{p-1}) + &&\;\big|\; \Xl_{h+2} \; x \; \Xr_{h+1} \; &&\Phi_{h+1}(s_{p+1}) &&\dots &&\Phi_{h+1}(s_n) \Xr_{h} \\[-0.5em] + \Phi_{h}(t) &\;=\; \Xl_{h+1} &&\Phi_{h+1}(t_1) &&\dots &&\Phi_{h+1}(t_{p-1}) + &&\;\big|\; \Xm_{h+1} \;\;\;\;\;\; &&\Phi_{h+1}(t_{p+1}) &&\dots &&\Phi_{h+1}(t_m) \Xr_{h} + \end{alignat*} + % + \begin{itemize} + \item[(2.1)] + If fork frame is the last one, + then both $\gamma_j$ and $\delta_j$ contain the closing parenthesis $\Xr_{h}$ + and we have $\rho_j = \rho'_j = h$. + + \item[(2.2)] + Otherwise fork frame is not the last one. + We have $minh(\gamma_j)$, $minh(\delta_j) \geq h + 1$ + and $lasth (\beta_j) = h + 1$ + (the last parenthesis in $\beta_j$ is either $\Xl_{h+1}$ if $p = 1$ and $s_{p-1}$ does not exist, + or else one of $\Xr_{h+1}$ and $\Xm_{h+1}$), + therefore $\rho_j = \rho'_j = h + 1$. + % + For subsequent frames $i$ such that $j < i < k$ we have $\rho_i = \rho'_i = h + 1$ + (on one hand $\rho_i, \rho'_i \leq h + 1$ because $\rho_j = \rho'_j = h + 1$, + but on the other hand $minh(\gamma_i)$, $minh(\delta_i) \geq h + 1$). + % + For the last pair of frames we have $\rho_k = \rho'_k = h$ (they both contain the closing parenthesis $\Xr_{h}$). + \end{itemize} - \medskip + In both cases $\rho_i = \rho'_i \;\forall i \geq j$. + Since $\rho_i = \rho'_i = -1 \;\forall i < j$, + we have $\rho_i = \rho'_i \;\forall i$ and therefore $\Phi_{h}(s) \sim \Phi_{h}(t)$. + % + Since $first (\gamma_j) = \Xl < \Xm = first (\delta_j)$ we have $\Phi_{h}(s) \subset \Phi_{h}(t)$. + Therefore $\Phi_{h}(s) < \Phi_{h}(t)$. + + \item[(3)] + Case $\infty > \snorm{s}{p} > \snorm{t}{p} \geq 0$. + In this case both $s_p$ and $t_p$ exist and none of them is $\varnothing$, + and fork happens somewhere after the opening parenthesis $\Xl_{h+2}$ + and before the closing parenthesis $\Xr_{h+1}$ in $\Phi_{h}(s_p)$, $\Phi_{h}(t_p)$: + \begin{alignat*}{9} + \Phi_{h}(s) &\;=\; \Xl_{h+1} &&\Phi_{h+1}(s_1) &&\dots &&\Phi_{h+1}(s_{p-1}) &&\; \Xl_{h+2} \; x + &&\;\big|\; y \; \Xr_{h+1} \; &&\Phi_{h+1}(s_{p+1}) &&\dots &&\Phi_{h+1}(s_n) \Xr_{h} \\[-0.5em] + \Phi_{h}(t) &\;=\; \Xl_{h+1} &&\Phi_{h+1}(t_1) &&\dots &&\Phi_{h+1}(t_{p-1}) &&\; \Xl_{h+2} \; x + &&\;\big|\; z \; \Xr_{h+1} \; &&\Phi_{h+1}(t_{p+1}) &&\dots &&\Phi_{h+1}(t_m) \Xr_{h} + \end{alignat*} + % + From $\snorm{s}{p} > \snorm{t}{p} \geq 0$ it follows that + $s_p$ contains more alphabet symbols than $t_p$. + Consequently $\Phi_{h+1}(s_p)$ contains more alphabet symbols, and thus spans more frames than $\Phi_{h+1}(t_p)$. + % + Let $l$ be the index of the frame $\delta_l$ that contains the closing parenthesis $\Xr_{h+1}$ of $\Phi_{h+1}(t_p)$. + By the above reasoning $\Phi_{h+1}(s_p)$ does not end in frame $\gamma_l$, + therefore $\gamma_l$ does not contain the closing parenthesis $\Xr_{h+1}$ + and we have $minh (\gamma_l) \geq h+2$ and $minh (\delta_l) = h+1$. + % + Furthermore, note that $minh(x)$, $minh(y)$, $minh(z) \geq h + 2$, + therefore $lasth(\beta_j) \geq h+2$ (including the case when $x$ is empty), + and for all frames $i$ such that $j \leq i < l$ (if any) we have $\rho_i, \rho'_i \geq h+2$. + % + Consequently, for $l$-th frame we have $\rho_l \geq h+2$ and $\rho'_l = h + 1$, thus $\rho_l > \rho'_l$. + % + For subsequent frames $i$ such that $l < i < k$ we have $minh(\gamma_i)$, $minh(\delta_i) \geq h + 1$, + therefore $\rho_i \geq h+1$ and $\rho'_i = h + 1$, thus $\rho_i \geq \rho'_i$. + % + For the last pair of frames we have $\rho_k = \rho'_k = h$, as they both contain the closing parenthesis $\Xr_{h}$. + % + Therefore $\Phi_{h}(s) \sqsubset \Phi_{h}(t)$, + which implies $\Phi_{h}(s) < \Phi_{h}(t)$. + \end{itemize} +\end{proofEnd} - Third case: $\infty > \|s_p\| > \|t_p\| \geq 0$. - In this case both $s_p$ and $t_p$ exist and none of them is $\varnothing$, - and fork happens somewhere after the opening parenthesis $\Xl$ - and before the closing parenthesis $\Xr$ in $\Phi_{h}(s_p)$, $\Phi_{h}(t_p)$: - \begin{alignat*}{9} - \Phi_{h}(s) &\;=\; \Xl_{h+1} &&\Phi_{h+1}(s_1) &&\dots &&\Phi_{h+1}(s_{p-1}) &&\; \Xl_{h+2} \; x - &&\;\big|\; y \; \Xr_{h+1} \; &&\Phi_{h+1}(s_{p+1}) &&\dots &&\Phi_{h+1}(s_n) \Xr_{h} \\[-0.5em] - \Phi_{h}(t) &\;=\; \Xl_{h+1} &&\Phi_{h+1}(t_1) &&\dots &&\Phi_{h+1}(t_{p-1}) &&\; \Xl_{h+2} \; x - &&\;\big|\; z \; \Xr_{h+1} \; &&\Phi_{h+1}(t_{p+1}) &&\dots &&\Phi_{h+1}(t_m) \Xr_{h} - \end{alignat*} - % - Let $l$ be an index such that the frame $\delta_l$ contains the closing parenthesis $\Xr_{h+1}$ of $\Phi_{h+1}(t_p)$. - It must be $l \geq j$ (equality is possible due to non-fully parenthesized expressions, - as in the example $(a|aa)^{0,\infty}$ shown on figure \ref{fig_pe3}). - Because $\|s_p\| > \|t_p\|$, - the closing parenthesis $\Xr_{h+1}$ of $\Phi_{h+1}(s_p)$ is not contained in $\gamma_{l}$, - and $l$-th frame is not the last one. - Therefore $minh (\gamma_l) \geq h+2$ and $minh (\delta_l) = h+1$. - Furthermore, $minh(x)$, $minh(y)$, $minh(z) \geq h + 2$, - therefore $lasth(\beta_j) \geq h+2$ and - for all frames $j \leq i < l$ (if such $i$ exist) we have $\rho_i, \rho'_i \geq h+2$ - (note that it might be $\rho_i < \rho'_i$). - For the $l$-th frame $\rho_l \geq h+2 > h+1 = \rho'_l$. - For subsequent frames $\gamma_i$, $\delta_i$ such that $l < i < k$ we have - $minh(\gamma_i)$, $minh(\delta_i) \geq h + 1$, - therefore $\rho_i \geq h+1 = \rho'_i$. - For the last pair of frames $\rho_k = \rho'_k = h$. - Therefore in this case $\Phi_{h}(s) \sqsubset \Phi_{h}(t)$, - which implies $\Phi_{h}(s) < \Phi_{h}(t)$. - $\square$ - \end{XLem} - - - \begin{XLem}\label{lemma_pe_less} +\begin{theoremEnd}[normal, no link to proof, no link to theorem]{lemma} + \label{lemma_pe_less} Let $s, t \in PT(r, w)$. - If $s <_p t$, then $\Phi_{h}(s) < \Phi_{h}(t) \; \forall h$. - \\ - Proof. - By induction on the length of $p$. - - \medskip - + If $s \prec_p t$, then $\Phi_{h}(s) < \Phi_{h}(t) \; \forall h$. +\end{theoremEnd} +\begin{proofEnd} + The proof is by induction on the length of $p$. + % Induction basis for $|p| = 1$ is given by lemma \ref{lemma_pe_less_1}. - - \medskip - - Induction step. - Let $|p| \geq 2$, then $s$ and $t$ are compound PT - $s = T^{d} (s_1, \dots, s_n)$ and - $t = T^{d} (t_1, \dots, t_m)$, where - $d \neq 0$ (because $\Lambda$ is a prefix of decision position $p$). % - Furthermore, let $p = p'.p''$, where $p' \in \YN$. - Subtrees $s' = s_{p'}$ and $t' = t_{p'}$ exist, because $p'$ a proper prefix of decision position $p$, - and they also must be compount PT - $s' = T^{d'} (s'_1, \dots, s'_{n'})$ and - $t' = T^{d'} (t'_1, \dots, t'_{m'})$, - because $|p''| > 0$, and it must be - $d' \neq 0$ (because $p'$ is a prefix of decision position $p$). + Induction step: suppose that the lemma is correct for all $p$ of length $|p| < h$ and let $|p| = h$ ($h \geq 2$). % - For subtrees $s_i$ and $t_i$ where $i < p'$ we have - $\|s_i\|_q = \|t_i\|_q \;\forall q$ (implied by $s <_p t$), - therefore by lemma \ref{incomparability_equivdef} - $s_i \sim t_i$, and by lemma \ref{lemma_pe_equiv} we have $\Phi_{h+1}(s_i) = \Phi_{h+1}(t_i)$. + Let $p = p'.p''$ where $p' \in \YN$. + % + At least one of $s|_p$ and $t|_p$ must exist (otherwise $\snorm{s}{p} = \infty = \snorm{t}{p}$ which contradicts $s \prec_p t$), + therefore both $e$ and $e|_{p'}$ are compound RE and $s$, $t$ can be represented as + $s = T^{d} (s_1, \dots, s_n)$ and + $t = T^{d} (t_1, \dots, t_m)$ where + $s' = s_{p'} = T^{d'} (s'_1, \dots, s'_{n'})$ and + $t' = t_{p'} = T^{d'} (t'_1, \dots, t'_{m'})$ + and both $d, d' \neq 0$ (because $\Lambda$ and $p'$ are prefixes of decision position $p$). % Therefore $\Phi_{h}(s)$, $\Phi_{h}(t)$ can be represented as follows: \begin{alignat*}{9} @@ -2950,12 +3024,21 @@ if the s-norms at all preceding submatch positions are equal. \;&& \underbrace {\Xl_{h+2} \Phi_{h+2}(t'_1) \dots \Phi_{h+2}(t'_{m'}) \Xr_{h+1}}_{\Phi_{h+1}(t')} \;&& \Phi_{h+1}(t_{p'+1}) \Phi_{h+1}(t_m) \Xr_{h} \end{alignat*} - - We have $\|s\|_q = \|t\|_q \;\forall q < p'$ (implied by $s <_p t$), - therefore by lemma \ref{lemma_subtrees} $\exists r', w' : s', t' \in PT(r', w')$. - Moreover, $s' <_{p''} t'$ and $|p''| < |p|$, therefore by induction hypothesis $\Phi_{p+1}(s') < \Phi_{p+1}(t')$. % - On the other hand, if $j$ is the fork and $f \leq j \leq k$ then + Consider any $i < p'$. + By lemma conditions $s \prec_p t$, therefore $\snorm{s}{q} = \snorm{t}{q} \;\forall q < p$, and + in particular $\snorm{s_i}{q} = \snorm{t_i}{q} \;\forall q$, therefore + by lemma \ref{lemma_incomparability_equivdef} $s_i \sim t_i$, + therefore by lemma \ref{lemma_pe_equiv} $\Phi_{h+1}(s_i) = \Phi_{h+1}(t_i)$. + % + Since $p' < p$ we have $\snorm{s}{q} = \snorm{t}{q} \;\forall q \leq p'$ and + by lemma \ref{lemma_subtrees} $\exists e', w' : s', t' \in PT(e', w')$. + Since $\snorm{s'}{q} = \snorm{s}{p'.q} \;\forall q$ + and $\snorm{t'}{q} = \snorm{t}{p'.q} \;\forall q$, + we have $s' \prec_{p''} t'$. + Since $|p''| < |p|$ by induction hypothesis we have $\Phi_{h+1}(s') < \Phi_{h+1}(t')$. + % + If $j$ is the fork and $f \leq j \leq k$, then $\Phi_{h}(s)$, $\Phi_{h}(t)$ can be represented as: \begin{alignat*}{9} \Phi_{h}(s) @@ -2970,104 +3053,78 @@ if the s-norms at all preceding submatch positions are equal. \;&& \underbrace {\beta_f^2 a_{f+1} \dots a_j \beta_j \;\big|\; \delta_j a_{j+1} \dots a_k \delta_k^1}_{\Phi_{h+1}(t')} \;&& \delta_k^2 a_{k+1} \dots a_l \delta_l \end{alignat*} - -% \begin{alignat*}{9} -% \Phi_{h}(s) -% \;&= -% \;&&\overbrace {\Xl_{h+1} \Phi_{h+1}(s_1) \dots \Phi_{h+1}(s_{p'-1})} -% ^{\beta_0 a_1 \dots a_i \beta_i^1} -% \;&&\overbrace {\Xl_{h+2} \Phi_{h+2}(s'_1) \dots \Phi_{h+2}(s'_{n'}) \Xr_{h+1}} -% ^{\beta_i^2 a_{i+1} \dots a_j \beta_j \;\big|\; \gamma_j a_{j+1} \dots a_k \gamma_k^1} -% \;&&\overbrace {\Phi_{h+1}(s_{p'+1}) \Phi_{h+1}(s_n) \Xr_{h}} -% ^{\gamma_k^2 a_{k+1} \dots a_l \gamma_l} -% \\ -% \Phi_{h}(t) -% \;&= -% \;&&\underbrace {\Xl_{h+1} \Phi_{h+1}(t_1) \dots \Phi_{h+1}(t_{p'-1})} -% _{\beta_0 a_1 \dots a_i \beta_i^1} -% \;&&\underbrace {\Xl_{h+2} \Phi_{h+2}(t'_1) \dots \Phi_{h+2}(t'_{m'}) \Xr_{h+1}} -% _{\beta_i^2 a_{i+1} \dots a_j \beta_j \;\big|\; \delta_j a_{j+1} \dots a_k \delta_k^1} -% \;&&\underbrace {\Phi_{h+1}(t_{p'+1}) \Phi_{h+1}(t_m) \Xr_{h}} -% _{\delta_k^2 a_{k+1} \dots a_l \delta_l} -% \end{alignat*} - + % Let $traces (\Phi_{h}(s), \Phi_{h}(t)) = \big( (\rho_0, \dots, \rho_l), (\rho'_0, \dots, \rho'_l) \big)$ and $traces (\Phi_{h+1}(s'), \Phi_{h+1}(t')) = \big( (\sigma_h, \dots, \sigma_k), (\sigma'_h, \dots, \sigma'_k) \big)$. % We show that for frames $i$ such that $j \leq i < k$ we have - $\rho_i = \sigma_i \wedge \rho'_i = \sigma'_i$, + $\rho_i = \sigma_i \wedge \rho'_i = \sigma'_i$ and for subsequent frames $k \leq i \leq l$ we have $\rho_i = \rho'_i$. - - \medskip - - First case: $i = j \leq k \leq l$ (the fork frame). - Because $\Phi_{h+1}(s')$ and $\Phi_{h+1}(t')$ have nonempty common prefix $\Xl_{h+2}$, - we have $lasht (\Phi_{h}(s) \sqcap \Phi_{h}(t)) = lasth (\Phi_{h+1}(s') \sqcap \Phi_{h+1}(t')) \geq h + 2$. - % - If $j < k$ then $minh (\gamma_j)$, $minh (\delta_j)$ are not affected by appending - $\gamma^2_k$, $\delta^2_k$ and therefore $\rho_j = \sigma_j \wedge \rho'_j = \sigma'_j$. - % - Else if $j = k < l$ then we have $minh (\gamma^1_k) = minh (\delta^1_k) = h + 1$ and - $minh (\gamma^2_k) = minh (\delta^2_k) \geq h + 1$, and - therefore $\rho_j = \rho'_j = h + 1$. % - Finally, if $j = l$ then $minh (\gamma_j) = minh (\delta_j) = h$ and $\rho_j = \rho'_j = h$. - - \medskip - - Second case: $j < i < k$. - In this case the calculation of $\rho_i$, $\rho'_i$ depends on $\rho_j$, $\rho'_j$ - (for which we have shown $\rho_j = \sigma_j \wedge \rho'_j = \sigma'_j$) and - is not affected by the appended $\gamma^2_k$, $\delta^2_k$, therefore - $\rho_i = \sigma_i \wedge \rho'_i = \sigma'_i$. - - \medskip - - Third case: $j < i = k < l$. We have - $minh (\gamma^1_k) = minh (\delta^1_k) = h + 1$ and - $minh (\gamma^2_k) = minh (\delta^2_k) \geq h + 1$, - and none of the preceding frames after the fork contain parentheses with height less than $h + 1$, - therefore $\rho_k = \rho'_k = h + 1$. + \begin{itemize}[itemsep=0.5em, topsep=0.5em] + \item[(1)] + Case $i = j < k \leq l$ (the fork frame). + Since we have shown that $\Phi_{h+1}(s_i) = \Phi_{h+1}(t_i) \;\forall i < p'$, + and since $\Phi_{h+1}(s')$ and $\Phi_{h+1}(t')$ have nonempty common prefix $\Xl_{h+2}$, + it follows that $lasht (\Phi_{h}(s) \sqcap \Phi_{h}(t)) = lasth (\Phi_{h+1}(s') \sqcap \Phi_{h+1}(t'))$. + % + From $j < k$ it follows that $\gamma_j$ and $\delta_j$ end before $a_k$ + and are not changed by appending $\gamma^2_k$ and $\delta^2_k$. + % + Therefore $\rho_j = \sigma_j \wedge \rho'_j = \sigma'_j$. - \medskip + \item[(2)] + Case $j < i < k \leq l$. + The computation of $\rho_i$, $\rho'_i$ depends only on + $\rho_j$, $\rho'_j$, + or which we have shown $\rho_j = \sigma_j \wedge \rho'_j = \sigma'_j$ in case (1), + and on $\Phi_{h+1}(s')$, $\Phi_{h+1}(t')$, + which are not changed by appending $\gamma^2_k$ and $\delta^2_k$ since $i < k$. + Therefore $\rho_i = \sigma_i \wedge \rho'_i = \sigma'_i$. + + \item[(3)] + Case $j \leq i = k < l$. We have + $minh (\gamma^1_k) = minh (\delta^1_k) = h + 1$ and + $minh (\gamma^2_k) = minh (\delta^2_k) \geq h + 1$. + None of the preceding frames after the fork contain parentheses with height less than $h + 1$, + therefore $\rho_k = \rho'_k = h + 1$. + + \item[(4)] + Case $j \leq k < i < l$. + We have $\rho_i = \rho'_i = h + 1$, + because $\rho_k = \rho'_k = h + 1$ and $minh(\gamma_i)$, $minh(\delta_i) \geq h + 1$. + + \item[(5)] + Case $j \leq k \leq i = l$. + We have $\rho_l = \rho'_l = h$, + because both $\gamma_l$ and $\delta_l$ contain the closing parenthesis $\Xr_{h}$. + \end{itemize} + % + We have shown that $\rho_i = \sigma_i \wedge \rho'_i = \sigma'_i \;\forall i: j \leq i < k$ + and $\rho_i = \rho'_i \;\forall i: k \leq i \leq l$. + It trivially follows that $\Phi_{h+1}(s') \sqsubset \Phi_{h+1}(t')$ $\Rightarrow \Phi_{h}(s) \sqsubset \Phi_{h}(t)$ + and $\Phi_{h+1}(s') \sim \Phi_{h+1}(t')$ $\Rightarrow \Phi_{h}(s) \sim \Phi_{h}(t)$. + Because none of $\Phi_{h+1}(s')$, $\Phi_{h+1}(t')$ is a proper prefix of another, + $\Phi_{h+1}(s') \subset \Phi_{h+1}(t')$ $\Rightarrow \Phi_{h}(s) \subset \Phi_{h}(t)$. + Therefore $\Phi_{h+1}(s') < \Phi_{h+1}(t') \Rightarrow \Phi_{h}(s) < \Phi_{h}(t)$ + (the premise has been shown). +\end{proofEnd} - Fourth case: $k < i < l$. - We have $\rho_i = \rho'_i = h + 1$, - because $\rho_k = \rho'_k = h + 1$ and $minh(\gamma_i)$, $minh(\delta_i) \geq h + 1$. +\printProofs[theorem_order_on_pe_same_as_on_pt] - \medskip - Fifth case: $i = l$. - We have $\rho_l = \rho'_l = h$. +\subsection*{Correctness of incremental path comparison} - \medskip +\printProofs[lemma_frames] +\printProofs[lemmata_closure] - So, we have shown that $\rho_i = \sigma_i \wedge \rho'_i = \sigma'_i$ for $j \leq i < k$ - and $\rho_i = \rho'_i$ for $k \leq i \leq l$. - It trivially follows that $\Phi_{h+1}(s') \sqsubset \Phi_{h+1}(t')$ implies $\Phi_{h}(s) \sqsubset \Phi_{h}(t)$, and - $\Phi_{h+1}(s') \sim \Phi_{h+1}(t')$ implies $\Phi_{h}(s) \sim \Phi_{h}(t)$. - Because none of $\Phi_{h+1}(s')$, $\Phi_{h+1}(t')$ is a proper prefix of another, - $\Phi_{h+1}(s') \subset \Phi_{h+1}(t')$ implies $\Phi_{h}(s) \subset \Phi_{h}(t)$. - Therefore $\Phi_{h+1}(s') < \Phi_{h+1}(t')$ implies $\Phi_{h}(s) < \Phi_{h}(t)$. - $\square$ - \end{XLem} - - - Proof of theorem \ref{theorem_order_on_pe_same_as_on_pt}. - \\[-1em] - - $\Rightarrow$. Given by lemma \ref{lemma_pe_less}. - \\[-1em] - - $\Leftarrow$. - We have $\Phi_{h}(s) < \Phi_{h}(t) \; \forall h$. - Suppose that $\nexists p: s <_p t$. - By lemma \ref{lemma_pe_order_antisymm} either $s = t$ - (in which case $\Phi_{h}(s) = \Phi_{h}(t)$, contradiction) - or $t <_q s$ for some $q$ - (in which case $\Phi_{h}(t) < \Phi_{h}(s)$ by lemma \ref{lemma_pe_less}, contradiction). - Therefore $\exists p: s <_p t$. - $\square$ +\iffalse +\begin{figure}\label{fig_gor1} +\includegraphics[width=\linewidth]{img/gor1.pdf} +\caption{Sub-TNFA for individual sub-RT with submatch groups: \\ +(a) -- union, (b) -- product, (c), (d) -- bounded repetition, (e), (f) -- unbounded repetition.} +\end{figure} +\fi \end{document}