Tidy computations

A machine computes tidily if it clears its work tapes before halting and moves all tape heads to their initial position. This means tidy computations can easily be iterated and when applied to a subset of work tapes, a combinator can run a tidy machine as a subroutine and rely on nothing but the word it emits.

A tidy computation is defined as a Turing.MultiTapeTM.TransformsTapes from blank work tapes to blank work tapes, so the lemmas about tape transformations apply to it directly. The three notions below add tidiness to Turing.MultiTapeTM.ComputesInTimeAndSpace, Turing.MultiTapeTM.ComputesFunInTimeAndSpace and Turing.MultiTapeTM.ComputableInTimeAndSpace.

Main definitions

• Turing.MultiTapeTM.ComputesTidilyInTimeAndSpace: a machine computes an output tidily.
• Turing.MultiTapeTM.ComputesFunTidilyInTimeAndSpace: a machine computes a function tidily.
• Turing.MultiTapeTM.ComputableTidilyInTimeAndSpace: some machine with binary alphabet and finitely many states computes a function tidily.
• Turing.MultiTapeTM.ComputableTidilyInTimeAndSpaceOfLength: the same, with bounds on the length of the encoded input.

Main results

• Turing.MultiTapeTM.computesTidily_iff: a tidy computation is a single run path between Turing.MultiTapeTM.wordsCfg configurations within the time and space bounds.

Tidy computations

@[reducible, inline]

abbrev Turing.MultiTapeTM.ComputesTidilyInTimeAndSpace {k : ℕ} {Symbol : Type u_1} {State : Type u_2} (tm : MultiTapeTM k Symbol State) (input output : List Symbol) (t s : ℕ) : Prop

ComputesTidilyInTimeAndSpace tm input output t s: started on input with blank work tapes, tm halts within t steps and s work-tape cells, having emitted output, with every work tape blank and every head back at its starting cell.

theorem Turing.MultiTapeTM.computesTidily_iff {k : ℕ} {Symbol : Type u_1} {State : Type u_2} {tm : MultiTapeTM k Symbol State} {t s : ℕ} {input output : List Symbol} : tm.ComputesTidilyInTimeAndSpace input output t s ↔ ∃ (p : tm.RunPath input), RelSeries.head p = wordsCfg input (some tm.q₀) (fun (x : Fin k) => []) [] ∧ RelSeries.last p = wordsCfg input none (fun (x : Fin k) => []) output ∧ p.time ≤ t ∧ p.space ≤ s

A tidy computation is a single run path between Turing.MultiTapeTM.wordsCfg configurations with blank work tapes, which emits the output, within the time and space bounds.

theorem Turing.MultiTapeTM.ComputesTidilyInTimeAndSpace.mono {k : ℕ} {Symbol : Type u_1} {State : Type u_2} {tm : MultiTapeTM k Symbol State} {t s : ℕ} {input output : List Symbol} {t' s' : ℕ} (h : tm.ComputesTidilyInTimeAndSpace input output t s) (ht : t ≤ t') (hs : s ≤ s') : tm.ComputesTidilyInTimeAndSpace input output t' s'

Resource bounds can be weakened.

Tidily computing a function

def Turing.MultiTapeTM.ComputesFunTidilyInTimeAndSpace {k : ℕ} {Symbol : Type u_1} {State : Type u_2} {α : Type u_3} {β : Type u_4} (tm : MultiTapeTM k Symbol State) (encIn : α ↪ List Symbol) (encOut : β ↪ List Symbol) (f : α → β) (t s : α → ℕ) : Prop

ComputesFunTidilyInTimeAndSpace tm encIn encOut f t s: for every a, the machine computes encOut (f a) from encIn a tidily, within t a steps and s a cells.

theorem Turing.MultiTapeTM.ComputesFunTidilyInTimeAndSpace.mono {k : ℕ} {Symbol : Type u_1} {State : Type u_2} {tm : MultiTapeTM k Symbol State} {α : Type u_3} {β : Type u_4} {encIn : α ↪ List Symbol} {encOut : β ↪ List Symbol} {f : α → β} {t s t' s' : α → ℕ} (h : tm.ComputesFunTidilyInTimeAndSpace encIn encOut f t s) (ht : ∀ (a : α), t a ≤ t' a) (hs : ∀ (a : α), s a ≤ s' a) : tm.ComputesFunTidilyInTimeAndSpace encIn encOut f t' s'

Resource bounds can be weakened independently on every input.

Tidy computability

def Turing.MultiTapeTM.ComputableTidilyInTimeAndSpace {α : Type u_3} {β : Type u_4} (f : α → β) (encIn : α ↪ List Bool) (encOut : β ↪ List Bool) (t s : α → ℕ) : Prop

Some machine with binary alphabet and finitely many states computes f tidily within the bounds t and s. The bounds include the cost of restoring the tapes.

@[reducible, inline]

abbrev Turing.MultiTapeTM.ComputableTidilyInTimeAndSpaceOfLength {α : Type u_3} {β : Type u_4} (f : α → β) (encIn : α ↪ List Bool) (encOut : β ↪ List Bool) (t s : ℕ → ℕ) : Prop

Turing.MultiTapeTM.ComputableTidilyInTimeAndSpace with the bounds t and s evaluated at the length of the encoded input: the tidy analog of Turing.MultiTapeTM.ComputableInTimeAndSpaceOfLength.

theorem Turing.MultiTapeTM.ComputableTidilyInTimeAndSpace.mono {α : Type u_3} {β : Type u_4} {f : α → β} {encIn : α ↪ List Bool} {encOut : β ↪ List Bool} {t s t' s' : α → ℕ} (h : ComputableTidilyInTimeAndSpace f encIn encOut t s) (ht : ∀ (a : α), t a ≤ t' a) (hs : ∀ (a : α), s a ≤ s' a) : ComputableTidilyInTimeAndSpace f encIn encOut t' s'

Tidy computability is monotone in the resource bounds.