Differences
This shows you the differences between two versions of the page.
Both sides previous revision Previous revision Next revision | Previous revision | ||
tree_automata [2010/05/25 15:33] vkuncak |
tree_automata [2015/04/21 17:32] (current) |
||
---|---|---|---|
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 60: | Line 58: | ||
Projection. | Projection. | ||
+ | |||
===== Weak Monadic Logic of Two Successors (WS2S) ===== | ===== Weak Monadic Logic of Two Successors (WS2S) ===== | ||
Line 76: | 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(succ) = \{ (\{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(succ) = \{ (\{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]]. |