Lax Lean Archive

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

Lax132576.LengthPreservingTyping

Length preservation through a typing of the states

concepts/Lax132576/LengthPreservingTyping.lean · lax-132576

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

    Fix an automaton with output computing a function ff, all of whose states are productive. A typing is a function τ:Q→Z\tau : Q \to \mathbb{Z} such that every run from an initial state to a state qq satisfies

    ∣output∣=∣input∣+τ(q).|\text{output}| = |\text{input}| + \tau(q).

    The function ff is length preserving if and only if a typing exists and maps every accepting state to zero (Claim B.4.4 of Transducers). If no typing exists, two runs reach the same state with different length differences and the function cannot be length preserving; if a typing exists but some accepting state has nonzero type, a run reaching it witnesses the same.

    Lean source view on GitHub

    1import Lax765601.ElementaryProperties
    2import Lax132576.RationalRelations
    3
    4/-!
    5---
    6title: Length preservation through a typing of the states
    7type: theorem
    8---
    9Fix an automaton with output computing a function ff, all of whose states are
    10productive. A *typing* is a function τ:Q→Z\tau : Q \to \mathbb{Z} such that every
    11run from an initial state to a state qq satisfies
    12∣output∣=∣input∣+τ(q).|\text{output}| = |\text{input}| + \tau(q).
    13The function ff is length preserving if and only if a typing exists and maps
    14every accepting state to zero (Claim B.4.4 of *Transducers*). If no typing
    15exists, two runs reach the same state with different length differences and
    16the function cannot be length preserving; if a typing exists but some accepting
    17state has nonzero type, a run reaching it witnesses the same.
    18
    19# Formalization notes
    20
    21The automaton `M` computes `f` in the sense that its relation is the graph of
    22`f`; productivity of all states is a hypothesis, as the book assumes
    23implicitly. Runs are paths from an initial state, and the typing condition is
    24stated for all of them.
    25-/
    26
    27namespace Lax132576.LengthPreservingTyping
    28
    29open Lax765601.ElementaryProperties Lax132576.LabelledAutomata Lax132576.RationalRelations
    30
    31/-- A function computed by an automaton with output with productive states is length
    32preserving if and only if the automaton has a typing vanishing on the accepting
    33states. -/
    34axiom lengthPreserving_iff_typing {A B Q : Type} (M : NFAO A B Q)
    35 (hprod : ∀ q, M.Productive q) {f : List A → List B} (hM : ∀ w v, M.rel w v ↔ v = f w) :
    36 LengthPreserving f ↔
    37 ∃ τ : Q → ℤ,
    38 (∀ q ∈ M.init, ∀ ts p, M.Path q ts p →
    39 ((NFAO.outputOf ts).length : ℤ) = (LabAut.inputOf ts).length + τ p) ∧
    40 ∀ p ∈ M.final, τ p = 0
    41
    42end Lax132576.LengthPreservingTyping
    43
    Show Proof

    Formalization notes

    The automaton MM computes ff in the sense that its relation is the graph of ff; productivity of all states is a hypothesis, as the book assumes implicitly. Runs are paths from an initial state, and the typing condition is stated for all of them.

    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…