structure
definition
TuringMachine
show as:
view math explainer →
open explainer
Read the cached plain-language explainer.
open lean source
IndisputableMonolith.Information.ChurchTuring on GitHub at line 46.
browse module
All declarations in this module, on Recognition.
explainer page
depends on
used by
formal source
43/-! ## Turing Machines -/
44
45/-- A Turing machine configuration. -/
46structure TuringMachine where
47 /-- Set of states -/
48 numStates : ℕ
49 /-- Tape alphabet size -/
50 alphabetSize : ℕ
51 /-- Nonempty states -/
52 states_nonempty : numStates > 0
53 /-- Nonempty alphabet -/
54 alphabet_nonempty : alphabetSize > 0
55
56/-- A TM transition: (state, symbol) → (new_state, new_symbol, direction). -/
57structure Transition where
58 currentState : ℕ
59 currentSymbol : ℕ
60 newState : ℕ
61 newSymbol : ℕ
62 moveRight : Bool -- True = right, False = left
63
64/-! ## Universal Turing Machine -/
65
66/-- A Universal Turing Machine (UTM) can simulate any other TM.
67
68 Given:
69 - Description of TM T (on tape)
70 - Input x
71
72 UTM computes T(x).
73
74 This is the foundation of programmable computers! -/
75structure UniversalTM where
76 base : TuringMachine