Page 23 - Textos de Matemática Vol. 40

1.2. Combinatory algebra 11
Therefore, one may ask what to do to model other evaluation strategies, first of all, call-by-name. This question was studied by Sta¨rk in [St¨a98] and [St¨a05] where the author introduced a Basic Logic of Partial Terms, BPT, which allows to handle both, call-by-name as well as call-by-value. However, this approach is carried out in a typed context.
Self-application. As already mentioned, applicative theories allow self- application, i.e., it is allowed to apply a term t to itself: t t. With regard to the understanding of a term as function constant this designation is justified. But, one should notice that formally the self-application is “just” a diagonalization over the function symbol · for the application: t t is only a short hand notation of ·(t,t). The recursion theoretic interpretation (cf. Section 1.4.1) provides a rather natural understanding of self-application. A note on the history of self- application is given in the appendix.
Totality. One can consider total versions of applicative theories, where the existence predicate is trivialized. In general, it is convenient to assume that the total versions are formulated in a language where the existence predicate is dropped, and, in contrast of the logic of partial terms, usual predicate logic with equality is assumed. However, it is also possible to show that these total variants are equivalent to the partial versions extended by the axiom of totality:
(Tot) ∀x,y.xy ↓.
1.2 Combinatory algebra
The combinatory logic goes back to Scho¨nfinkel [Sch24, Sch67]. It allows to get a very high, in some sense complete expressive power with a very restricted term language. In fact, the two constants k and s, together with their axioms, are sufficient to get combinatorial completeness.
Combinatory logic was elaborated first of all by Curry, [Cur30, CF58, CHS72]. Together with its twin theory, the λ calculus, it is nowadays an in- dependent research branch in mathematical logic. While the total version of combinatory logic is well-studied and its results are to a large extend folklore, the situation for the partial case is different. In fact, partiality results in some subtile technical differences which make it necessary to check carefully how re- sults from the total setting can be carried over. The most significant example is the λ abstraction, cf. Definition 1.2.1 below. Here, the inductive definition of the λ terms has to be modified to guarantee definedness, a property desirable for function terms. But this results in a loss of substitution properties. In the axiomatization the partiality is expressed in the axioms for the s combinator.
Formally, a language L for an applicative theory should contain at least the constants k and s. As non-logical axioms we have for these constants: