Theorems · Definition · logic and foundations

Turing.TM0.Machine

Type u_1 → (Λ : Type u_2) → [Inhabited Λ] → Type (max (max u_1 u_2) u_1 u_2)

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.

Defined in

Mathlib.Computability.TuringMachine.PostTuringMachine

Cited by

5 results in Mathlib

Foundations

Depth 1 from the axioms · uses no axioms

Assumes

Inhabited