main.bbl
main.blg
main.fdb_latexmk
+main.fls
main.glo
main.log
main.out
\newcommand{\stsi}{\ensuremath\mathcal{Q}_i}
\newcommand{\lab}[1]{\ensuremath{\mbox{label}\paren{#1}}}
-\newcommand{\tr}[1]{\ensuremath{\mbox{label}\paren{#1}}}
+\newcommand{\tr}[1]{\ensuremath{\mbox{tr}\paren{#1}}}
\newcommand{\maininclude}[2]{\section{#1} \label{sec:#2} \input{#2}}
\begin{itemize}
\item Subset testing implies equivalence testing.
\item Relative complement closure implies general complement closure.
- \item Intersection and general complement closures imply both subset testing
- and relative complement closure.
+ \item Intersection and general complement closures implies
+ relative complement closure. If, additionally, a class has
+ a decidable emptiness test, then it has a decidable subset test.
\item Closure under arbitrary homomorphism implies closure under
$\epsilon$-free homomorphisms.
\end{itemize}
\Note{I would feel a lot better if somebody checked this.}
\subsection{Necessarily Overlapping}
+\label{sec:tree-sepex:necessaryoverlap}
\begin{wrapfigure}{r}{1in}\centering\begin{tikzpicture}
\Tree [.f$_{1=22}$ X [.g$_{1=2}$ X X ] ]
all positions of $t$ which are in $\config$ must be so-labeled by the run.
\Note{That's not very clear, but I think it's right.}
-For a run $r$, we define $\tr(r|_p)$ to be the function which returns the
-$\Sigma$ of the original tree at position $p$. (Symbolically, $\tr =
-\pi_1$.)
+For a run $r$, we define $\tr{r|_p}$ to be the function which returns the
+$\Sigma$ of the original tree at position $p$.
Similarly, we define
-$\lab(r|_p)$ as the (partial) function which returns
-the output configuration at position $p$. ($\lab = \pi_2 \mbox{inr}^{-1}
-\pi_2$.)
+$\lab{r|_p}$ as the (partial) function which returns
+the output configuration at position $p$.
\subsection{Nondeterminism}
performs a series of tests as part of its transition function {\em after
pattern matching}, meaning that it may be expressed as a (possibly infinite)
union of transitions of the form $\mathcal{T}(\Sigma \sqcup \config)
-\stackrel{c}{\longrightarrow} \config$, where $c$ is a set of constraints.
-The \defn{constraint path} is the concatenation of the paths between the
-{\em labeled node whose labeling introduced the constraint} and the
-constrained positions.
+\stackrel{c}{\longrightarrow} \config$, where $c$ is a set of constraints
+between positions below the node under study. These positions are indicated
+by paths, and we often use the term \defn{constraint path} to refer to paths
+used specifically in this context.
\subsubsection{Metaconstraints}
\footnote{See \cite[Exercise 4.8]{tata} for an alternate formalization.}
\paragraph{Opaque} If a position is constrained by a transition, no other
-constraint path may cross this position.
+constraint path may cross this position.
+
+%
+%\Note{A state controls an address $i$ if
+%\begin{itemize}
+% \item $i = \epsilon$ and $q$ is opaque, or
+% \item $i = j\omega$, $q$ is transparent, and...
+%\end{itemize}
+%If a rule $q_1\ldots q_k \to q$ imposes an equality constraint
+%on address $i\omega$, $q_i$ must control $\omega$.
+%}
\paragraph{Reduction} There exists a partial order on $\config$ such that
$\forall_{t \in \mathcal{T}(\Sigma \sqcup \config), c \in \config}$, $t$ and
Single-ply automata necessarily satisfy Stated, as every node in a run is
labeled. Single-ply automata subject to Contained necessarily satisfy
-Opaque; this is not true of multi-ply automata, as there may be crossing
-constraints within a single multi-ply transition.
+Brother and Opaque; this is not true of multi-ply automata, as there may be
+a path that traverses another node tested for equality within a single
+multi-ply transition.
-In general, Contained and Stated together imply Opaque.
+Contained and Stated together imply Opaque. Non-Overlapping also implies
+Opaque (but the reverse is not true: see
+\autoref{sec:tree-sepex:necessaryoverlap}).
In a deterministic automaton, satisfiable equality constraints referencing
labeled nodes are necessarily $f$-Same-Stated (for all $f$) as equal trees
whose entries are a tuple of a symbol and $k$-many string registers. A PA
has four sets of symbols used during its computation: states
($\mathcal{Q}$), input symbols ($\Sigma$), output symbols ($\Delta$), and
-stack (``tape'') symbols ($\Gamma$). Let $\phi$ denote a symbol disjoint
-from all of these sets, and let $Q_0 \in \mathcal{Q}$ and $Z_0 \in \Gamma$
-be the initial state and stack symbol.
+stack (``tape'') symbols ($\Gamma$). Let $Q_0 \in \mathcal{Q}$ and $Z_0 \in
+\Gamma$ be the initial state and stack symbol.
For this family, the machine is described by a state and the contents of the
stack, which is a string of stack symbols and per-slot registers: $\config =
\mathcal{Q} \times \paren{1 + \Delta^*} \times \paren{ \Gamma \times
-\paren{\Delta^* + \phi}^k }^+$. The initial $\config_0 = Q_0 \times \inl{1}
-\times \brak{Z_0 \times \phi^k}$.
+\paren{\Delta^* + 1}^k }^+$. Denote by $\phi$ the constant $\inr{1} :
+\Delta^* + 1$. The initial configuration, $\config_0$, is $Q_0 \times
+\inl{1} \times \brak{Z_0 \times \phi^k}$.
The transition function is characterized by the union of three functions,
all of which are given the same visibility into $\config$, namely the state,
$c = q \times w \times \paren{Z\brak{x_1,\ldots,x_k}}\alpha$ and $c' \in
\delta\paren{c \times a}$ (where $q \in \mathcal{Q}$ is the state of the
machine, $w \in 1 + \Delta^*$, $Z\brak{x_1,\ldots,x_k}$ with $Z \in \Gamma$
-and $x_i \in \Delta^* + \phi$ is the head of the stack, $\alpha$ the
+and $x_i \in \Delta^* + 1$ is the head of the stack, $\alpha$ the
remainder, and $a \in \Sigma + 1$ the next input symbol or the empty string)
is as follows (see \cite[p. 48]{aho:pa}):
%
&\Leftarrow q' \times \paren{K_1 \ldots K_n} \in \lambda\paren{q,a, Z} \wedge w = \inl{1} \wedge n \ge 1 \\
%
% \lambda \epsilon output
- q'\times \inr{\paren{x_1 \ldots x_k}} \times \alpha \in \delta (c \times a)
+ q'\times \inr{\paren{f(x_1) \ldots f(x_k)}} \times \alpha \in \delta (c \times a)
%
&\Leftarrow q' \times \epsilon \in \lambda\paren{q,a, Z} \wedge w = \inl{1} \\
%
% \nu
- q'\times \inl{1} \times \paren{Z\brak{x_1,\ldots,x_{i-1},x,x_{i+1},\ldots,x_k}\alpha} \in\delta (c \times a)
+ q'\times \inl{1} \times \paren{Z\brak{x_1,\ldots,x_{i-1},\inl{x},x_{i+1},\ldots,x_k}\alpha} \in\delta (c \times a)
%
- &\Leftarrow q' \times i \in \nu\paren{q,a, Z} \wedge w = \inr{w'} \wedge x_i = \phi \\
+ &\Leftarrow q' \times i \in \nu\paren{q,a, Z} \wedge w = \inr{x} \wedge x_i = \inr{1} \\
%
% \mu
q'\times \inl{1} \times \paren{Z\brak{x_1,\ldots,x_{i-1},y,x_{i+1},\ldots,x_k}\alpha} \in\delta (c \times a)
%
- &\Leftarrow q' \times y \times i \in \mu\paren{q,a, Z} \wedge w = \inl{1} \wedge x_i = \phi
+ &\Leftarrow q' \times y \times i \in \mu\paren{q,a, Z} \wedge w = \inl{1} \wedge x_i = \inr{1} \\
%
\end{align*}
%
That is, $\lambda$ serves two roles: to push new $\Gamma$ to the stack or to
-concatinate registers into a distinguished placeholder. $\nu$ serves to
-consume that placeholder, placing it into a top-of-stack register (all other
-rules are blocked if the placeholder is nonempty). $\mu$ allows insertion
-of strings into top-of-stack registers.
+concatinate registers into a distinguished placeholder (the function $f :
+\Delta^* + 1 \to \Delta^*$ sends $\inr{1} \mapsto \epsilon$ and $\inl{s}
+\mapsto s$). $\nu$ serves to consume that placeholder, placing it into a
+top-of-stack register (all other rules are blocked if the placeholder is
+nonempty). $\mu$ allows insertion of strings into top-of-stack registers.
projects / autzoo / commitdiff