Page 27 - Textos de Matemática Vol. 40

1.3. The theory BON 15
the functional programming language scheme and applicative theories, [St¨a95] (for a sketchy description cf. [St¨a97, Section 4.6]). A comprehensive list of references which use applicative theories or related systems in relation with functional programming was already given in the Introduction.
For the practical use, first of all it is the definedness predicate which is convenient, since it allows to speak about termination within the language. However, it is also interesting to see how the special treatment which is needed to overcome strictness problems in the case of case-distinctions and streams in functional programming languages finds its counterpart in applicative theories: non-strict definition by cases is introduced in Subsection 1.3.4; streams are dis- cussed in Section 3.3 in relation to a concept of pointers which we will introduce for truth theories.
Primitive-recursive application. Schlu¨ter in [Sch95] introduced an al- ternative applicative theory in which the application t · s may be interpreted as [tN](sN) in terms of indices for primitive-recursive functions. Due to the Recursion Theorem, it is obvious that, in the presence of k and s, such an inter- pretation is not possible. Therefore, Schlu¨ter’s theory is based on another set of combinators. Since the usual method of “Currying” fails in this context, a proper binary pairing operation is needed to represent functions of higher arity. The underlying applicative structure is based on combinators k, i, a, b, p0, and p1 and an additional binary operation expressed by ⟨·, ·⟩. The axioms are:
1. kxy=x,
2. ix=x,
3. a⟨x,y⟩ ↓∧a⟨x,y⟩z ≃ ⟨xz,yz⟩, 4. b⟨x,y⟩ ↓∧b⟨x,y⟩z = x(yz), 5. p0⟨x,y⟩=x,
6. p1⟨x,y⟩=y.
These are the axioms of the theory PEA of Schlu¨ter [Sch95, Def. 4.1], however, the notation is slightly adapted here, following Steiner and Strahm, [Ste01, SS06].
With these axioms it is possible to prove a (restricted) form of λ abstraction as well as of recursion.
1.3 The theory BON 1.3.1 The axioms
The basic theory BON (Basic theory of operations and numbers) was introduced by Feferman and Ja¨ger in [FJ93]. It extends the combinatory algebra by pairing and axiomatically introduced natural numbers.