Lax Lean Archive

Thatcher–Wright–Doner theorem for finite ranked trees

Lax842588.MSOTreeAutomataEquivalence · concepts/Lax842588/MSOTreeAutomataEquivalence.lean · lax-842588

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.

    Natural Language Statement

    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.

    Concept map
    6 concepts
    100%
    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.

    1 automaton_definable_by_mso proven

    2 mso_definable_is_recognizable proven

    3 recognizable_iff_msoDefinable proven

    Lean source view on GitHub

    1import Lax146103.MSOSyntax
    2import Lax842588.RankedTree
    3import Lax842588.TreeStructure
    4import Lax842588.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 Lax842588.MSOTreeAutomataEquivalence
    25
    26open Lax842588.RankedTree
    27open Lax842588.TreeStructure
    28open Lax842588.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 : Lax146103.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 : Lax146103.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 : Lax146103.MSOSyntax.Sentence (treeSignature A), L = sentenceLanguage phi
    47
    48end Lax842588.MSOTreeAutomataEquivalence
    49
    Show ProofShow ProofShow Proof
    Builds on
    Used by

    none

    From Mathlib

    none

    Discussion

    Ask a question or add context. Endorsements and structured flags are kept in the review panel above.

    Loading discussion…