Removing the stack-machine bridge's word recoding

The forward bridges TM2.PolyTime and TM2.PolySpace produce computations over framed lists of encoded Boolean symbols (encIn.trans (encList (encFinEnum Bool))). Applying Turing.MultiTapeTM.trans_encList_polyTime transfers them to the caller's original binary encodings without requiring a computable inverse for either encoding.

Main results

• Turing.TM2ComputableInPolyTime.computableInPolyTime: forward polynomial-time transfer.
• Turing.TM2Computable.computableInPolySpace: forward polynomial-space transfer.

References

The word conventions are those of the forward bridges TM2.PolyTime and TM2.PolySpace.

theorem Turing.TM2ComputableInPolyTime.computableInPolyTime {α β : Type} {encIn : α ↪ List Bool} {encOut : β ↪ List Bool} {f : α → β} (h : TM2ComputableInPolyTime (⇑encIn) (⇑encOut) f) [∀ (stack : h.tm.K), Finite (h.tm.Γ stack)] : MultiTapeTM.ComputableInPolyTime f encIn encOut

The binary specialization of the forward bridge preserves the supplied encodings, without requiring either encoding to have a computable inverse.

theorem Turing.TM2Computable.computableInPolySpace {α β : Type} {encIn : α ↪ List Bool} {encOut : β ↪ List Bool} {f : α → β} (h : TM2Computable (⇑encIn) (⇑encOut) f) [∀ (stack : h.tm.K), Finite (h.tm.Γ stack)] {space : α → ℕ} (hspace : MultiTapeTM.PolyBounded (fun (a : α) => (encIn a).length) space) (hstacks : h.StacksBounded space) : MultiTapeTM.ComputableInPolySpace f encIn encOut

Termination and polynomially bounded stacks transfer to the original binary encodings. All target stacks, including the input and output stacks, count towards the bound.