The Mathlib computability library has theorems stating that Gödel codes of partial computable maps exist, but has no way of actually constructing them, because Nat.Partrec maps into Prop, evan though the proofs all seem to be explicit enough that the codes could be extracted.

 Consequently and unfortunately, we construct the first Kleene algebra in
 a non-computable manner.

@[reducible]

def FirstKleeneAlgebra.app : ℕ → ℕ →. ℕ

Equations

• FirstKleeneAlgebra.app = Nat.Partrec.Code.eval ∘ Denumerable.ofNat Nat.Partrec.Code

theorem FirstKleeneAlgebra.app_partrec₂ : Partrec₂ FirstKleeneAlgebra.app

instance FirstKleeneAlgebra.partialApplication : PartialApplication ℕ

Equations

• FirstKleeneAlgebra.partialApplication = { app := fun (u v : Part ℕ) => u.bind fun (m : ℕ) => v.bind fun (n : ℕ) => FirstKleeneAlgebra.app m n }

theorem FirstKleeneAlgebra.eq_ofNat_encodeCode (c : Nat.Partrec.Code) : Denumerable.ofNat Nat.Partrec.Code c.encodeCode = c

@[reducible]

def FirstKleeneAlgebra.K_map : ℕ → ℕ

Equations

• FirstKleeneAlgebra.K_map = Nat.Partrec.Code.encodeCode ∘ Nat.Partrec.Code.const

theorem FirstKleeneAlgebra.K_part : Computable FirstKleeneAlgebra.K_map

noncomputable def FirstKleeneAlgebra.K : Nat.Partrec.Code

Equations

• FirstKleeneAlgebra.K = FirstKleeneAlgebra.K.proof_1.choose

theorem FirstKleeneAlgebra.K_spec : FirstKleeneAlgebra.K.eval = fun (n : ℕ) => Part.some (Nat.Partrec.Code.const n).encodeCode

def FirstKleeneAlgebra.Partrec₃ {α β γ σ : Type} [Primcodable α] [Primcodable β] [Primcodable γ] [Primcodable σ] (f : α → β → γ →. σ) : Prop

Partially recursive partial functions α → β → σ between Primcodable types

Equations

• FirstKleeneAlgebra.Partrec₃ f = Partrec fun (p : α × β × γ) => f p.1 p.2.1 p.2.2

theorem FirstKleeneAlgebra.S_exists : ∃ (s : ℕ), ∀ (u v w : Part ℕ), u ⇓ → v ⇓ → w ⇓ → Part.some s ⬝ u ⬝ v ⬝ w = u ⬝ w ⬝ (v ⬝ w)

noncomputable instance FirstKleeneAlgebra.isPCA : PCA ℕ

Equations

• One or more equations did not get rendered due to their size.