Lax Lean Archive

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

Lax132576.EpsilonEliminationFinite

Elimination of ε-transitions for finitely valued relations

concepts/Lax132576/EpsilonEliminationFinite.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

    If a rational relation is such that every input string has finitely many outputs, then it is computed by an ordinary automaton with output in ε-free normal form: extended transitions are not needed (Lemma B.2.4 of Transducers, second sentence). In the elimination construction, the regular languages labelling the new transitions are then finite, and each such transition is replaced by finitely many transitions with one output string each.

    Lean source view on GitHub

    1import Lax132576.EpsilonFreeAutomata
    2
    3/-!
    4---
    5title: Elimination of ε-transitions for finitely valued relations
    6type: theorem
    7---
    8If a rational relation is such that every input string has finitely many
    9outputs, then it is computed by an ordinary automaton with output in ε-free
    10normal form: extended transitions are not needed (Lemma B.2.4 of
    11*Transducers*, second sentence). In the elimination construction, the regular
    12languages labelling the new transitions are then finite, and each such
    13transition is replaced by finitely many transitions with one output string
    14each.
    15
    16# Formalization notes
    17
    18The finiteness of the set of outputs of every input is the hypothesis
    19`∀ w, {v | R w v}.Finite`; the automaton is an ordinary `NFAO` and the normal
    20form is `EpsilonFree`. Both alphabets are assumed finite.
    21-/
    22
    23namespace Lax132576.EpsilonEliminationFinite
    24
    25open Lax132576.RationalRelations Lax132576.EpsilonFreeAutomata
    26
    27/-- A finitely valued rational relation is computed by an ε-free automaton with
    28output. -/
    29axiom exists_nfao_epsilonFree {A B : Type} [Finite A] [Finite B]
    30 {R : List A → List B → Prop} (hR : IsRationalRel R) (hfin : ∀ w, {v | R w v}.Finite) :
    31 ∃ (Q : Type) (_ : Finite Q) (M : NFAO A B Q), EpsilonFree M ∧ ∀ w v, R w v ↔ M.rel w v
    32
    33end Lax132576.EpsilonEliminationFinite
    34
    Show Proof

    Formalization notes

    The finiteness of the set of outputs of every input is the hypothesis ∀w,v∣Rwv.Finite∀ w, {v | R w v}.Finite; the automaton is an ordinary NFAONFAO and the normal form is EpsilonFreeEpsilonFree. Both alphabets are assumed finite.

    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…