Nat.Partrec.Code.fixed_point
theorem Nat.Partrec.Code.fixed_point :
∀ {f : Nat.Partrec.Code → Nat.Partrec.Code}, Computable f → ∃ c, (f c).eval = c.eval
Roger's fixed-point theorem asserts that for any total computable function `f` that transforms one piece of Nat.Partrec.Code into another, there exists a 'fixed point' code `c` such that when `f` is applied to `c`, the output code evaluates to the same value as `c` itself when interpreted via `Nat.Partrec.Code.eval`. In other words, there exists a code `c` such that the evaluation of `f(c)` equals the evaluation of `c`. This theorem is a manifestation of the fixed-point principle in the context of recursive functions and computability theory.
More concisely: For any total computable function `f` on `Nat.Partrec.Code`, there exists a fixed point `c` such that `f(c) = c` when evaluated with `Nat.Partrec.Code.eval`.
|
Nat.Partrec.Code.rec_computable
theorem Nat.Partrec.Code.rec_computable :
∀ {α : Type u_1} {σ : Type u_2} [inst : Primcodable α] [inst_1 : Primcodable σ] {c : α → Nat.Partrec.Code},
Computable c →
∀ {z : α → σ},
Computable z →
∀ {s : α → σ},
Computable s →
∀ {l : α → σ},
Computable l →
∀ {r : α → σ},
Computable r →
∀ {pr : α → Nat.Partrec.Code × Nat.Partrec.Code × σ × σ → σ},
Computable₂ pr →
∀ {co : α → Nat.Partrec.Code × Nat.Partrec.Code × σ × σ → σ},
Computable₂ co →
∀ {pc : α → Nat.Partrec.Code × Nat.Partrec.Code × σ × σ → σ},
Computable₂ pc →
∀ {rf : α → Nat.Partrec.Code × σ → σ},
Computable₂ rf →
let PR := fun a cf cg hf hg => pr a (cf, cg, hf, hg);
let CO := fun a cf cg hf hg => co a (cf, cg, hf, hg);
let PC := fun a cf cg hf hg => pc a (cf, cg, hf, hg);
let RF := fun a cf hf => rf a (cf, hf);
let F := fun a c =>
Nat.Partrec.Code.recOn c (z a) (s a) (l a) (r a) (PR a) (CO a) (PC a) (RF a);
Computable fun a => F a (c a)
This theorem states that recursion on `Nat.Partrec.Code` is computable. Given types `α` and `σ` that are `Primcodable`, and functions `c`, `z`, `s`, `l`, `r`, `pr`, `co`, `pc`, `rf` which are assumed to be computable, then the function `F` defined using recursion on the `Nat.Partrec.Code` of `c` is computable. Here, `F` is defined using the given functions: it takes `a` and `c` as inputs and then, according to the value of `c`, applies either `z`, `s`, `l`, `r`, or a pairing operation `PR`, `CO`, `PC`, `RF` respectively, with `a` and different combinations of the inputs.
More concisely: Given computable functions `c`, `z`, `s`, `l`, `r`, `pr`, `co`, `pc`, `rf` and a `Primcodable` type `α`, the recursive function `F` defined using `Nat.Partrec.Code` of `c` is computable.
|
Nat.Partrec.Code.exists_code
theorem Nat.Partrec.Code.exists_code : ∀ {f : ℕ →. ℕ}, Nat.Partrec f ↔ ∃ c, c.eval = f
This theorem states that a function is partially recursive if and only if there exists a code that implements it. In other words, for every function `f` from natural numbers to partial natural numbers, `f` is partially recursive if there is a code `c`, such that the evaluation of `c` equals `f`. This establishes `eval` as a universal partial recursive function.
More concisely: A function `f` from natural numbers to partial natural numbers is partially recursive if and only if there exists a code `c` such that for all natural numbers `x`, `eval(c)(x) = f(x)`.
|
Nat.Partrec.Code.eval_curry
theorem Nat.Partrec.Code.eval_curry : ∀ (c : Nat.Partrec.Code) (n x : ℕ), (c.curry n).eval x = c.eval (n.pair x) := by
sorry
The theorem `Nat.Partrec.Code.eval_curry` states that for any natural number code `c`, and any natural numbers `n` and `x`, evaluating the result of currying `c` with `n` at `x` is equivalent to evaluating `c` at the pair of `n` and `x`. In other words, the currying operation in the context of `Nat.Partrec.Code` behaves as expected: it binds the first argument of the input code to a specific value and the result is a code that takes one less argument.
More concisely: For any natural number code `c`, evaluating `c (n, x)` is equivalent to evaluating `(Nat.Partrec.Code.eval_curry c n) x` in `Nat.Partrec.Code`.
|
Nat.Partrec.Code.eval_part
theorem Nat.Partrec.Code.eval_part : Partrec₂ Nat.Partrec.Code.eval
The theorem `Nat.Partrec.Code.eval_part` states that the evaluation function for "partial recursive" natural number codes, `Nat.Partrec.Code.eval`, is a partial recursive function of two arguments. Here, a function is called "partially recursive" if it can be computed by a Turing machine. The function `Nat.Partrec.Code.eval` takes two arguments: a code and a natural number, and it returns a computation which may or may not return a natural number (captured by the `Part` in `Partrec₂`). The theorem shows that this function is computable.
More concisely: The theorem `Nat.Partrec.Code.eval_part` asserts that the function `Nat.Partrec.Code.eval` defining the evaluation of partial recursive natural number codes is a partial recursive function.
|
Nat.Partrec.Code.evaln_prim
theorem Nat.Partrec.Code.evaln_prim : Primrec fun a => Nat.Partrec.Code.evaln a.1.1 a.1.2 a.2
The theorem `Nat.Partrec.Code.evaln_prim` asserts that the function `Nat.Partrec.Code.evaln` is primitive recursive. This means that given an input tuple `a`, where `a` consists of a pair of natural numbers and another natural number (denoted as `a.1.1`, `a.1.2`, and `a.2`), the function `Nat.Partrec.Code.evaln` can be computed using only primitive recursion. Here, 'primitive recursion' refers to a restricted form of recursion where a function's value at a certain point depends only on the values at smaller points.
More concisely: The theorem `Nat.Partrec.Code.evaln_prim` states that the function `Nat.Partrec.Code.evaln` is primitive recursive.
|
Nat.Partrec.Code.eval_prec_zero
theorem Nat.Partrec.Code.eval_prec_zero :
∀ (cf cg : Nat.Partrec.Code) (a : ℕ), (cf.prec cg).eval (a.pair 0) = cf.eval a
This theorem, `Nat.Partrec.Code.eval_prec_zero`, states that for any given natural number `a` and any two partial recursive codes `cf` and `cg`, evaluating the 'precursor' function of `cf` and `cg` at a pair `(a, 0)` is equivalent to evaluating `cf` at `a`. In other words, it provides a base case for the evaluation of the 'precursor' operation in the world of partial recursive functions.
More concisely: For any natural number `a` and partial recursive codes `cf` and `cg`, `cf.precursor cf.code cg.code (a, 0)` is equivalent to `cf a`.
|
Nat.Partrec.Code.curry_prim
theorem Nat.Partrec.Code.curry_prim : Primrec₂ Nat.Partrec.Code.curry
The theorem `Nat.Partrec.Code.curry_prim` states that the function `Nat.Partrec.Code.curry`, which takes a code `c` and a natural number `n`, returning a new code that uses `n` as the first argument to `c`, is a binary primitive recursive function. In other words, the process of currying in the context of partial recursive functions on natural numbers, as defined by `Nat.Partrec.Code.curry`, is itself a primitive recursive operation. This means that it can be computed using only a finite number of steps, each of which may be a basic arithmetic operation, a conditional, or a composition of such steps.
More concisely: The function `Nat.Partrec.Code.curry` that curries a partial recursive function on natural numbers is a primitive recursive function.
|
Nat.Partrec.Code.eval_prec_succ
theorem Nat.Partrec.Code.eval_prec_succ :
∀ (cf cg : Nat.Partrec.Code) (a k : ℕ),
(cf.prec cg).eval (a.pair k.succ) = do
let ih ← (cf.prec cg).eval (a.pair k)
cg.eval (a.pair (k.pair ih))
This theorem, `Nat.Partrec.Code.eval_prec_succ`, is a helper lemma for evaluating the `prec` function in recursive cases. For any natural numbers `a` and `k`, and any partial recursive functions `cf` and `cg`, the evaluation of the `prec` function applied to `cf` and `cg` at `(a.pair k.succ)` is equivalent to first performing the evaluation of the `prec` function applied to `cf` and `cg` at `(a.pair k)`, and then evaluating `cg` at the pair made of `a` and the result of the first evaluation paired with `k`.
More concisely: For any natural numbers `a` and `k`, and partial recursive functions `cf` and `cg`, `prec cf cg (a.pair (k.succ))` equals `prec cf cg (a.pair k) ++ cg (a, prec cf cg (a.pair k))`.
|
Nat.Partrec.Code.rec_prim
theorem Nat.Partrec.Code.rec_prim :
∀ {α : Type u_1} {σ : Type u_2} [inst : Primcodable α] [inst_1 : Primcodable σ] {c : α → Nat.Partrec.Code},
Primrec c →
∀ {z : α → σ},
Primrec z →
∀ {s : α → σ},
Primrec s →
∀ {l : α → σ},
Primrec l →
∀ {r : α → σ},
Primrec r →
∀ {pr : α → Nat.Partrec.Code → Nat.Partrec.Code → σ → σ → σ},
(Primrec fun a => pr a.1 a.2.1 a.2.2.1 a.2.2.2.1 a.2.2.2.2) →
∀ {co : α → Nat.Partrec.Code → Nat.Partrec.Code → σ → σ → σ},
(Primrec fun a => co a.1 a.2.1 a.2.2.1 a.2.2.2.1 a.2.2.2.2) →
∀ {pc : α → Nat.Partrec.Code → Nat.Partrec.Code → σ → σ → σ},
(Primrec fun a => pc a.1 a.2.1 a.2.2.1 a.2.2.2.1 a.2.2.2.2) →
∀ {rf : α → Nat.Partrec.Code → σ → σ},
(Primrec fun a => rf a.1 a.2.1 a.2.2) →
let F := fun a c =>
Nat.Partrec.Code.recOn c (z a) (s a) (l a) (r a) (pr a) (co a) (pc a) (rf a);
Primrec fun a => F a (c a)
This theorem states that given some types `α` and `σ`, for which we have instances of `Primcodable`, and a function `c` from `α` to `Nat.Partrec.Code` that is primitive recursive, if we also have a set of primitive recursive functions `z`, `s`, `l`, `r`, `pr`, `co`, `pc`, and `rf` from `α` to `σ` or combinations of `α`, `Nat.Partrec.Code`, and `σ`, then the function `F` defined for each `a` in `α` and `c` in `Nat.Partrec.Code` as the result of the recursive application of these functions on `c` (with `z`, `s`, `l`, `r` for zero, successor, left and right projections, `pr`, `co`, `pc` for primitive recursion, composition and pair construction, and `rf` for result function) is also primitive recursive.
More concisely: Given primitive recursive functions `z, s, l, r, pr, co, pc, rf : α -> σ or α -> Nat.Partrec.Code -> σ, and a primitive recursive function `c : α -> Nat.Partrec.Code`, the function `F : α -> σ` defined as the result of recursive application of these functions on `c` is also primitive recursive.
|
Nat.Partrec.Code.smn
theorem Nat.Partrec.Code.smn :
∃ f, Computable₂ f ∧ ∀ (c : Nat.Partrec.Code) (n x : ℕ), (f c n).eval x = c.eval (n.pair x)
The theorem, often referred to as the $S^n_m$ theorem, states that there exists a computable function, specifically `Nat.Partrec.Code.curry`, that accepts a program and a natural number `n` and produces a new program in which `n` serves as the first argument. The theorem further ensures that for any program `c` and natural numbers `n` and `x`, evaluating the new program with `x` will yield the same result as evaluating the original program with `n` and `x` as a pair.
More concisely: There exists a computable function `Nat.Partrec.Code.curry` such that for all programs `c` and natural numbers `n` and `x`, `(Nat.Partrec.Code.curry c n) x = c (n, x)`.
|