Lax Lean Archive

Draft — mutable and not usable as a dependency; its citation marks the draft state.

Lax53.ValueTranslations

Value-level translations between MSO and tree automata

concepts/Lax53/ValueTranslations.lean · lax-53

proven

Loading review…

Community review

Flags

Each flag is tied to a public ORCID identity and explains why this concept may be incorrect.

No flags have been submitted.

    Community review

    Flag this concept

    State precisely what appears incorrect. This explanation will be public under your ORCID name.

    No source line selected.

    Concept map

    Proven claimDefinitionThis conceptRelated conceptA → B: B builds on A

    Evidence

    Each proof establishes this claim relative to its assumptions.

    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 lax−52lax-52. 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.

    Lean source view on GitHub

    1import Lax52.MSOSyntax
    2import Lax53.RankedTree
    3import Lax53.TreeStructure
    4import Lax53.TreeAutomaton
    5
    6/-!
    7---
    8title: Value-level translations between MSO and tree automata
    9type: theorem
    10---
    11
    12A finite ranked alphabet is described by the finite list of its symbol ranks;
    13symbols are numbered by their positions in that list. Automata use finite
    14lists of numbered transitions, while MSO formulas are represented directly by
    15their inductive syntax.
    16
    17There are mathematical translations between finite automaton values and the
    18intrinsically scoped MSO sentences of `lax-52`. The ranked alphabet is an
    19explicit parameter shared by source and target, so preservation of it is
    20enforced by the types. This statement is deliberately independent of
    21computability, serialization, memory layout, and a machine model; its
    22algorithmic realization and word-RAM execution are stated separately.
    23-/
    24
    25namespace Lax53.ValueTranslations
    26
    27open Lax52.MSOSyntax
    28open Lax53.RankedTree
    29open Lax53.TreeStructure
    30open Lax53.TreeAutomaton
    31
    32/-- A finite sequence of natural-number words. This is a carrier type, not a
    33serialization contract. -/
    34abbrev CodeString := List Nat
    35
    36/-- A finite ranked alphabet is described by listing the ranks of its symbols.
    37The symbol in position `i` has rank `code[i]`. -/
    38abbrev RankedAlphabetCode := List Nat
    39
    40namespace RankedAlphabetCode
    41
    42/-- The canonical ranked alphabet represented by a rank string. -/
    43def toRankedAlphabet (code : RankedAlphabetCode) : RankedAlphabet where
    44 Symbol := Fin code.length
    45 symbolsFintype := inferInstance
    46 symbolsDecidableEq := inferInstance
    47 rank i := code.get i
    48
    49end RankedAlphabetCode
    50
    51/-- A finite transition consists of a symbol number, a parent-state number,
    52and the ordered list of child-state numbers. -/
    53abbrev TransitionCode := Nat × Nat × List Nat
    54
    55/-- An automaton body consists of its number of states, transition list, and
    56accepting-state list. Its ranked alphabet is supplied separately. -/
    57abbrev AutomatonCode := Nat × List TransitionCode × List Nat
    58
    59/-- A represented automaton packages its ranked alphabet with its body. -/
    60abbrev EncodedAutomaton := RankedAlphabetCode × AutomatonCode
    61
    62namespace AutomatonCode
    63
    64/-- The tree automaton denoted by an automaton body over an encoded
    65ranked alphabet. Out-of-range states and malformed transitions are ignored. -/
    66def 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
    75ranked alphabet. -/
    76def language (alphabet : RankedAlphabetCode) (M : AutomatonCode) :
    77 TreeLanguage alphabet.toRankedAlphabet :=
    78 (M.toAutomaton alphabet).language
    79
    80end AutomatonCode
    81
    82/-- Value-level translations preserve the alphabet and denoted language in
    83both directions. Their domains are finite automaton values and the existing
    84intrinsic sentence syntax, not a second formula datatype. No physical
    85representation or algorithmic claim is part of this mathematical statement. -/
    86axiom 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
    98end Lax53.ValueTranslations
    99
    Show Proof

    Builds on

    Used by

    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

    Loading discussion…