Value-level translations between MSO and tree automata
Lax842588.ValueTranslations · concepts/Lax842588/ValueTranslations.lean · lax-842588
No public endorsements yet.
Loading review…
Sign in with ORCIDNatural Language Statement
Theorem
A finite ranked alphabet is described by the finite list of its symbol ranks; symbols are numbered by their positions in that list. Automata use finite lists of numbered transitions, while MSO formulas are represented directly by their inductive syntax.
There are mathematical translations between finite automaton values and the intrinsically scoped MSO sentences of . The ranked alphabet is an explicit parameter shared by source and target, so preservation of it is enforced by the types. This statement is deliberately independent of computability, serialization, memory layout, and a machine model; its algorithmic realization and word-RAM execution are stated separately.
Concept map
Evidence
Each proof establishes this claim relative to its assumptions.
Lean source view on GitHub
| 1 | import Lax146103.MSOSyntax |
| 2 | import Lax842588.RankedTree |
| 3 | import Lax842588.TreeStructure |
| 4 | import Lax842588.TreeAutomaton |
| 5 | |
| 6 | /-! |
| 7 | --- |
| 8 | title: Value-level translations between MSO and tree automata |
| 9 | type: theorem |
| 10 | --- |
| 11 | |
| 12 | A finite ranked alphabet is described by the finite list of its symbol ranks; |
| 13 | symbols are numbered by their positions in that list. Automata use finite |
| 14 | lists of numbered transitions, while MSO formulas are represented directly by |
| 15 | their inductive syntax. |
| 16 | |
| 17 | There are mathematical translations between finite automaton values and the |
| 18 | intrinsically scoped MSO sentences of `lax-52`. The ranked alphabet is an |
| 19 | explicit parameter shared by source and target, so preservation of it is |
| 20 | enforced by the types. This statement is deliberately independent of |
| 21 | computability, serialization, memory layout, and a machine model; its |
| 22 | algorithmic realization and word-RAM execution are stated separately. |
| 23 | -/ |
| 24 | |
| 25 | namespace Lax842588.ValueTranslations |
| 26 | |
| 27 | open Lax146103.MSOSyntax |
| 28 | open Lax842588.RankedTree |
| 29 | open Lax842588.TreeStructure |
| 30 | open Lax842588.TreeAutomaton |
| 31 | |
| 32 | /-- A finite sequence of natural-number words. This is a carrier type, not a |
| 33 | serialization contract. -/ |
| 34 | abbrev CodeString := List Nat |
| 35 | |
| 36 | /-- A finite ranked alphabet is described by listing the ranks of its symbols. |
| 37 | The symbol in position `i` has rank `code[i]`. -/ |
| 38 | abbrev RankedAlphabetCode := List Nat |
| 39 | |
| 40 | namespace RankedAlphabetCode |
| 41 | |
| 42 | /-- The canonical ranked alphabet represented by a rank string. -/ |
| 43 | def toRankedAlphabet (code : RankedAlphabetCode) : RankedAlphabet where |
| 44 | Symbol := Fin code.length |
| 45 | symbolsFintype := inferInstance |
| 46 | symbolsDecidableEq := inferInstance |
| 47 | rank i := code.get i |
| 48 | |
| 49 | end RankedAlphabetCode |
| 50 | |
| 51 | /-- A finite transition consists of a symbol number, a parent-state number, |
| 52 | and the ordered list of child-state numbers. -/ |
| 53 | abbrev TransitionCode := Nat × Nat × List Nat |
| 54 | |
| 55 | /-- An automaton body consists of its number of states, transition list, and |
| 56 | accepting-state list. Its ranked alphabet is supplied separately. -/ |
| 57 | abbrev AutomatonCode := Nat × List TransitionCode × List Nat |
| 58 | |
| 59 | /-- A represented automaton packages its ranked alphabet with its body. -/ |
| 60 | abbrev EncodedAutomaton := RankedAlphabetCode × AutomatonCode |
| 61 | |
| 62 | namespace AutomatonCode |
| 63 | |
| 64 | /-- The tree automaton denoted by an automaton body over an encoded |
| 65 | ranked alphabet. Out-of-range states and malformed transitions are ignored. -/ |
| 66 | def toAutomaton (alphabet : RankedAlphabetCode) (M : AutomatonCode) : |
| 67 | Automaton alphabet.toRankedAlphabet (Fin M.1) where |
| 68 | transition a q childStates := |
| 69 | M.2.1.any fun tr => |
| 70 | decide (tr.1 = a.val ∧ tr.2.1 = q.val ∧ |
| 71 | tr.2.2 = List.ofFn (fun i => (childStates i).val)) |
| 72 | accept q := M.2.2.contains q.val |
| 73 | |
| 74 | /-- The ranked-tree language denoted by an automaton body over an encoded |
| 75 | ranked alphabet. -/ |
| 76 | def language (alphabet : RankedAlphabetCode) (M : AutomatonCode) : |
| 77 | TreeLanguage alphabet.toRankedAlphabet := |
| 78 | (M.toAutomaton alphabet).language |
| 79 | |
| 80 | end AutomatonCode |
| 81 | |
| 82 | /-- Value-level translations preserve the alphabet and denoted language in |
| 83 | both directions. Their domains are finite automaton values and the existing |
| 84 | intrinsic sentence syntax, not a second formula datatype. No physical |
| 85 | representation or algorithmic claim is part of this mathematical statement. -/ |
| 86 | axiom language_equivalence : |
| 87 | (∃ automatonToMSO : (alphabet : RankedAlphabetCode) → AutomatonCode → |
| 88 | Sentence (treeSignature alphabet.toRankedAlphabet), |
| 89 | ∀ alphabet M, |
| 90 | AutomatonCode.language alphabet M = |
| 91 | sentenceLanguage (automatonToMSO alphabet M)) ∧ |
| 92 | (∃ msoToAutomaton : (alphabet : RankedAlphabetCode) → |
| 93 | Sentence (treeSignature alphabet.toRankedAlphabet) → AutomatonCode, |
| 94 | ∀ alphabet phi, |
| 95 | AutomatonCode.language alphabet (msoToAutomaton alphabet phi) = |
| 96 | sentenceLanguage phi) |
| 97 | |
| 98 | end Lax842588.ValueTranslations |
| 99 |
From Mathlib
none
Discussion
Ask a question or add context. Endorsements and structured flags are kept in the review panel above.
0 comments