Lax Lean Archive

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

Lax194892.ForOfPebble

Pebble transducers are computed by for-transducers

concepts/Lax194892/ForOfPebble.lean · lax-194892

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 pebble transducer is computed by a for-transducer (Theorem D.2.4 of Transducers, the implication from pebble to for-transducer). The run is organised as a tree of configurations; the children of a configuration are produced by a for-transducer (Lemma D.2.5), and iterating this over the height of the stack, with the output letters read off the leaves, gives a polyregular function, hence a for-transducer.

    Lean source view on GitHub

    1import Lax194892.PebbleTransducers
    2import Lax194892.ForTransducers
    3
    4/-!
    5---
    6title: Pebble transducers are computed by for-transducers
    7type: theorem
    8---
    9Every function computed by a pebble transducer is computed by a
    10for-transducer (Theorem D.2.4 of *Transducers*, the implication from pebble to
    11for-transducer). The run is organised as a tree of configurations; the
    12children of a configuration are produced by a for-transducer (Lemma D.2.5), and
    13iterating this over the height of the stack, with the output letters read off
    14the leaves, gives a polyregular function, hence a for-transducer.
    15
    16# Formalization notes
    17
    18Both alphabets are assumed finite, as in the book. The formal proof goes through
    19polyregularity by an induction on the number of pebbles rather than through
    20Lemma D.2.5.
    21-/
    22
    23namespace Lax194892.ForOfPebble
    24
    25open Lax194892.PebbleTransducers Lax194892.ForTransducers
    26
    27/-- A function computed by a pebble transducer is computed by a for-transducer. -/
    28axiom isForTransducer_of_isPebbleTransducer {A B : Type} [Finite A] [Finite B]
    29 {f : List A → List B} (hf : IsPebbleTransducer f) : IsForTransducer f
    30
    31end Lax194892.ForOfPebble
    32
    Show Proof

    Formalization notes

    Both alphabets are assumed finite, as in the book. The formal proof goes through polyregularity by an induction on the number of pebbles rather than through Lemma D.2.5.

    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…