Complexity of the identity function

A machine with a single state and no work tapes scans the input from left to right, copying each symbol to the output tape, and halts on the blank at the right end of the input. On input w it outputs w after w.length + 1 steps, and having no work tapes it uses zero space.

Main results

• Turing.MultiTapeTM.computableInTimeAndSpace_id: the identity is computable in one step per input symbol and zero space.

theorem Turing.MultiTapeTM.computableInTimeAndSpace_id {α : Type u_2} {enc : α ↪ List Bool} : ComputableInTimeAndSpace id enc enc (fun (a : α) => (enc a).length + 1) fun (x : α) => 0

The identity function is computable in one step per input symbol and zero space.