Content deleted Content added
Free magma |
Start working on combinators |
||
Line 3:
==Definition==
A ''partial applicative structure''{{r|van-oosten|p=1}} is simply a set <math>A</math> equipped with a [[partial function|partial]] binary operation <math>A \times A \rightharpoonup A</math>. In the context of realizability, this operation is usually denoted by simple juxtaposition, i.e., <math>(a, b) \mapsto a b</math>. It is usually ''not'' associative; by convention, the notation <math>a b c</math> associates to the left as <math>(a b) c</math>, matching the standard convention in [[
The ''terms''{{r|van-oosten|p=2}} (or ''expressions'') over a partial applicative structure <math>A</math> are defined inductively:
Line 23:
Informally, the combinatory completeness condition requires an analogue of the abstraction operation from lambda calculus to exist inside the pca.
==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 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 = 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>.
==Notes==
| |||