Page 50 - Textos de Matemática Vol. 40

38 Chapter 1. Applicative theories If g f has these properties, it follows immediately from the axioms of μ that
μ (λx.g f x) has the required properties for E0 f .
1. If f is total, then a straightforward calculation proves, that g f is total.
If gf is total, then gf 2 = μ(λy.hf y) belongs to N. So hf is total, and we get hf 2 = μf belongs to N, what yields the totality of f.
2. Suppose f is total (and therefore g f is total).
(a) Ifgf0=0,thenf(μf)=0,sof hasazero.
Iff hasazero,sof(μf)=0andfurthergf0=0andgf1=1. Since h f 0 = 1 and h f 1 = 0, μ (λy.h f y) ̸= 0, so g f x ̸= 0, if x > 1. Thus 0 is the only zero of gf.
(b) Ifgf0̸=0,thenf(μf)̸=0,sof hasnozero.
Iff hasnozero,sof(μf)̸=0. Thusgf0̸=0andgf1=0. ⊣
Note that there is a much simpler definition of E0μ in the presence of (N-Str): Define E0μ as λf.dN (f (μ f), 0, μ f, μ f) or λf.ifN (μ f) (f (μ f)).
To define μ from E0 we need formulae induction as well as N-strictness. (F-IN) is needed to find a zero by use of μrec, because E0 does not give any bound, if a zero exists. (N-Str) will save the totality test.
Proposition 1.7.19. There exists a term μE0 of LE0 such that
1. BON(E0)+(N-Str)+(F-IN)⊢(f :N→N)↔N(μE0 f),
2. BON(E0)+(N-Str)+(F-IN)⊢(f :N→N)∧(∃x∈N.fx=0)→
f(μE0 f)=0.
Proof. We define
μE0 := λf.ifN (E0 f)(dN (λx.μrec f)(λx.0)(E0 f)00).
1. ←: N(μE0 f) implies N(E0 f) by definition of ifN, and we get (f : N → N).
1. →and2.: Assume(f:N→N). SowehaveN(E0f)andμE0f= dN (λx.μrec f)(λx.0)(E0 f)00. By case distinction on E0 f ̸= 0 or E0 f = 0 we get in the former case μE0 f = 0, so N(μE0 f). In the latter one we have μE0 f = μrec f, and know that f has a zero. So μrec f will return it. ⊣
To define E0 by E#0 we have to find a way to test totality of a function also if it has a zero. An idea would be to test λx.sN (f x) instead of f. But to conclude the totality of f from that of λx.sN (f x) we need N-strictness. Moreover, it is needed to combine this test with the test for a zero.
Proposition 1.7.20. There exists a term E0E#0 of LE#0 such that