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 combinator I
• ordered pairs pair with projections fst and snd
• booleans tru, fal and the conditional statement ite
• fixed-point combinators Z and Y
• Curry numerals numeral n with successor succ, predecessor pred and primitive recursion primrec

For each combinator C we prove a definedness lemma df_C characterizing totality of expressions involving C. Characteristic equations for the simpler combinators (I, K', pair, fst, snd, the booleans, X, W, and the fixed-point combinators) are also proved here; equations for the more complex Curry-numeral predecessor and primitive-recursion combinators are omitted in this v4.30 port — they remain expressible in terms of the combinators themselves.

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

The identity combinator

Equations

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

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

The expression denoting the identity combinator

Equations

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

@[simp]

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

@[simp]

theorem LeanPool.PartialCombinatoryAlgebras.PCA.eq_I {A : Type u} [PCA A] {u : Part A} (hu : u ⇓) : I ⬝ u = u

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

The K I combinator: K' u v = v.

Equations

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

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

Formal expression denoting K'.

Equations

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

@[simp]

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

@[simp]

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

Pairing

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

The pairing combinator.

Equations

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

@[simp]

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

@[simp]

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

@[simp]

theorem LeanPool.PartialCombinatoryAlgebras.PCA.df_pair_app_app {A : Type u} [PCA A] (u v : Part A) (hu : u ⇓) (hv : v ⇓) : (pair ⬝ u ⬝ v) ⇓

@[simp]

theorem LeanPool.PartialCombinatoryAlgebras.PCA.eq_pair {A : Type u} [PCA A] (u v w : Part A) (hu : u ⇓) (hv : v ⇓) (hw : w ⇓) : pair ⬝ u ⬝ v ⬝ w = w ⬝ u ⬝ v

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

The first projection.

Equations

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

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

The first projection as a formal expression.

Equations

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

@[simp]

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

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

The second projection.

Equations

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

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

The second projection as a formal expression.

Equations

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

@[simp]

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

theorem LeanPool.PartialCombinatoryAlgebras.PCA.eq_fst_pair {A : Type u} [PCA A] (u v : Part A) (hu : u ⇓) (hv : v ⇓) : fst ⬝ (pair ⬝ u ⬝ v) = u

theorem LeanPool.PartialCombinatoryAlgebras.PCA.eq_snd_pair {A : Type u} [PCA A] (u v : Part A) (hu : u ⇓) (hv : v ⇓) : snd ⬝ (pair ⬝ u ⬝ v) = v

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

Conditional statements

Equations

• LeanPool.PartialCombinatoryAlgebras.PCA.ite = LeanPool.PartialCombinatoryAlgebras.PCA.I

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

The boolean false

Equations

• LeanPool.PartialCombinatoryAlgebras.PCA.fal = LeanPool.PartialCombinatoryAlgebras.PCA.K'

@[simp]

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

@[simp]

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

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

The boolean true

Equations

• LeanPool.PartialCombinatoryAlgebras.PCA.tru = LeanPool.PartialCombinatoryAlgebras.PCA.K

@[simp]

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

@[simp]

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

@[simp]

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

The fixed point combinator

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

Auxiliary combinator used to define the fixed point combinator Z.

Equations

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

@[simp]

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

@[simp]

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

@[simp]

theorem LeanPool.PartialCombinatoryAlgebras.PCA.df_X_app_app {A : Type u} [PCA A] (u v : Part A) (hu : u ⇓) (hv : v ⇓) : (X ⬝ u ⬝ v) ⇓

theorem LeanPool.PartialCombinatoryAlgebras.PCA.eq_X {A : Type u} [PCA A] (u v w : Part A) (hu : u ⇓) (hv : v ⇓) (hw : w ⇓) : X ⬝ u ⬝ v ⬝ w = v ⬝ (u ⬝ u ⬝ v) ⬝ w

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

The call-by-name fixed-point combinator.

Equations

• LeanPool.PartialCombinatoryAlgebras.PCA.Z = LeanPool.PartialCombinatoryAlgebras.PCA.X ⬝ LeanPool.PartialCombinatoryAlgebras.PCA.X

@[simp]

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

@[reducible]

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

The fixed-point combinator Z as a formal expression.

Equations

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

@[simp]

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

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

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

Auxiliary combinator used to define the call-by-value fixed point combinator Y.

Equations

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

@[simp]

theorem LeanPool.PartialCombinatoryAlgebras.PCA.df_W {A : Type u} [PCA A] : W ⇓

@[simp]

theorem LeanPool.PartialCombinatoryAlgebras.PCA.df_W_app {A : Type u} [PCA A] (u : Part A) (hu : u ⇓) : (W ⬝ u) ⇓

theorem LeanPool.PartialCombinatoryAlgebras.PCA.eq_W {A : Type u} [PCA A] (u v : Part A) (hu : u ⇓) (hv : v ⇓) : W ⬝ u ⬝ v = v ⬝ (u ⬝ u ⬝ v)

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

The call-by-value fixed-point combinator.

Equations

• LeanPool.PartialCombinatoryAlgebras.PCA.Y = LeanPool.PartialCombinatoryAlgebras.PCA.W ⬝ LeanPool.PartialCombinatoryAlgebras.PCA.W

@[simp]

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

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

Curry numerals

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

Curry numeral

Equations

• One or more equations did not get rendered due to their size.
• LeanPool.PartialCombinatoryAlgebras.PCA.numeral 0 = LeanPool.PartialCombinatoryAlgebras.PCA.I

@[simp]

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

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

The successor of a Curry numeral

Equations

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

@[simp]

theorem LeanPool.PartialCombinatoryAlgebras.PCA.df_succ {A : Type u} [PCA A] : succ ⇓

@[simp]

theorem LeanPool.PartialCombinatoryAlgebras.PCA.df_succ_app {A : Type u} [PCA A] (u : Part A) (hu : u ⇓) : (succ ⬝ u) ⇓

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

Is a numeral equal to zero?

Equations

• LeanPool.PartialCombinatoryAlgebras.PCA.iszero = LeanPool.PartialCombinatoryAlgebras.PCA.fst

@[simp]

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

@[simp]

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

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

Predecessor of a Curry numeral

Equations

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

@[simp]

theorem LeanPool.PartialCombinatoryAlgebras.PCA.df_pred {A : Type u} [PCA A] : pred ⇓

@[reducible]

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

The predecessor combinator as a formal expression.

Equations

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

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

Auxiliary combinator used in the definition of primitive recursion.

Equations

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

@[simp]

theorem LeanPool.PartialCombinatoryAlgebras.PCA.primrec.df_R {A : Type u} [PCA A] : R ⇓

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

The auxiliary combinator primrec.R as a formal expression.

Equations

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

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

Primitive recursion

Equations

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