Lax Lean Archive

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

Lax916827.TwoWayCodes

Codes of two-way transducers

concepts/Lax916827/TwoWayCodes.lean · lax-916827

definition

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

    In the paper

    Definition

    The equivalence problem for regular functions (Theorem C.1.4 of Transducers) is decided on two-way transducers, which by Theorem C.2.9 compute exactly the regular functions. A two-way transducer with states and letters in N\mathbb{N} is described by a finite code: a lookup table for its transition function, listing for finitely many triples (letter to the left, state, letter to the right) the transition taken there. The initial state is 00, and a triple absent from the table halts with empty output. A code is total if the transducer it describes halts on every input.

    Lean source view on GitHub

    1import Mathlib.Computability.Primrec.List
    2import Lax916827.TwoWayTransducers
    3
    4/-!
    5---
    6title: Codes of two-way transducers
    7type: definition
    8---
    9The equivalence problem for regular functions (Theorem C.1.4 of *Transducers*)
    10is decided on two-way transducers, which by Theorem C.2.9 compute exactly the
    11regular functions. A two-way transducer with states and letters in
    12N\mathbb{N} is described by a finite *code*: a lookup table for its transition
    13function, listing for finitely many triples (letter to the left, state, letter
    14to the right) the transition taken there. The initial state is 00, and a
    15triple absent from the table halts with empty output. A code is *total* if the
    16transducer it describes halts on every input.
    17
    18# Formalization notes
    19
    20`TwoWayCode` is a list of table entries; it is `Primcodable` as a list of pairs,
    21so that decidability can be stated with `DecidableUnderPromise` of
    22`Lax132576.TransducerCodes`. `twoWayCodeRel c` is the relation computed by the
    23coded transducer (a partial function, by determinism), and `TwoWayCodeTotal` the
    24promise that it is total.
    25-/
    26
    27namespace Lax916827.TwoWayCodes
    28
    29open Lax916827.TwoWayTransducers
    30
    31/-- A code of a two-way transducer over `ℕ`: a lookup table from triples (letter to
    32the left, state, letter to the right) to transitions. -/
    33abbrev TwoWayCode := List ((Option ℕ × ℕ × Option ℕ) × (List ℕ ⊕ (ℕ × List ℕ × Bool)))
    34
    35/-- The two-way transducer described by a code: initial state `0`, and the table
    36entry of a triple, or halting with empty output when the triple is absent. -/
    37def twoWayCodeAut (c : TwoWayCode) : TwoWay ℕ ℕ ℕ where
    38 init := 0
    39 step := fun l q r =>
    40 match c.lookup (l, q, r) with
    41 | some x => x
    42 | none => Sum.inl []
    43
    44/-- The relation computed by the coded transducer. -/
    45def twoWayCodeRel (c : TwoWayCode) : List ℕ → List ℕ → Prop := (twoWayCodeAut c).Computes
    46
    47/-- The coded transducer computes a total function: it halts on every input. -/
    48def TwoWayCodeTotal (c : TwoWayCode) : Prop := ∀ w, ∃ v, twoWayCodeRel c w v
    49
    50end Lax916827.TwoWayCodes
    51

    Formalization notes

    TwoWayCodeTwoWayCode is a list of table entries; it is PrimcodablePrimcodable as a list of pairs, so that decidability can be stated with DecidableUnderPromiseDecidableUnderPromise of Lax132576.TransducerCodesLax132576.TransducerCodes. twoWayCodeRelctwoWayCodeRel c is the relation computed by the coded transducer (a partial function, by determinism), and TwoWayCodeTotalTwoWayCodeTotal the promise that it is total.

    Builds on

    Used by

    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…