Lax53.MSOLinearTime
Uniform word-RAM model checking for intrinsic MSO sentences
concepts/Lax53/MSOLinearTime.lean · lax-53
No public endorsements yet.
Loading review…
Sign in with ORCIDConcept map
Evidence
This concept declares 3 statements. Each proof establishes one of them relative to its assumptions.
1st statement exists_fixed_sentence_modelChecking proven
2nd statement exists_uniform_msoModelChecking proven
3rd statement modelCheckingInput_length proven
Definition and theorem
One fixed word-RAM program decides monadic second-order satisfaction when the ranked alphabet, the intrinsically scoped Lax-52 sentence, and the ranked tree are all supplied at runtime. Their sole machine input is the distinguished constructor-certified Lax-58 arena. The actual Lax-13 instruction bound includes all sentence-to-automaton compilation and tree-automaton evaluation.
The resource coefficients are computable functions only of the constructor size of the alphabet and sentence and of the largest symbol rank. This leaves the unavoidable nonelementary dependence on the sentence abstract while stating the uniform runtime in terms of mathematical sizes rather than a serialization. For a fixed alphabet and sentence, a separate companion program receives only the tree and runs linearly in its number of nodes.
The reusable Lax58 predicate packages the single program, every sufficient word width, and the payload/address/capacity premises. No constructor tags, arena offsets, compiled automata, or intermediate syntax belong to this concept.
Lean source view on GitHub
| 1 | import Mathlib.Computability.Partrec |
| 2 | import Lax58.RamComplexity |
| 3 | import Lax53.StructuralRepresentations |
| 4 | import Lax53.TreeModelCheckingEncoding |
| 5 | |
| 6 | /-! |
| 7 | --- |
| 8 | title: Uniform word-RAM model checking for intrinsic MSO sentences |
| 9 | type: definition and theorem |
| 10 | --- |
| 11 | |
| 12 | One fixed word-RAM program decides monadic second-order satisfaction when the |
| 13 | ranked alphabet, the intrinsically scoped Lax-52 sentence, and the ranked tree |
| 14 | are all supplied at runtime. Their sole machine input is the distinguished |
| 15 | constructor-certified Lax-58 arena. The actual Lax-13 instruction bound |
| 16 | includes all sentence-to-automaton compilation and tree-automaton evaluation. |
| 17 | |
| 18 | The resource coefficients are computable functions only of the constructor |
| 19 | size of the alphabet and sentence and of the largest symbol rank. This leaves |
| 20 | the unavoidable nonelementary dependence on the sentence abstract while |
| 21 | stating the uniform runtime in terms of mathematical sizes rather than a |
| 22 | serialization. For a fixed alphabet and sentence, a separate companion |
| 23 | program receives only the tree and runs linearly in its number of nodes. |
| 24 | |
| 25 | The reusable Lax58 predicate packages the single program, every sufficient |
| 26 | word width, and the payload/address/capacity premises. No constructor tags, |
| 27 | arena offsets, compiled automata, or intermediate syntax belong to this |
| 28 | concept. |
| 29 | -/ |
| 30 | |
| 31 | namespace Lax53.MSOLinearTime |
| 32 | |
| 33 | open Lax52.MSOSyntax |
| 34 | open Lax53.RankedTree |
| 35 | open Lax53.TreeStructure |
| 36 | open Lax53.ValueTranslations |
| 37 | open Lax53.StructuralRepresentations |
| 38 | open Lax53.TreeModelCheckingEncoding |
| 39 | open Lax58.StructuralPresentation |
| 40 | open Lax58.StructuralPresentation.Presentation |
| 41 | open Lax58.StructuralCombinators |
| 42 | open Lax58.WordArena |
| 43 | open Lax58.RamComplexity |
| 44 | |
| 45 | /-- Constructor size of an intrinsic MSO sentence, including its term and |
| 46 | relation fields but excluding any physical arena layout. -/ |
| 47 | def sentenceSize (alphabet : RankedAlphabetCode) |
| 48 | (phi : Sentence (treeSignature alphabet.toRankedAlphabet)) : Nat := |
| 49 | (formulaStructure alphabet phi).nodes |
| 50 | |
| 51 | /-- Mathematical parameter size controlling the formula-dependent part of |
| 52 | the uniform algorithm. Symbol arity is explicit because one natural payload |
| 53 | can prescribe an arbitrarily large finite family. -/ |
| 54 | def parameterSize (alphabet : RankedAlphabetCode) |
| 55 | (phi : Sentence (treeSignature alphabet.toRankedAlphabet)) : Nat := |
| 56 | (derivedPresentation : Presentation RankedAlphabetCode).structuralSize alphabet + |
| 57 | sentenceSize alphabet phi + maximumRank alphabet |
| 58 | |
| 59 | /-- A complete dependent model-checking input, bundled as one ordinary type |
| 60 | for use with the reusable Lax58 RAM-complexity predicate. -/ |
| 61 | structure ModelCheckingInstance where |
| 62 | alphabet : RankedAlphabetCode |
| 63 | sentence : Sentence (treeSignature alphabet.toRankedAlphabet) |
| 64 | tree : Tree alphabet.toRankedAlphabet |
| 65 | |
| 66 | /-- Complete constructor-derived content of one uniform model-checking |
| 67 | instance. The dependent typing of the sentence and tree is enforced before |
| 68 | this representation is formed. -/ |
| 69 | def msoTreeRaw (alphabet : RankedAlphabetCode) |
| 70 | (phi : Sentence (treeSignature alphabet.toRankedAlphabet)) |
| 71 | (t : Tree alphabet.toRankedAlphabet) : Raw := |
| 72 | Raw.constructor "msoModelChecking" |
| 73 | [(derivedPresentation : Presentation RankedAlphabetCode).toRaw alphabet, |
| 74 | formulaStructure alphabet phi, |
| 75 | treeStructure alphabet t] |
| 76 | |
| 77 | /-- Exact structural content of a bundled uniform model-checking input. -/ |
| 78 | def modelCheckingInstanceRaw (input : ModelCheckingInstance) : Raw := |
| 79 | msoTreeRaw input.alphabet input.sentence input.tree |
| 80 | |
| 81 | /-- Presentation used by the reusable RAM predicate. Its encoder is exactly |
| 82 | `msoTreeRaw`, so bundling introduces no tags, advice, or alternate layout. -/ |
| 83 | noncomputable def modelCheckingPresentation : |
| 84 | Presentation ModelCheckingInstance := |
| 85 | presentationOf modelCheckingInstanceRaw |
| 86 | |
| 87 | /-- Structural size of the complete uniform runtime input. -/ |
| 88 | def inputStructuralSize (alphabet : RankedAlphabetCode) |
| 89 | (phi : Sentence (treeSignature alphabet.toRankedAlphabet)) |
| 90 | (t : Tree alphabet.toRankedAlphabet) : Nat := |
| 91 | (msoTreeRaw alphabet phi t).nodes |
| 92 | |
| 93 | /-- Largest primitive natural payload in the complete uniform input. -/ |
| 94 | def inputPayloadMax (alphabet : RankedAlphabetCode) |
| 95 | (phi : Sentence (treeSignature alphabet.toRankedAlphabet)) |
| 96 | (t : Tree alphabet.toRankedAlphabet) : Nat := |
| 97 | (msoTreeRaw alphabet phi t).maxNat |
| 98 | |
| 99 | /-- Primitive payloads in the complete uniform input fit in a `w`-bit word. -/ |
| 100 | def InputPayloadsFitInWord (alphabet : RankedAlphabetCode) |
| 101 | (phi : Sentence (treeSignature alphabet.toRankedAlphabet)) |
| 102 | (t : Tree alphabet.toRankedAlphabet) (w : Nat) : Prop := |
| 103 | (msoTreeRaw alphabet phi t).PayloadsFitInWord w |
| 104 | |
| 105 | /-- Distinguished Lax-13 input containing the alphabet, intrinsic sentence, |
| 106 | and tree. -/ |
| 107 | def modelCheckingInput (alphabet : RankedAlphabetCode) |
| 108 | (phi : Sentence (treeSignature alphabet.toRankedAlphabet)) |
| 109 | (t : Tree alphabet.toRankedAlphabet) : List Nat := |
| 110 | (encodeRaw (msoTreeRaw alphabet phi t)).toInput |
| 111 | |
| 112 | /-- Exact footprint of the uniform model-checking input. -/ |
| 113 | axiom modelCheckingInput_length (alphabet : RankedAlphabetCode) |
| 114 | (phi : Sentence (treeSignature alphabet.toRankedAlphabet)) |
| 115 | (t : Tree alphabet.toRankedAlphabet) : |
| 116 | (modelCheckingInput alphabet phi t).length = |
| 117 | 3 * inputStructuralSize alphabet phi t + 1 |
| 118 | |
| 119 | /-- The actual instruction allowance for the uniform model checker. The |
| 120 | computable coefficient absorbs sentence compilation and the automaton |
| 121 | workload; the remaining dependence is linear in tree nodes. -/ |
| 122 | def uniformTimeBound (coefficient : Nat → Nat) |
| 123 | (alphabet : RankedAlphabetCode) |
| 124 | (phi : Sentence (treeSignature alphabet.toRankedAlphabet)) |
| 125 | (t : Tree alphabet.toRankedAlphabet) : Nat := |
| 126 | coefficient (parameterSize alphabet phi) * (treeSize t + 1) |
| 127 | |
| 128 | /-- Public word-resource allowance for the uniform implementation. -/ |
| 129 | def uniformWordBound (coefficient : Nat → Nat) |
| 130 | (alphabet : RankedAlphabetCode) |
| 131 | (phi : Sentence (treeSignature alphabet.toRankedAlphabet)) |
| 132 | (t : Tree alphabet.toRankedAlphabet) : Nat := |
| 133 | coefficient (parameterSize alphabet phi) * |
| 134 | (inputStructuralSize alphabet phi t + inputPayloadMax alphabet phi t + 1) |
| 135 | |
| 136 | open Classical in |
| 137 | /-- A single program handles every alphabet, intrinsic sentence, tree, and |
| 138 | sufficient word width. Formula compilation is part of this measured run. -/ |
| 139 | axiom exists_uniform_msoModelChecking : |
| 140 | ∃ timeCoefficient wordCoefficient : Nat → Nat, |
| 141 | Computable timeCoefficient ∧ Computable wordCoefficient ∧ |
| 142 | RamComputableWithinUsing modelCheckingPresentation natOutput |
| 143 | (fun input => if input.tree ∈ sentenceLanguage input.sentence then 1 else 0) |
| 144 | (fun input => uniformTimeBound timeCoefficient input.alphabet |
| 145 | input.sentence input.tree) |
| 146 | (fun input => uniformWordBound wordCoefficient input.alphabet |
| 147 | input.sentence input.tree) |
| 148 | |
| 149 | /-- Structural size of a tree-only fixed-parameter input. -/ |
| 150 | def treeStructuralSize (alphabet : RankedAlphabetCode) |
| 151 | (t : Tree alphabet.toRankedAlphabet) : Nat := |
| 152 | (treeStructure alphabet t).nodes |
| 153 | |
| 154 | /-- Largest primitive payload in a tree-only fixed-parameter input. -/ |
| 155 | def treePayloadMax (alphabet : RankedAlphabetCode) |
| 156 | (t : Tree alphabet.toRankedAlphabet) : Nat := |
| 157 | (treeStructure alphabet t).maxNat |
| 158 | |
| 159 | /-- Primitive tree payloads fit in a `w`-bit word. -/ |
| 160 | def TreePayloadsFitInWord (alphabet : RankedAlphabetCode) |
| 161 | (t : Tree alphabet.toRankedAlphabet) (w : Nat) : Prop := |
| 162 | (treeStructure alphabet t).PayloadsFitInWord w |
| 163 | |
| 164 | /-- Distinguished tree-only input for a program specialized to a fixed |
| 165 | alphabet and sentence. -/ |
| 166 | def treeInput (alphabet : RankedAlphabetCode) |
| 167 | (t : Tree alphabet.toRankedAlphabet) : List Nat := |
| 168 | (encodeRaw (treeStructure alphabet t)).toInput |
| 169 | |
| 170 | open Classical in |
| 171 | /-- Once the alphabet and sentence are fixed before program choice, the |
| 172 | specialized program receives only a tree and has linear tree-node time. This |
| 173 | existential statement makes no effective program-generation claim. -/ |
| 174 | axiom exists_fixed_sentence_modelChecking |
| 175 | (alphabet : RankedAlphabetCode) |
| 176 | (phi : Sentence (treeSignature alphabet.toRankedAlphabet)) : |
| 177 | ∃ timeCoefficient wordCoefficient : Nat, |
| 178 | RamComputableWithinUsing (treePresentation alphabet) natOutput |
| 179 | (fun t => if t ∈ sentenceLanguage phi then 1 else 0) |
| 180 | (fun t => timeCoefficient * (treeSize t + 1)) |
| 181 | (fun t => wordCoefficient * inputMagnitudeUsing |
| 182 | (treePresentation alphabet) t) |
| 183 | |
| 184 | end Lax53.MSOLinearTime |
| 185 |
Used by
none
From Mathlib
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