Nat.Partrec'.of_eq
theorem Nat.Partrec'.of_eq :
∀ {n : ℕ} {f g : Vector ℕ n →. ℕ}, Nat.Partrec' f → (∀ (i : Vector ℕ n), f i = g i) → Nat.Partrec' g
The theorem `Nat.Partrec'.of_eq` states that for any natural number `n` and any two partial recursive functions `f` and `g` from a vector of `n` natural numbers to a natural number, if `f` is partial recursive and `f` and `g` are equal for every `i` of type `Vector ℕ n`, then `g` is also partial recursive. Here, `Nat.Partrec'` refers to partial recursive functions and `Vector ℕ n` indicates a list of length `n` with elements being natural numbers. This theorem essentially guarantees the preservation of partial recursion under pointwise equality.
More concisely: If two partial recursive functions from a vector of natural numbers to a natural number agree on every input vector, then the second function is also partial recursive.
|
ComputablePred.rice
theorem ComputablePred.rice :
∀ (C : Set (ℕ →. ℕ)),
(ComputablePred fun c => c.eval ∈ C) → ∀ {f g : ℕ →. ℕ}, Nat.Partrec f → Nat.Partrec g → f ∈ C → g ∈ C
**Rice's Theorem**: This theorem states that for any set `C` of partial functions from natural numbers to natural numbers, if the predicate stating that the evaluation of a certain code `c` belongs to `C` is computable, then for any two partial functions `f` and `g` from natural numbers to natural numbers, if `f` and `g` are both recursively enumerable (i.e., their values can be computed by a Turing machine) and `f` belongs to `C`, then `g` must also belong to `C`. In essence, this theorem is a fundamental result in computability theory that illustrates the limitations of mechanical computation.
More concisely: If a set `C` of partial functions from natural numbers to natural numbers has a computable membership predicate, then any recursively enumerable `f` in `C` implies that any recursively enumerable `g` is also in `C`.
|
ComputablePred.halting_problem
theorem ComputablePred.halting_problem : ∀ (n : ℕ), ¬ComputablePred fun c => (c.eval n).Dom
The theorem `ComputablePred.halting_problem` states that the Halting problem is not computable. It says that for every natural number `n`, there is no computable predicate for the function which takes a natural number `c` and checks if the evaluation of `c` at `n` is defined. This is a reflection of the famous result in computer science that the Halting problem, the problem of determining whether a given program halts or not for a given input, is undecidable.
More concisely: The theorem `ComputablePred.halting_problem` asserts that there is no computable predicate determining if a given natural number represents a computable function that halts when applied to a specific natural number `n`.
|
ComputablePred.halting_problem_re
theorem ComputablePred.halting_problem_re : ∀ (n : ℕ), RePred fun c => (c.eval n).Dom
The theorem `ComputablePred.halting_problem_re` states that for any natural number `n`, the Halting problem - defined as the predicate that determines if a given computable function halts on input `n` - is recursively enumerable. In other words, there is a computable partial function whose domain is exactly the set of such computable functions which halt on input `n`.
More concisely: The Halting problem, defined as a predicate determining if a computable function halts on a given input, is recursively enumerable.
|