inductive TuringMachine.Direction : Type

The two possible directions in which a Turing machine head can move on each step: L for left, R for right.

• L : Direction
• R : Direction

@[implicit_reducible]

instance TuringMachine.instDecidableEqDirection : DecidableEq Direction

@[implicit_reducible]

instance TuringMachine.instReprDirection : Repr Direction

def TuringMachine.instReprDirection.repr : Direction → ℕ → Std.Format

@[implicit_reducible]

instance TuringMachine.instInhabitedDirection : Inhabited Direction

def TuringMachine.instInhabitedDirection.default : Direction

structure TuringMachine.TM (Q Γ : Type) : Type

A Turing machine, formalizing Sipser's 7-tuple (Q, Σ, Γ, δ, q₀, q_acc, q_rej):

• Q is the set of states,
• Γ is the tape alphabet containing a distinguished blank symbol,
• inputAlpha ⊆ Γ is the input alphabet (excluding blank),
• δ : Q × Γ → Q × Γ × {L, R} is the transition function,
• q₀, qAccept, qReject are the start, accept and reject states (with qReject ≠ qAccept).

• blank : Γ
• inputAlpha : Set Γ
• blank_not_in_inputAlpha : ¬self.blank ∈ self.inputAlpha
• δ : Q → Γ → Q × Γ × Direction
• q₀ : Q
• qAccept : Q
• qReject : Q
• qReject_ne_qAccept : self.qReject ≠ self.qAccept

@[reducible, inline]

abbrev TuringMachine.Tape (Γ : Type) : Type

A (two-way infinite) Turing-machine tape: a function from cell index ℤ to tape-alphabet symbols.

structure TuringMachine.Config (Q Γ : Type) : Type

A configuration of a Turing machine: current state, head position headPos on the tape, and the full tape contents tape.

• state : Q
• headPos : ℤ
• tape : Tape Γ

def TuringMachine.TM.step {Q Γ : Type} [DecidableEq Q] (M : TM Q Γ) (c : Config Q Γ) : Config Q Γ

One computation step of M: if the current state is qAccept or qReject the configuration is fixed; otherwise apply δ to write a new symbol, move the head left or right, and update the state.

def TuringMachine.TM.initConfig {Q Γ : Type} (M : TM Q Γ) (w : List Γ) : Config Q Γ

The initial configuration of M on input w: state q₀, head at position 0, and the tape containing w at positions 0, …, |w|-1 with blanks elsewhere.

def TuringMachine.TM.run {Q Γ : Type} [DecidableEq Q] (M : TM Q Γ) (c : Config Q Γ) : ℕ → Config Q Γ

Iterate M.step starting from configuration c for n steps.

def TuringMachine.TM.runOnInput {Q Γ : Type} [DecidableEq Q] (M : TM Q Γ) (w : List Γ) (n : ℕ) : Config Q Γ

The configuration of M after running n steps on input w, starting from M.initConfig w.

def TuringMachine.TM.isAcceptConfig {Q Γ : Type} (M : TM Q Γ) (c : Config Q Γ) : Prop

A configuration is "accepting" if its state equals M.qAccept.

def TuringMachine.TM.isRejectConfig {Q Γ : Type} (M : TM Q Γ) (c : Config Q Γ) : Prop

A configuration is "rejecting" if its state equals M.qReject.

def TuringMachine.TM.isHaltConfig {Q Γ : Type} (M : TM Q Γ) (c : Config Q Γ) : Prop

A configuration is "halting" if it is either accepting or rejecting.

def TuringMachine.TM.accepts {Q Γ : Type} [DecidableEq Q] (M : TM Q Γ) (w : List Γ) : Prop

M accepts the input w if at some step n the computation enters qAccept.

def TuringMachine.TM.rejects {Q Γ : Type} [DecidableEq Q] (M : TM Q Γ) (w : List Γ) : Prop

M rejects the input w (by halting) if at some step n the computation enters qReject.

def TuringMachine.TM.halts {Q Γ : Type} [DecidableEq Q] (M : TM Q Γ) (w : List Γ) : Prop

M halts on input w if it reaches a halting (accept or reject) configuration after some number of steps.

def TuringMachine.TM.language {Q Γ : Type} [DecidableEq Q] (M : TM Q Γ) : Set (List Γ)

The language L(M) recognized by M: the set of inputs w that M accepts.

def TuringMachine.TM.yields {Q Γ : Type} [DecidableEq Q] (M : TM Q Γ) (c₁ c₂ : Config Q Γ) : Prop

c₁ yields c₂ in one step: c₁ is not a halting configuration and M.step c₁ = c₂.

def TuringMachine.TM.yieldsMulti {Q Γ : Type} [DecidableEq Q] (M : TM Q Γ) (c₁ c₂ : Config Q Γ) : Prop

The reflexive-transitive closure of one-step yielding: c₁ reaches c₂ after some finite number of computation steps.

def TuringMachine.TM.hasAcceptingHistory {Q Γ : Type} [DecidableEq Q] (M : TM Q Γ) (w : List Γ) : Prop

M has an accepting computation history on w: at some step n the configuration is in qAccept. (Same as M.accepts w.)

def TuringMachine.TM.isDecider {Q Γ : Type} [DecidableEq Q] (M : TM Q Γ) : Prop

M is a decider: it halts on every input (never loops forever).

def TuringMachine.IsTuringRecognizable {Γ : Type} (A : Set (List Γ)) : Prop

A language A is Turing-recognizable if there is some Turing machine M with L(M) = A.

def TuringMachine.IsTuringDecidable {Γ : Type} (A : Set (List Γ)) : Prop

A language A is Turing-decidable if some TM decider M (a TM that halts on every input) satisfies L(M) = A.

def TuringMachine.TM.decides {Q Γ : Type} [DecidableEq Q] (M : TM Q Γ) (A : Set (List Γ)) : Prop

M decides A if M is a decider and L(M) = A.

theorem TuringMachine.TM.step_of_accept {Q Γ : Type} [DecidableEq Q] (M : TM Q Γ) (c : Config Q Γ) (h : M.isAcceptConfig c) : M.step c = c

Stepping an accepting configuration leaves it unchanged.

theorem TuringMachine.TM.step_of_reject {Q Γ : Type} [DecidableEq Q] (M : TM Q Γ) (c : Config Q Γ) (h : M.isRejectConfig c) : M.step c = c

Stepping a rejecting configuration leaves it unchanged.

theorem TuringMachine.TM.step_of_halt {Q Γ : Type} [DecidableEq Q] (M : TM Q Γ) (c : Config Q Γ) (h : M.isHaltConfig c) : M.step c = c

Halting configurations (accept or reject) are fixed points of M.step.

theorem TuringMachine.TM.accepts_stable {Q Γ : Type} [DecidableEq Q] (M : TM Q Γ) (c : Config Q Γ) (n : ℕ) (h : M.isAcceptConfig c) : M.isAcceptConfig (M.run c n)

Acceptance is stable under further steps: once accepted, always accepted.

theorem TuringMachine.TM.run_of_isHaltConfig {Q Γ : Type} [DecidableEq Q] (M : TM Q Γ) (c : Config Q Γ) (n : ℕ) (h : M.isHaltConfig c) : M.run c n = c

Running a TM from any halting configuration for any number of steps leaves the configuration unchanged.

@[simp]

theorem TuringMachine.TM.run_zero {Q Γ : Type} [DecidableEq Q] (M : TM Q Γ) (c : Config Q Γ) : M.run c 0 = c

Running for 0 steps returns the same configuration.

@[simp]

theorem TuringMachine.TM.run_succ {Q Γ : Type} [DecidableEq Q] (M : TM Q Γ) (c : Config Q Γ) (n : ℕ) : M.run c (n + 1) = M.step (M.run c n)

Unfolding lemma: running for n + 1 steps equals one step after running for n steps.

structure TuringMachine.LBA (Q Γ : Type) [DecidableEq Q] : Type

A Linearly Bounded Automaton (LBA): a 1-tape Turing machine whose head can never move off the input portion of the tape. Formally, on every input w and every step n, the head position lies in [0, max 1 |w|).

• toTM : TM Q Γ
• head_bounded (w : List Γ) (n : ℕ) : let c := self.toTM.runOnInput w n; 0 ≤ c.headPos ∧ c.headPos < ↑(max 1 w.length)

def TuringMachine.LBA.accepts {Q Γ : Type} [DecidableEq Q] (B : LBA Q Γ) (w : List Γ) : Prop

An LBA B accepts w iff its underlying TM accepts w.

def TuringMachine.LBA.language {Q Γ : Type} [DecidableEq Q] (B : LBA Q Γ) : Set (List Γ)

The language recognized by an LBA, inherited from its underlying TM.

def TuringMachine.LBA.isDecider {Q Γ : Type} [DecidableEq Q] (B : LBA Q Γ) : Prop

An LBA is a decider iff its underlying TM halts on every input.

structure TuringMachine.TuringEnumerator (Q Γ : Type) [DecidableEq Q] : Type

A Turing enumerator: a deterministic TM together with a "printing" predicate prints specifying which strings have been output by step n (viewing each Config as the state of the enumerator after some number of steps). The enumerated language is the union of these print sets.

• toTM : TM Q Γ
• prints : Config Q Γ → Set (List Γ)

def TuringMachine.TuringEnumerator.initConfig {Q Γ : Type} [DecidableEq Q] (E : TuringEnumerator Q Γ) : Config Q Γ

The initial configuration of an enumerator: start state, head at 0, and an all-blank tape.

def TuringMachine.TuringEnumerator.run {Q Γ : Type} [DecidableEq Q] (E : TuringEnumerator Q Γ) (n : ℕ) : Config Q Γ

The configuration of the enumerator after n steps.

def TuringMachine.TuringEnumerator.language {Q Γ : Type} [DecidableEq Q] (E : TuringEnumerator Q Γ) : Set (List Γ)

The language L(E) enumerated by E: all strings w that appear in the print set of some run-step configuration.

def TuringMachine.IsTuringEnumerable {Γ : Type} (A : Set (List Γ)) : Prop

A language A is Turing-enumerable if there is a Turing enumerator E with L(E) = A.

noncomputable def TuringMachine.countingTM {Γ : Type} (blank : Γ) (inputAlpha : Set Γ) (h : ¬blank ∈ inputAlpha) : TM ℕ Γ

An auxiliary "counting" TM with state set ℕ: it starts in state 2, never halts (it never reaches the accept state 0 or reject state 1), and on each step increments its state by 1. Used as the driver for enumerators built from recognizers.

theorem TuringMachine.countingTM_step_state {Γ : Type} (blank : Γ) (inputAlpha : Set Γ) (h : ¬blank ∈ inputAlpha) (c : Config ℕ Γ) (hc : c.state ≥ 2) : ((countingTM blank inputAlpha h).step c).state = c.state + 1

One step of countingTM from a non-halting state (state ≥ 2) increments the state by 1.

theorem TuringMachine.countingTM_run_state {Γ : Type} (blank : Γ) (inputAlpha : Set Γ) (h : ¬blank ∈ inputAlpha) (c : Config ℕ Γ) (hc : c.state = 2) (n : ℕ) : ((countingTM blank inputAlpha h).run c n).state = 2 + n

Running countingTM for n steps starting from state 2 reaches state 2 + n; in particular, the step count can be read off from the state.

theorem TuringMachine.isTuringEnumerable_of_isTuringRecognizable {Γ : Type} {A : Set (List Γ)} (h : IsTuringRecognizable A) : IsTuringEnumerable A

Forward direction of the equivalence "T-recognizable ↔ T-enumerable": every Turing-recognizable language is Turing-enumerable. The proof simulates the recognizer M step-by-step on every input w, printing w exactly when M accepts w within the current step budget.

theorem TuringMachine.isTuringRecognizable_of_isTuringEnumerable {Γ : Type} {A : Set (List Γ)} (h : IsTuringEnumerable A) : IsTuringRecognizable A

Converse direction: every Turing-enumerable language is Turing-recognizable. A recognizer simulates the enumerator and accepts as soon as it prints the input string.

theorem TuringMachine.isTuringRecognizable_iff_isTuringEnumerable {Γ : Type} (A : Set (List Γ)) : IsTuringRecognizable A ↔ IsTuringEnumerable A

Sipser's theorem: a language A is Turing-recognizable iff it is Turing-enumerable (i.e. is the language of some Turing enumerator).

def TuringMachine.TM.haltsWithin {Q Γ : Type} [DecidableEq Q] (M : TM Q Γ) (w : List Γ) (t : ℕ) : Prop

M halts on w within the time bound t: there is some step count n ≤ t at which M is already in a halting configuration.

def TuringMachine.TM.decidesInTime {Q Γ : Type} [DecidableEq Q] (M : TM Q Γ) (A : Set (List Γ)) (f : ℕ → ℕ) : Prop

M decides A in time f: M decides A, and on every input w of length n it halts within f n steps.

def TuringMachine.IsDecidableInTime {Γ : Type} (A : Set (List Γ)) (f : ℕ → ℕ) : Prop

A is decidable in (big-O) time f: some TM M decides A within c · f n steps on inputs of length n, for some positive constant c.

inductive TuringMachine.ABSymbol : Type

A working tape alphabet for the language {a^k b^k} decider: input symbols a and b, plus a marker cross (used to cross off symbols during scanning) and a blank.

• a : ABSymbol
• b : ABSymbol
• cross : ABSymbol
• blank : ABSymbol

@[implicit_reducible]

instance TuringMachine.instDecidableEqABSymbol : DecidableEq ABSymbol

@[implicit_reducible]

instance TuringMachine.instReprABSymbol : Repr ABSymbol

def TuringMachine.instReprABSymbol.repr : ABSymbol → ℕ → Std.Format

@[implicit_reducible]

instance TuringMachine.instInhabitedABSymbol : Inhabited ABSymbol

def TuringMachine.instInhabitedABSymbol.default : ABSymbol

def TuringMachine.lang_akbk : Set (List ABSymbol)

The classic non-regular language A = {a^k b^k | k ≥ 0} over the alphabet {a, b}.

def TuringMachine.nlogn (n : ℕ) : ℕ

The time-bound function n · (⌊log₂ n⌋ + 1), used as an upper estimate for O(n log n) running times.

theorem TuringMachine.deciding_akbk_nlogn : IsDecidableInTime lang_akbk nlogn

Sipser's O(n log n) decider: a 1-tape Turing machine decides A = {a^k b^k | k ≥ 0} in time O(n log n).