Lax Lean Archive

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

Lax916827.ConfigurationGraphOutput

Checking the output of a configuration graph against a regular language

concepts/Lax916827/ConfigurationGraphOutput.lean · lax-916827

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.

    In the paper

    Theorem

    For a regular language LL over the output alphabet, the set of strings over CC that represent a reachable configuration graph whose output string belongs to LL is a regular language (Lemma C.2.4 of Transducers). An automaton checks that the string is a representation and guesses a labelling of the edges of the represented path by transitions of an automaton for LL.

    Lean source view on GitHub

    1import Mathlib.Computability.DFA
    2import Lax916827.ConfigurationGraphs
    3
    4/-!
    5---
    6title: Checking the output of a configuration graph against a regular language
    7type: theorem
    8---
    9For a regular language LL over the output alphabet, the set of strings over
    10CC that represent a reachable configuration graph whose output string belongs
    11to LL is a regular language (Lemma C.2.4 of *Transducers*). An automaton
    12checks that the string is a representation and guesses a labelling of the edges
    13of the represented path by transitions of an automaton for LL.
    14
    15# Formalization notes
    16
    17The output string of a representation is the string printed by the transducer
    18`pathTrans M` walking along the represented path; on the representation of the
    19graph of `M` on `w` it is the output of `M` on `w`. As in the book, the
    20transducer is assumed to compute a total function `f`, so that every
    21representation has an output.
    22-/
    23
    24namespace Lax916827.ConfigurationGraphOutput
    25
    26open Lax916827.TwoWayTransducers Lax916827.ConfigurationGraphs
    27
    28/-- The representations of reachable configuration graphs whose output lies in a
    29regular language form a regular language. -/
    30axiom isRegular_encOutputLang {A B Q : Type} [Finite A] [Finite Q] (M : TwoWay A B Q)
    31 {f : List A → List B} (hM : ∀ w, M.Computes w (f w)) {L : Language B} (hL : L.IsRegular) :
    32 Language.IsRegular {u : List (CLet Q (TwoWay.Lab M)) |
    33 (∃ w, u = TwoWay.enc M w) ∧ ∃ v, (TwoWay.pathTrans M).Computes u v ∧ v ∈ L}
    34
    35end Lax916827.ConfigurationGraphOutput
    36
    Show Proof

    Formalization notes

    The output string of a representation is the string printed by the transducer pathTransMpathTrans M walking along the represented path; on the representation of the graph of MM on ww it is the output of MM on ww. As in the book, the transducer is assumed to compute a total function ff, so that every representation has an output.

    Builds on

    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

    Loading discussion…