Experimental first-order Turing-machine routines — definitions

This module provides a deliberately small authoring layer over the existing executable Turing-machine combinators. A routine is either a call to a concrete machine, sequential composition, or a read-only-input loop. Routine.lower compiles the syntax structurally through TM.seqTM and TM.forInputTM, so the concrete TM remains the semantic and resource-accounting ground truth.

Routine.TransducerSafe is an explicit certificate that every called machine obeys the one-way-output discipline. Its name deliberately does not suggest input preservation, termination, or resource safety.

inductive Complexity.TM.Experimental.Routine (n : ℕ) : Type 1

An experimental first-order routine assembled from concrete machine calls and existing machine combinators.

• call {n : ℕ} (machine : TM n) : Routine n

  Invoke one concrete machine.

• seq {n : ℕ} (first second : Routine n) : Routine n

  Run two routines sequentially on the same named tapes.

• forInput {n : ℕ} (body : Routine n) : Routine n

  Run a routine once per Boolean input symbol, subject to the body's input-preservation contract at the proof layer.

def Complexity.TM.Experimental.Routine.lower {n : ℕ} : Routine n → TM n

Compile a first-order routine to the concrete Turing-machine model using the existing executable combinators.

Equations

• (Complexity.TM.Experimental.Routine.call machine).lower = machine
• (first.seq second).lower = first.lower.seqTM second.lower
• body.forInput.lower = body.lower.forInputTM

inductive Complexity.TM.Experimental.Routine.TransducerSafe {n : ℕ} : Routine n → Prop

Proof-carrying one-way-output safety for routines. Leaf calls expose the concrete TM.IsTransducer obligation; composition certificates are structural.

• call {n : ℕ} {machine : TM n} (h : machine.IsTransducer) : (Routine.call machine).TransducerSafe

  A concrete call is transducer-safe when the called machine is a transducer.

• seq {n : ℕ} {first second : Routine n} (hfirst : first.TransducerSafe) (hsecond : second.TransducerSafe) : (first.seq second).TransducerSafe

  Sequential composition is transducer-safe when both routines are.

• forInput {n : ℕ} {body : Routine n} (hbody : body.TransducerSafe) : body.forInput.TransducerSafe

  An input loop is transducer-safe when its body routine is.