Partial combinatory algebras

A partial combinatory algebra is a set equipped with a partial binary operation, which has the so-called combinators K and S. We formalize it in two stages.

We first define the class PartialApplication which equips a given set A with a partial binary operation. One might expect such an operation to have type A → A → Part A, but this leads to complications because it is not composable. So instead we specify that a partial operation is a map of type Part A → Part A → Part A. In other words, we always work with partial elements, and separately state that they are total as necessary.

(It would be natural to require that the applications be strict, i.e., if the result is defined so are its arguments. An early version did so, but the assumption of strictness was never used.)

We then define the class PCA (partial combinatory algebra) to be an extension of PartialApplication. It prescribed combinators K and S satisfying the usual properties. Following our strategy, K and S are again partial elements on the carrier set, with a separate claim that they are total.

class PCA (A : Type u_1) extends PartialApplication A : Type u_1

The partial combinatory structure on a set A.

• app : Part A → Part A → Part A
• K : Part A
• S : Part A
• df_K₀ : PCA.K ⇓
• df_K₁ : ∀ {u : Part A}, u ⇓ → (PCA.K ⬝ u) ⇓
• df_S₀ : PCA.S ⇓
• df_S₁ : ∀ {u : Part A}, u ⇓ → (PCA.S ⬝ u) ⇓
• df_S₂ : ∀ {u v : Part A}, u ⇓ → v ⇓ → (PCA.S ⬝ u ⬝ v) ⇓
• eq_K : ∀ (u v : Part A), u ⇓ → v ⇓ → PCA.K ⬝ u ⬝ v = u
• eq_S : ∀ (u v w : Part A), u ⇓ → v ⇓ → w ⇓ → PCA.S ⬝ u ⬝ v ⬝ w = u ⬝ w ⬝ (v ⬝ w)

instance PCA.inhabited {A : Type u_1} [PCA A] : Inhabited A

Every PCA is inhabited. We pick K as its default element.

Equations

• PCA.inhabited = { default := PCA.K.get ⋯ }

Expr Γ A is the type of expressions built inductively from constants K and S, variables in Γ (the variable context), the elements of a carrier set A, and formal binary application.

The usual accounts of PCAs typically do not introduce `K` and `S`
as separate constants, because a PCA `A` already contains such combinators.
However, as we defined the combinators to be partial elements, it is more
convenient to have separate primitive constants denoting them.
Also, this way `A` need not be an applicative structure.

inductive PCA.Expr (Γ : Type u_1) (A : Type u_2) : Type (max u_1 u_2)

Expressions with variables from context Γ and elements from A.

• K: {Γ : Type u_1} → {A : Type u_2} → PCA.Expr Γ A

  Formal expression denoting the K combinator

• S: {Γ : Type u_1} → {A : Type u_2} → PCA.Expr Γ A

  Formal expression denoting the S combinator

• elm: {Γ : Type u_1} → {A : Type u_2} → A → PCA.Expr Γ A

  An element as a formal expression

• var: {Γ : Type u_1} → {A : Type u_2} → Γ → PCA.Expr Γ A

  A variable as a formal expression

• app: {Γ : Type u_1} → {A : Type u_2} → PCA.Expr Γ A → PCA.Expr Γ A → PCA.Expr Γ A

  Formal expression application

instance PCA.Expr.hasDot {Γ : Type u_1} {A : Type u_2} : HasDot (PCA.Expr Γ A)

Formal application as a binary operation ·

Equations

• PCA.Expr.hasDot = { dot := PCA.Expr.app }

@[reducible]

def PCA.override {Γ : Type u} [DecidableEq Γ] {A : Type v} (x : Γ) (a : A) (η : Γ → A) (y : Γ) : A

A valuation η : Γ → A assigning elements to variables, with the value of x overridden to be a.

Equations

• PCA.override x a η y = if y = x then a else η y

def PCA.eval {Γ : Type u} {A : Type v} [PCA A] (η : Γ → A) : PCA.Expr Γ A → Part A

Evaluate an expression with respect to a given valuation η.

Equations

• PCA.eval η PCA.Expr.K = PCA.K
• PCA.eval η PCA.Expr.S = PCA.S
• PCA.eval η (PCA.Expr.elm a) = Part.some a
• PCA.eval η (PCA.Expr.var x_1) = Part.some (η x_1)
• PCA.eval η (e₁.app e₂) = PCA.eval η e₁ ⬝ PCA.eval η e₂

def PCA.defined {Γ : Type u} {A : Type v} [PCA A] (e : PCA.Expr Γ A) : Prop

An expression is said to be defined when it is defined at every valuation.

Equations

• PCA.defined e = ∀ (η : Γ → A), (PCA.eval η e) ⇓

def PCA.subst {Γ : Type u} [DecidableEq Γ] {A : Type v} (x : Γ) (a : A) : PCA.Expr Γ A → PCA.Expr Γ A

The substitution of an element for the extra variable.

Equations

• PCA.subst x a PCA.Expr.K = PCA.Expr.K
• PCA.subst x a PCA.Expr.S = PCA.Expr.S
• PCA.subst x a (PCA.Expr.elm a_1) = PCA.Expr.elm a_1
• PCA.subst x a (PCA.Expr.var x_2) = if x_2 = x then PCA.Expr.elm a else PCA.Expr.var x_2
• PCA.subst x a (e₁.app e₂) = PCA.subst x a e₁ ⬝ PCA.subst x a e₂

def PCA.abstr {Γ : Type u} [DecidableEq Γ] {A : Type v} (x : Γ) : PCA.Expr Γ A → PCA.Expr Γ A

abstr e is an expression with one fewer variables than the expression e, which works similarly to function abastraction in the λ-calculus. It is at the heart of combinatory completeness.

Equations

• PCA.abstr x PCA.Expr.K = PCA.Expr.K ⬝ PCA.Expr.K
• PCA.abstr x PCA.Expr.S = PCA.Expr.K ⬝ PCA.Expr.S
• PCA.abstr x (PCA.Expr.elm a) = PCA.Expr.K ⬝ PCA.Expr.elm a
• PCA.abstr x (PCA.Expr.var x_2) = if x_2 = x then PCA.Expr.S ⬝ PCA.Expr.K ⬝ PCA.Expr.K else PCA.Expr.K ⬝ PCA.Expr.var x_2
• PCA.abstr x (e₁.app e₂) = PCA.Expr.S ⬝ PCA.abstr x e₁ ⬝ PCA.abstr x e₂

@[simp]

theorem PCA.df_abstr {Γ : Type u} [DecidableEq Γ] {A : Type v} [PCA A] (x : Γ) (e : PCA.Expr Γ A) : PCA.defined (PCA.abstr x e)

An abstraction is defined.

theorem PCA.eval_abstr {Γ : Type u} [DecidableEq Γ] {A : Type v} [PCA A] (x : Γ) (e : PCA.Expr Γ A) (a : A) (η : Γ → A) : PCA.eval η (PCA.abstr x e ⬝ PCA.Expr.elm a) = PCA.eval (PCA.override x a η) e

eval_abstr e behaves like abstraction in the extra variable. This is known as combinatory completeness.

theorem PCA.eval_abstr_app {Γ : Type u} [DecidableEq Γ] {A : Type v} [PCA A] (η : Γ → A) (x : Γ) (e : PCA.Expr Γ A) (u : Part A) (hu : u ⇓ ) : PCA.eval η (PCA.abstr x e) ⬝ u = PCA.eval (PCA.override x (u.get hu) η) e

Like eval_abstr but with the application on the outside of eval.

@[simp]

theorem PCA.eval_override {Γ : Type u} [DecidableEq Γ] {A : Type v} [PCA A] (η : Γ → A) (x : Γ) (a : A) (e : PCA.Expr Γ A) : PCA.eval (PCA.override x a η) e = PCA.eval η (PCA.subst x a e)

def PCA.compile {Γ : Type u} {A : Type v} [PCA A] (e : PCA.Expr Γ A) : Part A

Compile an expression to a partial element, substituting the default value for any variables occurring in e.

Equations

• PCA.compile e = PCA.eval (fun (x : Γ) => default) e

def PCA.eval_closed {Γ : Type u} {A : Type v} [PCA A] : PCA.Expr Γ A → Γ ⊕ Part A

Evaluate an expression under the assumption that it is closed. Return inl x if variable x is encountered, otherwise inr u where u is the partial element so obtained.

Equations

• PCA.eval_closed PCA.Expr.K = pure PCA.K
• PCA.eval_closed PCA.Expr.S = pure PCA.S
• PCA.eval_closed (PCA.Expr.elm a) = pure ↑(some a)
• PCA.eval_closed (PCA.Expr.var x_1) = Sum.inl x_1
• PCA.eval_closed (e₁.app e₂) = do let a₁ ← PCA.eval_closed e₁ let a₂ ← PCA.eval_closed e₂ pure (a₁ ⬝ a₂)

def PCA.«term≪_≫_» : Lean.ParserDescr

Equations

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

def PCA.«term[pca:_]» : Lean.ParserDescr

Equations

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