Page 31 - Textos de Matemática Vol. 40

1.3. The theory BON 19 each of them it is easy to define such a term. However, it is not obvious that
there exists uniformly one single term for all models.
Corollary 1.3.2. There is a term notN of Lp such that BON ⊢ ¬N(notN).
Proof. Use Proposition 1.2.3 with φ(x) := N(x), ψ(x) := x = 0, and negψ := λy.dN 10y0. As notN we get rec(λf,x.(λy.dN 10y0)(f x))0 which is equal with rec(λf,x.dN 10(f x)0)0. ⊣
Note that we do not have notN ↓ in general. With respect to the recursion- theoretic models (cf. below), it is impossible to demand this property for notN, since ↓ and N coincide in the recursion-theoretic models.
Non-strict definition by cases. The case distinction given by dN is strict in the sense that dN rsuv ↓ implies r ↓ and s ↓. However, we often want to define a function by cases so that it is defined if one case holds, even if the value that would have been computed in the other case is undefined. We can do so, by defining ds r s u v as dN (λz.r) (λz.s) u v 0 where the variable z does not occur in the terms r and s. Note that due to the use of λz.r and λz.s in the definition the short-hand notation ds r s u v is not compatible with substitutions in r and s. Sometimes we will write non-strict definition by cases by use of the following notation:
r ifu=v, s otherwise.
This notation matches with the usual intuition only, if we assume N(u) and N(v). However, we will use it in a context where all N(t) holds for all terms of the language.
Note that evaluation of ds r s u v corresponds to the special evaluation strat- egy which is used also in strict functional programming languages for if-then- else constructs.
Types as predicates. Starting from the implicit typing of the colloquial mathematical language typed theories are used successfully in computer science. The idea is that terms come with a given type, and every syntactically correct formed term has automatically a specific type. In fact, there are several variants or liberalization possible of this concept, involving polymorphism (a term may belong to several different types) or the distinction of Church vs. Curry-style typing (in the latter one, variables do not carry types). Sometimes, the correct typing of the term cannot be read off from it construction, but have to be proven by use of an extra typing calculus (or type checker). However, the typing results always in a restriction of the expressiveness. For instance, the self-application t t is, in general, not typeable.2 In an untyped framework, like the one chosen
2There are some special cases which are typeable in polymorphic frameworks, but they do not cover all cases.
ds rsuv ≃