Partial combinatory algebra: Difference between revisions

Revision as of 17:11, 21 February 2025

Revision as of 17:12, 21 February 2025

Line 28:

In the same way as there is a translation from [[λ-term]]s to terms of the [[SKI combinator calculus]] by eliminating [[λ-abstraction]]s using combinators, pcas can be characterized by the existence of elements which satisfy equations analogous to the S and K combinators. Note, however, that some care must be taken in the statement and proof since application is not always defined in a pca.

'''Theorem:'''{{r|van-oosten|p=3}} A partial applicative structure <math>A</math> is combinatoriallycombinatory complete if and only if there exist two elements <math>k, s \in A</math> such that:

* <math>K x y \downarrow = x</math> for all <math>x, y \in A</math>,

Line 34:

* <math>S x y z \simeq (x z) (y z)</math> for all <math>x, y, z \in A</math>.

For the proof, in the forward direction, if <math>A</math> is combinatoriallycombinatory complete, it suffices to apply the definition of combinatorial completeness to the terms <math>t_K(x, y) := x</math> and <math>t_S(x, y, z) := (x z)(y z)</math> to obtain <math>K</math> and <math>S</math> with the required properties.

It is the converse that involves abstraction elimination. Assume we have <math>K</math> and <math>S</math> as stated. Given a variable <math>x</math> and a term <math>t</math>, we define a term <math>\langle x \rangle t</math> whose variables are those of <math>t</math> minus <math>x</math>, which plays a role similar to <math>\lambda x \cdot t</math> in λ-calculus. The definition is by induction on <math>t</math> as follows: