Experimental first-order Turing-machine routines #
This module exposes a small provisional authoring language for composing
concrete Turing machines. Routines lower definitionally through the established
TM.seqTM and TM.forInputTM combinators, while Routine.TransducerSafe
records only the one-way-output obligations of leaf calls. The namespace stays
experimental until a second independent construction validates the interface.
Main definitions #
TM.Experimental.Routine— first-order call, sequence, and input-loop syntax.TM.Experimental.Routine.lower— structural lowering to the concreteTMmodel.TM.Experimental.Routine.TransducerSafe— structural output-safety certificate.
Main result #
TM.Experimental.Routine.TransducerSafe.lower_isTransducer— certified routines lower to transducers.
theorem
Complexity.TM.Experimental.Routine.TransducerSafe.lower_isTransducer
{n : ℕ}
{routine : Routine n}
(h : routine.TransducerSafe)
:
routine.lower.IsTransducer
A transducer-safe routine lowers to a concrete machine satisfying the one-way-output discipline.