Degree-one certificates from finite transducers

The shared streaming machines give linear time and zero workspace. The actual runtime bounds encoded output growth, so these are degree-1/1 certificates. Copy, constant and composition rules come from the existing degree calculus.

theorem Turing.MultiTapeTM.ComputableInDegree.of_transducer {α : Type u_1} {β : Type u_2} {encIn : α ↪ List Bool} {encMid : β ↪ List Bool} {Q : Type} [Finite Q] (τ : Transducer Bool Q) {f : α → β} (h : ∀ (a : α), encMid (f a) = τ.run τ.q₀ (encIn a)) : ComputableInDegree f encIn encMid 1 1

A finite transducer gives a common linear bound from its actual clock and zero workspace.

theorem Turing.MultiTapeTM.ComputableInDegree.of_frame {α : Type u_1} {β : Type u_2} {encIn : α ↪ List Bool} {encMid : β ↪ List Bool} {f : α → β} (h : ∀ (a : α), encMid (f a) = frame (encIn a)) : ComputableInDegree f encIn encMid 1 1

Frame the encoded input using the shared streaming machine.

theorem Turing.MultiTapeTM.ComputableInDegree.of_unframe {α : Type u_1} {β : Type u_2} {encIn : α ↪ List Bool} {encMid : β ↪ List Bool} {f : α → β} (h : ∀ (a : α), encMid (f a) = unframe (encIn a)) : ComputableInDegree f encIn encMid 1 1

Read the first framed word, including the prescribed behavior on incomplete frames.

theorem Turing.MultiTapeTM.ComputableInDegree.of_dropFrame {α : Type u_1} {β : Type u_2} {encIn : α ↪ List Bool} {encMid : β ↪ List Bool} {f : α → β} (h : ∀ (a : α), encMid (f a) = dropFrame (encIn a)) : ComputableInDegree f encIn encMid 1 1

Drop the first framed word using the same shared parser.