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

A Nondeterministic Turing Machine (NTM): like a deterministic TM but with transition function δ : Q × Γ → 𝒫(Q × Γ × {L,R}), so each state/symbol may have multiple possible next moves.

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

def TuringMachine.NTM.stepWith {Q Γ : Type} (_M : NTM Q Γ) (c : Config Q Γ) (choice : Q × Γ × Direction) : Config Q Γ

Apply a specific nondeterministic choice = (q', b, d) to configuration c: write b, move the head in direction d, and transition to state q'.

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

The starting configuration of NTM M on input w: state q₀, head at position 0, tape containing w followed by blanks.

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

c is an accepting configuration of NTM M (state equals qAccept).

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

c is a rejecting configuration of NTM M (state equals qReject).

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

c is a halting configuration of NTM M: either accepting or rejecting.

def TuringMachine.NTM.IsBranch {Q Γ : Type} (M : NTM Q Γ) (w : List Γ) (branch : ℕ → Config Q Γ) : Prop

branch : ℕ → Config Q Γ is a valid computation branch of M on input w: it starts in initConfig w, stays put at halting configurations, and at each non-halting step picks some allowed nondeterministic transition.

def TuringMachine.NTM.branchHaltsWithOutput {Q Γ : Type} (M : NTM Q Γ) (branch : ℕ → Config Q Γ) (v : List Γ) : Prop

A branch halts with output v: it reaches an accepting configuration whose tape contents (from position 0) equal v, followed by blanks.

def TuringMachine.NTM.branchRejects {Q Γ : Type} (M : NTM Q Γ) (branch : ℕ → Config Q Γ) : Prop

A branch rejects: it reaches a rejecting configuration at some step n.

def TuringMachine.NTMComputes {Q Γ : Type} (M : NTM Q Γ) (f : List Γ → List Γ) : Prop

NTM M computes the function f : Σ* → Σ* (Sipser, Lecture 20): on every input w, every branch either halts with f w on the tape or rejects, and at least one branch does not reject.