inductive RecursionTheorem.TMResult : Type

Possible outcomes of running a Turing machine on an input: accept (enter the accept state), reject (halt in the reject state) or diverge (run forever). Matches the three TM outcomes described in Sipser's formal definition.

• accept : TMResult
• reject : TMResult
• diverge : TMResult

@[implicit_reducible]

instance RecursionTheorem.instDecidableEqTMResult : DecidableEq TMResult

structure RecursionTheorem.TMCoding (Γ : Type) : Type 1

An abstract acceptable indexing of Turing machines, stronger than the language-level version used in SelfReference.lean because it records the full behavior (accept/reject/diverge) of each machine on each input rather than just the language. Provides the standard ingredients needed to prove the Recursion Theorem: encoding/decoding, a pairing function, an smn function with the usual specification, a notion of computable index transformations, representability of computable transformations, and closure of IsComputable under composition and the diagonal x ↦ smn x x.

• TMIndex : Type
• encode : self.TMIndex → List Γ
• behavior : self.TMIndex → List Γ → TMResult
• decode : List Γ → Option self.TMIndex
• decode_encode (M : self.TMIndex) : self.decode (self.encode M) = some M
• pair : List Γ → List Γ → List Γ
• pair_injective (a b c d : List Γ) : self.pair a b = self.pair c d → a = c ∧ b = d
• smn : self.TMIndex → self.TMIndex → self.TMIndex
• smn_spec (e x : self.TMIndex) (w : List Γ) : self.behavior (self.smn e x) w = self.behavior e (self.pair w (self.encode x))
• IsComputable : (self.TMIndex → self.TMIndex) → Prop
• representable (h : self.TMIndex → self.TMIndex) : self.IsComputable h → ∃ (e : self.TMIndex), ∀ (x : self.TMIndex) (w : List Γ), self.behavior (self.smn e x) w = self.behavior (h x) w
• isComputable_smn_diag : self.IsComputable fun (x : self.TMIndex) => self.smn x x
• isComputable_comp (f g : self.TMIndex → self.TMIndex) : self.IsComputable f → self.IsComputable g → self.IsComputable (f ∘ g)
• isComputable_smn_apply (e : self.TMIndex) : self.IsComputable (self.smn e)

def RecursionTheorem.TMCoding.languageOf {Γ : Type} (C : TMCoding Γ) (M : C.TMIndex) : Set (List Γ)

The language of a TM index M: the set of inputs w on which M accepts.

theorem RecursionTheorem.recursion_theorem {Γ : Type} (C : TMCoding Γ) (t : C.TMIndex → C.TMIndex) (ht : C.IsComputable t) : ∃ (R : C.TMIndex), ∀ (w : List Γ), C.behavior R w = C.behavior (t R) w

Recursion Theorem (Sipser, Lecture 11). For any computable transformation t : TMIndex → TMIndex of TM indices there exists R such that for every input w, R and t R produce the same behavior — R operates the same as t R. In particular, R has access to its own description via t.

Proof sketch: let h x = t (smn x x); by representability of computable transformations there is e₀ with behavior (smn e₀ x) w = behavior (h x) w; take R = smn e₀ e₀.

theorem RecursionTheorem.recursion_theorem_language {Γ : Type} (C : TMCoding Γ) (t : C.TMIndex → C.TMIndex) (ht : C.IsComputable t) : ∃ (R : C.TMIndex), C.languageOf R = C.languageOf (t R)

Language-level corollary of the Recursion Theorem: for any computable t : TMIndex → TMIndex there exists R with L(R) = L(t R). Follows from recursion_theorem by taking accepting inputs on both sides.