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.
The partial combinatory structure on a set A
.
Instances
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.
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
Instances For
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
Instances For
Evaluate an expression with respect to a given valuation η
.
Equations
Instances For
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₂
Instances For
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₂
Instances For
An abstraction is defined.
eval_abstr e
behaves like abstraction in the extra variable.
This is known as combinatory completeness.
Like eval_abstr
but with the application on the outside of eval
.
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
Instances For
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₂)
Instances For
Equations
- One or more equations did not get rendered due to their size.
Instances For
Equations
- One or more equations did not get rendered due to their size.