Theorems · Definition · logic and foundations

Turing.TM0.Supports

{Γ : Type u_1} → {Λ : Type u_2} → [inst : Inhabited Λ] → Turing.TM0.Machine Γ Λ → Set Λ → Prop

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.

Defined in

Mathlib.Computability.TuringMachine.PostTuringMachine

Cited by

4 results in Mathlib

Foundations

Depth 4 from the axioms · uses no axioms

Assumes

Inhabited