Distinguished structural inputs for tree-automaton evaluation
Lax842588.TreeModelCheckingEncoding · concepts/Lax842588/TreeModelCheckingEncoding.lean · lax-842588
No public endorsements yet.
Loading review…
Sign in with ORCIDNatural Language Statement
Definition
An automaton together with a ranked tree is represented by one fixed constructor whose two fields use the certified structural presentations of automata and trees. This complete equation determines the entire represented content and therefore permits no compiled table, traversal order, semantic annotation, or other advice.
The physical word-RAM input is the distinguished input tape of this structural value: its root word followed by its immutable arena. The exact input length is three words per structural node plus the root word. No specialized evaluator layout is part of this concept.
Concept map
Lean source view on GitHub
| 1 | import Lax842588.StructuralRepresentations |
| 2 | |
| 3 | /-! |
| 4 | --- |
| 5 | title: Distinguished structural inputs for tree-automaton evaluation |
| 6 | type: definition |
| 7 | --- |
| 8 | |
| 9 | An automaton together with a ranked tree is represented by one fixed |
| 10 | constructor whose two fields use the certified structural presentations of |
| 11 | automata and trees. This complete equation determines the entire represented |
| 12 | content and therefore permits no compiled table, traversal order, semantic |
| 13 | annotation, or other advice. |
| 14 | |
| 15 | The physical word-RAM input is the distinguished `lax-58` input tape of this |
| 16 | structural value: its root word followed by its immutable arena. The exact |
| 17 | input length is three words per structural node plus the root word. No |
| 18 | specialized evaluator layout is part of this concept. |
| 19 | -/ |
| 20 | |
| 21 | namespace Lax842588.TreeModelCheckingEncoding |
| 22 | |
| 23 | open Lax842588.RankedTree |
| 24 | open Lax842588.ValueTranslations |
| 25 | open Lax842588.StructuralRepresentations |
| 26 | open Lax560851.StructuralPresentation |
| 27 | open Lax560851.StructuralPresentation.Presentation |
| 28 | open Lax560851.StructuralCombinators |
| 29 | open Lax560851.WordArena |
| 30 | |
| 31 | /-- Number of constructor occurrences in a ranked tree. -/ |
| 32 | def treeSize {A : RankedAlphabet} : Tree A → Nat |
| 33 | | .node _ children => |
| 34 | 1 + (List.ofFn fun i => treeSize (children i)).sum |
| 35 | |
| 36 | /-- Structural size of the certified automaton representation. -/ |
| 37 | def automatonSize (M : EncodedAutomaton) : Nat := |
| 38 | StructuralRepresentations.automatonPresentation.structuralSize M |
| 39 | |
| 40 | /-- Largest symbol rank in a finite encoded alphabet. This is mathematical |
| 41 | alphabet data, independently of any evaluator representation. -/ |
| 42 | def maximumRank (alphabet : RankedAlphabetCode) : Nat := |
| 43 | alphabet.foldl max 0 |
| 44 | |
| 45 | /-- A runtime instance for uniform tree-automaton acceptance. Bundling the |
| 46 | dependent tree with its automaton makes the complete input an ordinary type |
| 47 | that can be passed to reusable complexity predicates. -/ |
| 48 | structure AutomatonAcceptanceInstance where |
| 49 | automaton : EncodedAutomaton |
| 50 | tree : Tree automaton.1.toRankedAlphabet |
| 51 | |
| 52 | /-- Complete advice-free structural content of an automaton-evaluation |
| 53 | instance. Both fields use named, constructor-certified presentations. -/ |
| 54 | def automatonTreeRaw (M : EncodedAutomaton) |
| 55 | (t : Tree M.1.toRankedAlphabet) : Raw := |
| 56 | Raw.constructor "automatonAcceptance" |
| 57 | [StructuralRepresentations.automatonPresentation.toRaw M, |
| 58 | StructuralRepresentations.treeStructure M.1 t] |
| 59 | |
| 60 | /-- The complete certified content of a bundled uniform acceptance input. -/ |
| 61 | def automatonAcceptanceRaw (input : AutomatonAcceptanceInstance) : Raw := |
| 62 | automatonTreeRaw input.automaton input.tree |
| 63 | |
| 64 | /-- Explicit presentation used by the uniform reusable RAM predicate. Its |
| 65 | encoder is exactly `automatonTreeRaw`; no evaluator-specific data is added. -/ |
| 66 | noncomputable def automatonAcceptancePresentation : |
| 67 | Presentation AutomatonAcceptanceInstance := |
| 68 | presentationOf automatonAcceptanceRaw |
| 69 | |
| 70 | /-- Explicit presentation for the old fixed-automaton input convention. The |
| 71 | fixed automaton remains physically present, exactly as in `automatonInput`. -/ |
| 72 | noncomputable def fixedAutomatonPresentation (M : EncodedAutomaton) : |
| 73 | Presentation (Tree M.1.toRankedAlphabet) := |
| 74 | presentationOf (automatonTreeRaw M) |
| 75 | |
| 76 | /-- Structural size of the complete runtime input. -/ |
| 77 | def inputStructuralSize (M : EncodedAutomaton) |
| 78 | (t : Tree M.1.toRankedAlphabet) : Nat := |
| 79 | (automatonTreeRaw M t).nodes |
| 80 | |
| 81 | /-- All primitive natural payloads in the complete runtime input fit in one |
| 82 | `w`-bit word. -/ |
| 83 | def InputPayloadsFitInWord (M : EncodedAutomaton) |
| 84 | (t : Tree M.1.toRankedAlphabet) (w : Nat) : Prop := |
| 85 | (automatonTreeRaw M t).PayloadsFitInWord w |
| 86 | |
| 87 | /-- Largest primitive natural payload in the complete structural input. -/ |
| 88 | def inputPayloadMax (M : EncodedAutomaton) |
| 89 | (t : Tree M.1.toRankedAlphabet) : Nat := |
| 90 | (automatonTreeRaw M t).maxNat |
| 91 | |
| 92 | /-- The unique machine input admitted by the runtime theorem. -/ |
| 93 | def automatonInput (M : EncodedAutomaton) |
| 94 | (t : Tree M.1.toRankedAlphabet) : List Nat := |
| 95 | (encodeRaw (automatonTreeRaw M t)).toInput |
| 96 | |
| 97 | end Lax842588.TreeModelCheckingEncoding |
| 98 |
Builds on
From Mathlib
none
Discussion
Ask a question or add context. Endorsements and structured flags are kept in the review panel above.
0 comments