On Decidable Growth-Rate Properties of Imperative
Programs
(invited talk paper)
Amir M. Ben-Amram
School of Computer Science, Tel-Aviv Academic College
amirben@mta.ac.il

In 2008, Ben-Amram, Jones and Kristiansen showed that for a simple “core” programming language—
an imperative language with bounded loops, and arithmetics limited to addition and multiplication—
it is possible to decide precisely whether a program has certain growth-rate properties, namely polynomial (or linear) bounds on computed values, or on the running time.
This work emphasized the role of the core language in mitigating the notorious undecidability
of program properties, so that one deals with decidable problems, while allowing the application
of the technique to programs in a more realistic language. This is done by over-approximating the
semantics of the concrete program.
A natural and intriguing problem was whether more elements can be added to the core language,
improving the precision of approximation, while keeping the growth-rate properties decidable. In
particular, the method presented could not handle a command that resets a variable to zero. This
paper shows how to handle resets. The analysis is given in a logical style (proof rules), and the
complexity of the algorithm is shown to be PSPACE. The problem is shown PSPACE-complete (in
contrast, without resets, the problem was PTIME). The analysis algorithm evolved from the previous
solution in an interesting way: focus was shifted from proving a bound to disproving it, and the
algorithm works top-down rather than bottom-up.

1

Introduction

Central to the field of Implicit Computational Complexity (ICC) is the following observation: it is possible to restrict a programming language syntactically so that the admitted programs will possess a certain
complexity, say polynomial time, or polynomial output size. Since programmers want their programs to
have well-behaved complexity, this appears at first to be a useful approach. However, languages designed
to capture a complexity class tend to be too restrictive or cumbersome for practical programming. The
programmer would prefer to program normally—which means that algorithms of undesirable complexity
can be written—and would be happy to have them detected at compile time, just as type-related errors
are. Thus, we move into the realm of static program analysis.
Automated complexity analysis (or “cost analysis”) as a kind of static analysis has a long history,
with classic contributions including Wegbreit [Weg75], Rosendahl [Ros89] and Le Métayer [LM88].
Today it enjoys a flurry of research.
Static analysis targets program properties that are typically uncomputable in any Turing-complete
language. Complexity properties, such as having a polynomial running time, are no different (in fact,
they are still undecidable if termination is guaranteed). The common approach in static analysis is to just
give up a complete solution; usually, one takes a conservative approach, which means that an algorithm
P. Baillot (Ed.): Workshop on Developments in
Implicit Computational complExity (DICE 2010).
EPTCS 23, 2010, pp. 1–14, doi:10.4204/EPTCS.23.1

c Amir M. Ben-Amram
This work is licensed under the Creative Commons
Attribution-Noncommercial License.

2

Growth-Rate Properties of Imperative Programs

that has to certify programs as “good” may only err by rejecting a good program. In other words, it may
be sound but incomplete.
The downside of the conservative approach is that it gives up one of the hallmarks of algorithm
theory: studying well-defined problems and developing algorithms that actually solve them. Besides
losing the satisfaction of proving that a goal has been achieved, one loses the ability to precisely state
what has been achieved by a new algorithm, other than by anecdotal evidence such as examples that it
succeeds on.
The approach taken in this paper establishes a middle path. It consists of breaking the analysis of programs in two stages: the first is abstraction, in which the concrete program is replaced with an abstract
one, a simplified model of the original; the second stage is analysis of the abstract program. Abstract
programs are a weak model of computation where the properties of interest are, hopefully, decidable.
Their relation to concrete programs may be specified precisely by first assigning an approximate semantics to the source program—more precisely, one which over-approximates the behaviour of the concrete
program—then translating the program to a simplified “core” language, whose semantics is equal to the
approximate semantics of the original. The over-approximation ensures that the conclusions drawn for
the concrete programs are in the conservative zone. The analysis of core-language programs becomes
a new, well-defined problem that may well be solvable. Another benefit of the approach is that abstract
(core) programs may be rather independent of the concrete programming language, and their analysis
more widely applicable—one only needs “front ends” for the concrete languages of interest.
In areas other than complexity analysis, this approach is well known. Probably the best-known
example is the abtraction of programs into finite automata, central to software model checking. Closer to
complexity analysis is termination analysis. The size-change abstraction reduces a program to a transition
system specified by order-based constraints [LJBA01, BA09], whose termination is decidable.
The current paper is part of a plan to apply the “abstract and conquer” approach to complexity
analysis, based on previous work by Jones, Kristiansen and the author [BJK08]. This work defined an
imperative-style core language with restricted arithmetics and bounded loops. The loop bounds may be
computed values (this is the main source of difficulty in analysis). It was shown that certain growthrate questions are decidable for this language. Specifically, algorithms were given to decide whether
the running time is linear, polynomial or otherwise (as a function of input values); and which computed
values are polynomially (or linearly) bounded. Suprisingly, the analysis itself takes polynomial time.
Once a result of this kind is established, a program of further research arises automatically: investigate the tradeoff between the strength of the core language (the abstraction) and the decidability of the
properties of interest. A stronger core language can model more closely the concrete semantics of real
programs; in other words, it constitutes a finer abstraction. Make it too fine, and decidability will be
lost. It is interesting to find out how far we can venture while maintaining decidability: what language
features are the real impediments? What extensions will increase the difficulty of the analysis? Note that
since we are dealing with decidable problems, we can classify their complexity. Thus, in our approach,
if a polynomial algorithm for some problem is not found, we can look for a hardness proof to justify it.
This paper makes a contribution to this program by analysing a mild extension to the core language
of [BJK08]. Specifically, we add resetting assignments (X:=0). It is shown that the analysis problem
becomes PSPACE-hard. This is tight: a PSPACE algorithm is given. The algorithm evolved from the
previous solution in an interesting way: focus was shifted from proving a bound to disproving it, and the
algorithm works top-down rather than bottom-up.

Amir M. Ben-Amram

3

X, Y ∈ Variable

::=

X1 | X2 | X3 | . . . | Xn

e ∈ Expression

::=

X|X + Y|X * Y|0

C ∈ Command

::=

skip | X:=e | C1 ;C2 | loop X {C}

|

choose C1 or C2

Figure 1: Syntax of the core language Lr . Variables hold nonnegative integers.
Related work. Prior to our work in [BJK08], Niggl and Wunderlich [NW06] and later Jones and
Kristiansen [JK09] studied similar languages with similar methods—except that their programs were
“too concrete” and their analyses sound but incomplete. While both works consider branch conditionals
as “uninterpreted,” which technically means the same as abstracting them the way we do here, the loops
are considered as exact (in contrast to the non-deterministic loops used here, see the following section).
An important feature of our core language, crucial in our analyses, is being structured (which allows for a compositional analysis, or proof rules, as in this paper). In contrast, Albert et al. [AAGP08]
propose an “intermediate language” for complexity analysis that is essentially unstructured—quite natural, given that its original application was to Java bytecode. They emphasize that this language “can be
formally defined independent of the [source] programming language.” This agrees with our approach,
however their language is too strong—it is, in fact, Turing-complete for computations over integers—so
its analysis is as undecidable as for any concrete language.

2

Problem Statement

First, we define our core language, Lr .
Syntax is described in Figure 1 and should be self-explanatory. In a command loop X {C}, variable X
is not allowed to appear on the left-hand side of an assignment in the loop body C. There is no special
syntax for a “program.”
Data. It is most convenient to assume that the only type of data is nonnegative integers. More generality
is possible but will not be treated in this presentation.
Command semantics. The semantics of the core language is intended for over-approximating a realistic program’s semantics. Therefore, the core language is nondeterministic. The choose command
represents a nondeterministic choice, and can be used to abstract any concrete conditional command by
simply ignoring the condition. The loop command loop X` {C} repeats C a number of times bounded
by the value of X` . Thus, it may be used to model different kinds of loops (for-loops, while-loops)
as long as a bounding expression can be statically determined (possibly by an auxiliary analysis such
as [CS01, PR04]).
The use of bounded loops restricts the computable functions to be primitive recursive, but this is still
rich enough to make the analysis problem challenging.
Formally, the semantics associates with every command C over variables X1 , . . . , Xn a relation [[C]] ⊆
Nn × Nn . In the expression ~x[[C]]~y, vector ~x (respectively ~y) is the store before (after) the execution of C.

4

Growth-Rate Properties of Imperative Programs

The semantics of skip is the identity. The semantics of an assignment leaves some room for variation: either the precise value of the expression is assigned, or a nonnegative integer bounded by that
value. Because our analysis only involves monotone increasing functions, this choice does not affect the
results; but the second, non-deterministic definition increases the coverage of the core language, since
additional numeric operations can be modelled (over-approximated). Finally, composite commands are
described by the equations:
[[C1 ; C2 ]] = [[C2 ]] ◦ [[C1 ]]
[[choose C1 or C2 ]] = [[C1 ]] ∪ [[C2 ]]
[[loop X` {C}]] = {(~x,~y) | ∃i ≤ x` :~x[[C]]i~y}
where [[C]]i represents [[C]] ◦ · · · ◦ [[C]] (i occurrences of [[C]]); and [[C]]0 = [[skip]].
For every command we also define its step count (informally referred to as running time). The step
count of an atomic command is defined as 1. The step count of a loop command is the sum of the step
counts of the iterations taken. Because of the nondeterminism in if and loop commands, the step count
is also a relation.
Goals of the analysis. The polynomial-bound analysis problem is to find, for any given command,
which output variables are bounded by a polynomial in the input variables. This is the problem we
will fix our attention on, although some variants may also be of interest: The linear-bound problem
identifies linearly-bounded output values instead. The feasibility problem finds whether all the values
througout any computation of the command are polynomially bounded. This problem differs from the
polynomial-bound problem, because an exponential value may be computed and discarded. But it can be
solved with a small modification to the algorithm. The polynomial (linear) step-count problem is what
its name implies, and can be reduced to the the corresponding bound analysis problem by simple means
(see [BJK08]).
An example.
check).

In the following program, variables may grow exponentially (the reader is invited to

loop X4 {
X3 := X1 +X2 ;
choose { X1 := X3 } or { X2 := X3 };
}
However, the following version is polynomially bounded:
loop X4 {
X3 := X1 +X2 ;
choose { X1 := X3 } or { X2 := 0 };
}

3

Background: the Analysis of [BJK08]

The language treated in [BJK08] differs from our Lr only on one essential point: the constant 0 is not
included. Another difference is that expressions could be nested; but assignments with nested expressions
can be easily unfolded to unnested ones. Let LBJK denote the language obtained from Lr by omitting the
constant 0. Then from [BJK08] we have

Amir M. Ben-Amram

5

THEOREM 3.1. The polynomial-bound analysis problem for LBJK is in PTIME.
The algorithm that does this evolved from ideas in previous papers such as [NW06, JK09]. These
works, too, considered a structured imperative language, and gave an algorithm that evaluates any given
command to a so-called certificate. The certificate is a finite structure (basically, a matrix) which summarizes the input-output dependences in the command: how each of the output values depends on each
of the inputs. The analysis is compositional, which means that a certificate for a composite command
only depends on those of its parts. In fact, it parallels the (compositional) definition of semantics, and
can be stated as an abstract interpretation [Cou96]. The main novelty in the algorithm of [BJK08] was
a new kind of certificates, which encode sufficient information for precise analysis of the chosen core
language.
One of the open problems left by [BJK08] was analysis of extended versions of the core language,
and this paper presents a first step forward. The extension considered is the capability to reset a variable to
zero. One way to explain the difficulty caused by resets is as increased context-sensitivity: for example,
the command X:=Y*Z introduces a dependence of X on Z, but not if Y is fixed at zero. We shall solve this
problem by employing context-sensitive analysis [NNH05]. When applied to the compositional (bottomup) approach, this would mean creating a set of certificates for a given command, each annotated with
the context to which it applies, and indicating the context that results. This would create an explosion in
the algorithm’s complexity: the results of analysing a command would be exponentially big. We want to
avoid that (though polynomial time must be given up—witness the hardness result in Section 6.2). This
is why this paper presents not just an extension, but a redesign of the analysis of LBJK .
The design of the new solution was motivated by an observation on the correctness proofs of [BJK08]:
the soundness theorem (if the algorithm concludes that an output is polynomially bounded, it really is)
was more difficult to prove than the completeness theorem (if the algorithm concludes “not polynomial,”
this is correct). In retrospect, there is a simple reason: an output variable may be a function of several
input variables, and may depend on them differently in different executions; the positive conclusion must
account for all of these dependences—it is a universal statement. A negative conclusion, its negation, is
existential: just find some execution pattern in which the output depends exponentially on some input!
Noting this imbalance we will give, not an algorithm to certify outputs as polynomial, but a proof system
to prove that an output can be exponential1 . Searching for a proof is naturally performed top-down, and
it is in this way that we can prove it to be in PSPACE. Thus, this design is the converse of [BJK08] in a
second sense: favouring the top-down progress to bottom-up.

4

A Proof System for (Lack of) Polynomial Bounds

4.1

Ingredients

The basic ingredient in the proof system is called a dependence fact. In its simple (unary) form, it
indicates that an output variable depends, in a certain way, on some input variable. The set of variable
indices is denoted by I with generic elements i, j, k etc.
Definition 4.1. The set of dependence types is D = {1, 1+ , 2, 3}, with order 1 < 1+ < 2 < 3, and binary
maximum operator t. We write x ' 1 for x ∈ {1, 1+ }.
Verbally, we may refer to these types as:
1 =identity dependence, 1+ =additive dependence, 2 =multiplicative dependence, 3 =exponential
dependence.
1 Which

in this case is equivalent to not being polynomial.

6

Growth-Rate Properties of Imperative Programs

Definition 4.2. The set of dependences F is the union of two sets:
(1) The set of unary dependences, isomorphic to I × D × I . The notation for an element is i −
→ j.
(2) The set of binary dependences, isomorphic to I × I × I × I , where the notation for an element
is ij ⇒ k` .
δ

Informally, a binary dependence represents a conjunction, namely the fact that two unary dependences hold simultaneously. This is only used when the dependences in question are of types 1 or 1+ ,
and when i 6= j ∨ k 6= ` (a similar mechanism was used in [BJK08]).
Definition 4.3. A context is a subset of I . A dependence judgement is C, P ` D, Q where C is a command, P, Q are contexts and D is a dependence.
The pre-context P specifies variables that are presumed to hold zero; the post-context Q specifies
zeros guaranteed to come out. For an example, let C be the command loop X3 {X1 := X2 +X3 }. We have
1+

1

C, 0/ ` 2 −
→ 2, 0/ (X2 is not modified) and C, 0/ ` 2 −
→ 1, 0/ (X1 may be set to X2 plus something else). If X3 is
1+

initially zero, the loop does not execute. Therefore C, {3} ` 2 −
→ 1, Q does not hold for any Q. However,
1
C, {3} ` 1 −
→ 1, {3} holds: X1 is not modified and X3 is guaranteed to remain zero.
The inference rules for assignment commands, listed next, may further clarify the function of judgements.

4.2

Inference rules for assignments

We list the skip command among the assignments. It is, in fact, equivalent to X1 := X1 . Nonetheless, it
is instructive to examine it first.
1. (Unary rule for skip)
i∈
/P
1

skip, P ` i −
→ i, P
2. (Unary rule for Xl :=0)
i∈
/ P, i 6= l
1

Xl :=0, P ` i −
→ i, P ∪ {l}
3. (Unary rules for Xl :=Xr )
For any context P, let P`,r = P \ {l} ∪ {l | if r ∈ P}.
i∈
/ P, i 6= l
1

Xl :=Xr , P ` i −
→ i, P`,r

r∈
/P
1

Xl :=Xr , P ` r −
→ l, P`,r

4. (Unary rules for Xl :=Xr *Xs )
For any context P, let Pl,r,s = P \ {l} ∪ {l | if r ∈ P or s ∈ P}.
i∈
/ P, i 6= l
1

Xl :=Xr *Xs , P ` i −
→ i, Pl,r,s

r, s ∈
/ P, t ∈ {r, s}
2

Xl :=Xr *Xs , P ` t −
→ l, Pl,r,s

Amir M. Ben-Amram

7

5. (Unary rules for Xl :=Xr +Xs , where r 6= s)
For any context P, let Pl,r,s = P \ {l} ∪ {l | if r, s ∈ P}.
r∈
/ P, s ∈ P

i∈
/ P, i 6= l
1

1

Xl :=Xr +Xs , P ` i −
→ i, Pl,r,s

Xl :=Xr +Xs , P ` r −
→ l, Pl,r,s

r ∈ P, s ∈
/P
r, s ∈
/P

1

Xl :=Xr +Xs , P ` s −
→ l, Pl,r,s

1+

Xl :=Xr +Xs , P ` t −
→ l, Pl,r,s for t ∈ {r, s}.
6. (Binary rules for assignments)
Let C be any of the above commands. If, for i, i0 ∈
/ P, and j, j0 ∈
/ Q, where i 6= i0 or j 6= j0 , we have
r2 0
r1
0
→ j , Q, where r1 , r2 ' 1, then C, P ` ii0 ⇒ jj0 , Q.
→ j, Q and C, P ` i −
C, P ` i −

4.3

Inference rules for composite commands

The composite commands are the choice, sequential composition and the loop.
Choice is simplest, handled by the obvious rules:

(C)

C1 , P ` D, Q
choose C1 or C2 , P ` D, Q

C2 , P ` D, Q
choose C1 or C2 , P ` D, Q

Sequential composition requires an operator for abstract composition, that is, composition of dependences.
Definition 4.4. The binary operation · is defined on F by the following rules:
β

α

(i −
→ j) · ( j −
→ k)
α

(i −
→ j) · ( jj ⇒ kk0 )
α

( ii0 ⇒ jj ) · ( j −
→ k)
( ii0

⇒

j
j
j0 ) · ( j0

⇒

k
k0 )

αtβ

= i −−→ k
=

( ii ⇒ kk0 ),

provided α ' 1

=

( ii0 ⇒ kk ),

provided α ' 1

=






i
i0

⇒ kk0 ,


2

 i−
→ k,

if i 6= i0 or k 6= k0
if i = i0 and k = k0

We now have the rule
(S)

C1 , P ` D1 , Q C2 , Q ` D2 , R
C1 ; C2 , P ` D1 · D2 , R

Naturally, the rule is only applicable if D1 · D2 is defined.

8

Growth-Rate Properties of Imperative Programs

The loop involves the possibility of growth that depends on the number of iterations. To handle this,
we introduce a loop correction operator (not unlike the one in [BJK08]).
Definition 4.5. The loop correction operator LC` : F → F is defined by
1+

2

2

3

LC` (i −
→ i) = ` −
→i
LC` (i −
→ i) = ` −
→i
Explanation: in the first case, Xi has something added to it. Intuitively, if this happens inside a loop,
it results in growth that is at least linear in the number of iterations. In the second case, Xi is multiplied
by something, which results in exponential growth.
There are three loop rules. The first covers the case that the body is not executed.
skip, P ` D, P
loop X` {C}, P ` D, P

(L0)

The second describes the result of any number m > 0 of iterations.
C, P0 ` D1 , P1

(L1)

C, P1 ` D2 , P2 . . . C, Pm−1 ` Dm , Pm
loop X` {C}, P0 ` D1 · D2 · . . . · Dm , Pm

`∈
/ P0

The third applies the LC operator.
(L2)

loop X` {C}, P0 ` D1 , P1

loop X` {C}, P1 ` D2 , P1 loop X` {C}, P1 ` D3 , P3
loop X` {C}, P0 ` D1 · LC` (D2 ) · D3 , P3

`∈
/ P0

Note that as LC` is applied to D2 , we require that D2 be a dependence that can be iterated: this
requires that the pre-context and post-context be the same. An example may help to clarify this rule.
Consider first the following loop L:
loop X4 {
loop X3 { X1 := X2 } ;
X2 := X1 + X2 ;
}
It is easy to see that the outer loop’s body, C, consisting of the inner loop and the subsequent assign2
ment, may set X2 to twice its initial value. This is expressed by the judgement 0,
/ C`2−
→ 2, 0/ (the reader
may want to construct the proof for this); it therefore follows by (L1) that
(1)

2

L, 0/ ` 2 −
→ 2, 0/ .

It is also the case that
(2)

1

L,0/ ` 2 −
→ 1, 0/

and by (L0),
(3)

1

L,0/ ` 4 −
→ 4, 0/ .

Amir M. Ben-Amram

9

Since the pre-context and the post-context are the same in (1), this judgement describes an iterative
dependence and by (L2) we obtain
1

2

1

L, 0/ ` (4 −
→ 4) · LC` (2 −
→ 2) · (2 −
→ 1), 0/
that is
3

L, 0/ ` 4 −
→ 1, 0/
The result in X1 depends exponentially on the input X4 .
Change now the loop as follows:
loop X4 {
loop X3 { X1 := X2 } ;
X2 := X1 + X2 ;
X3 := 0;
}
Now instead of (1), we have
2

L, 0/ ` 2 −
→ 2, {3}

(4)

Where the post-context represents the resetting of X3 . This dependence is not iterative: the post-context
differs from the pre-context. (L2) is not applicable as above and indeed, the modified loop does not
generate exponential growth any more.
Another subtle point with this rule is the role of the “preamble” D1 that comes before the iterative
part. Since the LC` operator only expresses dependence on the loop variable X` , and this variable is not
1
modified within the loop, the dependence D1 can only be ` −
→ `. Why is it included then? The reason
is that a certain, finite number of initial iterations may set up a context necessary for the iterative part.
Consider the following command.
X2 := 0;

loop X3 { X1 := X2 *X1 ; X2 := X1 }
2

The loop command, L, satisfies L, 0/ ` 1 −
→ 1, 0/ which leads to exponential dependence of X1 (and
consequently X2 ) on X3 . But the loop is entered in the context {2} (note the preceding reset), and L, {2} `
2
1−
→ 1, {2} does not hold. It is therefore crucial to note that an initial iteration can modify X2 . This
appears formally as:
1

(5)

L, {2} ` 3 −
→ 3, 0/

2

1

L, 0/ ` 1 −
→ 1, 0/ L, 0/ ` 1 −
→ 2, 0/
1

2

3∈
/ {2}

1

L, {2} ` (3 −
→ 3) · LC` (1 −
→ 1) · (1 −
→ 2), 0/
3

L, {2} ` 3 −
→ 2, 0/

4.4

Correctness theorem

THEOREM 4.6. Let C be a command of Lr (interpreted over the non-negative integers). If C, {} `
3
i−
→ j, Q for some i and Q, then the values that y j can take, given~x[[C]]~y, cannot be bounded polynomially
in ~x. If no such judgement can be proved, a polynomial bound exists.

10

Growth-Rate Properties of Imperative Programs

While the full proof will not be given here, here is a very brief overview. The first direction (soundness of the conclusion of exponential growth) is proved in the natural way: after defining carefully the
semantics of judgments, one proceeds to prove that each inference rule is sound. This requires some care
in the case of loops, while the rest is straight-forward.
The second direction (soundness of the conclusion of polynomial boundedness) requires more effort.
It is helpful to view the analysis as an abstract interpretation where the abstract semantics of a command
is the set of judgements that can be proved about it. We prove that when this set does not contain a Type 3
dependence for X j , its final value admits a polynomial bound. Clearly, this set can be exponentially big,
but without contexts it is of polynomial size. Thus, the result of [BJK08] can be reconstructed as a special
case.

5

Checking for Linear Bounds

In Section 2 a few variants of our problem were described. Here we give the details of solving one of
them: the linear-bound problem. This problem differs from the polynomial-bound problem only in the
definition of “good” and “bad” growth: now every non-linear dependence is “bad” and will be labeled
by a 3. Thus, 2’s only describe linear bounds.
1
2
For example, the command X1 := X1 +2*X2 (with empty pre-context) satisfies X2 → X2 , X2 → X1 ,
1+

3

X1 → X1 ; while X1 := X1 +X2 *X2 yields X2 → X1 .
Judgements `lin for linear bounds are proved just like their counterparts for polynomial bounds (judgments `) except as follows.
1. The second unary rule for multiplication (Page 6) is changed into
r, s ∈
/ P, t ∈ {r, s}
3

Xl :=Xr *Xs , P ` t −
→ l, Pl,r,s for t ∈ {r, s}.
2. In the definition of the loop correction operator (Page 8) one case is modified:
1+

3

LC` (i −
→ i) = ` −
→ i.
THEOREM 5.1. Let C be a command of Lr (interpreted over the non-negative integers). If C, {} `lin
3
i−
→ j, Q for some i and Q, then the values that y j can take, given ~x[[C]]~y, cannot be bounded linearly in ~x.
If no such judgement can be proved, a linear bound exists.

6

Complexity

Here we establish the complexity class of the polynomial-bound (or linear-bound) analysis problem for
Lr . Note that the complexity is in terms of the size of the analysed program.

6.1

Inclusion in PSPACE

Savitch’s theorem makes it easy to prove inclusion in PSPACE by giving a polynomial-space nondeterministic algorithm, which is quite easy to do here.
3
Consider a recursive algorithm that tries to prove C, {} ` i −
→ j, Q with i and Q non-deterministically
chosen (and j too, if we do not query a particular output). The algorithm attempts to develop a proof tree

Amir M. Ben-Amram

11

non-deterministically, in a depth-first manner. To ensure polynomial space complexity, it is necessary
to bound the depth of the proof tree, and the amount of memory needed to process each node. The
latter is easily seen to be polynomial (this is the case even with rule L1, despite the fact that m is not
polynomially bounded, since the rule can be applied without keeping the whole list of steps in memory).
As for the depth, for all commands except the loop, the subgoals of a proof node for the command relate
to its sub-commands; thus the proof tree would have precisely the depth of the syntax tree, were it not for
the loop rule L2, which recursively uses judgements on the same loop. However, the following lemma
(stated without proof) solves the problem.
LEMMA 6.1. Let C be a loop command. If C, P ` D, Q can be proved using rule L2, then it can be
proved using L2 where the premises are only proved using L0 and L1.

6.2

Hardness

We prove PSPACE-hardness of the linear-bound problem. The proof can be tweaked to apply to polynomial bounds as well. It is a reduction from a binary-alphabet version of the well-known PSPACEcomplete problem, NFA Universality. The problem is defined as follows.
INSTANCE: A nondeterministic finite automaton A = (Q, Σ, δ , q0 , F), where Σ = {0, 1},
δ ⊆ Q × Σ × Q is the set of transitions, q0 the initial state and F the (non-empty) set of
accepting states.
QUESTION: Is L(A) = Σ∗ ?
Let A be given, with Q = {1, . . . , n}. We construct a program with variables X1 , . . . , Xn , X01 , . . . , X0n , Y, Z.
For convenience we use compound expressions (but these can be taken to be syntactic sugar).
For each q ∈ Q and a ∈ Σ, let Cq,a be the command
X0q := Z*Xi1*Xi2 * . . . *Xi p
where {i1 , . . . , i p } are all the predecessors of q under a-transitions. The multiplication by Z solves the
difficulty with states having no predecessors.
For each a ∈ Σ, let Ca be
C1,a ; C2,a ; . . . Cn,a ; X1 :=X01 ; . . . ; Xn :=X0n
and let Fin be the command
Z := Z*Xi1*Xi2 · · · *Xi|F|
where F = {i1 , . . . , i|F| }.
Let P be the program:
Xq0 :=0; loop Y {choose C0 or C1 }; Fin
Suppose that the loop performs k iterations, where the ith iteration chose Ca j . At its end, variable Xq
will be 0 if and only if state q is reached on the word w = a1 . . . ak . In Fin, Z will be set to 0 if and only
if at least one accepting state is reached, that is, if A accepts w. If it does not, Z will be set to a non-linear
function of the inputs (and this can then happen for all inputs satisfying Y ≥ k). We conclude that Z is
linearly bounded if and only if A is universal.
Note that by this proof, PSPACE-hardness holds for Lr without the addition operation, since it is not
used in the construction. Alternatively, since multiplication can be simulated by a loop of additions, we
can also conclude hardness for Lr without multiplication. The choice command can also be eliminated,
since it can be simulated by the non-deterministic loop. We obtain

12

Growth-Rate Properties of Imperative Programs

THEOREM 6.2. The linear-bound analysis problem is PSPACE-hard for the following subset of Lr :
X, Y ∈ Variable
e ∈ Expression
C ∈ Command

::=
::=
::=

X1 | X2 | X3 | . . . | Xn
X|X + Y|0
X:=e | C1 ;C2 | loop X {C}

The same holds for the other problems enumerated in Section 2.

7

Can we take it further?

There are many directions in which this work in particular, and the approach in a looser sense, can be
taken further. The most immediate and obvious question to ask is how else can LBJK be extended while
keeping our problems solvable. In other words, we would like to understand what programming-language
features lend themselves to growth-rate analysis and which make trouble.
From our work in [BJK08], one of the clear insights was that key to our success was the property of
monotonicity. Firstly, of the functions computed by arithmetic operators that we admitted—and indeed,
if we extend LBJK with subtraction of integers (assuming exact arithmetics), we obtain a language where
none of our problems is decidable.
Monotonicity is also necessary in the semantics of commands. While for the choose command and
sequential composition, a suitable notion of monotonicity can be easily established, the loop command
is more difficult. What we found was that exact loop semantics, where the number of iterations specified
by the loop header is always completed, destroys monotonicity: a second iteration may erase the result
of the first, so that increasing the iteration count does not increase the output. Our non-deterministic loop
semantics restores monotonicity, since increasing the loop variable only makes more outcomes possible.
That is the key to success, and happily, it may also be useful (the kind of loops with non-monotone
behaviour are probably not a natural programming style, but loops that allow premature termination are).
Moreover, exact loops do defy analysis—and not much is required besides! The following tiny language
has an undecidable linear-bound analysis problem, given that the loop semantics is exact [BK09]:
X, Y ∈ Variable
C ∈ Command

::=
::=

X1 | X2 | X3 | . . . | Xn
X:=Y | X:=Y+Z | C1 ;C2 | loop X {C}

From this point of view, we may explain the difficultly of including resetting assignments in the
analysis of [BJK08] by observing that they introduce a pinch of non-monotonicity. But not too much:
the introduction of contexts solves this problem. If you know where the zeros are, the rest is monotone.
Let us consider a few other possible extensions.

max and min operators
The command X := max(Y,Z), with the natural semantics (over non-negative integers), can be added
to Lr completely for free. It is, for the purpose of our analysis, equivalent to choose X:=Y or X:=Z.
Not so for X := min(Y,Z). It is non-monotone, and adding it to LBJK makes the analysis PSPACEhard, by essentially the reduction of Section 6.2 (minimum can play the role of multiplication by zero).
Conjecture: this problem, too, is PSPACE-complete.

Amir M. Ben-Amram

13

The constant 1
Allowing the constant 1 in is a significant extension. Note that once you have 1, you can generate
other positive constants. You can also compute fractions, in a sense: for example, The following loop
repeatedly exchanges variables, so that the value increases every other iteration:
X1 := Z; X2 := Z; loop Y { Z:= X1 ; X1 := X2 + 1; X2 := Z }
Thus the effect of this loop is described by the pseudo-command Z := Z+ 21 Y.
It remains an open problem whether the analysis problems for this language are decidable.

Space bounds
We mentioned the size of integers and running time. What about space bounds? If we are interested in
the number of bits taken by an integer-manipulating program, then bounding the numbers polynomially
is equivalent to bounding the space linearly. For another setting, assume that the program allocates arrays
by specifying their size, and that the arrays can be left out of the abstraction (because there is no data flow
from the contents of the arrays to the variables used as allocation sizes and loop indices; this is true for
many programs). Then one can test for polynomial space, essentially by including a variable that sums
all allocations. A greater challenge, left for future work, is the analysis of programs that can allocate as
well as de-allocate memory blocks; such programs are likely to use much less space then the sum of all
allocations (but note that our analysis cannot handle subtraction!).

Other challenges
• Extending the types of growth-rates that can be decided beyond the current selection of linear and
polynomial. In light of the results in [KN03, KN04], it seems plausible that the method could be
extended to classify the Grzegorczyk-degree of the growth rate.
• Moving to different language styles, such as programs with recursion, programs with high-order
functions, or unstructured (flowchart) programs.

8

Conclusion

This paper presents progress in a project of investigating program abstractions with decidable growthrate analysis problems, and establishing the computational complexity of such problems. In particular,
we have added a reset-to-zero command to the language of [BJK08]. We have suggested a solution
based on inference rules that are targeted at proving non-polynomial growth, instead of the previous
approach of computing certificates to polynomiality. This idea may be interesting in its own right; note
that we can freely exchange a problem with its complement precisely because we are designing a precise
decision procedure! This also allows us to classify the complexity of the analysis problem. In the case
of resets, we have shown that the analysis problem rises from PTIME to PSPACE-complete. There are
other possible extensions whose complexity (even decidability) are not known. An intriguing theoretical
question is: are there any (reasonably natural) “core languages” for which the analysis is decidable, yet
has a complexity above PSPACE-complete?

Acknowledgement
The author is indebted to Lars Kristiansen for some helpful comments on the manuscript.

14

Growth-Rate Properties of Imperative Programs

References
[AAGP08] Elvira Albert, Puri Arenas, Samir Genaim, and Germán Puebla. Automatic inference of upper bounds
for recurrence relations in cost analysis. In Marı́a Alpuente and Germán Vidal, editors, Static Analysis,
15th International Symposium, SAS 2008, Valencia, Spain, Proceedings, volume 5079 of Lecture Notes
in Computer Science, pages 221–237. Springer, 2008.
[BA09]

Amir M. Ben-Amram. Size-change termination, monotonicity constraints and ranking functions. In
Ahmed Bouajjani and Oded Maler, editors, Computer Aided Verification, 20th International Conference, CAV 2009, Grenoble, France, volume 5643 of Lecture Notes in Computer Science, pages
109–123. Springer, 2009.

[BJK08]

Amir M. Ben-Amram, Neil D. Jones, and Lars Kristiansen. Linear, polynomial or exponential? complexity inference in polynomial time. In Arnold Beckmann, Costas Dimitracopoulos, and Benedikt
Löwe, editors, Logic and Theory of Algorithms, Fourth Conference on Computability in Europe, CiE
2008, volume 5028 of LNCS, pages 67–76. Springer, 2008.

[BK09]

Amir M. Ben-Amram and Lars Kristiansen. The limits of decidability and tractability in growth-rate
analysis for programs. An informal presentation within the Fifth Conference on Computability in
Europe, CiE 2009, Heidelberg, Germany, 2009.

[Cou96]

Patrick Cousot. Abstract interpretation. ACM Computing Surveys, 28(2):324–328, June 1996.

[CS01]

Michael Colón and Henny Sipma. Synthesis of linear ranking functions. In 7th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS), volume 2031 of
Lecture Notes in Computer Science, pages 67–81. Springer, 2001.

[JK09]

Neil D. Jones and Lars Kristiansen. A flow calculus of mwp-bounds for complexity analysis. ACM
Trans. Computational Logic, 10(4):1–41, 2009.
Lars Kristiansen and Karl-Heinz Niggl. The garland measure and computational complexity of stack
programs. Electr. Notes Theor. Comput. Sci., 90(1), 2003.

[KN03]
[KN04]

Lars Kristiansen and Karl-Heinz Niggl. On the computational complexity of imperative programming
languages. Theor. Comp. Sci., 318(1-2):139–161, 2004.

[LJBA01] Chin Soon Lee, Neil D. Jones, and Amir M. Ben-Amram. The size-change principle for program
termination. In Proceedings of the Twenty-Eigth ACM Symposium on Principles of Programming
Languages, January 2001, volume 28, pages 81–92. ACM press, January 2001.
[LM88]

Daniel Le Métayer. Ace: an automatic complexity evaluator. ACM Trans. Program. Lang. Syst.,
10(2):248–266, 1988.

[NNH05]

Flemming Nielson, Hanne Riis Nielson, and Chris Hankin. Principles of Program Analysis. SpringerVerlag, second printing edition, 2005. (1st ed. 1999).

[NW06]

Karl-Heinz Niggl and Henning Wunderlich. Certifying polynomial time and linear/polynomial space
for imperative programs. SIAM J. Comput, 35(5):1122–1147, 2006.

[PR04]

Andreas Podelski and Andrey Rybalchenko. A complete method for synthesis of linear ranking functions. In Bernhard Steffen and Giorgio Levi, editors, VMCAI 2003: Verification, Model Checking, and
Abstract Interpretation, volume 2937 of LNCS, pages 239–251. Springer, 2004.

[Ros89]

M. Rosendahl. Automatic complexity analysis. In Proceedings of the Conference on Functional
Programming Languages and Computer Architecture FPCA’89, pages 144–156. ACM, 1989.

[Weg75]

Ben Wegbreit. Mechanical program analysis. Communications of the ACM, 18(9):528–539, September
1975.

