Computability and undecidability

Recursive and recursively enumerable predicates and their closure properties, the halting problem, Rice's and Rice–Shapiro theorems, the recursion and s-m-n theorems, enumerators, index sets such as totality, finiteness and minimal programs, and Busy Beaver functions.

TheoremParametrized s-m-n theorem#✓fully proved

Let \(\alpha\) be a type with a primitive recursive encoding into the natural numbers, and for each \(a \in \alpha\) let \(F_a\) be a partial function from \(\mathbb{N}\) to \(\mathbb{N}\), such that \((a, x) \mapsto F_a(x)\) is partial recursive. Then there is a computable map \(g\) from \(\alpha\) to codes of partial recursive functions such that for all \(a \in \alpha\) and \(x \in \mathbb{N}\), the partial function with code \(g(a)\) agrees with \(F_a\) at \(x\): both are undefined, or both are defined with the same value.

theorem exists_computable_code {α : Type*} [Primcodable α] {F : α → ℕ →. ℕ} (hF : Partrec₂ F) :
    ∃ g : α → Code, Computable g ∧ ∀ a x, (g a).eval x = F a x

Used by 6

Used byHalting reduces to finiteness · Non-halting reduces to finiteness · Effective Rice–Shapiro, necessity · Rice–Shapiro, finite approximation · Rice–Shapiro, upward closure · Non-halting on zero reduces to totality

• Busy beaver
• Decidable and recognizable predicates
• Enumerators
• Halting problem and Rice's theorem
• Emptiness and equivalence problems for programs
• Halting problem for single-tape Turing machines
• Kleene's recursion theorem
• Minimal programs
• Rice's theorem for acceptable numberings
• Rice–Shapiro theorem
• Totality problem for programs
• Finiteness problem for programs

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.