Logspace functions compose

Logspace functions compose without storing the intermediate value (Turing.MultiTapeTM.ComputableInLogSpace.comp): Christian Reitwiessner's composition within small space (Turing.MultiTapeTM.ComputableInTimeAndSpace.comp_space) recomputes each symbol of the intermediate value when the second machine reads it, and stores only the two machines' work tapes and counters of logarithmic length Sipser, Section 8.5.

The composed machine simulates both machines through the universal machine, so this directory, unlike the base logspace API, depends on Universal. This module also registers the composition rule of fun_prop for ComputableInLogSpace.

Main results

• Turing.MultiTapeTM.ComputableInLogSpace.comp: logspace functions compose.
• Turing.MultiTapeTM.ComputableInLogSpace.comp', Turing.MultiTapeTM.ComputableInLogSpace.bool_not: composition and negation in the form used by fun_prop.

References

• M. Sipser, Introduction to the Theory of Computation, Section 8.5

theorem Turing.MultiTapeTM.ComputableInLogSpace.comp {α β γ : Type} {encIn : α ↪ List Bool} {encMid : β ↪ List Bool} {encOut : γ ↪ List Bool} {g : β → γ} {f : α → β} (hg : ComputableInLogSpace g encMid encOut) (hf : ComputableInLogSpace f encIn encMid) : ComputableInLogSpace (g ∘ f) encIn encOut

Logspace functions compose, without storing the intermediate value: each of its symbols is recomputed when the second machine reads it (ComputableInTimeAndSpace.comp_space). The counters for positions in the input and in the intermediate value have logarithmic length, since the intermediate value is polynomially long.

theorem Turing.MultiTapeTM.ComputableInLogSpace.comp' {α β γ : Type} {encIn : α ↪ List Bool} {encMid : β ↪ List Bool} {encOut : γ ↪ List Bool} {g : β → γ} {f : α → β} (hg : ComputableInLogSpace g encMid encOut) (hf : ComputableInLogSpace f encIn encMid) : ComputableInLogSpace (fun (a : α) => g (f a)) encIn encOut

Composition, in the form used by fun_prop.

theorem Turing.MultiTapeTM.ComputableInLogSpace.bool_not {α : Type} {encIn : α ↪ List Bool} {c : α → Bool} (hc : ComputableInLogSpace c encIn encBool) : ComputableInLogSpace (fun (a : α) => !c a) encIn encBool

Negating a computed Boolean, in the form used by fun_prop.