Page 66 - Textos de Matemática Vol. 40

54 Chapter 1. Applicative theories Proof. By the previous Lemma l g ⊑T g (l g) holds. In order to show the other
direction let x ∈ Ai. By the last Claim of the previous Lemma we obtain ∃n.g (l g) x ⊑ g (h g n) x.
By the definition of h we get ∃n.g(lg)x⊑hg(n+1)x. Using Claim 4 of the previous Lemma we find ∀n.h g (n + 1) x ⊑ l g x. Hence, by Lemma 1.8.7 we have g(lg)x⊑lgx. Finally,weconcludeg(lg)⊑T lg. ⊣
The next Theorem states that l g is the least fixed point of g.
Theorem 1.8.12. We can prove in LFP that if g ∈ (T → T ) is T monotonic for
T given as in Definition 1.8.6, then
f ∈ T ∧ g f ∼= T f → l g ⊑ T f .
Proof. Let f be such that gf ∼=T f. First, we show by induction on N that
∀n.hgn⊑T f. (17)
We obviously have hg0⊑T f. Suppose hgn⊑T f for a natural number n. By the T monotonicity of g we get hg(n+1) = g(hgn)⊑T gf ∼=T f. Therefore, by Lemma 1.8.7 we obtain hg(n+1)⊑T f and (17) is shown. By g(hgn) = h g (n + 1) this implies
∀n.g(hgn)⊑T f. (18)
Itremainstoshow∀x∈Ai.lgx⊑fxforeachi. Soletx∈Ai. ByClaim 5 of Lemma 1.8.10 we get lgx⊑g(lg)x. By Claim 7 of the same Lemma we obtain ∃n.g (l g) x⊑g (h g n) x. Therefore with (18) and Lemma 1.8.7 we conclude l g x ⊑ f x. ⊣
1.8.3 Discussion
Let us look at the following recursively defined method written in a java like language.
A m (B x) {
return m(x);
}
Of course, any program calling m with some argument s is non-terminating. The semantics of the method m is usually given as the least fixed point of the functional λf, x.f x. If we model this fixed point by rec (λf, x.f x), then we cannot prove in BON that ¬ rec (λf, x.f x) s ↓ for any argument s. This is simply because of the consistency of BON + (Tot).
On the other hand, defining the semantics of the method m using our least fixed point operator l enables us to prove non-termination in LFP. Let V be