Title: Theory / Unimportant / CS / Fundamental / Automata / TATA / Automata
Tags: fromMath mathToDef fromAlgorithm hasNotNewEffectReturnsMeaning hasSeenConjDef mathToSee

Name: Ranked alphabet
Definition: \((\mathcal F,Arity)\), where \(\mathcal F\) is a finite set and \(Arity:\mathcal F\to N\).
Page: 15
Chapter: Introduction
Section: Preliminaries

Definition: \(\{f\in \mathcal F\mid Arity(f)=p\}\)
Page: 15
Chapter: Introduction
Section: Preliminaries
Variables: \((\mathcal F,Arity)\) a ranked alphabet
\(p\in N\).
Context: Ranked alphabet
Notation: \(\mathcal F_p\)

Name: The set of terms
Definition: The smallest set containing \(\mathcal F_0\), \(X\) and \(f(t_1,\dots,t_{Arity(f)})\) for \(f\in \mathcal F\) and the \(t_i\) in this set.
Page: 15
Chapter: Introduction
Section: Preliminaries
Variables: \((\mathcal F,Arity)\) a ranked alphabet and \(X\) a set of variables.
Notation: \(T(\mathcal F,X)\)

Name: The set of ground terms
Definition: \(T(\mathcal F,\emptyset)\).
Page: 15
Chapter: Introduction
Section: Preliminaries
Variables: \((\mathcal F,Arity)\) a ranked alphabet.
Notation: \(T(\mathcal F)\)

Name: Linear term
Definition: An element of \(T(\mathcal F,X)\) where each variables occurs at most once in \(t\).
Page: 15
Chapter: Introduction
Section: Preliminaries
Variables: \((\mathcal F,Arity)\) a ranked alphabet,
\(X\) a set of variables

Name: A finite ordered tree over a set of labels \(E\)
Definition: A mapping from a prefix-closed set \(\mathcal{P}os(t)\subseteq N^*\) into \(E\).
Page: 15
Chapter: Introduction
Section: Preliminaries
Variables: \(E\) a set of labels.

Q: [...] are [...].
A: The positions of \(t\); the elements of \(\mathcal{P}os(t)\)
Page: 15
Chapter: Introduction
Section: Preliminaries
Variables: \(t\) a term

Name: The set of frontier positions of \(t\)
Definition: The elements \(p\in\mathcal{P}os(t)\) such that \(pj\not\in\mathcal Pos(t)\) for any \(j\in N\).
Page: 16
Chapter: Introduction
Section: Preliminaries
Variables: \(t\) a term
Notation: \(\mathcal {FP}os(t)\)

Name: The variable positions of \(t\)
Definition: The elements \(p\in\mathcal{P}os(t)\) such that \(t(p)\in X\).
Page: 16
Chapter: Introduction
Section: Preliminaries
Variables: \(t\) a term and \(X\) a set of variables
Notation: \(\mathcal {VP}os(t)\)

Definition: \(t(\epsilon)\).
Page: 16
Chapter: Introduction
Section: Preliminaries
Variables: \(t\) a term
Notation: \(\mathcal {H}ead(t)\)

Name: The subterm of \(t\) at positions \(p\)
Definition: \(\left(\{j\mid pj\in\mathcal Pos(t)\}, q\mapsto t(pq)\right)\)
Page: 16
Chapter: Introduction
Section: Preliminaries
Variables: \(t\) a term
\(p\in\mathcal P(t)\)
Notation: \(t_p\)

Definition: \(t\) where the subterm at position \(p\) is replaced by \(u\).
Page: 16
Chapter: Introduction
Section: Preliminaries
Variables: \(t,u\) terms
\(p\in\mathcal P(t)\)
Notation: \(t[u]_p\)

Definition: \(t\) is a subterm of \(t'\).
Page: 16
Chapter: Introduction
Section: Preliminaries
Variables: \(t,t'\) terms.
Notation: \(t\trianglelefteq t'\)

Definition: \(t\trianglelefteq t'\) and \(t'\ne t\).
Page: 16
Chapter: Introduction
Section: Preliminaries
Variables: \(t,t'\) terms.
Notation: \(t\triangleleft t'\)

Name: Closed set of terms
Definition: A set of terms which is closed under the subterm relation.
Page: 16
Chapter: Introduction
Section: Preliminaries

Name: The size of \(t\)
Definition: The inductive function \(f\) sending \(\mathcal X\) to \(0\), \(\mathcal F_{0}\) to 1, and \(g(t_1,\dots,t_n)\) to \(1+\sum _{i=1}^n f(t_i)\)
Page: 16
Chapter: Introduction
Section: Preliminaries
Variables: \(t\) a tree.
Notation: \(\parallel t\parallel \)

Name: The height of \(t\)
Definition: The inductive function \(f\) sending \(\mathcal X\) to \(0\), \(\mathcal F_{0}\) to 1, and \(g(t_1,\dots,t_n)\) to \(1+\max _{i=1}^n f(t_i)\).
Page: 16
Chapter: Introduction
Section: Preliminaries
Variables: \(t\) a tree
Abbreviation: \(\mathcal Height(t)\)

Name: A substitution
Definition: A mapping from \(X\) to \(T(\mathcal F,X)\) with only finitely many variables not mapped to themselves.
Page: 16
Chapter: Introduction
Section: Preliminaries
Variables: \(X\) a set of variables
\((\mathcal F,Arity)\) a set of symbols

Name: A ground substitution
Definition: A substitution from \(X\) to \(T(\mathcal F)\).
Page: 16
Chapter: Introduction
Section: Preliminaries
Variables: \(X\) a set of variables and \((\mathcal F,Arity)\) a set of symbols

Name: The domain of \(\sigma\)
Definition: \(\{x\mid \sigma(x)\ne x\}\)
Page: 17
Chapter: Introduction
Section: Preliminaries
Variables: \(X\) a set of variables
\((\mathcal F,Arity)\) a set of symbols
\(\sigma\) a substitution

Definition: \(t\) where each variable \(x\) is replaced by \(\sigma(x)\).
Page: 17
Chapter: Introduction
Section: Preliminaries
Variables: \(X\) a set of variables, \((\mathcal F,Arity)\) a set of symbols, \(t\) a term and \(\sigma\) a substitution
Notation: \(t\sigma\)

Definition: A set of \(n\) variables.
Page: 17
Chapter: Introduction
Section: Preliminaries
Variables: \(n\in N\)
Notation: \(\mathcal X_n\)

Name: A context
Definition: a linear elements of \(T(\mathcal F,\mathcal X_n)\).
Page: 17
Chapter: Introduction
Section: Preliminaries
Variables: \(n\in N\)
\(\mathcal F\) a set of symbols.

Definition: \(\mathcal C^1(\mathcal F)\).
Page: 17
Chapter: Introduction
Section: Preliminaries
Variables: \(\mathcal F\) a set of symbols.
Notation: \(\mathcal C(\mathcal F)\)

Name: A context
Definition: An element of \(\mathcal C^n(\mathcal F)\) for some integer \(n\).
Page: 17
Chapter: Introduction
Section: Preliminaries
Variables: \(\mathcal F\) a set of symbols.

Definition: \(C\) where \(x_i\) is replaced by \(t_i\).
Page: 17
Chapter: Introduction
Section: Preliminaries
Variables: \(t\in N\), \(\mathcal F\) a set of symbols
\(C\in\mathcal C^n(\mathcal F)\),
\(t_1,\dots,t_n\) terms.
Notation: \(C[t_1,\dots,t_n]\)

Name: A finite Tree Automaton over \(\mathcal F\)
Definition: \(Q\) is a set of (unary) states,
Page: 20
Chapter: 1
Variables: \(\mathcal F\) a set of symbols.
Definition2: \(Q_f\subseteq Q\) is a set of final states
Conjdef: A tuple \(\mathcal A=(Q,\mathcal F,Q_f,\Delta)\) where
Definition3: \(\Delta\) is a set of transitions rules of the type: \(f(q_1(x_1),\dots,f_{Arity(f)}(x_{Arity(f)}))\to q(f(x_1,\dots,x_n))\) where \(f\in\mathcal F\), \(q,q_1,\dots,q_{Arity(f)}\in Q\) and \(x_1,\dots,x_n\in\mathcal X\).

Name: The move relation
Definition: The relation sending \(C[f(q_1(x_1),\dots,f_{Arity(f)}(x_{Arity(f)})]\) to \(C[q(f(x_1,\dots,x_n)]\), where \(C\in\mathcal C(\mathcal F\cup Q)\), \(u_1,\dots,u_{Arity(f)}\in T(\mathcal F)\) and \(f(q_1(x_1),\dots,f_{Arity(f)}(x_{Arity(f)}))\to q(f(x_1,\dots,x_{Arity(f)}))\in \Delta\).
Page: 20
Chapter: 1
Variables: \(\mathcal F\) a set of symbols
\(\mathcal A=(Q,\mathcal F,Q_f,\Delta)\) a finite tree automaton over \(\mathcal F\)
Notation: \(\to_{\mathcal A}\)

Definition: The reflexive transitive closure of \(\to_\mathcal A\)
Page: 20
Chapter: 1
Variables: \(\mathcal F\) a set of symbols
\(\mathcal A=(Q,\mathcal F,Q_f,\Delta)\) a finite tree automaton over \(\mathcal F\)
Notation: \(\to^*_\mathcal A\)

Name: The language of tree recognized by \(\mathcal A\)
Definition: The set of ground terms accepted by \(\mathcal A\).
Page: 21
Chapter: 1
Variables: \(\mathcal F\) a set of symbols
\(\mathcal A=(Q,\mathcal F,Q_f,\Delta)\) a finite tree automaton over \(\mathcal F\).
Notation: \(L(\mathcal A)\)

Name: A recognisable language
Definition: \(L(\mathcal A)\) for some \(\mathcal A\) finite tree automaton.
Page: 21
Chapter: 1
Variables: \(L\) a set of ground terms
Extra: variable

Name: Equivalent NFTA
Definition: NFTAs which recognize the same tree language.
Page: 21
Chapter: 1

Name: A run of \(\mathcal A\) on \(t\)
Definition: A mapping \(\mathcal Pos(t)\to Q\) compatible with \(\Delta\).
Page: 22
Chapter: 1
Variables: \(\mathcal {A}\) a NFTA and \(t\) a term

Name: Successful run
Definition: A run \(r\) of \(\mathcal A\) to \(Q\) such that \(r(\epsilon)\in Q_f\).
Page: 22
Chapter: 1
Variables: \(\mathcal {A}\) a NFTA, \(t\) a term

Name: NFTA with \(\epsilon\)-rule
Definition: A NFTA with a rule of the form \(q\to q'\).
Page: 22
Chapter: 1

Question: \(L\) is
Answer: recognized by a complete NFTA without \(\epsilon\)-rule.
Page: 23
Chapter: 1
Variables: Let \(\mathcal A\) a NFTA with \(\epsilon\)-rule and \(L\) the language it recognize

Name: Deterministic NFTA with \(\epsilon\)-rule
Definition: A NFTA with \(\epsilon\)-rule which does not contain two rules with the same left-hand side and no \(\epsilon\)-rule.
Page: 23
Chapter: 1

Name: Unambiguous NFTA with \(\epsilon\)-rule
Definition: A NFTA with \(\epsilon\)-rule with had at most one run for each ground term.
Page: 23
Chapter: 1

Name: Complete NFTA with \(\epsilon\)-rule
Definition: A NFTA such that there is at least one rule for each ground term.
Page: 24
Chapter: 1
Variables: Let \(\mathcal A\) a NFTA with \(\epsilon\)-rule.

Name: Accessible NFTA with \(\epsilon\)-rule
Definition: A NFTA such that, for each state \(q\), there exists a ground term \(T\) such that \(t\to^*_{\mathcal A}q\).
Page: 24
Chapter: 1

Name: The set of context with \(n\) variables
Page: 17
Chapter: Introduction
Section: Preliminaries
Variables: \(n\in\mathbb N\)
Notation: \(\mathcal C^n(\mathcal F)\)

Name: A ground term accepted by \(\mathcal A\)
Definition: A term \(t\) such that \(t\to^*_{\mathcal A}q(t)\) with \(q\in Q_f\),
Page: 20
Chapter: 1
Variables: \(\mathcal F\) a set of symbols
\(\mathcal A=(Q,\mathcal F,Q_f,\Delta)\) a finite tree automaton over \(\mathcal F\).
Definition2: A term \(t\) such that there exists an accepting run \(r\) of \(\mathcal A\) on \(t\)

Name: A reduced NTFA
Definition: An NFTA whose every states are accessible.
Page: 24
Chapter: 1

Question: W.L.O.G. an NFTA can be assumed to be
Answer: complete or reduced.
Page: 24
Chapter: 1
Index: 17, 18
Kind: Theo

Page: 26
Implementation: the least fixed-point for \(Q_d,\Delta_d\), such that:
\(Q_d\) contains \(s\), \(\Delta_d\) contains \(f(s_1,\dots,s_n)\to s\), for \(f\in\mathcal F_n,s_1,\dots,s_n\in Q_d\) and \(s=\{q\in Q\mid \exists q_1\in s_1,\dots, q_n\in s_n,f(q_1,\dots,q_n)\to q\in\Delta\}\)
\(Q_{df}\) is \(\{s\in Q_d\mid s\cap Q_f\ne \emptyset\}\)
Section: 1
Effect: A DFTA accepting the same tree language than \(\mathcal A\)
Variables: \(\mathcal A=(Q,\mathcal F,Q_f,\Delta)\) an NFTA
Index: 17
Kind: Theo

Question: Example of family of tree language whose minimal DFTA tree is exponentially smaller than some NFTA tree recognizing it ?
Answer: The language of words with two 0's separated by length exactly \(n\)
Page: 24
Chapter: 1
Index: 11
Kind: Ex

Name: A Finite tree automaton
Definition: Either a DFTA or a NFTA
Page: 28
Chapter: 1
Kind: Ex
Abbreviation: FTA