\define@key{autinfo}{reginter} {\def\autabsregi{#1}} % trio
\define@key{autinfo}{hom} {\def\autabshom {#1}} % full trio
+\define@key{autinfo}{cylind} {\def\autcylind {#1}}
+\define@key{autinfo}{proj} {\def\autproj {#1}}
+
\define@key{autinfo}{regops} {\def\autregintr{#1} % all regops at once
\def\autregun {#1}
\def\autregkstr{#1}}
\def\autabsmoh {}
\def\autabsregi{}
\def\autabshom {}
+ \def\autcylind {}
+ \def\autproj {}
\setkeys{autinfo}{#2}
{\centering
\ifdefempty{\autabshom} {}{Arbitrary Hom. & \autabshom \\ \hline}
\ifdefempty{\autabsehom}{}{$\epsilon$-free Hom. & \autabsehom \\ \hline}
\ifdefempty{\autabsregi}{}{Intersect reg. lang. & \autabsregi \\ \hline}
+ \ifdefempty{\autcylind }{}{Cylindrification & \autcylind \\ \hline}
+ \ifdefempty{\autproj }{}{Projection & \autproj \\ \hline}
\textbf{Automata Operations} & \\ \hline
\ifdefempty{\autmiscdet}{}{Determinizable & \autmiscdet \\ \hline}
\ifdefempty{\autmiscmin}{}{Minimizable & \autmiscmin \\ \hline}
where $\delta$ is restricted to manipulation of trees of the form
$\mathcal{T}(\Sigma_+ \sqcup \config)$.
+% \subsection{New Operations: Cylindrification and Projection}
+%
+% Originally defined for automata operating on tuples of trees \cite[Sec
+% 3.2.4]{tata}
+
\subsection{Local Constraints}
\label{sec:treeaut:con:loc}
\subsubsection{Metaconstraints}
-In general, tree automata with arbitrary constraints have very poor closure
-properties (see \autoref{xxx}). A variety of restrictions have been
-developed throughout the literature and are summarized here.
+In general, tree automata with arbitrary local constraints have undecidable
+decision procedures (see \autoref{sec:zoo-tree/awedc}). A variety of
+restrictions have been developed throughout the literature and are
+summarized here.
\paragraph{Brothers} The transition function may only mutually constrain
positions which differ only in the last index.
\paragraph{Contained} All positions tested for equality must be within the
fragment of the tree being labeled (or generated); that is, constraint paths
-may not involve a $\config$-labeled run node other than at their apex.
+may not involve a $\config$-labeled run node other than at their apex and
+endpoints.
\paragraph{Opaque} If a position is constrained by a transition, no other
constraint path may cross this position.
}
\subsection{Non-deterministic PDAs}
+\label{sec:zoo-str/pda-nd}
Non-deterministic PDAs' recognition corresponds exactly to context free languages.
Deterministic PDAs can recognize the subset of context-free languages,
\hyperref[sec:zoo-str/tm]{TM}. \cite{xxx}},
equiv={Undecidable; $\Sigma^*$ is recognizable, but universality is
undecidable.},
+ intersect={Undecidable; reduction from Post Correspondance \cite{xxx}},
}
-\Note{AWCBB is single-ply AWEDC subject to Brother and Contained
-metaconstraints (and, by implication, Opaque and Stated).}
+AWCBB is a sub-class of AWEDC wherein all transitions are single-ply and all
+(dis)equalities adhere to the Brother and Contained metaconstraints (by
+implication, they are also Opaque and Stated). See \cite[Sec 4.3]{tata}.
+
+\autinfo{
+ member={},
+ empty={Yes; EXPTIME \cite[Thm 4.3.5]{tata}; PTIME for det case \cite[Thm 4.3.6]{tata}},
+ union={Yes, as with AWEDC; \cite[Prop 4.3.2]{tata}},
+ intersect={Yes, as with AWEDC; \cite[Prop 4.3.2]{tata}},
+ compl={Yes, as with AWEDC; \cite[Prop 4.3.2]{tata}},
+ cylind={No; \cite[Sec 4.3.4]{tata}},
+ proj={No; \cite[Sec 4.3.4]{tata}},
+}
+Also called ``Automata With Equality and Disequality Constraints'' (AWEDC),
+this class of automata augments regular tree automata with the ability to
+require (dis)equality of positions in accepted trees, using local
+constraints. In general, the configuration space of these machines is
+$\config = \mathcal{Q} \times \mathcal{T}(\Sigma)$ for states $\mathcal{Q}$
+and input alphabet $\Sigma$; however, $\delta$ is constrained as outlined in
+\autoref{sec:treeaut:con:loc} to only perform comparisons within the tree
+structure; it may not compare against external trees. The automata is
+accepting when the root node of a run is labeled by a configuration whose
+first component is in a set of accepting states, $\mathcal{Q}_f$. See
+\cite[Sec 4.2]{tata} for details.
+
+\autinfo{
+ member={Yes; PTIME (linear for deterministic) \cite[Prop 4.2.9]{tata}},
+ empty={Undecidable by reduction of PCP; \cite[Thm 4.2.10]{tata}},
+ compl={Yes; \cite[Prop 4.2.8]{tata}},
+ union={Yes; linear time and space \cite[Prop 4.2.8]{tata}},
+ intersect={Yes; quadratic time and space \cite[Prop 4.2.8]{tata}},
+ determinize={Yes; exponential space cost \cite[Prop 4.2.6]{tata}}
+}
Given a family of trees accepted by a regular tree automata, the set of
strings formed by labels along paths in this set is a regular finite string
-language. The same is true of accepting runs.
+language. The same is true of accepting runs. The set of strings formed by
+leaves of a regular tree automata (its ``leaf language'') is a context-free
+language; dually, every context-free language is the leaf language of some
+regular tree automaton.%
+%
+\footnote{While intersection of two context free language is undecidable
+(see \autoref{sec:zoo-str/pda-nd}), the intersection of regular tree languages
+is decidable: the leaf language of the intersection of two regular tree
+languages is a {\em subset} of the intersection of their leaf languages.}
For bottom-up automata, we have:
\autinfo{