No public endorsements yet.
Loading review…
Sign in with ORCIDConcept map
Definition
A bottom-up tree automaton over a ranked alphabet has a set of states, a Boolean acceptance test, and a Boolean transition test. For a symbol of rank , the transition test decides whether a proposed state at the node and the ordered -tuple of states at its children form a transition. This includes rank-zero transitions for constants.
A run to a state is defined recursively at every node by the same transition rule. A tree is accepted when it has a run to an accepting state. A language is recognizable when it is the language of such an automaton with finitely many states. The automaton is deterministic when every symbol and tuple of child states has exactly one possible state at the parent.
Lean source view on GitHub
| 1 | import Lax53.RankedTree |
| 2 | |
| 3 | /-! |
| 4 | --- |
| 5 | title: Bottom-up tree automata |
| 6 | type: definition |
| 7 | --- |
| 8 | |
| 9 | A bottom-up tree automaton over a ranked alphabet has a set of states, a |
| 10 | Boolean acceptance test, and a Boolean transition test. For a symbol of rank |
| 11 | , the transition test decides whether a proposed state at the node and the |
| 12 | ordered -tuple of states at its children form a transition. This includes |
| 13 | rank-zero transitions for constants. |
| 14 | |
| 15 | A run to a state is defined recursively at every node by the same transition |
| 16 | rule. A tree is accepted when it has a run to an accepting state. A language is |
| 17 | recognizable when it is the language of such an automaton with finitely many |
| 18 | states. The automaton is deterministic when every symbol and tuple of child |
| 19 | states has exactly one possible state at the parent. |
| 20 | -/ |
| 21 | |
| 22 | namespace Lax53.TreeAutomaton |
| 23 | |
| 24 | open Lax53.RankedTree |
| 25 | |
| 26 | universe u v |
| 27 | |
| 28 | /-- A bottom-up tree automaton with state type `Q`. This basic structure allows |
| 29 | arbitrary state types; recognizable languages and the main theorems explicitly |
| 30 | require finitely many states. -/ |
| 31 | structure Automaton (A : RankedAlphabet.{u}) (Q : Type v) where |
| 32 | transition : (a : A.Symbol) → Q → (Fin (A.rank a) → Q) → Bool |
| 33 | accept : Q → Bool |
| 34 | |
| 35 | namespace Automaton |
| 36 | |
| 37 | /-- A run of `M` on `t` leading to state `q`. -/ |
| 38 | def RunsTo {A : RankedAlphabet.{u}} {Q : Type v} (M : Automaton A Q) : |
| 39 | Tree A → Q → Prop |
| 40 | | .node a children, q => |
| 41 | ∃ childStates : Fin (A.rank a) → Q, |
| 42 | M.transition a q childStates = true ∧ |
| 43 | ∀ i : Fin (A.rank a), M.RunsTo (children i) (childStates i) |
| 44 | |
| 45 | /-- A tree is accepted if some run leads to an accepting state. -/ |
| 46 | def Accepts {A : RankedAlphabet.{u}} {Q : Type v} (M : Automaton A Q) |
| 47 | (t : Tree A) : Prop := |
| 48 | ∃ q : Q, M.accept q = true ∧ M.RunsTo t q |
| 49 | |
| 50 | /-- The language accepted by a tree automaton. -/ |
| 51 | def language {A : RankedAlphabet.{u}} {Q : Type v} (M : Automaton A Q) : |
| 52 | TreeLanguage A := |
| 53 | {t | M.Accepts t} |
| 54 | |
| 55 | /-- A bottom-up tree automaton is deterministic when every symbol and ordered |
| 56 | tuple of child states has a unique resulting parent state. -/ |
| 57 | def Deterministic {A : RankedAlphabet.{u}} {Q : Type v} (M : Automaton A Q) : Prop := |
| 58 | ∀ (a : A.Symbol) (childStates : Fin (A.rank a) → Q), |
| 59 | ∃! q : Q, M.transition a q childStates = true |
| 60 | |
| 61 | end Automaton |
| 62 | |
| 63 | /-- Recognizability by a tree automaton with finitely many states. -/ |
| 64 | def Recognizable {A : RankedAlphabet.{u}} (L : TreeLanguage A) : Prop := |
| 65 | ∃ Q : Type, ∃ _ : Fintype Q, ∃ M : Automaton A Q, M.language = L |
| 66 | |
| 67 | end Lax53.TreeAutomaton |
| 68 |
Builds on
From Mathlib
none
Community review
Discussion
Ask a question or add context. Endorsements and structured flags are kept in the review panel above; your ORCID profile must share a public name.
0 comments