Lax53.TreeModelCheckingEncoding
Distinguished structural inputs for tree-automaton evaluation
concepts/Lax53/TreeModelCheckingEncoding.lean · lax-53
No public endorsements yet.
Loading review…
Sign in with ORCIDConcept map
Evidence
Each proof establishes this claim relative to its assumptions.
Definition and theorem
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.
Lean source view on GitHub
| 1 | import Lax53.StructuralRepresentations |
| 2 | |
| 3 | /-! |
| 4 | --- |
| 5 | title: Distinguished structural inputs for tree-automaton evaluation |
| 6 | type: definition and theorem |
| 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 Lax53.TreeModelCheckingEncoding |
| 22 | |
| 23 | open Lax53.RankedTree |
| 24 | open Lax53.ValueTranslations |
| 25 | open Lax53.StructuralRepresentations |
| 26 | open Lax58.StructuralPresentation |
| 27 | open Lax58.StructuralPresentation.Presentation |
| 28 | open Lax58.StructuralCombinators |
| 29 | open Lax58.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 | /-- Exact footprint of the distinguished structural machine input. -/ |
| 98 | axiom automatonInput_length (M : EncodedAutomaton) |
| 99 | (t : Tree M.1.toRankedAlphabet) : |
| 100 | (automatonInput M t).length = 3 * inputStructuralSize M t + 1 |
| 101 | |
| 102 | end Lax53.TreeModelCheckingEncoding |
| 103 |
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