LARA

Differences

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

Link to this comparison view

Both sides previous revision Previous revision
tree_automata [2012/05/15 15:48]
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 75: 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]].