Deterministic multi-input multi-tape Turing machines

Defines deterministic Turing machines with i two-way read-only input tapes, w work tapes and one write-only output tape — the machine model of MIP* = RE's normal form verifiers (a decider is a 5-input Turing machine; blueprint def:decider).

This file generalizes the vendored CSLib development (MIPRE.Cslib.Computability.Machines.Turing.MultiTape.Deterministic, upstream Turing.MultiTapeTM) from one input tape to i of them, declaration for declaration and under the same names; Turing.MultiTapeTM is exactly the case i = 1 (the exact correspondence is proved in MIPRE.TM.MultiInput.OneInputEquiv). All conventions are inherited:

• tape symbols are Option Symbol, with none the blank symbol;
• each input head moves freely on its own input, clamped one cell beyond either end (Turing.moveInputPos is reused unchanged, one input tape at a time);
• the transition can optionally write and move on every work tape, and optionally emit one output symbol;
• halting is the absent successor state (none), and halted configurations are fixed points of step;
• space usage counts the work-tape cells visited by the heads; the input and output tapes are ignored for space.

Native multiple input tapes (rather than packing several inputs onto one tape by concatenation) keep the paper's per-input time bounds honest: accessing one input never costs time proportional to the lengths of the others. See planning/tm-infrastructure.md (Milestone A) for the design record.

Important declarations

• MultiInputTM: the machine
• MultiInputTM.Cfg: configurations, relative to the tuple of inputs
• MultiInputTM.step, MultiInputTM.configs: one step, and the step-indexed run
• MultiInputTM.outputString: the output emitted during the first t steps
• MultiInputTM.spaceUsed: the number of work-tape cells visited up to a step
• MultiInputTM.TransitionRelation: the relational view of step, tied to the iterated view by relatesInSteps_iff_configs_eq
• MultiInputTM.haltsAtStep, MultiInputTM.halting_step_unique: the exact halting step

The resource-bound packaging (ComputesInTimeAndSpace, ComputesFunWithBounds) is in MIPRE.TM.MultiInput.Complexity.

structure Turing.MultiInputTM.TransitionOut (i w : ℕ) (Symbol : Type u_3) (State : Type u_4) : Type (max u_3 u_4)

The output of the transition function of a multi-input Turing machine.

• inputMoves : Fin i → SignType

  The movement (attempt) of each input head.

• workActions : Fin w → Option (Option Symbol) × SignType

  Actions on the work tapes: optionally a symbol to write and the head movement.

• outS : Option Symbol

  An optional symbol to output.

• q' : Option State

  The successor state or none to halt.

theorem Turing.MultiInputTM.TransitionOut.ext {i w : ℕ} {Symbol : Type u_3} {State : Type u_4} {x y : TransitionOut i w Symbol State} (inputMoves : x.inputMoves = y.inputMoves) (workActions : x.workActions = y.workActions) (outS : x.outS = y.outS) (q' : x.q' = y.q') : x = y

theorem Turing.MultiInputTM.TransitionOut.ext_iff {i w : ℕ} {Symbol : Type u_3} {State : Type u_4} {x y : TransitionOut i w Symbol State} : x = y ↔ x.inputMoves = y.inputMoves ∧ x.workActions = y.workActions ∧ x.outS = y.outS ∧ x.q' = y.q'

structure Turing.MultiInputTM (i w : ℕ) (Symbol : Type u_3) (State : Type u_4) : Type (max u_3 u_4)

A deterministic Turing machine with i two-way read-only input tapes and w work tapes over the alphabet Option Symbol (where none is the blank symbol). Note that it is not required that Symbol or State are finite; finiteness enters only with the canonically coded machines of MIPRE.TM.Code.

• q₀ : State

  initial state

• tr (q : State) (inputs : Fin i → Option Symbol) (work : Fin w → Option Symbol) : TransitionOut i w Symbol State

  transition function, mapping a state, the tuple of symbols under the input heads and the tuple of symbols under the work heads to a movement for each input head, actions on the work tapes, optionally a symbol to output and the successor state

Configurations

This section defines the configurations of a multi-input Turing machine, the step function that lets the machine transition from one configuration to the next, the resulting sequence of configurations and the initial configuration. Input-head movement reuses Turing.moveInputPos from the vendored CSLib file, one input tape at a time.

structure Turing.MultiInputTM.Cfg (i w : ℕ) (Symbol : Type u_3) (State : Type u_4) (input : Fin i → List Symbol) : Type (max u_3 u_4)

The configurations of a multi-input Turing machine are relative to the tuple of inputs of the machine and consist of:

• an Optional state (or none for the halting state),
• the position of each input head (shifted by one),
• the contents of the work tapes,
• the positions of the work tape heads.

• state : Option State

  the state of the machine (or none for the halting state)

• inputPos (j : Fin i) : Fin ((input j).length + 2)

  the position of each input head, shifted by one

• workTapes : Fin w → ℤ → Option Symbol

  the work tapes

• workTapePos : Fin w → ℤ

  the positions of the heads on the work tapes

theorem Turing.MultiInputTM.Cfg.ext_iff {i w : ℕ} {Symbol : Type u_3} {State : Type u_4} {input : Fin i → List Symbol} {x y : Cfg i w Symbol State input} : x = y ↔ x.state = y.state ∧ x.inputPos = y.inputPos ∧ x.workTapes = y.workTapes ∧ x.workTapePos = y.workTapePos

theorem Turing.MultiInputTM.Cfg.ext {i w : ℕ} {Symbol : Type u_3} {State : Type u_4} {input : Fin i → List Symbol} {x y : Cfg i w Symbol State input} (state : x.state = y.state) (inputPos : x.inputPos = y.inputPos) (workTapes : x.workTapes = y.workTapes) (workTapePos : x.workTapePos = y.workTapePos) : x = y

@[instance_reducible]

instance Turing.MultiInputTM.instInhabitedCfg {a✝ a✝¹ : ℕ} {a✝² : Type u_3} {a✝³ : Type u_4} {a✝⁴ : Fin a✝ → List a✝²} : Inhabited (Cfg a✝ a✝¹ a✝² a✝³ a✝⁴)

Equations

• Turing.MultiInputTM.instInhabitedCfg = { default := Turing.MultiInputTM.instInhabitedCfg.default }

def Turing.MultiInputTM.Cfg.inputSymbol {i w : ℕ} {State : Type u_1} {Symbol : Type u_2} {input : Fin i → List Symbol} (cfg : Cfg i w Symbol State input) (j : Fin i) : Option Symbol

The symbol currently under the head of input tape j.

Equations

• cfg.inputSymbol j = if h₁ : cfg.inputPos j = 0 then none else if h₂ : ↑(cfg.inputPos j) = (input j).length + 1 then none else some (input j)[↑(cfg.inputPos j) - 1]

@[simp]

theorem Turing.MultiInputTM.inputSymbolInner {i w : ℕ} {State : Type u_1} {Symbol : Type u_2} {input : Fin i → List Symbol} {cfg : Cfg i w Symbol State input} (j : Fin i) (p : ℕ) (h₁ : ↑(cfg.inputPos j) = 1 + p) (h₂ : p < (input j).length) : cfg.inputSymbol j = some (input j)[p]

def Turing.MultiInputTM.Cfg.inputSymbols {i w : ℕ} {State : Type u_1} {Symbol : Type u_2} {input : Fin i → List Symbol} (cfg : Cfg i w Symbol State input) : Fin i → Option Symbol

The tuple of symbols under the input heads.

Equations

• cfg.inputSymbols j = cfg.inputSymbol j

@[simp]

theorem Turing.MultiInputTM.Cfg.inputSymbols_apply {i w : ℕ} {State : Type u_1} {Symbol : Type u_2} {input : Fin i → List Symbol} (cfg : Cfg i w Symbol State input) (j : Fin i) : cfg.inputSymbols j = cfg.inputSymbol j

def Turing.MultiInputTM.Cfg.workTapeSymbols {i w : ℕ} {State : Type u_1} {Symbol : Type u_2} {input : Fin i → List Symbol} (cfg : Cfg i w Symbol State input) (d : Fin w) : Option Symbol

The symbol read by work tape d.

Equations

• cfg.workTapeSymbols d = cfg.workTapes d (cfg.workTapePos d)

def Turing.MultiInputTM.step {i w : ℕ} {State : Type u_1} {Symbol : Type u_2} {tm : MultiInputTM i w Symbol State} {input : Fin i → List Symbol} (cfg : Cfg i w Symbol State input) : Cfg i w Symbol State input

The step function corresponding to a MultiInputTM.

Equations

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

def Turing.MultiInputTM.outputSymbol {i w : ℕ} {State : Type u_1} {Symbol : Type u_2} {tm : MultiInputTM i w Symbol State} {input : Fin i → List Symbol} (cfg : Cfg i w Symbol State input) : Option Symbol

The symbol (optionally) output when executing one step starting from configuration cfg.

Equations

• Turing.MultiInputTM.outputSymbol cfg = match cfg.state with | none => none | some q => (tm.tr q cfg.inputSymbols cfg.workTapeSymbols).outS

def Turing.MultiInputTM.initCfg {i w : ℕ} {State : Type u_1} {Symbol : Type u_2} {tm : MultiInputTM i w Symbol State} (input : Fin i → List Symbol) : Cfg i w Symbol State input

The initial configuration corresponding to a tuple of input strings.

Equations

• Turing.MultiInputTM.initCfg input = { state := some tm.q₀, inputPos := fun (x : Fin i) => 1, workTapes := fun (x : Fin w) (x_1 : ℤ) => none, workTapePos := fun (x : Fin w) => 0 }

@[simp]

theorem Turing.MultiInputTM.step_of_halt {i w : ℕ} {State : Type u_1} {Symbol : Type u_2} {tm : MultiInputTM i w Symbol State} {input : Fin i → List Symbol} {cfg : Cfg i w Symbol State input} (h : cfg.state = none) : step cfg = cfg

def Turing.MultiInputTM.configs {i w : ℕ} {State : Type u_1} {Symbol : Type u_2} {tm : MultiInputTM i w Symbol State} {input : Fin i → List Symbol} (cfg : Cfg i w Symbol State input) (t : ℕ) : Cfg i w Symbol State input

The sequence of configurations of the Turing machine starting from cfg. If the Turing machine halts, it will stay at the halting configuration.

Equations

• Turing.MultiInputTM.configs cfg t = Turing.MultiInputTM.step^[t] cfg

@[simp]

theorem Turing.MultiInputTM.configs_zero {i w : ℕ} {State : Type u_1} {Symbol : Type u_2} {tm : MultiInputTM i w Symbol State} {input : Fin i → List Symbol} {cfg : Cfg i w Symbol State input} : configs cfg 0 = cfg

theorem Turing.MultiInputTM.configs_succ_eq_step {i w : ℕ} {State : Type u_1} {Symbol : Type u_2} {tm : MultiInputTM i w Symbol State} {input : Fin i → List Symbol} {cfg : Cfg i w Symbol State input} {t : ℕ} : configs cfg (t + 1) = configs (step cfg) t

theorem Turing.MultiInputTM.configs_succ_eq_step' {i w : ℕ} {State : Type u_1} {Symbol : Type u_2} {tm : MultiInputTM i w Symbol State} {input : Fin i → List Symbol} {cfg : Cfg i w Symbol State input} {t : ℕ} : configs cfg (t + 1) = step (configs cfg t)

theorem Turing.MultiInputTM.configs_add {i w : ℕ} {State : Type u_1} {Symbol : Type u_2} {tm : MultiInputTM i w Symbol State} {input : Fin i → List Symbol} (cfg : Cfg i w Symbol State input) (a b : ℕ) : configs cfg (a + b) = configs (configs cfg a) b

Running a + b steps equals running b steps from the configuration reached after a.

@[simp]

theorem Turing.MultiInputTM.configs_of_halts {i w : ℕ} {State : Type u_1} {Symbol : Type u_2} {tm : MultiInputTM i w Symbol State} {input : Fin i → List Symbol} (cfg : Cfg i w Symbol State input) (h : cfg.state = none) {n : ℕ} : configs cfg n = cfg

The sequence of configurations from a halting state is constant.

@[simp]

theorem Turing.MultiInputTM.outputSymbol_of_halt {i w : ℕ} {State : Type u_1} {Symbol : Type u_2} {tm : MultiInputTM i w Symbol State} {input : Fin i → List Symbol} {cfg : Cfg i w Symbol State input} (h_halt : cfg.state = none) : outputSymbol cfg = none

theorem Turing.MultiInputTM.workTapePos_step_le {i w : ℕ} {State : Type u_1} {Symbol : Type u_2} {tm : MultiInputTM i w Symbol State} {input : Fin i → List Symbol} (c : Cfg i w Symbol State input) (d : Fin w) : |(step c).workTapePos d - c.workTapePos d| ≤ 1

Each work-tape head moves by at most one cell in a single step.

Space usage

def Turing.MultiInputTM.visitedByTapeHead {i w : ℕ} {State : Type u_1} {Symbol : Type u_2} {tm : MultiInputTM i w Symbol State} {input : Fin i → List Symbol} (cfg : Cfg i w Symbol State input) (t : ℕ) (d : Fin w) : Finset ℤ

The set of positions visited by the head of work tape d in the computation starting from configuration cfg up to step t.

Equations

• Turing.MultiInputTM.visitedByTapeHead cfg t d = Finset.image (fun (t' : ℕ) => (Turing.MultiInputTM.configs cfg t').workTapePos d) (Finset.range (t + 1))

def Turing.MultiInputTM.spaceUsedByTape {i w : ℕ} {State : Type u_1} {Symbol : Type u_2} {tm : MultiInputTM i w Symbol State} {input : Fin i → List Symbol} (cfg : Cfg i w Symbol State input) (t : ℕ) (d : Fin w) : ℕ

The number of work tape cells touched by the head of tape d in the computation starting from configuration cfg up to step t.

Equations

• Turing.MultiInputTM.spaceUsedByTape cfg t d = (Turing.MultiInputTM.visitedByTapeHead cfg t d).card

def Turing.MultiInputTM.spaceUsed {i w : ℕ} {State : Type u_1} {Symbol : Type u_2} {tm : MultiInputTM i w Symbol State} {input : Fin i → List Symbol} (cfg : Cfg i w Symbol State input) (t : ℕ) : ℕ

The number of work tape cells touched by a computation starting from configuration cfg up to step t.

Equations

• Turing.MultiInputTM.spaceUsed cfg t = ∑ d : Fin w, Turing.MultiInputTM.spaceUsedByTape cfg t d

@[simp]

theorem Turing.MultiInputTM.spaceUsed_zero_tapes_eq_zero {i w : ℕ} {State : Type u_1} {Symbol : Type u_2} {tm : MultiInputTM i w Symbol State} {input : Fin i → List Symbol} (cfg : Cfg i w Symbol State input) (t : ℕ) (h_zero : w = 0) : spaceUsed cfg t = 0

A machine without work tapes uses zero space.

theorem Turing.MultiInputTM.spaceUsedByTape_le_spaceUsed {i w : ℕ} {State : Type u_1} {Symbol : Type u_2} {tm : MultiInputTM i w Symbol State} {input : Fin i → List Symbol} (cfg : Cfg i w Symbol State input) (t : ℕ) (d : Fin w) : spaceUsedByTape cfg t d ≤ spaceUsed cfg t

Each tape's space usage is bounded by the total space used.

def Turing.MultiInputTM.TransitionRelation {i w : ℕ} {State : Type u_1} {Symbol : Type u_2} {tm : MultiInputTM i w Symbol State} {input : Fin i → List Symbol} (c₁ c₂ : Cfg i w Symbol State input) : Prop

The TransitionRelation corresponding to a MultiInputTM i w Symbol State is defined by the step function, which maps a configuration to its next configuration.

Equations

• Turing.MultiInputTM.TransitionRelation c₁ c₂ = (Turing.MultiInputTM.step c₁ = c₂)

def Turing.MultiInputTM.outputString {i w : ℕ} {State : Type u_1} {Symbol : Type u_2} {input : Fin i → List Symbol} (tm : MultiInputTM i w Symbol State) (cfg₀ : Cfg i w Symbol State input) (t : ℕ) : List Symbol

The string output by the Turing machine tm starting in configuration cfg₀, executing for t steps. It is the concatenation of the symbols (optionally) emitted at each of the first t steps.

Equations

• tm.outputString cfg₀ t = List.flatMap (fun (t' : ℕ) => (Turing.MultiInputTM.outputSymbol (Turing.MultiInputTM.configs cfg₀ t')).toList) (List.range t)

theorem Turing.MultiInputTM.outputString_succ {i w : ℕ} {State : Type u_1} {Symbol : Type u_2} {input : Fin i → List Symbol} (tm : MultiInputTM i w Symbol State) (cfg : Cfg i w Symbol State input) (t : ℕ) : tm.outputString cfg (t + 1) = tm.outputString cfg t ++ (outputSymbol (configs cfg t)).toList

The output produced in t + 1 steps is the output produced in t steps followed by the symbol (optionally) emitted at step t.

theorem Turing.MultiInputTM.outputString_halt {i w : ℕ} {State : Type u_1} {Symbol : Type u_2} {input : Fin i → List Symbol} (tm : MultiInputTM i w Symbol State) (cfg : Cfg i w Symbol State input) (h_halt : cfg.state = none) (t : ℕ) : tm.outputString cfg t = []

From a halting configuration, a machine does not output anything.

theorem Turing.MultiInputTM.outputString_add_eq_append {i w : ℕ} {State : Type u_1} {Symbol : Type u_2} {input : Fin i → List Symbol} (tm : MultiInputTM i w Symbol State) (cfg : Cfg i w Symbol State input) (t₁ t₂ : ℕ) : tm.outputString cfg (t₁ + t₂) = tm.outputString cfg t₁ ++ tm.outputString (configs cfg t₁) t₂

theorem Turing.MultiInputTM.outputString_eq_of_halt {i w : ℕ} {State : Type u_1} {Symbol : Type u_2} {input : Fin i → List Symbol} (tm : MultiInputTM i w Symbol State) (cfg : Cfg i w Symbol State input) {τ t : ℕ} (hle : τ ≤ t) (hhalt : (configs cfg τ).state = none) : tm.outputString cfg t = tm.outputString cfg τ

The output does not change after the machine has halted.

theorem Turing.MultiInputTM.relatesInSteps_iff_configs_eq {i w : ℕ} {State : Type u_1} {Symbol : Type u_2} {input : Fin i → List Symbol} (tm : MultiInputTM i w Symbol State) (cfg₁ cfg₂ : Cfg i w Symbol State input) (t : ℕ) : Relation.RelatesInSteps TransitionRelation cfg₁ cfg₂ t ↔ configs cfg₁ t = cfg₂

This lemma translates between the relational notion and the iterated step notion. The latter can be more convenient especially for deterministic machines as we have here.

def Turing.MultiInputTM.haltsAtStep {i w : ℕ} {State : Type u_1} {Symbol : Type u_2} (tm : MultiInputTM i w Symbol State) (input : Fin i → List Symbol) (t : ℕ) : Bool

The Turing machine tm halts after exactly t steps on input tuple input if its state is none at step t and non-none at step t - 1. Note that every Turing machine has to perform at least one step to halt.

Equations

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

theorem Turing.MultiInputTM.halting_step_unique {i w : ℕ} {State : Type u_1} {Symbol : Type u_2} {tm : MultiInputTM i w Symbol State} {input : Fin i → List Symbol} {t₁ t₂ : ℕ} (h_halts₁ : tm.haltsAtStep input t₁ = true) (h_halts₂ : tm.haltsAtStep input t₂ = true) : t₁ = t₂

If a Turing machine halts, the time step is uniquely determined.

theorem Turing.MultiInputTM.not_halts_of_repeat_nonhalt {i w : ℕ} {State : Type u_1} {Symbol : Type u_2} {tm : MultiInputTM i w Symbol State} {input : Fin i → List Symbol} (cfg : Cfg i w Symbol State input) (h_not_halt : cfg.state ≠ none) (t : ℕ) (heq : configs cfg (t + 1) = cfg) (t' : ℕ) : (configs cfg t').state ≠ none

If a deterministic machine repeats a non-halting configuration, it never halts, because the sequence between the two configurations will loop forever. Note that this can be applied to two arbitrary and different time steps t and t + Δ using tm.configs_add.