Lax Lean Archive

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

Lax916827.TwoWayContinuity

Two-way transducers are continuous

concepts/Lax916827/TwoWayContinuity.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

    Every function computed by a two-way transducer is continuous (Theorem C.2.2 of Transducers, Rabin–Scott and Shepherdson). The book computes the reachable configuration graph by a rational function (Lemma C.2.3) and checks membership of the output in a regular language on the representation (Lemma C.2.4); a direct proof runs a deterministic automaton for the output language inside the transducer, turning it into a two-way automaton, whose language is regular by Shepherdson's theorem.

    Lean source view on GitHub

    1import Lax765601.Continuity
    2import Lax916827.TwoWayTransducers
    3
    4/-!
    5---
    6title: Two-way transducers are continuous
    7type: theorem
    8---
    9Every function computed by a two-way transducer is continuous (Theorem C.2.2 of
    10*Transducers*, Rabin–Scott and Shepherdson). The book computes the reachable
    11configuration graph by a rational function (Lemma C.2.3) and checks membership
    12of the output in a regular language on the representation (Lemma C.2.4); a
    13direct proof runs a deterministic automaton for the output language inside the
    14transducer, turning it into a two-way automaton, whose language is regular by
    15Shepherdson's theorem.
    16
    17# Formalization notes
    18
    19Both alphabets are assumed finite, as in the book.
    20-/
    21
    22namespace Lax916827.TwoWayContinuity
    23
    24open Lax765601.Continuity Lax916827.TwoWayTransducers
    25
    26/-- A function computed by a two-way transducer is continuous. -/
    27axiom continuous_of_isTwoWay {A B : Type} [Finite A] [Finite B] {f : List A → List B}
    28 (hf : IsTwoWay f) : Continuous f
    29
    30end Lax916827.TwoWayContinuity
    31
    Show Proof

    Formalization notes

    Both alphabets are assumed finite, as in the book.

    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…