A direction for the turing machine move command, either left or right.

A Turing machine "statement" is just a command to either move left or right, or write a symbol on the tape.

A Post-Turing machine with symbol type Γ and label type Λ is a function which, given the current state q : Λ and the tape head a : Γ, either halts (returns none) or returns a new state q' : Λ and a stmt describing what to do, either a move left or right, or a write command.

Both Λ and Γ are required to be inhabited; the default value for Γ is the "blank" tape value, and the default value of Λ is the initial state.

The configuration state of a Turing machine during operation consists of a label (machine state), and a tape, represented in the form (a, L, R) meaning the tape looks like L.rev ++ [a] ++ R with the machine currently reading the a. The lists are automatically extended with blanks as the machine moves around.

Execution semantics of the Turing machine.

The statement reaches M s₁ s₂ means that s₂ is obtained starting from s₁ after a finite number of steps from s₂.

The initial configuration.

Evaluate a Turing machine on initial input to a final state, if it terminates.

The raw definition of a Turing machine does not require that Γ and Λ are finite, and in practice we will be interested in the infinite Λ case. We recover instead a notion of "effectively finite" Turing machines, which only make use of a finite subset of their states. We say that a set S ⊆ Λ supports a Turing machine M if S is closed under the transition function and contains the initial state.

The TM1 model is a simplification and extension of TM0 (Post-Turing model) in the direction of Wang B-machines. The machine's internal state is extended with a (finite) store σ of variables that may be accessed and updated at any time. A machine is given by a Λ indexed set of procedures or functions. Each function has a body which is a stmt, which can either be a move or write command, a branch (if statement based on the current tape value), a load (set the variable value), a goto (call another function), or halt. Note that here most statements do not have labels; goto commands can only go to a new function. All commands have access to the variable value and current tape value.

The configuration of a TM1 machine is given by the currently evaluating statement, the variable store value, and the tape.

The semantics of TM1 evaluation.

A set S of labels supports machine M if all the goto statements in the functions in S refer only to other functions in S.

The TM2 model removes the tape entirely from the TM1 model, replacing it with an arbitrary (finite) collection of stacks. The operation push puts an element on one of the stacks, and pop removes an element from a stack (and modifying the internal state based on the result). peek modifies the internal state but does not remove an element.