Page 24 - Textos de Matemática Vol. 40

12
Chapter 1. Applicative theories
I. Partial combinatory algebra. (1) kxy=x,
(2) sxy↓∧sxyz≃xz(yz).
To exclude trivial models one could add the axiom k ̸= s. However, as soon as there are at least two provable different terms in an applicative theory, it is derivable. Since the axiomatization of the natural numbers (or of any other datatype) should contain at least one inequality axiom, we do not need to include this axiom.
The axiom for the s combinators differs obviously from the standard one in the total case: s x y z = x z (y z). The first conjunct of I.(2) serves to guarantee that terms representing functions are always defined (in the sense of ↓): s x y may be considered as a function term “waiting” for its third argument, before it can be evaluated. Note, that s x ↓ follows from it by the strictness axiom (S2). The partial equality s x y z ≃ x z (y z) may be interpreted, for instance, that the evaluation of the function application s x y z might not terminate.
In the axiom I.(1) of the k combinator we can use the total equality since the right hand side of the equation is always defined by the strictness axiom (S4). As a consequence, k can only be used to define constant functions which return a defined value. For the constantly undefined function we will need a more complex term. This becomes visible in the following definition of λ terms which differs in the partial context from the total one.
1.2.1 First results.
λ abstraction. It is known that the axioms for k and s are sufficient to introduce λ abstraction. Thus, we define the λ notation as abbreviation in applicative theories:
Proposition 1.2.1. For every variable x and every term t of an applicative lan- guage L there exists a term λx.t of L whose free variables are those of t, exclud- ing x, such that we can prove from I.(1) and I.(2):
λx.t ↓ ∧(λx.t) x ≃ t.
Proof. (λx.t) is inductively defined as follows, cf. [Bee85, p. 101]:
1. λx.x:=skk,
2. λx.y:=ky,ifx̸≡y,
3. λx.c:=kc, if c is a constant, and 4. λx.rs:=s(λx.r)(λx.s).
The verification of the properties is straightforward. ⊣