Bill Halchin writes:
I understand (to some degree) full combinatory algebra, but I don't understand the motivation behind the definition of a partial combinatory algebra. E.g. why do we have Sxy converges/is defined? Or Kxy ~ x?
The somewhat mysterious definition of (partial or full) combinatory algebras is really motivated by the fact that it is equivalent to a "combinatory completeness" property, which is a bit less mysterious but more cumbersome to state. Informally, combinatory completeness says that all functions definable in the language of A are themselves representable by elements of A. More precisely: A is a PCA iff for every formal expression e (built up from variables x,y_1,...,y_n and constants from A via juxtaposition), there is a formal expression called (\lambda x.e), whose variables are just y_1,...,y_n, such that (\lambda x.e)[b_1/y_1,...,b_n/y_n] is defined for all b_1,...,b_n \in A, (\lambda x.e) a [b_1/y_1,...,b_n/y_n] ~ e[a/x,b_1/y_1,...,b_n/y_n] (This is easiest to understand in the case n=0.) A similar statement holds for full combinatory algebras where everything is always defined. The term (\lambda x.e) can be constructed via the Curry translation from lambda calculus to combinatory logic. The condition "Sxy is defined" is needed for this to work. Also, I should say the whole theory of realizability models goes through much more smoothly with this condition, otherwise one has to keep making tiresome exemptions for the case of the object 0. I imagine the condition becomes strictly necessary at some point, e.g. in the proof that PER is an internal category. As for Kxy ~ x, that's the same as saying Kxy=x, because all elements x of A are of course defined. Cheers, John