# Differences

This shows you the differences between two versions of the page.

 tree_automata [2010/05/27 18:10]vkuncak tree_automata [2015/04/21 17:32] (current) Both sides previous revision Previous revision 2012/05/15 15:48 vkuncak 2010/05/27 18:10 vkuncak 2010/05/25 15:33 vkuncak 2010/05/25 15:32 vkuncak 2010/05/25 15:32 vkuncak 2010/05/25 15:24 vkuncak 2010/05/25 15:23 vkuncak 2010/05/25 10:48 vkuncak 2010/05/25 10:44 vkuncak 2010/05/21 02:34 vkuncak 2010/05/20 20:21 vkuncak 2009/04/29 11:06 vkuncak 2009/04/28 23:27 vkuncak 2008/05/15 14:06 vkuncak 2008/05/15 13:59 vkuncak 2008/05/15 13:46 vkuncak 2008/05/15 13:45 vkuncak 2008/05/15 13:41 vkuncak 2008/05/15 13:38 vkuncak 2008/05/15 13:36 vkuncak 2008/05/15 13:34 vkuncak 2008/05/15 13:23 vkuncak 2008/05/15 13:13 vkuncak 2008/05/15 13:07 vkuncak 2008/05/15 13:06 vkuncak 2007/05/16 00:53 vkuncak 2007/05/16 00:15 vkuncak created Next revision Previous revision 2012/05/15 15:48 vkuncak 2010/05/27 18:10 vkuncak 2010/05/25 15:33 vkuncak 2010/05/25 15:32 vkuncak 2010/05/25 15:32 vkuncak 2010/05/25 15:24 vkuncak 2010/05/25 15:23 vkuncak 2010/05/25 10:48 vkuncak 2010/05/25 10:44 vkuncak 2010/05/21 02:34 vkuncak 2010/05/20 20:21 vkuncak 2009/04/29 11:06 vkuncak 2009/04/28 23:27 vkuncak 2008/05/15 14:06 vkuncak 2008/05/15 13:59 vkuncak 2008/05/15 13:46 vkuncak 2008/05/15 13:45 vkuncak 2008/05/15 13:41 vkuncak 2008/05/15 13:38 vkuncak 2008/05/15 13:36 vkuncak 2008/05/15 13:34 vkuncak 2008/05/15 13:23 vkuncak 2008/05/15 13:13 vkuncak 2008/05/15 13:07 vkuncak 2008/05/15 13:06 vkuncak 2007/05/16 00:53 vkuncak 2007/05/16 00:15 vkuncak created Line 10: Line 10: Represent $a_1 a_2 \ldots a_{n-1} a_n$ as a ground term Represent $a_1 a_2 \ldots a_{n-1} a_n$ as a ground term - $+ \begin{equation*} ​a_n(a_{n-1}(\ldots a_2(a_1(\epsilon))\ldots)) ​a_n(a_{n-1}(\ldots a_2(a_1(\epsilon))\ldots)) -$ + \end{equation*} We define the notion of [[finite state machine]] as accepting a set of such terms. We define the notion of [[finite state machine]] as accepting a set of such terms. Line 23: Line 23: * $F$ is the set of final states * $F$ is the set of final states * $\Delta$ is a set of rewrite rules * $\Delta$ is a set of rewrite rules - $+ \begin{equation*} f(q_1,​\ldots,​q_n) \to q f(q_1,​\ldots,​q_n) \to q -$ + \end{equation*} where $f$ is a function symbol of arity $n$ and where $q_1,​\ldots,​q_n,​q \in Q$. where $f$ is a function symbol of arity $n$ and where $q_1,​\ldots,​q_n,​q \in Q$. Line 37: Line 37: Example: Example: - * bottom up tree automaton ​checking the parity of the number of nodes in the tree + * bottom up tree automaton ​accepting trees with an even number of nodes in the tree, in alphabet with constant '​a',​ binary function '​f'​. + * bottom up tree automaton accepting expressions with complement, union, intersection;​ accepting only expressions that are monotonic in each variable Non-deterministic top-down tree automaton: reverse a bottom-up tree automaton Non-deterministic top-down tree automaton: reverse a bottom-up tree automaton Deterministic top-down tree automaton: more restrictive. Is there deterministic automaton to check the parity of the number of nodes? Deterministic top-down tree automaton: more restrictive. Is there deterministic automaton to check the parity of the number of nodes? - - - ===== Closure Properties of Tree Automata ====== ===== Closure Properties of Tree Automata ====== Line 77: Line 75: We consider interpretations $(D,​\alpha)$ where We consider interpretations $(D,​\alpha)$ where - $+ \begin{equation*} ​\alpha({\subseteq}) = \{ (S_1,S_2) \mid S_1 \subseteq S_2 \} ​\alpha({\subseteq}) = \{ (S_1,S_2) \mid S_1 \subseteq S_2 \} -$ + \end{equation*} where $succ0$ takes a tree node and finds its left child: where $succ0$ takes a tree node and finds its left child: - $+ \begin{equation*} ​\alpha(succ0) = \{ (\{w\},​\{w0\}) \mid w \in \Sigma^* \} ​\alpha(succ0) = \{ (\{w\},​\{w0\}) \mid w \in \Sigma^* \} -$ + \end{equation*} and where $succ1$ takes a tree node and finds its right child: and where $succ1$ takes a tree node and finds its right child: - $+ \begin{equation*} ​\alpha(succ1) = \{ (\{w\},​\{w1\}) \mid w \in \Sigma^* \} ​\alpha(succ1) = \{ (\{w\},​\{w1\}) \mid w \in \Sigma^* \} -$ + \end{equation*} The meaning of formulas is then given by standard [[sav08:​First-order logic semantics]]. The meaning of formulas is then given by standard [[sav08:​First-order logic semantics]].