A Calculus for Modular Loop Acceleration
61
Theorem 1 (Acceleration via Monotonic Decrease [28]). If
ϕ(a(x)) =⇒ ϕ(x),
then the following acceleration technique is exact:
T loop → x
= a
n (x) ∧ ϕ(a
n−1 (x))
So for example, Thm. 1 accelerates T exp to ψ exp . However, the requirement
ϕ(a(x)) =⇒ ϕ(x) is often violated in practice. To see this, consider the loop
while x 1 > 0 ∧ x 2 > 0 do (
x1
x2 ) ←
x1−1
x2+1
.
(T non-dec )
It cannot be accelerated with Thm. 1 as
x 1 − 1 > 0 ∧ x 2 + 1 > 0
=⇒ x 1 > 0 ∧ x 2 > 0.
A dual acceleration technique is obtained by “reversing” the implication in
the prerequisites of Thm. 1. Then I ϕ is monotonically increasing w.r.t. a. So ϕ
is an invariant and thus {x ∈ Z
d
| ϕ(x)} is a recurrent set [22] of T loop .
Theorem 2 (Acceleration via Monotonic Increase). If
ϕ(x) =⇒ ϕ(a(x)),
then the following acceleration technique is exact:
T loop → x
= a
n (x) ∧ ϕ(x)
As a minimal example, Thm. 2 accelerates
while x > 0 do x ← x + 1
to x
= x + n ∧ x > 0.
3.2 Acceleration via Decrease and Increase
Both acceleration techniques presented so far have been generalized in [11].
Theorem 3 (Acceleration via Monotonicity [11]). If
ϕ(x) ⇐⇒ ϕ 1 (x) ∧ ϕ 2 (x) ∧ ϕ 3 (x),
ϕ 1 (x) =⇒ ϕ 1 (a(x)),
ϕ 1 (x) ∧ ϕ 2 (a(x)) =⇒ ϕ 2 (x),
and
ϕ 1 (x) ∧ ϕ 2 (x) ∧ ϕ 3 (x) =⇒ ϕ 3 (a(x)),
then the following acceleration technique is exact:
T loop → x
= a
n (x) ∧ ϕ 1 (x) ∧ ϕ 2 (a
n−1 (x)) ∧ ϕ 3 (x)