The copy machine, public

The change of Christian Reitwiessner's branch crei/tidy-universal to Cslib.Computability.Machines.Turing.MultiTape.Combinators.Id: the copy machine and its specification become public, under the names copyInput and CopyInput.computesInTimeAndSpace, for use by Turing.MultiTapeTM.tidyCopy. The pinned machine copy is private to its module, so the machine is defined here anew.

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 definitions

• Turing.MultiTapeTM.copyInput: the copy machine.

Main results

• Turing.MultiTapeTM.CopyInput.computesInTimeAndSpace: it computes the identity in one step per input symbol and zero space.

def Turing.MultiTapeTM.copyInput {Symbol : Type u_1} : MultiTapeTM 0 Symbol Unit

The copy machine: a single state and no work tapes. It copies every input symbol to the output tape while moving right, and halts on reading the blank at the right end of the input.

theorem Turing.MultiTapeTM.CopyInput.computesInTimeAndSpace {Symbol : Type u_1} (input : List Symbol) : copyInput.ComputesInTimeAndSpace input input (input.length + 1) 0

The copy machine outputs its input unchanged, in input.length + 1 steps and zero space.