Lax Lean Archive

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

Lax53.MSOTreeAutomataEquivalence

Thatcher–Wright–Doner theorem for finite ranked trees

concepts/Lax53/MSOTreeAutomataEquivalence.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

    This concept declares 3 statements. Each proof establishes one of them relative to its assumptions.

    1st statement automaton_definable_by_mso proven

    2nd statement mso_definable_is_recognizable proven

    3rd statement recognizable_iff_msoDefinable proven

    Theorem

    Over a finite ranked alphabet, a language of finite ranked trees is recognizable by a bottom-up tree automaton with finitely many states if and only if it is definable by a monadic second-order sentence in the relational tree structure with unary label predicates and indexed child relations. This is the ranked-tree automata–MSO characterization proved by Thatcher and Wright (1968) and, independently, by Doner (1970).

    The two directions are stated explicitly here as well: every automaton has an equivalent MSO sentence, and every MSO sentence defines a recognizable language.

    Lean source view on GitHub

    1import Lax52.MSOSyntax
    2import Lax53.RankedTree
    3import Lax53.TreeStructure
    4import Lax53.TreeAutomaton
    5
    6/-!
    7---
    8title: Thatcher–Wright–Doner theorem for finite ranked trees
    9type: theorem
    10---
    11
    12Over a finite ranked alphabet, a language of finite ranked trees is recognizable
    13by a bottom-up tree automaton with finitely many states if and only if it is
    14definable by a monadic second-order sentence in the relational tree structure
    15with unary label predicates and indexed child relations. This is the ranked-tree
    16automata--MSO characterization proved by Thatcher and Wright (1968) and,
    17independently, by Doner (1970).
    18
    19The two directions are stated explicitly here as well: every automaton has
    20an equivalent MSO sentence, and every MSO sentence defines a recognizable
    21language.
    22-/
    23
    24namespace Lax53.MSOTreeAutomataEquivalence
    25
    26open Lax53.RankedTree
    27open Lax53.TreeStructure
    28open Lax53.TreeAutomaton
    29
    30universe u v
    31
    32/-- Every tree automaton with finitely many states has an equivalent MSO sentence. -/
    33axiom automaton_definable_by_mso {A : RankedAlphabet.{u}} {Q : Type v}
    34 [Fintype Q] (M : Automaton A Q) :
    35 ∃ phi : Lax52.MSOSyntax.Sentence (treeSignature A), M.language = sentenceLanguage phi
    36
    37/-- Every MSO sentence defines a recognizable ranked-tree language. -/
    38axiom mso_definable_is_recognizable {A : RankedAlphabet.{u}}
    39 (phi : Lax52.MSOSyntax.Sentence (treeSignature A)) :
    40 Recognizable (sentenceLanguage phi)
    41
    42/-- Recognizability and MSO definability characterize the same languages. -/
    43axiom recognizable_iff_msoDefinable {A : RankedAlphabet.{u}}
    44 (L : TreeLanguage A) :
    45 Recognizable L ↔
    46 ∃ phi : Lax52.MSOSyntax.Sentence (treeSignature A), L = sentenceLanguage phi
    47
    48end Lax53.MSOTreeAutomataEquivalence
    49
    Show ProofShow ProofShow Proof

    Builds on

    Used by

    none

    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…