Uniform word-RAM model checking for intrinsic MSO sentences
Lax842588.MSOLinearTime · concepts/Lax842588/MSOLinearTime.lean · lax-842588
No public endorsements yet.
Loading review…
Sign in with ORCIDNatural Language Statement
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 Lax560851 arena. The actual Lax808846 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 Lax560851 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.
Concept map
Evidence
Each proof establishes this claim relative to its assumptions.
Lean source view on GitHub
| 1 | import Mathlib.Computability.Partrec |
| 2 | import Lax560851.RamComplexity |
| 3 | import Lax842588.StructuralRepresentations |
| 4 | import Lax842588.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 Lax560851 arena. The actual Lax808846 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 Lax560851 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 Lax842588.MSOLinearTime |
| 32 | |
| 33 | open Lax146103.MSOSyntax |
| 34 | open Lax842588.RankedTree |
| 35 | open Lax842588.TreeStructure |
| 36 | open Lax842588.ValueTranslations |
| 37 | open Lax842588.StructuralRepresentations |
| 38 | open Lax842588.TreeModelCheckingEncoding |
| 39 | open Lax560851.StructuralPresentation |
| 40 | open Lax560851.StructuralPresentation.Presentation |
| 41 | open Lax560851.StructuralCombinators |
| 42 | open Lax560851.WordArena |
| 43 | open Lax560851.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 Lax560851 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 Lax808846 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 | /-- The actual instruction allowance for the uniform model checker. The |
| 113 | computable coefficient absorbs sentence compilation and the automaton |
| 114 | workload; the remaining dependence is linear in tree nodes. -/ |
| 115 | def uniformTimeBound (coefficient : Nat → Nat) |
| 116 | (alphabet : RankedAlphabetCode) |
| 117 | (phi : Sentence (treeSignature alphabet.toRankedAlphabet)) |
| 118 | (t : Tree alphabet.toRankedAlphabet) : Nat := |
| 119 | coefficient (parameterSize alphabet phi) * (treeSize t + 1) |
| 120 | |
| 121 | /-- Public word-resource allowance for the uniform implementation. -/ |
| 122 | def uniformWordBound (coefficient : Nat → Nat) |
| 123 | (alphabet : RankedAlphabetCode) |
| 124 | (phi : Sentence (treeSignature alphabet.toRankedAlphabet)) |
| 125 | (t : Tree alphabet.toRankedAlphabet) : Nat := |
| 126 | coefficient (parameterSize alphabet phi) * |
| 127 | (inputStructuralSize alphabet phi t + inputPayloadMax alphabet phi t + 1) |
| 128 | |
| 129 | open Classical in |
| 130 | /-- A single program handles every alphabet, intrinsic sentence, tree, and |
| 131 | sufficient word width. Formula compilation is part of this measured run. -/ |
| 132 | axiom exists_uniform_msoModelChecking : |
| 133 | ∃ timeCoefficient wordCoefficient : Nat → Nat, |
| 134 | Computable timeCoefficient ∧ Computable wordCoefficient ∧ |
| 135 | RamComputableWithinUsing modelCheckingPresentation natOutput |
| 136 | (fun input => if input.tree ∈ sentenceLanguage input.sentence then 1 else 0) |
| 137 | (fun input => uniformTimeBound timeCoefficient input.alphabet |
| 138 | input.sentence input.tree) |
| 139 | (fun input => uniformWordBound wordCoefficient input.alphabet |
| 140 | input.sentence input.tree) |
| 141 | |
| 142 | /-- Structural size of a tree-only fixed-parameter input. -/ |
| 143 | def treeStructuralSize (alphabet : RankedAlphabetCode) |
| 144 | (t : Tree alphabet.toRankedAlphabet) : Nat := |
| 145 | (treeStructure alphabet t).nodes |
| 146 | |
| 147 | /-- Largest primitive payload in a tree-only fixed-parameter input. -/ |
| 148 | def treePayloadMax (alphabet : RankedAlphabetCode) |
| 149 | (t : Tree alphabet.toRankedAlphabet) : Nat := |
| 150 | (treeStructure alphabet t).maxNat |
| 151 | |
| 152 | /-- Primitive tree payloads fit in a `w`-bit word. -/ |
| 153 | def TreePayloadsFitInWord (alphabet : RankedAlphabetCode) |
| 154 | (t : Tree alphabet.toRankedAlphabet) (w : Nat) : Prop := |
| 155 | (treeStructure alphabet t).PayloadsFitInWord w |
| 156 | |
| 157 | /-- Distinguished tree-only input for a program specialized to a fixed |
| 158 | alphabet and sentence. -/ |
| 159 | def treeInput (alphabet : RankedAlphabetCode) |
| 160 | (t : Tree alphabet.toRankedAlphabet) : List Nat := |
| 161 | (encodeRaw (treeStructure alphabet t)).toInput |
| 162 | |
| 163 | end Lax842588.MSOLinearTime |
| 164 |
Builds on
Used by
none
From Mathlib
Discussion
Ask a question or add context. Endorsements and structured flags are kept in the review panel above.
0 comments