Programming with PCAs

A (non-trivial) PCA is Turing-complete in the sense that it implements every partial computable function. We develop here basic programming constructs that witness this fact:

• the identity combinatory I
• ordered pairs pair with projections fst and snd
• booleans true, false and the conditional statement ite
• fixed-point combinators Z and Y
• Curry numerals numeral n with zero, successor succ, predecessor pred and primitive recursion primrec
• TODO: general recursion (but it should be easy given what we have)

For any of the combinators so defined, say C, we also prove two lemmas: df_C characterizes totality of expressions involving C, and eq_C gives the characteristic equation for C. These lemmas are automatically used by simp.

def PCA.I {A : Type u} [PCA A] : Part A

The identity combinator

Equations

• PCA.I = PCA.S ⬝ PCA.K ⬝ PCA.K

def PCA.Expr.I {A : Type u} {Γ : Type u_1} : PCA.Expr Γ A

The expression denoting the identity combinator

Equations

• PCA.Expr.I = PCA.Expr.S ⬝ PCA.Expr.K ⬝ PCA.Expr.K

@[simp]

theorem PCA.df_I {A : Type u} [PCA A] : PCA.I ⇓

@[simp]

theorem PCA.eq_I {A : Type u} [PCA A] {u : Part A} : u ⇓ → PCA.I ⬝ u = u

def PCA.K' {A : Type u} [PCA A] : Part A

Equations

• PCA.K' = PCA.K ⬝ PCA.I

def PCA.Expr.K' {A : Type u} {Γ : Type u_1} : PCA.Expr Γ A

Equations

• PCA.Expr.K' = PCA.Expr.K ⬝ PCA.Expr.I

@[simp]

theorem PCA.df_K' {A : Type u} [PCA A] : PCA.K' ⇓

@[simp]

theorem PCA.eq_K' {A : Type u} [PCA A] (u v : Part A) : u ⇓ → v ⇓ → PCA.K' ⬝ u ⬝ v = v

Pairing

def PCA.pair {A : Type u} [PCA A] : Part A

Equations

• PCA.pair = PCA.compile (PCA.abstr `x (PCA.abstr `y (PCA.abstr `z (PCA.Expr.var `z ⬝ PCA.Expr.var `x ⬝ PCA.Expr.var `y))))

@[simp]

theorem PCA.df_pair {A : Type u} [PCA A] : PCA.pair ⇓

@[simp]

theorem PCA.df_pair_app {A : Type u} [PCA A] (u : Part A) : u ⇓ → (PCA.pair ⬝ u) ⇓

@[simp]

theorem PCA.df_pair_app_app {A : Type u} [PCA A] (u v : Part A) : u ⇓ → v ⇓ → (PCA.pair ⬝ u ⬝ v) ⇓

@[simp]

theorem PCA.eq_pair {A : Type u} [PCA A] (u v w : Part A) : u ⇓ → v ⇓ → w ⇓ → PCA.pair ⬝ u ⬝ v ⬝ w = w ⬝ u ⬝ v

def PCA.fst {A : Type u} [PCA A] : Part A

Equations

• PCA.fst = PCA.compile (PCA.abstr `x (PCA.Expr.var `x ⬝ PCA.Expr.K))

def PCA.fst.elm {A : Type u} [PCA A] {Γ : Type u_1} : PCA.Expr Γ A

Equations

• PCA.fst.elm = PCA.Expr.elm (PCA.fst.get ⋯)

@[simp]

theorem PCA.eq_fst {A : Type u} [PCA A] (u : Part A) : u ⇓ → PCA.fst ⬝ u = u ⬝ PCA.K

def PCA.snd {A : Type u} [PCA A] : Part A

Equations

• PCA.snd = PCA.compile (PCA.abstr `x (PCA.Expr.var `x ⬝ PCA.Expr.K'))

def PCA.snd.elm {A : Type u} [PCA A] {Γ : Type u_1} : PCA.Expr Γ A

Equations

• PCA.snd.elm = PCA.Expr.elm (PCA.snd.get ⋯)

@[simp]

theorem PCA.eq_snd {A : Type u} [PCA A] (u : Part A) : u ⇓ → PCA.snd ⬝ u = u ⬝ PCA.K'

@[simp]

def PCA.eq_fst_pair {A : Type u} [PCA A] (u v : Part A) : u ⇓ → v ⇓ → PCA.fst ⬝ (PCA.pair ⬝ u ⬝ v) = u

Equations

• ⋯ = ⋯

@[simp]

def PCA.eq_snd_pair {A : Type u} [PCA A] (u v : Part A) : u ⇓ → v ⇓ → PCA.snd ⬝ (PCA.pair ⬝ u ⬝ v) = v

Equations

• ⋯ = ⋯

def PCA.ite {A : Type u} [PCA A] : Part A

Conditional statements

Equations

• PCA.ite = PCA.I

def PCA.fal {A : Type u} [PCA A] : Part A

The bollean false

Equations

• PCA.fal = PCA.K'

@[simp]

theorem PCA.df_fal {A : Type u} [PCA A] : PCA.fal ⇓

@[simp]

theorem PCA.eq_fal {A : Type u} [PCA A] (u v : Part A) : u ⇓ → v ⇓ → PCA.fal ⬝ u ⬝ v = v

def PCA.tru {A : Type u} [PCA A] : Part A

The boolean true

Equations

• PCA.tru = PCA.K

@[simp]

theorem PCA.df_tru {A : Type u} [PCA A] : PCA.tru ⇓

@[simp]

theorem PCA.eq_ite_fal {A : Type u} [PCA A] (u v : Part A) : u ⇓ → v ⇓ → PCA.ite ⬝ PCA.fal ⬝ u ⬝ v = v

@[simp]

theorem PCA.eq_ite_tru {A : Type u} [PCA A] (u v : Part A) : u ⇓ → v ⇓ → PCA.ite ⬝ PCA.tru ⬝ u ⬝ v = u

The fixed point combinator

def PCA.X {A : Type u} [PCA A] : Part A

Equations

• PCA.X = PCA.compile (PCA.abstr `x (PCA.abstr `y (PCA.abstr `z (PCA.Expr.var `y ⬝ (PCA.Expr.var `x ⬝ PCA.Expr.var `x ⬝ PCA.Expr.var `y) ⬝ PCA.Expr.var `z))))

@[simp]

theorem PCA.df_X {A : Type u} [PCA A] : PCA.X ⇓

@[simp]

theorem PCA.df_X_app {A : Type u} [PCA A] (u : Part A) : u ⇓ → (PCA.X ⬝ u) ⇓

@[simp]

theorem PCA.df_X_app_app {A : Type u} [PCA A] (u v : Part A) : u ⇓ → v ⇓ → (PCA.X ⬝ u ⬝ v) ⇓

theorem PCA.eq_X {A : Type u} [PCA A] (u v w : Part A) : u ⇓ → v ⇓ → w ⇓ → PCA.X ⬝ u ⬝ v ⬝ w = v ⬝ (u ⬝ u ⬝ v) ⬝ w

def PCA.Z {A : Type u} [PCA A] : Part A

Equations

• PCA.Z = PCA.X ⬝ PCA.X

@[simp]

theorem PCA.df_Z {A : Type u} [PCA A] : PCA.Z ⇓

@[reducible]

def PCA.Z.elm {A : Type u} [PCA A] {Γ : Type u_1} : PCA.Expr Γ A

Equations

• PCA.Z.elm = PCA.Expr.elm (PCA.Z.get ⋯)

@[simp]

theorem PCA.df_Z_app {A : Type u} [PCA A] (u : Part A) : u ⇓ → (PCA.Z ⬝ u) ⇓

theorem PCA.eq_Z {A : Type u} [PCA A] (u v : Part A) : u ⇓ → v ⇓ → PCA.Z ⬝ u ⬝ v = u ⬝ (PCA.Z ⬝ u) ⬝ v

def PCA.W {A : Type u} [PCA A] : Part A

Equations

• PCA.W = PCA.compile (PCA.abstr `x (PCA.abstr `y (PCA.Expr.var `y ⬝ (PCA.Expr.var `x ⬝ PCA.Expr.var `x ⬝ PCA.Expr.var `y))))

@[simp]

def PCA.df_W {A : Type u} [PCA A] : PCA.W ⇓

Equations

• ⋯ = ⋯

@[simp]

def PCA.df_W_app {A : Type u} [PCA A] (u : Part A) : u ⇓ → (PCA.W ⬝ u) ⇓

Equations

• ⋯ = ⋯

def PCA.eq_W {A : Type u} [PCA A] (u v : Part A) : u ⇓ → v ⇓ → PCA.W ⬝ u ⬝ v = v ⬝ (u ⬝ u ⬝ v)

Equations

• ⋯ = ⋯

def PCA.Y {A : Type u} [PCA A] : Part A

Equations

• PCA.Y = PCA.W ⬝ PCA.W

@[simp]

theorem PCA.df_Y {A : Type u} [PCA A] : PCA.Y ⇓

theorem PCA.eq_Y {A : Type u} [PCA A] (u : Part A) : u ⇓ → PCA.Y ⬝ u = u ⬝ (PCA.Y ⬝ u)

Curry numerals

def PCA.numeral {A : Type u} [PCA A] : ℕ → Part A

Curry numeral

Equations

• PCA.numeral 0 = PCA.I
• PCA.numeral n.succ = PCA.pair ⬝ PCA.fal ⬝ PCA.numeral n

@[simp]

theorem PCA.df_numeral {A : Type u} [PCA A] (n : ℕ) : (PCA.numeral n) ⇓

def PCA.succ {A : Type u} [PCA A] : Part A

The successor of a Curry numeral

Equations

• PCA.succ = PCA.pair ⬝ PCA.fal

@[simp]

def PCA.df_succ {A : Type u} [PCA A] : PCA.succ ⇓

Equations

• ⋯ = ⋯

@[simp]

def PCA.df_succ_app {A : Type u} [PCA A] (u : Part A) : u ⇓ → (PCA.succ ⬝ u) ⇓

Equations

• ⋯ = ⋯

def PCA.iszero {A : Type u} [PCA A] : Part A

Is a numeral equal to zero?

Equations

• PCA.iszero = PCA.fst

@[simp]

theorem PCA.eq_iszero_0 {A : Type u} [PCA A] : PCA.iszero ⬝ PCA.numeral 0 = PCA.tru

@[simp]

theorem PCA.eq_iszero_succ {A : Type u} [PCA A] (n : ℕ) : PCA.iszero ⬝ PCA.numeral n.succ = PCA.fal

def PCA.pred {A : Type u} [PCA A] : Part A

Predecessor of a Curry numeral

Equations

• PCA.pred = PCA.compile (PCA.abstr `x (PCA.fst.elm ⬝ PCA.Expr.var `x ⬝ PCA.Expr.I ⬝ (PCA.snd.elm ⬝ PCA.Expr.var `x)))

@[simp]

def PCA.df_pred {A : Type u} [PCA A] : PCA.pred ⇓

Equations

• ⋯ = ⋯

@[reducible]

def PCA.pred.elm {A : Type u} [PCA A] {Γ : Type u_1} : PCA.Expr Γ A

Equations

• PCA.pred.elm = PCA.Expr.elm (PCA.pred.get ⋯)

@[simp]

theorem PCA.eq_pred {A : Type u} [PCA A] (u : Part A) : u ⇓ → PCA.pred ⬝ u = PCA.fst ⬝ u ⬝ PCA.I ⬝ (PCA.snd ⬝ u)

@[simp]

theorem PCA.eq_pred_succ {A : Type u} [PCA A] (u : Part A) : u ⇓ → PCA.pred ⬝ (PCA.succ ⬝ u) = u

def PCA.primrec.R {A : Type u} [PCA A] : Part A

Equations

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

def PCA.primrec.eq_R {A : Type u} [PCA A] (r u f m : Part A) (hr : r ⇓ ) (hu : u ⇓ ) (hf : f ⇓ ) (hm : m ⇓ ) : PCA.primrec.R ⬝ r ⬝ u ⬝ f ⬝ m = PCA.fst ⬝ m ⬝ (PCA.K ⬝ u) ⬝ PCA.compile (PCA.abstr `y (PCA.Expr.elm (f.get hf) ⬝ (PCA.pred.elm ⬝ PCA.Expr.elm (m.get hm)) ⬝ (PCA.Expr.elm (r.get hr) ⬝ PCA.Expr.elm (u.get hu) ⬝ PCA.Expr.elm (f.get hf) ⬝ (PCA.pred.elm ⬝ PCA.Expr.elm (m.get hm)) ⬝ (PCA.Expr.S ⬝ PCA.Expr.K ⬝ PCA.Expr.K))))

Equations

• ⋯ = ⋯

@[simp]

def PCA.primrec.df_R {A : Type u} [PCA A] : PCA.primrec.R ⇓

Equations

• ⋯ = ⋯

def PCA.primrec.R.elm {A : Type u} [PCA A] {Γ : Type u_1} : PCA.Expr Γ A

Equations

• PCA.primrec.R.elm = PCA.Expr.elm (PCA.primrec.R.get ⋯)

def PCA.primrec {A : Type u} [PCA A] : Part A

Primitive recursion

Equations

• PCA.primrec = PCA.compile (PCA.abstr `x (PCA.abstr `f (PCA.abstr `m (PCA.Z.elm ⬝ PCA.primrec.R.elm ⬝ PCA.Expr.var `x ⬝ PCA.Expr.var `f ⬝ PCA.Expr.var `m ⬝ PCA.Expr.I))))

@[simp]

theorem PCA.eq_primrec {A : Type u} [PCA A] (u f m : Part A) : u ⇓ → f ⇓ → m ⇓ → PCA.primrec ⬝ u ⬝ f ⬝ m = PCA.Z ⬝ PCA.primrec.R ⬝ u ⬝ f ⬝ m ⬝ PCA.I

theorem PCA.eq_primrec_zero {A : Type u} [PCA A] (u f : Part A) : u ⇓ → f ⇓ → PCA.primrec ⬝ u ⬝ f ⬝ PCA.numeral 0 = u

theorem PCA.eq_primrec_succ {A : Type u} [PCA A] (u f n : Part A) : u ⇓ → f ⇓ → n ⇓ → PCA.primrec ⬝ u ⬝ f ⬝ (PCA.succ ⬝ n) = f ⬝ n ⬝ (PCA.primrec ⬝ u ⬝ f ⬝ n)