Content deleted Content added
Start working on combinators |
Proof of combinators criterion |
||
Line 26:
==Characterization by combinators==
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 combinatorially 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>,
* <math>S x y \downarrow</math> for all <math>x, y \in A</math>,
* <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 combinatorially 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:
* <math>\langle x \rangle a = K a</math> for a constant <math>a \in A</math>,
* <math>\langle x \rangle x = I</math> where <math>I := S K K</math>,
* <math>\langle x \rangle y = K y</math> if <math>y</math> is a variable different from <math>x</math>,
* <math>\langle x \rangle (u v) = S (\langle x \rangle u) (\langle x \rangle v)</math>.
Beware that the analogy between <math>\langle x \rangle t</math> and <math>\lambda x \cdot t</math> is not perfect. For example, the terms <math>(\langle x \rangle t) t'</math> and <math>t[t'/x]</math> are not generally equivalent in a reasonable sense, e.g., taking a variable <math>y</math> different from <math>x</math> and <math>a, b \in A</math> constants, we have <math>(\langle x \rangle y)(a b) = K y (a b)</math>, which cannot be considered equivalent to <math>y</math> because the latter always evaluates to <math>c</math> if <math>y</math> is replaced by a constant <math>c \in A</math>, while the former may not as <math>a b</math> may be undefined.
However, if <math>t'</math> is a constant <math>a</math>, then <math>(\langle x \rangle t) a</math> is indeed equivalent to <math>t[a/x]</math> in the sense that substituting all variables for some constants in these two terms gives the same result (per <math>\simeq</math>).
Moreover, substituting variables by constants in <math>\langle x \rangle t</math> ''always'' evaluates to a defined result, even if this would not be the case by substituting variables in <math>t</math>. For example, if <math>a, b \in A</math> are two constants, the term <math>\langle x \rangle (a b)</math> (abstracting a variable which does not appear) is equal to <math>S (K a) (K b)</math>. By the assumptions on <math>K</math> and <math>S</math>, this is well-defined, even though <math>a b</math> may not be well-defined.
These remarks imply that for all term <math>t(x_0, \dots, x_n)</math>, the value <math>a := \langle x_0 \rangle \dots \langle x_n \rangle t \downarrow</math> is well-defined and satisfies the two requirements of combinatory completeness.
==Notes==
| |||