Lax Lean Archive

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

Proof of `Polyregular functions are computed by for-transducers`

groundedproofs/Lax194892Proofs/Results.lean · lax-194892

What this proof establishes

no assumptions

thm✓Lax194892.ForOfPolyregular

Assuming the claims on the left, the claim on the right holds — checked by the archive's pipeline. Proof code is not displayed here.

Read the Lean proof on GitHub

Description

Every polyregular function is computed by a for-transducer (Theorem D.1.1, from polyregular to for-transducers): for-transducers for the regular primes through their two-way transducers (Corollary C.2.8), a for-transducer for marked squaring, and Lemma D.1.4 for the composition (Transducers.isForTransducerofisPolyregularTransducers.isForTransducer_of_isPolyregular).

Proof strategy

The concept's for-transducer syntax is a distinct inductive type from the source's; the bridge's toSrcProgtoSrcProg/ofSrcProgofSrcProg are mutually inverse and preserve the semantics (exectoSrcProgexec_toSrcProg, by induction on the program), which gives isForTransduceriffisForTransducer_iff; isPolyregulariffisPolyregular_iff transports the hypothesis.

Attribution

Theorem D.1.1 of Transducers, Part D; formalised by Aristotle (Harmonic), PartD/PolyFor.leanPartD/PolyFor.lean, PartD/PolyStep∗.leanPartD/PolyStep*.lean, PartD/TwoWayTotal.leanPartD/TwoWayTotal.lean.