Composition within small space

If f and g are computable within space sf and sg, then g ∘ f is computable within space O(sf a + sg (f a) + log |a| + log |f a|), without ever writing down f a: a multi-pass fold over the input simulates the machine of g on descriptions, and whenever it needs the symbol of f a under the input head of g, it simulates the machine of f from the start, reading a in place and counting down its emitted symbols to the one needed.

Main results

• Turing.MultiTapeTM.ComputableInTimeAndSpace.comp_space: composition within small space.
• Turing.MultiTapeTM.ComputableInTimeAndSpace.comp_logSpace: logarithmic space is closed under composition.
• Turing.MultiTapeTM.Universal.computableTidily_compose: the composition, on descriptions, as a multi-pass fold.

Halting and space

theorem Turing.MultiTapeTM.output_haltsAt {k : ℕ} {State : Type u_1} {Symbol : Type u_2} {tm : MultiTapeTM k Symbol State} {input output : List Symbol} {h : ℕ} (hc : tm.Computes input output) (hh : tm.HaltsAt (tm.initCfg input) h) : (runFrom (tm.initCfg input) h).output = output

The output at the first halt is the computed output.

theorem Turing.MultiTapeTM.exists_haltsAt_of_runsInTime {k : ℕ} {State : Type u_1} {Symbol : Type u_2} {tm : MultiTapeTM k Symbol State} {input : List Symbol} {t : ℕ} (ht : tm.RunsInTime input t) : ∃ h ≤ t, tm.HaltsAt (tm.initCfg input) h

The first halt is no later than the time bound.

theorem Turing.MultiTapeTM.haltsAt_pos {k : ℕ} {State : Type u_1} {Symbol : Type u_2} {tm : MultiTapeTM k Symbol State} {input : List Symbol} {h : ℕ} (hh : tm.HaltsAt (tm.initCfg input) h) : 0 < h

The machine starts in a state, so it halts at a positive time.

theorem Turing.MultiTapeTM.RunsInSpace.space_le {k : ℕ} {State : Type u_1} {Symbol : Type u_2} {tm : MultiTapeTM k Symbol State} {input : List Symbol} {s : ℕ} (h : tm.RunsInSpace input s) (t : ℕ) : space (tm.initCfg input) t ≤ s

A space bound bounds the space of every run.

Reading bits in place

def Turing.MultiTapeTM.Universal.bitTr : Translator Unit Bool

The translator whose events are the bits.

theorem Turing.MultiTapeTM.Universal.bitTr_events (w : List Bool) : bitTr.events w = w

def Turing.MultiTapeTM.Universal.eBit : Bool ↪ ℕ

Bits as symbols.

def Turing.MultiTapeTM.Universal.bitScan (p : ℕ × ℕ) (b : Bool) : ℕ × ℕ

A round of the countdown over bits: the countdown goes down, and at 1 the bit is read.

theorem Turing.MultiTapeTM.Universal.inputSymbol_bitScan (w : List Bool) (p : ℕ) : inputSymbol (List.map (⇑eBit) w) p = if p = 0 ∨ (List.foldl bitScan (p, 0) w).1 ≠ 0 then none else some (List.foldl bitScan (p, 0) w).2

The countdown over bits finds the symbol under the input head.

theorem Turing.MultiTapeTM.Universal.bitScan_le (l : List Bool) (k cur : ℕ) (hcur : cur ≤ 1) : (List.foldl bitScan (k, cur) l).1 ≤ k ∧ (List.foldl bitScan (k, cur) l).2 ≤ 1

Along the bits, the countdown does not go up and the bit read is a bit.

Counting down emitted symbols

def Turing.MultiTapeTM.Universal.emitScan (p : ℕ × ℕ) (o : Option ℕ) : ℕ × ℕ

A round of the countdown over emitted symbols: nothing, or the events of a symbol.

theorem Turing.MultiTapeTM.Universal.emitScan_some (p : ℕ × ℕ) (n : ℕ) : emitScan p (some n) = (p.1 - 1, if p.1 = 1 then p.2 + n else p.2)

theorem Turing.MultiTapeTM.Universal.foldl_emitScan (l : List (Option ℕ)) (p : ℕ × ℕ) : List.foldl emitScan p l = List.foldl scan p (events (List.map Option.toList l).flatten)

The countdown over emitted symbols is the countdown over their events.

theorem Turing.MultiTapeTM.Universal.emitScan_le (l : List (Option ℕ)) (hl : ∀ o ∈ l, o.getD 0 ≤ 1) (k cur : ℕ) (hcur : cur ≤ 1) (hk : 1 ≤ k → cur = 0) : (List.foldl emitScan (k, cur) l).1 ≤ k ∧ (List.foldl emitScan (k, cur) l).2 ≤ 1

Along symbols that are bits, the countdown does not go up and the symbol read is a bit.

The control of the composition

@[reducible, inline]

abbrev Turing.MultiTapeTM.Universal.Ctl : Type

The control state: the description and configuration of the outer machine g and of the inner machine f, and the countdown over the symbols emitted by f to the one under the input head of g.

def Turing.MultiTapeTM.Universal.gSym (c : Ctl) : Option ℕ

The symbol under the input head of g, once f has halted.

def Turing.MultiTapeTM.Universal.cstep (c : Ctl) (sym : Option ℕ) : Ctl

A step of the composition, with sym under the input head of f: a step of f, counting down its emitted symbol, or, once f has halted, a step of g, restarting f.

def Turing.MultiTapeTM.Universal.decodeBit (o : Option ℕ) : List Bool

A bit as a symbol, decoded.

def Turing.MultiTapeTM.Universal.gEmit (c : Ctl) : List Bool

What a step of the composition emits: the bit emitted by g, if any.

def Turing.MultiTapeTM.Universal.ctl₀ (dg df : Desc) : Ctl

The initial control state.

def Turing.MultiTapeTM.Universal.emitCount (df : Desc) (x : List ℕ) (p r : ℕ) : ℕ × ℕ

The countdown over the symbols that f emits in its first r steps.

theorem Turing.MultiTapeTM.Universal.iterate_cstep (dg df : Desc) (x y : List ℕ) (uf : ℕ) (hhalt : ∀ (r : ℕ), (run df x r).state = none ↔ uf ≤ r) (hy : (List.map (fun (j : ℕ) => (step df x (run df x j)).2.toList) (List.range uf)).flatten = y) (q r : ℕ) (hr : r ≤ uf) : (fun (c : Ctl) => cstep c (inputSymbol x c.1.2.2.inputPos))^[q * (uf + 1) + r] (ctl₀ dg df) = (((dg, run dg y q), df, run df x r), emitCount df x (run dg y q).inputPos r)

The composition after q steps of g and r ≤ uf steps of f, where f halts after uf steps with the output y.

theorem Turing.MultiTapeTM.Universal.gEmit_iterate (dg df : Desc) (x y : List ℕ) (uf : ℕ) (hhalt : ∀ (r : ℕ), (run df x r).state = none ↔ uf ≤ r) (hy : (List.map (fun (j : ℕ) => (step df x (run df x j)).2.toList) (List.range uf)).flatten = y) (q r : ℕ) (hr : r ≤ uf) : gEmit ((fun (c : Ctl) => cstep c (inputSymbol x c.1.2.2.inputPos))^[q * (uf + 1) + r] (ctl₀ dg df)) = if r = uf then decodeBit (step dg y (run dg y q)).2 else []

What the composition emits after q steps of g and r ≤ uf steps of f: the bit g emits, once f has halted.

theorem Turing.MultiTapeTM.Universal.flatten_gEmit (dg df : Desc) (x y : List ℕ) (uf : ℕ) (hhalt : ∀ (r : ℕ), (run df x r).state = none ↔ uf ≤ r) (hy : (List.map (fun (j : ℕ) => (step df x (run df x j)).2.toList) (List.range uf)).flatten = y) (ug : ℕ) : (List.map (fun (i : ℕ) => gEmit ((fun (c : Ctl) => cstep c (inputSymbol x c.1.2.2.inputPos))^[i] (ctl₀ dg df))) (List.range (ug * (uf + 1)))).flatten = List.map (fun (n : ℕ) => decide (n ≠ 0)) (simulate dg y ug).1

The output of the composition after ug steps of g: the bits g emits.

The fold

@[reducible, inline]

abbrev Turing.MultiTapeTM.Universal.CSt : Type

The state of the fold: the control state, and the countdown over the input of f.

def Turing.MultiTapeTM.Universal.cNext (p : CSt × Bool) : CSt

A round: one bit of the countdown.

def Turing.MultiTapeTM.Universal.xSym (s : CSt) : Option ℕ

The symbol under the input head of f, at the end of a pass.

def Turing.MultiTapeTM.Universal.cEnd (s : CSt) : CSt

The end of a pass: a step of the composition, and the countdown reset to the new input head of f.

def Turing.MultiTapeTM.Universal.cInit (dg df : Desc) : CSt

The initial state.

theorem Turing.MultiTapeTM.Universal.passState_cInit (dg df : Desc) (w : List Bool) (i : ℕ) : passState (cInit dg df) cNext cEnd w i = ((fun (c : Ctl) => cstep c (inputSymbol (List.map (⇑eBit) w) c.1.2.2.inputPos))^[i] (ctl₀ dg df), ((fun (c : Ctl) => cstep c (inputSymbol (List.map (⇑eBit) w) c.1.2.2.inputPos))^[i] (ctl₀ dg df)).1.2.2.inputPos, 0)

The passes are the steps of the composition.

The parts of the fold, within bounds in the length of the state

@[reducible, inline]

abbrev Turing.MultiTapeTM.Universal.eCtl : Ctl ↪ List Bool

The encoding of control states.

@[reducible, inline]

abbrev Turing.MultiTapeTM.Universal.eCSt : CSt ↪ List Bool

The encoding of states of the fold.

theorem Turing.MultiTapeTM.Universal.wTime_le' (c : WCtx) : wTime c ≤ 2 * ((eWCtx c).length + 1) ^ 3

The time of a step, in the length of its context.

theorem Turing.MultiTapeTM.Universal.stepG_inO : ComputableTidilyInO (fun (s : CSt) => stepWith s.1.1.1.1 s.1.1.1.2 (gSym s.1)) eCSt (encPair eCfg eSym) (fun (s : CSt) => ((eCSt s).length + 1) ^ 3) fun (s : CSt) => (eCSt s).length + 1

A step of g, with the symbol found by the countdown.

theorem Turing.MultiTapeTM.Universal.stepF_inO : ComputableTidilyInO (fun (s : CSt) => stepWith s.1.1.2.1 s.1.1.2.2 (xSym s)) eCSt (encPair eCfg eSym) (fun (s : CSt) => ((eCSt s).length + 1) ^ 3) fun (s : CSt) => (eCSt s).length + 1

A step of f, with the symbol found by the countdown over the input.

theorem Turing.MultiTapeTM.Universal.cEnd_inO : ComputableTidilyInO cEnd eCSt eCSt (fun (s : CSt) => ((eCSt s).length + 1) ^ 3) fun (s : CSt) => (eCSt s).length + 1

The end of a pass.

theorem Turing.MultiTapeTM.Universal.cEmit_inO : ComputableTidilyInO (fun (s : CSt) => gEmit s.1) eCSt encBits (fun (s : CSt) => ((eCSt s).length + 1) ^ 3) fun (s : CSt) => (eCSt s).length + 1

What a pass emits.

theorem Turing.MultiTapeTM.Universal.cCont_inO : ComputableTidilyInO (fun (s : CSt) => s.1.1.1.2.state.isSome) eCSt encBool (fun (s : CSt) => ((eCSt s).length + 1) ^ 3) fun (s : CSt) => (eCSt s).length + 1

Whether another pass follows: g has not halted.

theorem Turing.MultiTapeTM.Universal.cNext_inO : ComputableTidilyInO cNext (encPair eCSt encBool) eCSt (fun (p : CSt × Bool) => (((encPair eCSt encBool) p).length + 1) ^ 2) fun (p : CSt × Bool) => ((encPair eCSt encBool) p).length + 1

A round: one bit of the countdown over the input.

The size of the states

def Turing.MultiTapeTM.Universal.composeSpace (dg df : Desc) (x y : List ℕ) (uf ug : ℕ) : ℕ

A bound on the states of the composition: the descriptions and configurations of both machines, and the positions of their input heads in binary.

theorem Turing.MultiTapeTM.Universal.length_eCSt_le (dg df : Desc) (w : List Bool) (y : List ℕ) (uf ug : ℕ) (hhalt : ∀ (r : ℕ), (run df (List.map (⇑eBit) w) r).state = none ↔ uf ≤ r) (hy : (List.map (fun (j : ℕ) => (step df (List.map (⇑eBit) w) (run df (List.map (⇑eBit) w) j)).2.toList) (List.range uf)).flatten = y) (hbits : ∀ n ∈ y, n ≤ 1) {i : ℕ} (hi : i ≤ ug * (uf + 1)) (j : ℕ) : (eCSt (streamState (passState (cInit dg df) cNext cEnd w i) cNext w j)).length ≤ composeSpace dg df (List.map (⇑eBit) w) y uf ug

The size of the states of the composition.

The composition as a fold

theorem Turing.MultiTapeTM.Universal.computableTidily_compose {α γ : Type} {encIn : α ↪ List Bool} {encOut : γ ↪ List Bool} (h : α → γ) (dg df : Desc) (y : α → List ℕ) (uf ug : α → ℕ) (hhaltf : ∀ (a : α) (r : ℕ), (run df (List.map (⇑eBit) (encIn a)) r).state = none ↔ uf a ≤ r) (hy : ∀ (a : α), (List.map (fun (j : ℕ) => (step df (List.map (⇑eBit) (encIn a)) (run df (List.map (⇑eBit) (encIn a)) j)).2.toList) (List.range (uf a))).flatten = y a) (hbits : ∀ (a : α), ∀ n ∈ y a, n ≤ 1) (hhaltg : ∀ (a : α) (q : ℕ), (run dg (y a) q).state = none ↔ ug a ≤ q) (hug : ∀ (a : α), 0 < ug a) (hout : ∀ (a : α), encOut (h a) = List.map (fun (n : ℕ) => decide (n ≠ 0)) (simulate dg (y a) (ug a)).1) : ∃ (c : ℕ), ComputableTidilyInTimeAndSpace h encIn encOut (fun (a : α) => c * (ug a * (uf a + 1) * ((encIn a).length + 1) ^ 2 * (composeSpace dg df (List.map (⇑eBit) (encIn a)) (y a) (uf a) (ug a) + 1) ^ 3)) fun (a : α) => c * (composeSpace dg df (List.map (⇑eBit) (encIn a)) (y a) (uf a) (ug a) + 1)

The composition, on given descriptions. If the machine described by df halts on the bits of every input after uf steps with the symbols y, which are bits, and the machine described by dg halts on y after ug steps with the encoded value of h, then h is tidily computable in space linear in composeSpace.

Machines

theorem Turing.MultiTapeTM.ComputableInTimeAndSpace.comp_space {α β γ : Type} {encIn : α ↪ List Bool} {encMid : β ↪ List Bool} {encOut : γ ↪ List Bool} {f : α → β} {g : β → γ} {tf sf : α → ℕ} {tg sg : β → ℕ} (hf : ComputableInTimeAndSpace f encIn encMid tf sf) (hg : ComputableInTimeAndSpace g encMid encOut tg sg) : ∃ (c : ℕ), ComputableInTimeAndSpace (g ∘ f) encIn encOut (fun (a : α) => c * ((tg (f a) + 1) * (tf a + 1) * ((encIn a).length + 1) ^ 2 * (sf a + sg (f a) + (encNat ((encIn a).length + 1)).length + (encNat ((encMid (f a)).length + 1)).length + 1) ^ 3)) fun (a : α) => c * (sf a + sg (f a) + (encNat ((encIn a).length + 1)).length + (encNat ((encMid (f a)).length + 1)).length + 1)

Composition within small space. If f and g are computable within the time bounds tf, tg and the space bounds sf, sg, then g ∘ f is computable within space linear in sf a + sg (f a) plus the logarithms of the lengths of the input and of the intermediate value, without ever writing down the intermediate value. Its time is polynomial in the time bounds, the length of the input and the space bound.

theorem Turing.MultiTapeTM.ComputableInTimeAndSpace.comp_logSpace {α β γ : Type} {encIn : α ↪ List Bool} {encMid : β ↪ List Bool} {encOut : γ ↪ List Bool} {f : α → β} {g : β → γ} {tf : α → ℕ} {tg : β → ℕ} {kf kg d : ℕ} (hf : ComputableInTimeAndSpace f encIn encMid tf fun (a : α) => kf * (encNat ((encIn a).length + 1)).length) (hg : ComputableInTimeAndSpace g encMid encOut tg fun (b : β) => kg * (encNat ((encMid b).length + 1)).length) (hlen : ∀ (a : α), (encMid (f a)).length + 1 ≤ ((encIn a).length + 1) ^ d) : ∃ (c : ℕ), ComputableInTimeAndSpace (g ∘ f) encIn encOut (fun (a : α) => c * ((tg (f a) + 1) * (tf a + 1) * ((encIn a).length + 1) ^ 2 * (encNat ((encIn a).length + 1)).length ^ 3)) fun (a : α) => c * (encNat ((encIn a).length + 1)).length

Logarithmic space is closed under composition. If f and g are computable in space logarithmic in the lengths of their inputs, and f takes inputs of length n to values of length less than (n + 1) ^ d, then g ∘ f is computable in space logarithmic in the length of its input.