Page 25 - Textos de Matemática Vol. 40

1.2. Combinatory algebra 13
This definition ensures that λx.t is always defined. However, in contrast to the usual definition of λ abstraction in the total setting, it is not compatible with substitution: For x ̸≡ y the equality (λx.t)[s/y] = λx.t[s/y] does not hold in general. This problem, noted in [Kah92], is extensively discussed by Strahm in [Str96b], cf. also Feferman [Fef95].
Let us note that we get back the substitution property when the λ expres- sion is applied to a term, i.e., we have
((λx.t)[s/y])r ≃ t[s/y][r/x].
Note that the formation of the λ terms is generic in the sense that the Theorem holds for arbitrary applicative languages L, i.e., for languages with an arbitrary set of individual constants, containing at least k and s.
Recursion Theorem. Furthermore, we can define a recursion operator which may be used to solve recursive equations. However, to ensure the de- finedness of functions introduced by this operator, we get—in some sense—only pointwise solutions of the recursive equations (in contrast to the total case).
Proposition 1.2.2. There exists a term rec based on k and s so that we can prove with I.(1) and I.(2):
recf ↓∧∀x.recf x ≃ f (recf)x.
Proof. To get the existence property rec f ↓, the definition of rec is slightly more
complicated than in the total setting, cf. [Bee85, p. 103]:
rec := λf.(λy, x.f (y y) x) (λy, x.f (y y) x). ⊣
To solve a recursive equation we can use the term rec in the following way. In general a recursive definition is given by
f x := t[f, x].
¿From such an equation we get a solution f for f by defining:
f := rec λg, x.t[g, x].
Here, λg, x.t[g, x] plays the role of f in the Proposition above. Using this Propo- sition, it follows immediately f ↓ and it is easy to verify that f fulfills (pointwise) the recursion equation of f.
Diagonalization over negation. Whenever there is a negation for a certain domain available, the Recursion Theorem may be used to diagonalize over this negation and thus showing that there exists a term outside of the considered domain. In the partial setting we can prove such a Diagonalization Theorem for arbitrary properties φ(x), provided that they are “strict”, i.e., that φ(t) → t ↓ holds for all terms t.