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 LeanPool.PartialCombinatoryAlgebras.PCA (A : Type u_1) extends LeanPool.PartialCombinatoryAlgebras.PartialApplication A : Type u_1

The partial combinatory structure on a set A.

• app : Part A → Part A → Part A
• K : Part A

  The K combinator as a partial element.

• S : Part A

  The S combinator as a partial element.

• df_K₀ : K ⇓

  The K combinator is total.

• df_K₁ {u : Part A} : u ⇓ → (K ⬝ u) ⇓

  Applying K to a total argument is total.

• df_S₀ : S ⇓

  The S combinator is total.

• df_S₁ {u : Part A} : u ⇓ → (S ⬝ u) ⇓

  Applying S to one total argument is total.

• df_S₂ {u v : Part A} : u ⇓ → v ⇓ → (S ⬝ u ⬝ v) ⇓

  Applying S to two total arguments is total.

• eq_K (u v : Part A) : u ⇓ → v ⇓ → K ⬝ u ⬝ v = u

  The defining equation of K.

• eq_S (u v w : Part A) : u ⇓ → v ⇓ → w ⇓ → S ⬝ u ⬝ v ⬝ w = u ⬝ w ⬝ (v ⬝ w)

  The defining equation of S.

@[implicit_reducible]

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

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

Equations

• LeanPool.PartialCombinatoryAlgebras.PCA.inhabited = { default := LeanPool.PartialCombinatoryAlgebras.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 LeanPool.PartialCombinatoryAlgebras.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} : Expr Γ A

  Formal expression denoting the K combinator

• S {Γ : Type u_1} {A : Type u_2} : Expr Γ A

  Formal expression denoting the S combinator

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

  An element as a formal expression

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

  A variable as a formal expression

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

  Formal expression application

@[implicit_reducible]

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

Formal application as a binary operation ·

Equations

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

@[reducible]

def LeanPool.PartialCombinatoryAlgebras.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

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

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

Evaluate an expression with respect to a given valuation η.

Equations

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

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

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

Equations

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

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

The substitution of an element for the extra variable.

Equations

• One or more equations did not get rendered due to their size.
• LeanPool.PartialCombinatoryAlgebras.PCA.subst x a LeanPool.PartialCombinatoryAlgebras.PCA.Expr.K = LeanPool.PartialCombinatoryAlgebras.PCA.Expr.K
• LeanPool.PartialCombinatoryAlgebras.PCA.subst x a LeanPool.PartialCombinatoryAlgebras.PCA.Expr.S = LeanPool.PartialCombinatoryAlgebras.PCA.Expr.S
• LeanPool.PartialCombinatoryAlgebras.PCA.subst x a (LeanPool.PartialCombinatoryAlgebras.PCA.Expr.elm a_1) = LeanPool.PartialCombinatoryAlgebras.PCA.Expr.elm a_1
• LeanPool.PartialCombinatoryAlgebras.PCA.subst x a (e₁.app e₂) = LeanPool.PartialCombinatoryAlgebras.PCA.subst x a e₁ ⬝ LeanPool.PartialCombinatoryAlgebras.PCA.subst x a e₂

def LeanPool.PartialCombinatoryAlgebras.PCA.abstr {Γ : Type u} [DecidableEq Γ] {A : Type v} (x : Γ) : Expr Γ A → 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

• One or more equations did not get rendered due to their size.
• LeanPool.PartialCombinatoryAlgebras.PCA.abstr x LeanPool.PartialCombinatoryAlgebras.PCA.Expr.K = LeanPool.PartialCombinatoryAlgebras.PCA.Expr.K ⬝ LeanPool.PartialCombinatoryAlgebras.PCA.Expr.K
• LeanPool.PartialCombinatoryAlgebras.PCA.abstr x LeanPool.PartialCombinatoryAlgebras.PCA.Expr.S = LeanPool.PartialCombinatoryAlgebras.PCA.Expr.K ⬝ LeanPool.PartialCombinatoryAlgebras.PCA.Expr.S

@[simp]

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

An abstraction is defined.

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

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

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

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

@[simp]

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

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

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

Equations

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

def LeanPool.PartialCombinatoryAlgebras.PCA.evalClosed {Γ : Type u} {A : Type v} [PCA A] : 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

• One or more equations did not get rendered due to their size.
• LeanPool.PartialCombinatoryAlgebras.PCA.evalClosed LeanPool.PartialCombinatoryAlgebras.PCA.Expr.K = Sum.inr LeanPool.PartialCombinatoryAlgebras.PCA.K
• LeanPool.PartialCombinatoryAlgebras.PCA.evalClosed LeanPool.PartialCombinatoryAlgebras.PCA.Expr.S = Sum.inr LeanPool.PartialCombinatoryAlgebras.PCA.S
• LeanPool.PartialCombinatoryAlgebras.PCA.evalClosed (LeanPool.PartialCombinatoryAlgebras.PCA.Expr.elm a) = Sum.inr (Part.some a)
• LeanPool.PartialCombinatoryAlgebras.PCA.evalClosed (LeanPool.PartialCombinatoryAlgebras.PCA.Expr.var x_1) = Sum.inl x_1

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

Notation for combinatory abstraction in an expression.

Equations

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

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

Notation for compiling a closed PCA expression to a partial element.

Equations

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