Proof of `Regular functions are MSO transductions`
What this proof establishes
no assumptions
Assuming the claims on the left, the claim on the right holds — checked by the archive's pipeline. Proof code is not displayed here.
Description
A regular function is defined by an mso transduction (Theorem C.4.8, the converse implication): the formulas describing the run of a two-way transducer (, right to left).
Proof strategy
The source takes a two-way transducer for (Theorem C.2.9) and, with one copy of the positions per state and direction, writes mso formulas saying that a configuration is visited by the run, which letter it outputs and which of two visited configurations comes first — the runs being described in mso through Büchi's theorem (). The bridge transports the transduction along .
Attribution
Theorem C.4.8 of Transducers, Part C; formalised by Aristotle (Harmonic), , .