Machines as transformers of tape words

The interface through which combinators use machines: a machine reads words from its work tapes and leaves words on them. A combinator composing such machines talks about words only, never about individual cells, head positions or the set of tapes a machine has touched.

Configurations are described by equalities: wordsCfg input q ws out is the configuration whose work tape i holds exactly the word ws i (contents tapeOfList (ws i), head at the start), with the input head at the start of the input and output out. A specification TransformsTapes tm P Q t s says: started on word-holding tapes satisfying P, the machine has a run path to the halted normal form wordsCfg input none ws' (out ++ emitted) (every head reset to its initial position, tapes blank outside their words, the word emitted appended to the output it was handed), with the new words related to the old ones by Q, taking at most t steps and visiting at most s work-tape cells. The time and space are those of the path, so specifications compose by joining their paths. Requiring this normal form is what lets specifications compose by rewriting: the halting configuration of one machine is already a valid start for the next, so which words survived a step is read off the equation, not re-established cell by cell.

The output is described as the word the machine appends, never as an absolute value, so that a specification is insensitive to the output it is handed — which is what lets specifications compose: along a sequence the emitted words concatenate.

Main definitions

• Turing.MultiTapeTM.TransformsTapes: the specification format described above.
• Turing.MultiTapeTM.nop: the machine that does nothing.

Main results

• Turing.MultiTapeTM.TransformsTapes.imp: strengthen the precondition, weaken the postcondition and raise the bounds.
• Turing.MultiTapeTM.transformsTapes_iff_nil_output: the generality in the ambient output is free, so a concrete machine need only be run with no prior output.
• Turing.MultiTapeTM.transformsTapes_nop: nop leaves every word as it was, the first machine of the interface and the check that the format is inhabited as intended.

def Turing.MultiTapeTM.TransformsTapes {k : ℕ} {Symbol : Type u_1} {State : Type u_2} (tm : MultiTapeTM k Symbol State) (P : List Symbol → (Fin k → List Symbol) → Prop) (Q : List Symbol → (Fin k → List Symbol) → (Fin k → List Symbol) → List Symbol → Prop) (t s : ℕ) : Prop

TransformsTapes tm P Q t s: started in its initial state on tapes holding words ws that satisfy the precondition P, the machine has a run path of at most t steps, visiting at most s work-tape cells, to the halted configuration whose tapes hold words ws' and which has appended emitted to the output it was handed, with Q input ws ws' emitted.

The bounds are numbers; a specification whose bounds depend on the data is a family ∀ j, TransformsTapes tm (P j) (Q j) (t j) (s j) over one fixed machine.

theorem Turing.MultiTapeTM.TransformsTapes.imp {k : ℕ} {Symbol : Type u_1} {State : Type u_2} {tm : MultiTapeTM k Symbol State} {P P' : List Symbol → (Fin k → List Symbol) → Prop} {Q Q' : List Symbol → (Fin k → List Symbol) → (Fin k → List Symbol) → List Symbol → Prop} {t s t' s' : ℕ} (h : tm.TransformsTapes P Q t s) (hP : ∀ (input : List Symbol) (ws : Fin k → List Symbol), P' input ws → P input ws) (hQ : ∀ (input : List Symbol) (ws ws' : Fin k → List Symbol) (emitted : List Symbol), P' input ws → Q input ws ws' emitted → Q' input ws ws' emitted) (ht : t ≤ t') (hs : s ≤ s') : tm.TransformsTapes P' Q' t' s'

A TransformsTapes statement can be read with a stronger precondition, a weaker postcondition and larger bounds.

theorem Turing.MultiTapeTM.TransformsTapes.mono {k : ℕ} {Symbol : Type u_1} {State : Type u_2} {tm : MultiTapeTM k Symbol State} {P : List Symbol → (Fin k → List Symbol) → Prop} {Q : List Symbol → (Fin k → List Symbol) → (Fin k → List Symbol) → List Symbol → Prop} {t s t' s' : ℕ} (h : tm.TransformsTapes P Q t s) (ht : t ≤ t') (hs : s ≤ s') : tm.TransformsTapes P Q t' s'

A TransformsTapes statement can be read with larger bounds.

theorem Turing.MultiTapeTM.transformsTapes_iff_nil_output {k : ℕ} {Symbol : Type u_1} {State : Type u_2} {tm : MultiTapeTM k Symbol State} {P : List Symbol → (Fin k → List Symbol) → Prop} {Q : List Symbol → (Fin k → List Symbol) → (Fin k → List Symbol) → List Symbol → Prop} {t s : ℕ} : tm.TransformsTapes P Q t s ↔ ∀ (input : List Symbol) (ws : Fin k → List Symbol), P input ws → ∃ (ws' : Fin k → List Symbol) (emitted : List Symbol), Q input ws ws' emitted ∧ ∃ (p : tm.RunPath input), RelSeries.head p = wordsCfg input (some tm.q₀) ws [] ∧ RelSeries.last p = wordsCfg input none ws' emitted ∧ p.time ≤ t ∧ p.space ≤ s

The ambient output is a concern of sequencing, not of machines. A specification holds for every prior output as soon as it holds for none, because a machine never reads what it has already written. This is where that generality is discharged, once, rather than by every caller: a concrete machine enters the interface by proving the right-hand side.

The only consumer of the generality is Turing.MultiTapeTM.transformsTapes_seq, which runs the second machine after the first has emitted.

def Turing.MultiTapeTM.nop (k : ℕ) (Symbol : Type u_3) : MultiTapeTM k Symbol Unit

The machine that does nothing: it halts on its first step, leaving the configuration unchanged.

@[simp]

theorem Turing.MultiTapeTM.step_nop {k : ℕ} {Symbol : Type u_1} {input : List Symbol} (ws : Fin k → List Symbol) (out : List Symbol) : step (wordsCfg input (some ()) ws out) = wordsCfg input none ws out

A single step of nop halts and leaves the words alone.

@[simp]

theorem Turing.MultiTapeTM.runFrom_nop_one {k : ℕ} {Symbol : Type u_1} {input : List Symbol} (ws : Fin k → List Symbol) (out : List Symbol) : runFrom (wordsCfg input (some ()) ws out) 1 = wordsCfg input none ws out

nop reaches its halting configuration after exactly one step.

theorem Turing.MultiTapeTM.transformsTapes_nop (k : ℕ) (Symbol : Type u_3) : (nop k Symbol).TransformsTapes (fun (x : List Symbol) (x_1 : Fin k → List Symbol) => True) (fun (x : List Symbol) (ws ws' : Fin k → List Symbol) (emitted : List Symbol) => ws' = ws ∧ emitted = []) 1 k

The machine that does nothing halts in one step, leaving every word as it was and emitting nothing. Its heads never move, so it visits one cell per tape. This is the first machine of the interface: it checks that the specification format is inhabited exactly as intended.