halting_problem — Mathlib

English

For every n, the halting problem is not recursively enumerable; there is no computable predicate that decides halting on input n.

Русский

Для каждого n проблема останова не перечислима; не существует вычислимого предиката, который определял бы останавку на входе n.

LaTeX

$$$$\forall n \in \mathbb{N},\; \neg \mathrm{REPred}(\lambda c. \text{halts on } n).$$$$

Lean4

/-- The **Halting problem** is not computable -/
theorem halting_problem (n) : ¬ComputablePred fun c => (eval c n).Dom
  | h => rice {f | (f n).Dom} h Nat.Partrec.zero Nat.Partrec.none trivial

Похожие утверждения