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, after exactly t steps the machine sits in the halted normal form wordsCfg input none ws' out (every head reset to its initial position, tapes blank outside their words, output untouched), with the new words related to the old ones by Q and using at most s work-tape cells. The machine may halt earlier than t; since a halted machine stays put and stops visiting new cells, running on to t costs nothing, so a fixed step count loses no generality and spares every composition an existential. 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.

Main definitions

• Turing.MultiTapeTM.tapeOfList: the tape holding exactly a given word.
• Turing.MultiTapeTM.wordsCfg: the configuration whose tapes hold given words.
• 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_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.tapeOfList {Symbol : Type u_1} (xs : List Symbol) : ℤ → Option Symbol

A tape containing exactly the symbols of xs at positions 0, ..., xs.length - 1.

Equations

• Turing.MultiTapeTM.tapeOfList xs (Int.ofNat n) = xs[n]?
• Turing.MultiTapeTM.tapeOfList xs (Int.negSucc a) = none

@[simp]

theorem Turing.MultiTapeTM.tapeOfList_ofNat {Symbol : Type u_1} (xs : List Symbol) (n : ℕ) : tapeOfList xs ↑n = xs[n]?

@[simp]

theorem Turing.MultiTapeTM.tapeOfList_negSucc {Symbol : Type u_1} (xs : List Symbol) (n : ℕ) : tapeOfList xs (Int.negSucc n) = none

theorem Turing.MultiTapeTM.tapeOfList_append_single {Symbol : Type u_1} (xs : List Symbol) (x : Symbol) : tapeOfList (xs ++ [x]) = Function.update (tapeOfList xs) (↑xs.length) (some x)

Appending one symbol writes precisely the cell after the existing word.

@[simp]

theorem Turing.MultiTapeTM.tapeOfList_nil {Symbol : Type u_1} : tapeOfList [] = fun (x : ℤ) => none

The blank tape holds the empty word.

theorem Turing.MultiTapeTM.tapeOfList_zero {Symbol : Type u_1} (xs : List Symbol) : tapeOfList xs 0 = xs.head?

The cell at position 0 holds the first symbol of the word.

def Turing.MultiTapeTM.wordsCfg {k : ℕ} {Symbol : Type u_1} {State : Type u_2} (input : List Symbol) (q : Option State) (ws : Fin k → List Symbol) (out : List Symbol) : Cfg k Symbol State input

The configuration whose work tape i holds exactly the word ws i with its head at the start, whose input head is at the start of the input, in state q with output out.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem Turing.MultiTapeTM.wordsCfg_workTapePos {k : ℕ} {Symbol : Type u_1} {State : Type u_2} (input : List Symbol) (q : Option State) (ws : Fin k → List Symbol) (out : List Symbol) (x✝ : Fin k) : (wordsCfg input q ws out).workTapePos x✝ = 0

@[simp]

theorem Turing.MultiTapeTM.wordsCfg_state {k : ℕ} {Symbol : Type u_1} {State : Type u_2} (input : List Symbol) (q : Option State) (ws : Fin k → List Symbol) (out : List Symbol) : (wordsCfg input q ws out).state = q

@[simp]

theorem Turing.MultiTapeTM.wordsCfg_inputPos {k : ℕ} {Symbol : Type u_1} {State : Type u_2} (input : List Symbol) (q : Option State) (ws : Fin k → List Symbol) (out : List Symbol) : (wordsCfg input q ws out).inputPos = 1

@[simp]

theorem Turing.MultiTapeTM.wordsCfg_workTapes {k : ℕ} {Symbol : Type u_1} {State : Type u_2} (input : List Symbol) (q : Option State) (ws : Fin k → List Symbol) (out : List Symbol) (i : Fin k) (a✝ : ℤ) : (wordsCfg input q ws out).workTapes i a✝ = tapeOfList (ws i) a✝

@[simp]

theorem Turing.MultiTapeTM.wordsCfg_output {k : ℕ} {Symbol : Type u_1} {State : Type u_2} (input : List Symbol) (q : Option State) (ws : Fin k → List Symbol) (out : List Symbol) : (wordsCfg input q ws out).output = out

@[simp]

theorem Turing.MultiTapeTM.mapState_wordsCfg {k : ℕ} {Symbol : Type u_1} {State : Type u_2} {State' : Type u_3} (φ : Option State → Option State') (input : List Symbol) (q : Option State) (ws : Fin k → List Symbol) (out : List Symbol) : Cfg.mapState φ (wordsCfg input q ws out) = wordsCfg input (φ q) ws out

Remapping the state of a wordsCfg remaps its state and leaves the words alone.

theorem Turing.MultiTapeTM.initCfg_eq_wordsCfg {k : ℕ} {Symbol : Type u_1} {State : Type u_2} (tm : MultiTapeTM k Symbol State) (input : List Symbol) : initCfg input = wordsCfg input (some tm.q₀) (fun (x : Fin k) => []) []

The initial configuration is the word configuration with blank tapes and no output.

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) → 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 is halted after exactly t steps in the configuration whose tapes hold words ws' with Q input ws ws', having used at most s work-tape cells. The machine is free to halt before step t, because it then stays in that configuration.

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.

Equations

• One or more equations did not get rendered due to their size.

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) → 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), P' input ws → Q input ws ws' → Q' input ws ws') (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.

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.

Equations

• One or more equations did not get rendered due to their size.

@[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) => ws' = ws) 1 k

The machine that does nothing halts in one step, leaving every word as it was. 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.