Composing step machines

g.comp f runs g on the output of f without ever writing that output down. It keeps the state of g and the position of its head on the output of f. Whenever g needs the symbol under its head, g.comp f runs f from the start on its own input, counting down the bits that f emits to the one under the head of g, and then makes a step of g and rewinds its input head to restart f.

Main definitions

• Turing.StepMachine.comp: the composition.

Main results

• Turing.StepMachine.simulates_comp: g.comp f simulates g on the output of f, with compPeriod steps per step of g.
• Turing.StepMachine.exists_haltsAt_comp: g.comp f halts within ug * compPeriod steps, with the output of g on the output of f.
• Turing.StepMachine.Computes.comp: g.comp f computes g after f.

inductive Turing.StepMachine.CompPhase : Type

The phases of g.comp f: running f, or rewinding the input head, before or after the first move to the left.

• run : CompPhase
• rewindStart : CompPhase
• rewind : CompPhase

@[instance_reducible]

instance Turing.StepMachine.instDecidableEqCompPhase : DecidableEq CompPhase

structure Turing.StepMachine.Countdown : Type

A countdown over the bits emitted by f to the bit under the head of g.

• k : ℕ

  The number of bits still to come, up to the one sought.

• found : Bool

  The bit found.

• len : ℕ

  The number of bits emitted so far.

def Turing.StepMachine.Countdown.start (p : ℕ) : Countdown

The countdown to the bit at the position p, before any bit is emitted.

@[simp]

theorem Turing.StepMachine.Countdown.len_start (p : ℕ) : (start p).len = 0

def Turing.StepMachine.Countdown.push (c : Countdown) (b : Bool) : Countdown

One more emitted bit: the countdown goes down, and at 1 the bit is found.

def Turing.StepMachine.Countdown.symbol (p : ℕ) (c : Countdown) : Option Bool

The symbol at the position p, once all bits are emitted: a blank before the first bit and after the last one.

structure Turing.StepMachine.CompState (σf : Type u_4) (σg : Type u_5) : Type (max u_4 u_5)

The state of g.comp f: the state of g with the position of its head on the output of f, the phase, the state of f, and the countdown.

• g : σg × ℕ

  The state of g and the position of its head on the output of f.

• phase : CompPhase

  The phase.

• f : σf

  The state of f.

• cd : Countdown

  The countdown to the bit under the head of g.

def Turing.StepMachine.moveOn (n p : ℕ) : SignType → ℕ

The head of g after the move d from p on an output of length n: as moveInputPos, it stays on the blanks at 0 and n + 1.

def Turing.StepMachine.compStep {σf : Type u_1} {σg : Type u_2} {Out : Type u_3} (f : StepMachine σf Bool Bool) (g : StepMachine σg Bool Out) (s : CompState σf σg) (a : Option Bool) : CompState σf σg × SignType × List Out

The step of g.comp f on the symbol a under the input head.

def Turing.StepMachine.comp {σf : Type u_1} {σg : Type u_2} {Out : Type u_3} (g : StepMachine σg Bool Out) (f : StepMachine σf Bool Bool) : StepMachine (CompState σf σg) Bool Out

The composition: g run on the output of f, which is never written down.

The head of g and the countdown

theorem Turing.StepMachine.val_moveInputPos {n p : ℕ} (hp : p < n + 2) (d : SignType) : ↑(moveInputPos ⟨p, hp⟩ d) = moveOn n p d

theorem Turing.StepMachine.Countdown.foldl_push_zero (w : List Bool) (fd : Bool) (len : ℕ) : List.foldl push { k := 0, found := fd, len := len } w = { k := 0, found := fd, len := len + w.length }

theorem Turing.StepMachine.Countdown.foldl_push (w : List Bool) {k : ℕ} (fd : Bool) (len : ℕ) (hk : 1 ≤ k) : List.foldl push { k := k, found := fd, len := len } w = { k := k - w.length, found := if k ≤ w.length then w.getD (k - 1) false else fd, len := len + w.length }

theorem Turing.StepMachine.Countdown.k_foldl (w : List Bool) (c : Countdown) : (List.foldl push c w).k = c.k - w.length

theorem Turing.StepMachine.Countdown.len_foldl (w : List Bool) (c : Countdown) : (List.foldl push c w).len = c.len + w.length

theorem Turing.StepMachine.Countdown.symbol_foldl (y : List Bool) (p : ℕ) (hp : p < y.length + 2) : symbol p (List.foldl push (start p) y) = MultiTapeTM.inputSymbolAt y ⟨p, hp⟩

The countdown finds the bit under the head of g.

The run of the composition

theorem Turing.StepMachine.rewind_iterate {σf : Type u_1} {σg : Type u_2} {Out : Type u_3} (f : StepMachine σf Bool Bool) (g : StepMachine σg Bool Out) (x : List Bool) (s : CompState σf σg) (out : List Out) (r : ℕ) (hr : r ≤ x.length) : (g.comp f).stepCfg^[r + 1] { state := { g := s.g, phase := CompPhase.rewind, f := s.f, cd := s.cd }, pos := ⟨r, ⋯⟩, out := out } = { state := { g := s.g, phase := CompPhase.run, f := s.f, cd := s.cd }, pos := 1, out := out }

Rewinding: from the position r on the input in the rewinding phase, the input head reaches the first cell after r + 1 steps, and the phase is back to running f.

theorem Turing.StepMachine.rewind_iterate_le {σf : Type u_1} {σg : Type u_2} {Out : Type u_3} (f : StepMachine σf Bool Bool) (g : StepMachine σg Bool Out) (x : List Bool) (s : CompState σf σg) (out : List Out) {j r : ℕ} (hj : j ≤ r) (hr : r ≤ x.length) : (g.comp f).stepCfg^[j] { state := { g := s.g, phase := CompPhase.rewind, f := s.f, cd := s.cd }, pos := ⟨r, ⋯⟩, out := out } = { state := { g := s.g, phase := CompPhase.rewind, f := s.f, cd := s.cd }, pos := ⟨r - j, ⋯⟩, out := out }

While rewinding, the input head moves to the left and nothing else changes.

def Turing.StepMachine.rewindTime (p : ℕ) : ℕ

The time of the rewind from the position p.

theorem Turing.StepMachine.stepCfg_rewindStart {σf : Type u_1} {σg : Type u_2} {Out : Type u_3} (f : StepMachine σf Bool Bool) (g : StepMachine σg Bool Out) (x : List Bool) (s : CompState σf σg) (out : List Out) (p : Fin (x.length + 2)) : (g.comp f).stepCfg { state := { g := s.g, phase := CompPhase.rewindStart, f := s.f, cd := s.cd }, pos := p, out := out } = { state := { g := s.g, phase := CompPhase.rewind, f := s.f, cd := s.cd }, pos := ⟨↑p - 1, ⋯⟩, out := out }

The rewind from the position p: after rewindTime p steps the input head is on the first cell and the phase is back to running f.

theorem Turing.StepMachine.rewindStart_iterate {σf : Type u_1} {σg : Type u_2} {Out : Type u_3} (f : StepMachine σf Bool Bool) (g : StepMachine σg Bool Out) (x : List Bool) (s : CompState σf σg) (out : List Out) (p : Fin (x.length + 2)) : (g.comp f).stepCfg^[rewindTime ↑p] { state := { g := s.g, phase := CompPhase.rewindStart, f := s.f, cd := s.cd }, pos := p, out := out } = { state := { g := s.g, phase := CompPhase.run, f := s.f, cd := s.cd }, pos := 1, out := out }

theorem Turing.StepMachine.rewindStart_iterate_le {σf : Type u_1} {σg : Type u_2} {Out : Type u_3} (f : StepMachine σf Bool Bool) (g : StepMachine σg Bool Out) (x : List Bool) (s : CompState σf σg) (out : List Out) (p : Fin (x.length + 2)) {j : ℕ} (hj : j ≤ rewindTime ↑p) : ∃ (ph : CompPhase), ((g.comp f).stepCfg^[j] { state := { g := s.g, phase := CompPhase.rewindStart, f := s.f, cd := s.cd }, pos := p, out := out }).state = { g := s.g, phase := ph, f := s.f, cd := s.cd }

During the rewind, only the phase changes.

theorem Turing.StepMachine.run_f_iterate {σf : Type u_1} {σg : Type u_2} {Out : Type u_3} (f : StepMachine σf Bool Bool) (g : StepMachine σg Bool Out) (x : List Bool) {uf : ℕ} (hf : f.HaltsAt x uf) (sg : σg) (hsg : g.halt sg = false) (pg : ℕ) (out : List Out) {r : ℕ} (hr : r ≤ uf) : (g.comp f).stepCfg^[r] { state := { g := (sg, pg), phase := CompPhase.run, f := f.init, cd := Countdown.start pg }, pos := 1, out := out } = { state := { g := (sg, pg), phase := CompPhase.run, f := (f.run x r).state, cd := List.foldl Countdown.push (Countdown.start pg) (f.run x r).out }, pos := (f.run x r).pos, out := out }

Running f: from the start of a round, the composition follows the run of f on the input, counting down its output to the position pg of the head of g.

def Turing.StepMachine.roundCfg {σf : Type u_1} {σg : Type u_2} {Out : Type u_3} (f : StepMachine σf Bool Bool) (x : List Bool) {y : List Bool} (c : Cfg σg Out y) : Cfg (CompState σf σg) Out x

The configuration of g.comp f at the start of the round for the configuration c of g: the input head on the first cell, ready to run f.

theorem Turing.StepMachine.round_g {σf : Type u_1} {σg : Type u_2} {Out : Type u_3} (f : StepMachine σf Bool Bool) (g : StepMachine σg Bool Out) (x : List Bool) {uf : ℕ} (hf : f.HaltsAt x uf) (c : Cfg σg Out (f.run x uf).out) (hc : g.halt c.state = false) : (g.comp f).stepCfg^[uf + 1] (f.roundCfg x c) = { state := { g := ((g.stepCfg c).state, ↑(g.stepCfg c).pos), phase := CompPhase.rewindStart, f := f.init, cd := Countdown.start ↑(g.stepCfg c).pos }, pos := (f.run x uf).pos, out := (g.stepCfg c).out }

A round: after running f to its halt, the composition makes the step of g on the bit under its head and starts rewinding.

def Turing.StepMachine.compPeriod {σf : Type u_1} (f : StepMachine σf Bool Bool) (x : List Bool) (uf : ℕ) : ℕ

The length of a round: running f, the step of g and the rewind.

theorem Turing.StepMachine.run_zero_comp {σf : Type u_1} {σg : Type u_2} {Out : Type u_3} (f : StepMachine σf Bool Bool) (g : StepMachine σg Bool Out) (x : List Bool) {y : List Bool} : (g.comp f).run x 0 = f.roundCfg x (g.initCfg y)

The composition starts at the start of the first round.

theorem Turing.StepMachine.simulates_comp {σf : Type u_1} {σg : Type u_2} {Out : Type u_3} (f : StepMachine σf Bool Bool) (g : StepMachine σg Bool Out) (x : List Bool) {uf : ℕ} (hf : f.HaltsAt x uf) : (g.comp f).Simulates x g.stepCfg (fun (c : Cfg σg Out (f.run x uf).out) => g.halt c.state) Cfg.out (fun (c : Cfg σg Out (f.run x uf).out) (C : Cfg (CompState σf σg) Out x) => C = f.roundCfg x c) (f.compPeriod x uf)

The composition simulates g on the output of f, a step of g per round.

structure Turing.StepMachine.CompState.Along {σf : Type u_1} {σg : Type u_2} {Out : Type u_3} (f : StepMachine σf Bool Bool) (g : StepMachine σg Bool Out) (x : List Bool) (uf ug : ℕ) (s : CompState σf σg) : Prop

s is made of states along the runs of f on x up to uf and of g on the output of f up to ug, with its countdown within the output of f.

• exists_g : ∃ q ≤ ug, s.g = ((g.run (f.run x uf).out q).state, ↑(g.run (f.run x uf).out q).pos)
• exists_f : ∃ r ≤ uf, s.f = (f.run x r).state
• k_le : s.cd.k ≤ (f.run x uf).out.length + 1
• len_le : s.cd.len ≤ (f.run x uf).out.length

theorem Turing.StepMachine.along_run_comp {σf : Type u_1} {σg : Type u_2} {Out : Type u_3} (f : StepMachine σf Bool Bool) (g : StepMachine σg Bool Out) (x : List Bool) {uf ug : ℕ} (hf : f.HaltsAt x uf) (hg : g.HaltsAt (f.run x uf).out ug) {i : ℕ} (hi : i ≤ ug * f.compPeriod x uf) : CompState.Along f g x uf ug ((g.comp f).run x i).state

The states along the run of g.comp f are made of states along the runs of f and g.

theorem Turing.StepMachine.exists_haltsAt_comp {σf : Type u_1} {σg : Type u_2} {Out : Type u_3} (f : StepMachine σf Bool Bool) (g : StepMachine σg Bool Out) (x : List Bool) {uf ug : ℕ} (hf : f.HaltsAt x uf) (hg : g.HaltsAt (f.run x uf).out ug) : ∃ t ≤ ug * f.compPeriod x uf, (g.comp f).HaltsAt x t ∧ ((g.comp f).run x t).out = (g.run (f.run x uf).out ug).out

Composition: when f halts after uf steps and g on its output after ug steps, g.comp f halts within ug rounds, with the output of g.

theorem Turing.StepMachine.Computes.comp {σf : Type u_1} {σg : Type u_2} {Out : Type u_3} (f : StepMachine σf Bool Bool) (g : StepMachine σg Bool Out) (x : List Bool) {y : List Bool} {z : List Out} (hf : f.Computes x y) (hg : g.Computes y z) : (g.comp f).Computes x z

Composition: g.comp f computes g after f.