computability.partrec_code

let PR : α → nat.partrec.code → nat.partrec.code → σ → σ → σ := λ (a : α) (cf cg : nat.partrec.code) (hf hg : σ), pr a (cf, cg, hf, hg), CO : α → nat.partrec.code → nat.partrec.code → σ → σ → σ := λ (a : α) (cf cg : nat.partrec.code) (hf hg : σ), co a (cf, cg, hf, hg), PC : α → nat.partrec.code → nat.partrec.code → σ → σ → σ := λ (a : α) (cf cg : nat.partrec.code) (hf hg : σ), pc a (cf, cg, hf, hg), RF : α → nat.partrec.code → σ → σ := λ (a : α) (cf : nat.partrec.code) (hf : σ), rf a (cf, hf), F : α → nat.partrec.code → σ := λ (a : α) (c : nat.partrec.code), c.rec_on (z a) (s a) (l a) (r a) (PR a) (CO a) (PC a) (RF a) in primrec (λ (a : α), F a (c a))

source

theorem nat.partrec.code.rec_prim {α : Type u_1} {σ : Type u_2} [primcodable α] [primcodable σ] {c : α → nat.partrec.code} (hc : primrec c) {z : α → σ} (hz : primrec z) {s : α → σ} (hs : primrec s) {l : α → σ} (hl : primrec l) {r : α → σ} (hr : primrec r) {pr : α → nat.partrec.code → nat.partrec.code → σ → σ → σ} (hpr : primrec (λ (a : α × nat.partrec.code × nat.partrec.code × σ × σ), pr a.fst a.snd.fst a.snd.snd.fst a.snd.snd.snd.fst a.snd.snd.snd.snd)) {co : α → nat.partrec.code → nat.partrec.code → σ → σ → σ} (hco : primrec (λ (a : α × nat.partrec.code × nat.partrec.code × σ × σ), co a.fst a.snd.fst a.snd.snd.fst a.snd.snd.snd.fst a.snd.snd.snd.snd)) {pc : α → nat.partrec.code → nat.partrec.code → σ → σ → σ} (hpc : primrec (λ (a : α × nat.partrec.code × nat.partrec.code × σ × σ), pc a.fst a.snd.fst a.snd.snd.fst a.snd.snd.snd.fst a.snd.snd.snd.snd)) {rf : α → nat.partrec.code → σ → σ} (hrf : primrec (λ (a : α × nat.partrec.code × σ), rf a.fst a.snd.fst a.snd.snd)) :

let F : α → nat.partrec.code → σ := λ (a : α) (c : nat.partrec.code), c.rec_on (z a) (s a) (l a) (r a) (pr a) (co a) (pc a) (rf a) in primrec (λ (a : α), F a (c a))

Recursion on nat.partrec.code is primitive recursive.

source

theorem nat.partrec.code.rec_computable {α : Type u_1} {σ : Type u_2} [primcodable α] [primcodable σ] {c : α → nat.partrec.code} (hc : computable c) {z : α → σ} (hz : computable z) {s : α → σ} (hs : computable s) {l : α → σ} (hl : computable l) {r : α → σ} (hr : computable r) {pr : α → nat.partrec.code × nat.partrec.code × σ × σ → σ} (hpr : computable₂ pr) {co : α → nat.partrec.code × nat.partrec.code × σ × σ → σ} (hco : computable₂ co) {pc : α → nat.partrec.code × nat.partrec.code × σ × σ → σ} (hpc : computable₂ pc) {rf : α → nat.partrec.code × σ → σ} (hrf : computable₂ rf) :

let PR : α → nat.partrec.code → nat.partrec.code → σ → σ → σ := λ (a : α) (cf cg : nat.partrec.code) (hf hg : σ), pr a (cf, cg, hf, hg), CO : α → nat.partrec.code → nat.partrec.code → σ → σ → σ := λ (a : α) (cf cg : nat.partrec.code) (hf hg : σ), co a (cf, cg, hf, hg), PC : α → nat.partrec.code → nat.partrec.code → σ → σ → σ := λ (a : α) (cf cg : nat.partrec.code) (hf hg : σ), pc a (cf, cg, hf, hg), RF : α → nat.partrec.code → σ → σ := λ (a : α) (cf : nat.partrec.code) (hf : σ), rf a (cf, hf), F : α → nat.partrec.code → σ := λ (a : α) (c : nat.partrec.code), c.rec_on (z a) (s a) (l a) (r a) (PR a) (CO a) (PC a) (RF a) in computable (λ (a : α), F a (c a))

Recursion on nat.partrec.code is computable.

source

def nat.partrec.code.eval :

nat.partrec.code → ℕ →. ℕ

The interpretation of a nat.partrec.code as a partial function.

nat.partrec.code.zero: The constant zero function.
nat.partrec.code.succ: The successor function.
nat.partrec.code.left: Left unpairing of a pair of ℕ (encoded by nat.mkpair)
nat.partrec.code.right: Right unpairing of a pair of ℕ (encoded by nat.mkpair)
nat.partrec.code.pair: Pairs the outputs of argument codes using nat.mkpair.
nat.partrec.code.comp: Composition of two argument codes.
nat.partrec.code.prec: Primitive recursion. Given an argument of the form nat.mkpair a n:
- If n = 0, returns eval cf a.
- If n = succ k, returns eval cg (mkpair a (mkpair k (eval (prec cf cg) (mkpair a k))))
nat.partrec.code.rfind': Minimization. For f an argument of the form nat.mkpair a m, rfind' f m returns the least a such that f a m = 0, if one exists and f b m terminates for b < a

Equations

cf.rfind'.eval = nat.unpaired (λ (a m : ℕ), part.map (λ (_x : ℕ), _x + m) (nat.rfind (λ (n : ℕ), (λ (m : ℕ), decidable.to_bool (m = 0)) <$> cf.eval (nat.mkpair a (n + m)))))
(cf.prec cg).eval = nat.unpaired (λ (a n : ℕ), nat.elim (cf.eval a) (λ (y : ℕ) (IH : part ℕ), IH >>= λ (i : ℕ), cg.eval (nat.mkpair a (nat.mkpair y i))) n)
(cf.comp cg).eval = λ (n : ℕ), cg.eval n >>= cf.eval
(cf.pair cg).eval = λ (n : ℕ), nat.mkpair <$> cf.eval n <*> cg.eval n
nat.partrec.code.right.eval = ↑(λ (n : ℕ), (nat.unpair n).snd)
nat.partrec.code.left.eval = ↑(λ (n : ℕ), (nat.unpair n).fst)
nat.partrec.code.succ.eval = ↑nat.succ
nat.partrec.code.zero.eval = has_pure.pure 0

source

@[simp]

theorem nat.partrec.code.eval_prec_zero (cf cg : nat.partrec.code) (a : ℕ) :

(cf.prec cg).eval (nat.mkpair a 0) = cf.eval a

Helper lemma for the evaluation of prec in the base case.

source

theorem nat.partrec.code.eval_prec_succ (cf cg : nat.partrec.code) (a k : ℕ) :

(cf.prec cg).eval (nat.mkpair a k.succ) = (cf.prec cg).eval (nat.mkpair a k) >>= λ (ih : ℕ), cg.eval (nat.mkpair a (nat.mkpair k ih))

Helper lemma for the evaluation of prec in the recursive case.

source

@[protected, instance]

def nat.partrec.code.has_mem :

has_mem (ℕ →. ℕ) nat.partrec.code

Equations

nat.partrec.code.has_mem = {mem := λ (f : ℕ →. ℕ) (c : nat.partrec.code), c.eval = f}

source

@[simp]

theorem nat.partrec.code.eval_const (n m : ℕ) :

(nat.partrec.code.const n).eval m = part.some n

source

@[simp]

theorem nat.partrec.code.eval_id (n : ℕ) :

nat.partrec.code.id.eval n = part.some n

source

@[simp]

theorem nat.partrec.code.eval_curry (c : nat.partrec.code) (n x : ℕ) :

(c.curry n).eval x = c.eval (nat.mkpair n x)

source

theorem nat.partrec.code.const_prim :

primrec nat.partrec.code.const

source

theorem nat.partrec.code.curry_prim :

primrec₂ nat.partrec.code.curry

source

theorem nat.partrec.code.curry_inj {c₁ c₂ : nat.partrec.code} {n₁ n₂ : ℕ} (h : c₁.curry n₁ = c₂.curry n₂) :

c₁ = c₂ ∧ n₁ = n₂

source

theorem nat.partrec.code.smn :

∃ (f : nat.partrec.code → ℕ → nat.partrec.code), computable₂ f ∧ ∀ (c : nat.partrec.code) (n x : ℕ), (f c n).eval x = c.eval (nat.mkpair n x)

The $S_n^m$ theorem: There is a computable function, namely nat.partrec.code.curry, that takes a program and a ℕ n, and returns a new program using n as the first argument.

source

theorem nat.partrec.code.exists_code {f : ℕ →. ℕ} :

nat.partrec f ↔ ∃ (c : nat.partrec.code), c.eval = f

A function is partial recursive if and only if there is a code implementing it.

source

def nat.partrec.code.evaln (k : ℕ) :

nat.partrec.code → ℕ → option ℕ

A modified evaluation for the code which returns an option ℕ instead of a part ℕ. To avoid undecidability, evaln takes a parameter k and fails if it encounters a number ≥ k in the course of its execution. Other than this, the semantics are the same as in nat.partrec.code.eval.

Equations

nat.partrec.code.evaln (k + 1) cf.rfind' = λ (n : ℕ), guard (n ≤ k) >> nat.unpaired (λ (a m : ℕ), nat.partrec.code.evaln (k + 1) cf (nat.mkpair a m) >>= λ (x : ℕ), ite (x = 0) (has_pure.pure m) (nat.partrec.code.evaln k cf.rfind' (nat.mkpair a (m + 1)))) n
nat.partrec.code.evaln (k + 1) (cf.prec cg) = λ (n : ℕ), guard (n ≤ k) >> nat.unpaired (λ (a n : ℕ), nat.cases (nat.partrec.code.evaln (k + 1) cf a) (λ (y : ℕ), nat.partrec.code.evaln k (cf.prec cg) (nat.mkpair a y) >>= λ (i : ℕ), nat.partrec.code.evaln (k + 1) cg (nat.mkpair a (nat.mkpair y i))) n) n
nat.partrec.code.evaln (k + 1) (cf.comp cg) = λ (n : ℕ), guard (n ≤ k) >> (nat.partrec.code.evaln (k + 1) cg n >>= λ (x : ℕ), nat.partrec.code.evaln (k + 1) cf x)
nat.partrec.code.evaln (k + 1) (cf.pair cg) = λ (n : ℕ), guard (n ≤ k) >> nat.mkpair <$> nat.partrec.code.evaln (k + 1) cf n <*> nat.partrec.code.evaln (k + 1) cg n
nat.partrec.code.evaln (k + 1) nat.partrec.code.right = λ (n : ℕ), guard (n ≤ k) >> has_pure.pure (nat.unpair n).snd
nat.partrec.code.evaln (k + 1) nat.partrec.code.left = λ (n : ℕ), guard (n ≤ k) >> has_pure.pure (nat.unpair n).fst
nat.partrec.code.evaln (k + 1) nat.partrec.code.succ = λ (n : ℕ), guard (n ≤ k) >> has_pure.pure n.succ
nat.partrec.code.evaln (k + 1) nat.partrec.code.zero = λ (n : ℕ), guard (n ≤ k) >> has_pure.pure 0
nat.partrec.code.evaln 0 _x = λ (m : ℕ), option.none

source

theorem nat.partrec.code.evaln_bound {k : ℕ} {c : nat.partrec.code} {n x : ℕ} :

x ∈ nat.partrec.code.evaln k c n → n < k

source

theorem nat.partrec.code.evaln_mono {k₁ k₂ : ℕ} {c : nat.partrec.code} {n x : ℕ} :

k₁ ≤ k₂ → x ∈ nat.partrec.code.evaln k₁ c n → x ∈ nat.partrec.code.evaln k₂ c n

source

theorem nat.partrec.code.evaln_sound {k : ℕ} {c : nat.partrec.code} {n x : ℕ} :

x ∈ nat.partrec.code.evaln k c n → x ∈ c.eval n

source

theorem nat.partrec.code.evaln_complete {c : nat.partrec.code} {n x : ℕ} :

x ∈ c.eval n ↔ ∃ (k : ℕ), x ∈ nat.partrec.code.evaln k c n

source

theorem nat.partrec.code.evaln_prim :

primrec (λ (a : (ℕ × nat.partrec.code) × ℕ), nat.partrec.code.evaln a.fst.fst a.fst.snd a.snd)

The nat.partrec.code.evaln function is primitive recursive.

source

theorem nat.partrec.code.eval_eq_rfind_opt (c : nat.partrec.code) (n : ℕ) :

c.eval n = nat.rfind_opt (λ (k : ℕ), nat.partrec.code.evaln k c n)

source

theorem nat.partrec.code.eval_part :

partrec₂ nat.partrec.code.eval

source

theorem nat.partrec.code.fixed_point {f : nat.partrec.code → nat.partrec.code} (hf : computable f) :

∃ (c : nat.partrec.code), (f c).eval = c.eval

Roger's fixed-point theorem: Any total, computable f has a fixed point: That is, under the interpretation given by nat.partrec.code.eval, there is a code c such that c and f c have the same evaluation.

source

theorem nat.partrec.code.fixed_point₂ {f : nat.partrec.code → ℕ →. ℕ} (hf : partrec₂ f) :

∃ (c : nat.partrec.code), c.eval = f c

mathlib3 documentation

Gödel Numbering for Partial Recursive Functions. #

Main Definitions #

Main Results #

References #