Theorems · Inductive type · logic and foundations

Turing.TM1.Stmt

Type u_1 → Type u_2 → Type u_3 → Type (max (max u_1 u_2) u_3)

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.

Defined in

Mathlib.Computability.TuringMachine.PostTuringMachine

Cited by

49 results in Mathlib

Foundations

Depth 0 from the axioms · uses no axioms