68
F. Frohn
With Thm. 10, we can accelerate T ev-dec to
x
1
x
2
=
n−n
2
2 +x2·n+x1
x2−n
∧ x 1 > 0 ∧
n−1−(n−1)
2
2
+ x 2 · (n − 1) + x 1 > 0
as we have
(x 1 ≥ x 1 + x 2 ) ≡ (0 ≥ x 2 ) =⇒ (0 ≥ x 2 − 1) ≡ (x 1 + x 2 ≥ x 1 + x 2 + x 2 − 1).
Turning Thm. 10 into a conditional acceleration technique is straightforward.
Theorem 11 (Conditional Acceleration via Eventual Decrease). If we
have χ(x) ≡
k
i=1 C i where each C i contains an inequation expr i (x) > 0 such
that
q
ϕ(x) ∧ expr i (x) ≥ expr i (a(x)) =⇒ expr i (a(x)) ≥ expr i (a
2 (x)),
(3)
then the following conditional acceleration technique is sound:
(χ, a, q
ϕ) → x
= a
n (x) ∧
k
i=1
expr i (x) > 0 ∧ expr i (a
n−1 (x)) > 0
If C i ≡ expr i > 0 for all i ∈ [1, k], then it is exact.
Example 5. Consider the following variant of T ev-dec .
while x 1 > 0 ∧ x 3 > 0 do
x1
x2
x3
←
x1+x2
x2−x3
x3
Starting with its canonical acceleration problem, we get
x
= a
n (x)
x 1 > 0 ∧ x 3 > 0
a :=
x1+x2
x2−x3
x3
T hm. 8
e x
= a
n (x) ∧ x 3 > 0 | x 3 > 0 | x 1 > 0 | a
T hm. 11
e
x
= a
n (x) ∧ x 3 > 0 ∧ x 1 > 0 ∧ x
(n−1)
1
> 0
x 3 > 0 ∧ x 1 > 0
a
where the second step can be performed via Thm. 11 as
( q
ϕ(x) ∧ expr (x) ≥ expr (a(x))) ≡ (x 3 > 0 ∧ x 1 ≥ x 1 + x 2 ) ≡ (x 3 > 0 ∧ 0 ≥ x 2 )
implies
(0 ≥ x 2 − x 3 ) ≡ (x 1 + x 2 ≥ x 1 + x 2 + x 2 − x 3 ) ≡ (expr (a(x)) ≥ expr (a
2 (x))).
6.2 Acceleration via Eventual Increase
Still, all (combinations of) techniques presented so far fail for
while x 1 > 0 do (
x1
x2 ) ←
x1+x2
x2+1
.
(T ev-inc )
As in the case of T ev-dec , the value of x 1 does not behave monotonically, i.e.,
x 1 > 0 is neither an invariant nor a converse invariant. However, this time x 1 is
eventually increasing, i.e., once x 1 starts to grow, it never decreases again. Thus,
in this case it suffices to require that x 1 is positive and (weakly) increasing.
F. Frohn
With Thm. 10, we can accelerate T ev-dec to
x
1
x
2
=
n−n
2
2 +x2·n+x1
x2−n
∧ x 1 > 0 ∧
n−1−(n−1)
2
2
+ x 2 · (n − 1) + x 1 > 0
as we have
(x 1 ≥ x 1 + x 2 ) ≡ (0 ≥ x 2 ) =⇒ (0 ≥ x 2 − 1) ≡ (x 1 + x 2 ≥ x 1 + x 2 + x 2 − 1).
Turning Thm. 10 into a conditional acceleration technique is straightforward.
Theorem 11 (Conditional Acceleration via Eventual Decrease). If we
have χ(x) ≡
k
i=1 C i where each C i contains an inequation expr i (x) > 0 such
that
q
ϕ(x) ∧ expr i (x) ≥ expr i (a(x)) =⇒ expr i (a(x)) ≥ expr i (a
2 (x)),
(3)
then the following conditional acceleration technique is sound:
(χ, a, q
ϕ) → x
= a
n (x) ∧
k
i=1
expr i (x) > 0 ∧ expr i (a
n−1 (x)) > 0
If C i ≡ expr i > 0 for all i ∈ [1, k], then it is exact.
Example 5. Consider the following variant of T ev-dec .
while x 1 > 0 ∧ x 3 > 0 do
x1
x2
x3
←
x1+x2
x2−x3
x3
Starting with its canonical acceleration problem, we get
x
= a
n (x)
x 1 > 0 ∧ x 3 > 0
a :=
x1+x2
x2−x3
x3
T hm. 8
e x
= a
n (x) ∧ x 3 > 0 | x 3 > 0 | x 1 > 0 | a
T hm. 11
e
x
= a
n (x) ∧ x 3 > 0 ∧ x 1 > 0 ∧ x
(n−1)
1
> 0
x 3 > 0 ∧ x 1 > 0
a
where the second step can be performed via Thm. 11 as
( q
ϕ(x) ∧ expr (x) ≥ expr (a(x))) ≡ (x 3 > 0 ∧ x 1 ≥ x 1 + x 2 ) ≡ (x 3 > 0 ∧ 0 ≥ x 2 )
implies
(0 ≥ x 2 − x 3 ) ≡ (x 1 + x 2 ≥ x 1 + x 2 + x 2 − x 3 ) ≡ (expr (a(x)) ≥ expr (a
2 (x))).
6.2 Acceleration via Eventual Increase
Still, all (combinations of) techniques presented so far fail for
while x 1 > 0 do (
x1
x2 ) ←
x1+x2
x2+1
.
(T ev-inc )
As in the case of T ev-dec , the value of x 1 does not behave monotonically, i.e.,
x 1 > 0 is neither an invariant nor a converse invariant. However, this time x 1 is
eventually increasing, i.e., once x 1 starts to grow, it never decreases again. Thus,
in this case it suffices to require that x 1 is positive and (weakly) increasing.