Proof of `Reachability between configurations of a pebble transducer is regular`
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.
In the paper
- page 166 of the paper of lax-157538, Transducers
Description
The string representations of pairs of configurations connected by a run form a regular language (Lemma D.2.2), .
Proof strategy
The source builds a pebble automaton that reads the pair of configurations off its input, places its pebbles on the source configuration and simulates the transducer until it reaches the target (, , ); the language is regular by the regularity of pebble automata behind Theorem D.2.1. The encodings unfold identically () and reachability is transported by .
Attribution
Lemma D.2.2 of Transducers, Part D; formalised by Aristotle (Harmonic), .