1624 LABEL:LastPageJun. 25, 2019May 13, 2020

*A preliminary version of this paper appeared in FoSSaCS 2019, LNCS 11425:80–97

# Tight Polynomial Worst-Case Bounds
for Loop Programs*

Amir M. Ben-Amrama  aQiryat Ono, Israel<EMAIL_ADDRESS>and  Geoff
Hamiltonb  bSchool of Computing, Dublin City University, Ireland
<EMAIL_ADDRESS>
###### Abstract.

In 2008, Ben-Amram, Jones and Kristiansen showed that for a simple programming
language—representing non-deterministic imperative programs with bounded
loops, and arithmetics limited to addition and multiplication—it is possible
to decide precisely whether a program has certain growth-rate properties, in
particular whether a computed value, or the program’s running time, has a
polynomial growth rate.

A natural and intriguing problem was to move from answering the decision
problem to giving a quantitative result, namely, a tight polynomial upper
bound. This paper shows how to obtain _asymptotically-tight_ , _multivariate_
, _disjunctive_ polynomial bounds for this class of programs. This is a
complete solution: whenever a polynomial bound exists it will be found.

A pleasant surprise is that the algorithm is quite simple; but it relies on
some subtle reasoning. An important ingredient in the proof is the _forest
factorization theorem_ , a strong structural result on homomorphisms into a
finite monoid.

###### Key words and phrases:

asymptotically-tight, multivariate, disjunctive, worst-case, polynomial bounds

##  1\. Introduction

One of the most important properties we would like to know about programs is
their _resource usage_ , i.e., the amount of resources (such as time, memory
and energy) required for their execution. This information is useful during
development, when performance bugs and security vulnerabilities exploiting
performance issues can be avoided. It is also particularly relevant for mobile
applications, where resources are limited, and for cloud services, where
resource usage is a major cost factor.

In the literature, a lot of different “cost analysis” problems (also called
“resource bound analysis”, etc.) have been studied (e.g. [Weg75, Ros89, LM88,
AAG+12, GAB+17, LDK+18, CHS15, SZV17]); several of them may be grouped under
the following general definition. The _countable resource problem_ asks about
the maximum usage of a “resource” that accumulates during execution, and which
one can explicitly count, by instrumenting the program with an accumulator
variable and instructions to increment it where necessary. For example, we can
estimate the _execution time_ of a program by counting certain “basic steps”.
Another example is counting the number of visits to designated program
locations. Realistic problems of this type include bounding the number of
calls to specific functions, perhaps to system services; the number of I/O
operations; number of accesses to memory, etc. The consumption of resources
such as _energy_ suits our problem formulation as long as such explicit
bookkeeping is possible (we have to assume that the increments, if not
constant, are given by a monotone polynomial expression).

In this paper we solve the _bound analysis problem_ for a particular class of
programs, defined in [BJK08]. The bound analysis problem is to find symbolic
bounds on the maximal possible value of an integer variable at the end of the
program, in terms of some integer-valued variables that appear in the initial
state of a computation. Thus, a solution to this problem might be used for any
of the resource-bound analyses above. In this work we focus on values that
grow polynomially (in the sense of being bounded by a polynomial), and our
goal is to find polynomial bounds that are tight, in the sense of being
precise up to a constant factor.

The programs we study are expressed by the so-called _core language_. It is an
imperative language, including bounded loops, non-deterministic branches and
restricted arithmetic expressions; the syntax is shown in Figure 1. The
semantics is explained and motivated below, but is largely intuitive; see also
the illustrative example in Figure 2. In 2008, it was proved [BJK08] that for
this language it is decidable whether a computed result is polynomially
bounded or not. This makes the language an attractive target for work on the
problem of computing tight bounds. However, for the past ten years there has
been no improvement on [BJK08]. We now present an algorithm to compute, for
every program in the language, and every variable in the program which has a
polynomial upper bound (in terms of input values), a tight polynomial bound on
its largest attainable value (informally, “the worst-case value”) as a
function of the input values. The bound is guaranteed to be tight up to a
multiplicative constant factor but constants are left implicit (for example a
bound quadratic in $n$ will always be represented as $n^{2}$). The algorithm
could be extended to compute upper and lower bounds with explicit constant
factors, but choosing to ignore coefficients simplifies the algorithm
considerably. In fact, we have striven for a simple, comprehensible algorithm,
and we believe that the algorithm we present is sufficiently simple that,
beyond being comprehensible, offers insight into the structure of computations
in this model.

Our philosophy is that research on complete solutions to static analysis
questions regarding weak languages is desirable for several reasons. First, it
is theoretically satisfying—it establishes a clear and definite result. The
algorithm can be possibly employed later in more complex situations, and we
will at least have an assurance that it does its part; arguments about the
value of relying on decidable problems in program analysis have recently been
given in [MP18], and [K18] gives a methodology for incorporating them as parts
in a bigger system (albeit for safety problems). Knowing that a problem is
solvable for a certain weak language gives us a point of reference for future
research, and makes it meaningful to further discuss questions of
computational complexity. As pointed out in [MP18], when an algorithm to prove
a property has a completeness proof, it usually means that it is possible to
furnish a justification for a negative answer, which is of value to the user.
In our case, if the algorithm returns a bound which is higher than what you
wanted, you can obtain from it an _execution pattern_ which shows how the
result arose. Finally, the quest for complete solutions drives research
forward by setting challenges which invite new insights and ideas.

Next, we explain the definition of the language in more detail. We will
comment about the motivation for the definitions, in particular vis-à-vis the
analysis of fuller programming languages. The main argument is that choices in
the definition of the language are driven by the idea of using it as a
_conservative abstraction_.

###  1.1. The core language

$\begin{array}[]{rcl}\verb+X+\in\mbox{Variable}&\;\;::=&\texttt{X}_{1}\mid\texttt{X}_{2}\mid\texttt{X}_{3}\mid\ldots\mid\texttt{X}_{n}\\\
\verb+E+\in\mbox{Expression}&::=&\verb+X+\mid\verb/E + E/\mid\verb+E * E+\\\
\verb+C+\in\mbox{Command}&::=&\verb+skip+\mid\verb+X:=E+\mid\verb+C+_{1}\texttt{;}\verb+C+_{2}\mid\texttt{loop
E
\\{C\\}}\mid\texttt{choose}\;\texttt{C}_{1}\;\texttt{or}\;\texttt{C}_{2}\end{array}$
Figure 1. Syntax of the core language.

##### Data.

The only type of data in the core language is non-negative integers.111This
could be modified to all integers, as explained later. In a practical setting,
a program may include statements that manipulate non-integer data that can,
however, be abstracted away without losing the information critical to loop
control —hence to a complexity analysis—as loops are often controlled by
integer variables. In other cases, it is possible to preprocess a program to
replace complex data values with their size (or “norm”), which is the quantity
of importance for loop control. Methods for this process have been widely
studied in conjunction with termination and cost analysis. These
considerations motivate the study of weak languages that handle integers.

##### Command semantics.

The core language is inherently non-deterministic. The choose command
represents a non-deterministic choice, and can be used to abstract any
concrete conditional command by simply ignoring the condition. Note that what
we ignore is branches within a loop body and not branches that implement the
loop control, as loops are represented by a dedicated loop command. The
command $\verb+loop E {C}+$ repeats C a non-deterministic number of times
bounded by the value of ${\tt E}$, which is evaluated just before the loop is
entered. Thus, as a conservative abstraction, it may be used to model
different forms of loops (for-loops, while-loops) as long as a bound on the
number of iterations, as a function of the program state on loop initiation,
can be determined and expressed in the language. There is an ample body of
research on analysing programs to find such bounds where they are not
explicitly given by the programmer; in particular, bounds can be obtained from
a _ranking function_ for the loop [PR04, BHZ08, ADFG10, BAG14, BG17]. Note
that the arithmetic in our language is too restricted to allow for the
maintenance of counters and the management of _while_ loops, as there is no
subtraction, no explicit constants and no tests. Thus, for realistic
“concrete” programs which use such devices, loop-bound analysis is supposed to
be performed _on the concrete program_ as part of the process of abstracting
it to the core language. This process is illustrated in [BAP16, Sect. 2]. The
semantics of the loop is non-deterministic, so that the loop is allowed to
actually perform fewer iterations than indicated by the bound expression; this
is useful both for modeling loops that can “break,” as well as for using the
results of auxiliary analyses, as those usually provide just a bound, not a
precise number of iterations.

An interesting observation has been made by Jones and Kristiansen [JK09]:
typically, algorithms whose goal is to prove loop termination and establish
loop bounds do so by focusing on values that _decrease_ (examples are the
Size-Change Termination principle [LJB01] and numerous methods that discover
_ranking functions_). In contrast, by abstracting to our core language ([JK09]
uses a very similar language), we focus on values that _grow_. Recent work in
static analysis [BEF+16] describes an analysis system which combines a
subsystem for loop-bound analysis (via ranking functions) with a subsystem for
growth-rate analysis, which establishes symbolic bounds on data that grow
along a loop. Our definition of the core language separates the concerns and
concentrates on the problem of value growth, for a program (or program
fragment) where loop bounds are already known. Note however that the loop
bound is to be given as a function of the state in which the loop is started,
and may well depend on values that are the result of previous computations, as
our example program in Figure 2 illustrates.

loop X1 { loop X2 \+ X3 { choose { X3:= X1; X2:= X4 } or { X3:= X4; X2:= X1 }
}; X4:= X2 \+ X3};loop X4 { choose { X3:= X1 \+ X2 \+ X3 } or { X3:= X2; X2:=
X1 } }

Figure 2. A core-language program. loop $n$ C means “do C at most $n$ times.”

From a computability viewpoint, the use of bounded loops restricts the
programs that can be represented to such that compute primitive recursive
functions; this is a rich enough class to cover a lot of useful algorithms and
make the analysis problem challenging. In fact, our language resembles a weak
version of Meyer and Ritchie’s LOOP language [MR67], which computes all the
primitive recursive functions, and where behavioral questions like “is the
result linearly bounded” are undecidable.

###  1.2. The algorithm

Consider the program in Figure 2. Suppose that it is started with the values
of the variables $\texttt{X}_{1},\texttt{X}_{2},\dots$ being
$x_{1},x_{2},\dots$. Our purpose is to bound the values of all variables at
the conclusion of the program in terms of those initial values. Indeed, they
are all polynomially bounded, and our algorithm provides tight bounds. For
instance, it establishes that the final value of $\texttt{X}_{3}$ is tightly
bounded (up to a constant factor) by
$\max(x_{4}(x_{4}+x_{1}^{2}),x_{4}(x_{2}+x_{3}+x_{1}^{2}))$.

Actually, the algorithm produces information in a more precise form, as _a
disjunction of simultaneous bounds_. This means that it generates a set of
tuples of polynomials, called _multi-polynomials_. Each such tuple provides
simultaneous bounds on all variables in a subset of possible executions; for
example, with the program in Figure 2, one such multi-polynomial is $\langle
x_{1},x_{2},x_{3},x_{2}+x_{3}\rangle$, which means that, starting with the
valuation $\texttt{X}_{1}\mapsto x_{1},\ \texttt{X}_{2}\mapsto x_{2},\
\texttt{X}_{3}\mapsto x_{3},\texttt{X}_{4}\mapsto x_{4}$ the value of
$\texttt{X}_{4}$ at the end of some possible execution (specifically, one in
which the second and the third loop commands both exit immediately) is tightly
(in this case, exactly) described by $x_{2}+x_{3}$; while the other three
variable retain their initial values. Other multi-polynomials will represent
other sets of possible executions, their union covering all executions. This
_disjunctive_ form is important in the context of a compositional analysis. To
see why, suppose that we provide, for a command with variables
$\texttt{X},\texttt{Y}$, the bounds $\langle x,y\rangle$ and $\langle
y,x\rangle$. Then we know that the _sum_ of their values is always bounded by
$x+y$, a result that would have not been deduced had we given the bound
$\max(x,y)$ on each of the variables. The difference may be critical for the
success of analyzing an enclosing or subsequent command.

_Multivariate_ bounds are often of interest, and perhaps require no
justification, but let us point out that multivariate polynomials are
necessary even if we are ultimately interested in a univariate bound, in terms
of some single initial value, say $n$. This is, again, due to the analysis
being compositional. When we analyze an internal command that uses variables
$\texttt{X},\texttt{Y},\dots$ we do not know in what possible contexts the
command will be executed and how the values of these variables will be related
to $n$.

Some highlights of our solution are as follows.

  * •

We reduce the problem of analyzing any core-language program to the problem of
analyzing a single loop, whose body is already processed, and therefore
presented as a collection of abstract state-transitions. This is typical of
algorithms that analyze a structured imperative language and do so
compositionally.

  * •

Since we are computing bounds only up to a constant factor, we work with
_abstract polynomials_ , that have no numeric coefficients.

  * •

We further introduce _$\tau$ -polynomials_, to describe the evolution of
values in a loop. These have an additional parameter $\tau$ (for “time”; more
precisely, number of iterations). Introducing $\tau$-polynomials was a key
step in the solution.

  * •

The analysis of a loop is simply a closure computation under two operations:
ordinary composition, and _generalization_ which is the operation that
predicts the evolution of values by judiciously adding $\tau$’s to
_idempotent_ abstract transitions.

The remainder of this paper is structured as follows. In Section 2 we give
some definitions and state our main result. In Sections 3—5 we present our
algorithm. In Section 6, we give the correctness statement for our algorithm,
and in Section 7 we give the correctness proofs for this. In Section 8 we
consider the computational complexity of our algorithm, and in Section 9 we
consider extensions to our algorithm and open problems. Section 10 describes
related work, and Section 11 concludes and discusses ideas for further work.

##  2\. Preliminaries

In this section, we give some basic definitions, complete the presentation of
our programming language and precisely state the main result.

###  2.1. Some notation and terminology

##### The language

We remark that in our language syntax there is no special form for a “program
unit;” in the text we sometimes use “program” for the subject of our analysis,
yet syntactically it is just a command.

##### Polynomials and multi-polynomials

We work throughout this article with multivariate polynomials in
$x_{1},\dots,x_{n}$ that have non-negative integer coefficients and no
variables other than $x_{1},\dots,x_{n}$; when we speak of a polynomial we
always mean one of this kind. Note that over the non-negative integers, such
polynomials are monotonically (weakly) increasing in all variables. Our
algorithm sometimes deals with monomials, and the reader may assume that a
polynomial is always represented as a non-redundant set of monomials (i.e.,
$p(x)=2x$ is never represented as $x+x$ or $2x+0x^{2}$).

The post-fix substitution operator $[a/b]$ may be applied to any sort of
expression containing a variable $b$, to substitute $a$ instead; e.g.,
$(x^{2}+yx+y)[2z/y]=x^{2}+2zx+2z$.

When discussing a command, state-transition, or program trace, with a variable
$\texttt{X}_{i}$, $x_{i}$ will denote, as a rule, the initial value of this
variable, and $x^{\prime}_{i}$ its final value. Thus we distinguish the
syntactic entity by the typewriter font.

The parameter $n$ always refers to the number of variables in the subject
program. The set $[n]$ is $\\{1,\dots,n\\}$. For a set $S$ an $n$-tuple over
$S$ is a mapping from $[n]$ to $S$. The set of these tuples is denoted by
$S^{n}$. Throughout the paper, various natural liftings of operators to
collections of objects are used, e.g., if $S$ is a set of integers then $S+1$
is the set $\\{s+1\mid s\in S\\}$ and $S+S$ is $\\{s+t\mid s,t\in S\\}$. We
use such lifting with sets as well as with tuples. If $S$ is ordered, we
extend the ordering to $S^{n}$ by comparing tuples element-wise (this leads to
a partial order, in general, e.g., with natural numbers, $\langle 1,3\rangle$
and $\langle 2,2\rangle$ are incomparable).

A function of the form
$\langle{{\mathbf{p}}}[1],\dots,{{\mathbf{p}}}[n]\rangle$, i.e., an $n$-tuple
of polynomials, is called _a multi-polynomial (MP)_. We denote by MPol the set
of multi-polynomials, namely ${(\mathbb{N}[{\mathbf{x}}])}^{n}$,where the
number of variables $n$ is fixed by context.

A _polynomial transition (PT)_ is a computation that transforms an initial
state ${\mathbf{x}}=\langle x_{1},\dots,x_{n}\rangle$ to a new state
${{\mathbf{x}}}^{\prime}=\langle
x^{\prime}_{1},\dots,x^{\prime}_{n}\rangle={{\mathbf{p}}}({{\mathbf{x}}})$
where ${\mathbf{p}}\in{\texttt{MPol}}$.

The distinction between a MP and a PT is perhaps a bit philosophical: An MP is
a function: a mathematical object that exists independently of computation. A
PT is a computation whose effect is described by such a function. We can say,
for example, that the command $\texttt{X}_{2}\verb/:= X/_{2}+\texttt{X}_{1}$
performs a PT. Its associated MP is $\langle x_{1},x_{2}+x_{1}\rangle$.

Various operations will be applied to MPs, mostly obvious—in particular,
composition (which corresponds to sequential application of the transitions).
Note that composition of multi-polynomials,
${{\mathbf{q}}}\circ{{\mathbf{p}}}$, is naturally defined since ${\mathbf{p}}$
supplies $n$ values for the $n$ variables of ${\mathbf{q}}$, and we have:
$({{\mathbf{p}}}\circ{{\mathbf{q}}})[i]={{\mathbf{p}}}[i]\circ{{\mathbf{q}}}$.
We define $\mathit{Id}$ to be the identity transformation,
${{\mathbf{x}}}^{\prime}={{\mathbf{x}}}$ (in MP notation:
${{\mathbf{p}}}[i]=x_{i}$ for $i=1,\dots,n$).

###  2.2. Formal semantics of the core language

The semantics associates with every command `C` over variables
$\texttt{X}_{1},\dots,\texttt{X}_{n}$ a relation $\mbox{\mbox{$[[$}{\tt
C}\mbox{$]]$}}\subseteq\mathbb{N}^{n}\times\mathbb{N}^{n}$. In the expression
${\mathbf{x}}\mbox{\mbox{$[[$}{\tt C}\mbox{$]]$}}{\mathbf{y}}$, vector
${\mathbf{x}}$ (respectively ${\mathbf{y}}$) is the state before (after) the
execution of `C`.

The semantics of skip is the identity. The semantics of an assignment
$\texttt{X}_{i}\verb+:=E+$ associates to each state ${\mathbf{x}}$ a new state
${\mathbf{y}}$ obtained by replacing the component $x_{i}$ by the value of the
expression `E` when evaluated over state ${\mathbf{x}}$. This is defined in
the natural way (details omitted), and is denoted by $\mbox{\mbox{$[[$}{\tt
E}\mbox{$]]$}}{{\mathbf{x}}}$. Composite commands are described by the
straightforward equations:

$\displaystyle\mbox{$[[$}{\tt C}_{1}{\tt;C}_{2}\mbox{$]]$}$ $\displaystyle=$
$\displaystyle\mbox{\mbox{$[[$}{\tt
C${}_{2}$}\mbox{$]]$}}\circ\mbox{\mbox{$[[$}{\tt C${}_{1}$}\mbox{$]]$}}$
$\displaystyle\mbox{$[[$}\verb+choose C+_{1}\verb+ or C+_{2}\mbox{$]]$}$
$\displaystyle=$ $\displaystyle\mbox{\mbox{$[[$}{\tt
C${}_{1}$}\mbox{$]]$}}\cup\mbox{\mbox{$[[$}{\tt C${}_{2}$}\mbox{$]]$}}$
$\displaystyle\mbox{$[[$}\verb+loop E {C}+\mbox{$]]$}$ $\displaystyle=$
$\displaystyle\\{({\mathbf{x}},{\mathbf{y}})\mid\exists
i\leq\mbox{\mbox{$[[$}{\tt
E}\mbox{$]]$}}{{\mathbf{x}}}:{\mathbf{x}}\mbox{\mbox{$[[$}{\tt
C}\mbox{$]]$}}^{i}{\mathbf{y}}\\}$

where $\mbox{\mbox{$[[$}{\tt C}\mbox{$]]$}}^{i}$ represents
$\mbox{\mbox{$[[$}{\tt C}\mbox{$]]$}}\circ\cdots\circ\mbox{\mbox{$[[$}{\tt
C}\mbox{$]]$}}$ (with $i$ occurrences of $[[$C$]]$); and
$\mbox{\mbox{$[[$}{\tt C}\mbox{$]]$}}^{0}=\mathit{Id}$.

##### Remarks

The following two changes may enhance the applicability of the core language
for simulating concrete programs; we include them as “options” because they do
not affect the validity of our proofs.

  1. (1)

The semantics of an assignment operation may be non-deterministic: `X := E`
assigns to X some non-negative value _bounded_ by E. This is useful to
abstract expressions which are not in the core language, and also to use the
results of size analysis of subprograms. Such an analysis may determine
invariants such as “the value of `f(X,Y)` is at most the sum of X and Y.” The
reason that this change does not affect our results is that we work
exclusively with monotone increasing functions. This assignment semantics is
called _a lossy assignment_ in [BAK12], due to an analogy with lossy counter
machines [May03].

  2. (2)

The domain of the integer variables may be extended to $\mathbb{Z}$. In this
case the bounds that we seek are on the absolute value of the output in terms
of absolute values of the inputs. This change does not affect our conclusions
because of the facts $|xy|=|x|\cdot|y|$ and $|x+y|\leq|x|+|y|$. The semantics
of the loop command may be defined either as doing nothing if the loop bound
is not positive, or using the absolute value as a bound.

###  2.3. Detailed statement of the main result

The _polynomial-bound analysis problem_ is to find, for any given command,
which output variables are bounded by a polynomial in the input values (which
are simply the values of all variables upon commencement of the program), and
to bound these output values tightly (up to constant factors). The problem of
_identifying_ the polynomially-bounded variables is completely solved by
[BJK08]. We rely on that algorithm, which is polynomial-time, for doing this
classification (as further explained in Section 4). Our main result is thus
stated as follows.

######  Theorem 1.

There is an algorithm which, for a command `C`, over variables
$\texttt{X}_{1}$ through $\texttt{X}_{n}$, outputs a set $\mathcal{B}$ of
multi-polynomials, such that the following hold, where PB is the set of
indices $i$ of variables $\texttt{X}_{i}$ whose final value under $[[$C$]]$ is
polynomially bounded.

  1. (1)

(Bounding) There is a constant $c_{{\mathbf{p}}}$ associated with each
${{\mathbf{p}}}\in\mathcal{B}$, such that

$\forall{\mathbf{x}},{\mathbf{y}}\ .\ {\mathbf{x}}\mbox{\mbox{$[[$}{\tt
C}\mbox{$]]$}}{\mathbf{y}}\Longrightarrow\exists{{\mathbf{p}}}\in\mathcal{B}\,.\forall
i\in{\texttt{PB}}\,.\,y_{i}\leq
c_{{\mathbf{p}}}{{\mathbf{p}}}[i]({\mathbf{x}})$

  2. (2)

(Tightness) For every ${{\mathbf{p}}}\in\mathcal{B}$ there are constants
$d_{{\mathbf{p}}}>0$, ${{\mathbf{x}}}_{0}$ such that for all
${{\mathbf{x}}}\geq{{\mathbf{x}}}_{0}$ there is a ${\mathbf{y}}$ such that

${\mathbf{x}}\mbox{\mbox{$[[$}{\tt C}\mbox{$]]$}}{\mathbf{y}}\text{ and
}\forall i\in{\texttt{PB}}\,.\,y_{i}\geq
d_{{\mathbf{p}}}{{\mathbf{p}}}[i]({\mathbf{x}})$

A remark regarding the decision to provide bounds only up to constant factors:
based on the proof, the algorithm could be extended to explicitly generate the
coefficients $c_{{\mathbf{p}}}$ and $d_{{\mathbf{p}}}$ in the above statement;
but ignoring constant factors simplifies the algorithm significantly. In
essence, all the considerations regarding constants are removed from the
algorithm to the proofs. Moreover, methodically, our goal was to show that in
the sense that we consider (i.e., “big Theta” bounds), the problem could be
solved _completely_. We do not attempt to completely solve the problem of
computing bounds with the utmost precise constants. We assume that readers
with a Computer Science background are aware of the ubiquity of “big Theta”
bounds in the analysis of algorithms and dispense with a discussion of
justifications for using them.

##### A comment on counters

As discussed in the introduction, various _countable resource problems_ , such
as bounding the number of program steps, may be reduced to the bound analysis
problem. We’d like to point out that the reduction, by introducing a variable
to count the events of interest, may be carried out in our core language,
despite the lack of explicit constants. It suffices to reserve a dedicated
variable, say U, to represent a unit of the resource. Then, we advance the
counter by adding U, and its worst-case bound will equal the worst-case bound
of the resource, times U. As an example, Figure 3 shows how the program from
Figure 2 could be instrumented for computing its time complexity. We use a
fresh variable $\texttt{X}_{5}$ as a “unit” and another one $\texttt{X}_{6}$
to count the steps. The algorithm will deduce that the final value of
$\texttt{X}_{6}$, $x_{6}^{\prime}$, is tightly bounded by
$(x_{2}+x_{3}+x_{1}^{3}+x_{1}x_{4})x_{5}$. Erasing the $x_{5}$ factor we
obtain a tight bound on the unit-cost time.

loop X1 X6 := X6 \+ X5; loop X2 \+ X3 { X6 := X6 \+ X5; choose { X3:= X1; X2:=
X4 } or { X3:= X4; X2:= X1 } }; X4:= X2 \+ X3};loop X4 { X6 := X6 \+ X5;
choose { X3:= X1 \+ X2 \+ X3 } or { X3:= X2; X2:= X1 } }

Figure 3. An instrumented core-language program.

##  3\. Analysis Algorithm: First Concepts

The following sections describe our analysis algorithm. Naturally, the most
intricate part of the analysis concerns loops. In fact we break the
description into stages: first we reduce the problem of analyzing any program
to that of analyzing _simple disjunctive loops_ , defined next. Then, we
approach the analysis of such loops, which is the main effort in this work.

A _simple disjunctive loop (SDL)_ is a finite set $\mathcal{S}$ of polynomial
transitions. The loop is “disjunctive” because its meaning is that in every
iteration, any of the given transitions may be chosen. A SDL does not specify
the number of iterations; our analysis generates polynomials that depend on
the number of iterations as well as the initial state. For this purpose, we
now introduce $\tau$-polynomials where $\tau$ represents the number of
iterations. $\tau$-polynomials are polynomials in $x_{1},\dots,x_{n}$ and
$\tau$. If $p$ is a $\tau$-polynomial, then $p(v_{1},\dots,v_{n})$ is the
result of substituting each $v_{i}$ for the respective $x_{i}$; and we also
write $p(v_{1},\dots,v_{n},t)$ for the result of substituting $t$ for $\tau$
as well. The set of $\tau$-polynomials in $n$ variables ($n$ known from
context) is denoted $\tau$Pol.

Multi-polynomials and polynomial transitions are formed from
$\tau$-polynomials just as previously defined and are used to represent the
effect of a variable number of iterations. For example, the $\tau$-polynomial
transition $\langle x^{\prime}_{1},x^{\prime}_{2}\rangle=\langle x_{1},\
x_{2}+\tau x_{1}\rangle$ represents the effect of repeating ($\tau$ times) the
assignment $\texttt{X}_{2}\verb/:= X/_{2}+\texttt{X}_{1}$. The effect of
iterating the composite command $\texttt{X}_{2}\verb/:=
X/_{2}+\texttt{X}_{1}\verb/; X/_{3}\verb/:= X/_{3}+\texttt{X}_{2}$ is
described by ${{\mathbf{x}}}^{\prime}=\langle x_{1},\ x_{2}+\tau x_{1},\
x_{3}+\tau x_{2}+\tau^{2}x_{1}\rangle$ (here we already have an upper bound
which is not reached precisely, but is correct up to a constant factor).

We denote the set of $\tau$-polynomial transitions by $\tau$MPol. Note that
$\tau$ has a special status: as it does not represent a program variable,
there is no component in the multi-polynomial for giving its value. We should
note that composition ${{\mathbf{q}}}\circ{{\mathbf{p}}}$ over $\tau$MPol is
performed by substituting ${{\mathbf{p}}}[i]$ for each occurrence of $x_{i}$
in ${\mathbf{q}}$. Occurrences of $\tau$ are unaffected (since $\tau$ is not
part of the state).

##  4\. Reduction to Simple Disjunctive Loops

We show how to reduce the problem of analysing core-language programs to the
analysis of simple disjunctive loops.

###  4.1. Symbolic evaluation of straight-line code

Straight-line code consists of atomic commands—namely assignments (or skip,
equivalent to $\texttt{X}_{1}\texttt{:=}\,\texttt{X}_{1}$), composed
sequentially. It is obvious that symbolic evaluation of such code leads to
polynomial transitions.

Consider the following command:

$\texttt{X}_{2}\verb/:= X/_{1}\verb/; X/_{4}\verb/:= X/_{2}\verb/ +
X/_{3}\verb/; X/_{1}\verb/:= X/_{2}\verb/ * X/_{3}$

This is precisely represented by the transition $\langle
x_{1},x_{2},x_{3},x_{4}\rangle^{\prime}=\langle x_{1}x_{3},\ x_{1},\ x_{3},\
x_{1}+x_{3}\rangle$.

###  4.2. Evaluation of non-deterministic choice

Evaluation of the command

$\texttt{choose}\;\texttt{C}_{1}\;\texttt{or}\;\texttt{C}_{2}$

yields a set of possible outcomes. Hence, the result of analyzing a command
will be a _set_ of multi-polynomial transitions. We express this in the common
notation of abstract semantics:

${\mbox{\mbox{$[[$}{\tt C}\mbox{$]]$}}}^{S}\in\wp({\texttt{MPol}})\,.$

For uniformity, we consider $\mbox{\mbox{$[[$}{\tt C}\mbox{$]]$}}^{S}$ for an
atomic command to be a singleton in $\wp({\texttt{MPol}})$. Composition is
naturally extended to sets, and the semantics of a choice command is now
simply set union, so we have:

$\displaystyle\mbox{$[[$}{\tt C}_{1}{\tt;C}_{2}\mbox{$]]$}^{S}$
$\displaystyle=$ $\displaystyle\mbox{\mbox{$[[$}{\tt
C${}_{2}$}\mbox{$]]$}}^{S}\circ\mbox{\mbox{$[[$}{\tt
C${}_{1}$}\mbox{$]]$}}^{S}$ $\displaystyle\mbox{$[[$}\verb+choose C+_{1}\verb+
or C+_{2}\mbox{$]]$}^{S}$ $\displaystyle=$ $\displaystyle\mbox{\mbox{$[[$}{\tt
C${}_{1}$}\mbox{$]]$}}^{S}\cup\mbox{\mbox{$[[$}{\tt
C${}_{2}$}\mbox{$]]$}}^{S}$

Consider the following command:

$\texttt{X}_{2}\texttt{:= X}_{1}\texttt{; choose \\{ X}_{4}\texttt{:=
X}_{2}\texttt{ + X}_{3}\texttt{ \\} or \\{ X}_{1}\texttt{:= X}_{2}\texttt{*
X}_{3}\texttt{ \\}}$

This is represented by the set $\\{\langle
x_{1},x_{1},x_{3},x_{1}+x_{3}\rangle,\langle
x_{1}x_{3},x_{1},x_{3},x_{4}\rangle\\}$.

###  4.3. Handling loops

The above shows that any loop-free command in our language can be _precisely_
represented by a finite set of MPs, that is, its semantics $[[$C$]]$ equals
the union of a finite number of PTs, which we can compute by symbolic
evaluation. Consequently, the problem of analyzing any loop command is reduced
to the analysis of simple disjunctive loops, by first analyzing the loop body.
The goal of the loop analysis is to produce a set of multi-polynomials that
provide tight worst-case bounds on the results of any number of iterations of
the loop body—“tight” in the sense of Theorem 1 (see also Example 4.3 below).
We will refer to this, concisely, as _solving_ the loop.

Suppose that we have an algorithm Solve that takes a simple disjunctive loop
and computes tight bounds for its results, with explicit dependence on the
number of iterations using the parameter $\tau$. We use it to complete the
analysis of any program by the following definition:

$\displaystyle\mbox{$[[$}\verb+loop E {C}+\mbox{$]]$}^{S}$ $\displaystyle=$
$\displaystyle(\textsc{Solve}(\mbox{\mbox{$[[$}{\tt
C}\mbox{$]]$}}^{S}))[\mbox{\mbox{$[[$}{\tt E}\mbox{$]]$}}/\tau]\ .$

Thus, the whole solution is constructed as an ordinary abstract
interpretation, following the semantics of the language, except for what
happens inside Solve, which is the subtle part of the algorithm; this
procedure accepts a set of multi-polynomials, describing the body of the loop,
and generates a set of $\tau$-MPs that finitely describes the result of all
execution sequences of the loop, thanks to a _generalization_ procedure that
captures the dependence of results on the iteration count by means of the
parameter $\tau$. After completing this procedure, we replace $\tau$ with the
expression $[[$E$]]$, which gives the actual loop bound as a polynomial in
$x_{1},\dots,x_{n}$.

Consider the following command:

$\texttt{X}_{4}\texttt{:= X}_{1}\texttt{; loop X}_{4}\texttt{ \\{
X}_{2}\texttt{:= X}_{1}\texttt{ + X}_{2}\texttt{; X}_{3}\texttt{:=
X}_{2}\texttt{\\}}$

Solving just the loop yields the set $\mathcal{L}=\\{\langle
x_{1},x_{2},x_{3},x_{4}\rangle$, $\langle x_{1},x_{2}+\tau x_{1},x_{2}+\tau
x_{1},x_{4}\rangle\\}$ (the first MP accounts for zero iterations, the second
covers any positive number of iterations). We can now compute the effect of
the given command as:

$\displaystyle{\mathcal{L}}[x_{4}/\tau]\circ\mbox{\mbox{$[[$}{\tt X${}_{4}$ :=
X${}_{1}$}\mbox{$]]$}}^{S}$
$\displaystyle={\mathcal{L}}[x_{4}/\tau]\circ\\{\langle
x_{1},x_{2},x_{3},x_{1}\rangle\\}$ $\displaystyle=\\{\langle
x_{1},x_{2},x_{3},x_{1}\rangle,\langle
x_{1},x_{2}+x_{1}^{2},x_{2}+x_{1}^{2},x_{1}\rangle\\}.$

We can now demonstrate that the analysis of a loop may involve approximation.
Suppose that we slightly modify the code as follows:

$\texttt{X}_{4}\texttt{:= X}_{1}\texttt{; loop X}_{4}\texttt{ \\{
X}_{3}\texttt{:= X}_{2}\texttt{; X}_{2}\texttt{:= X}_{1}\texttt{ +
X}_{2}\texttt{\\}}$

Our algorithm will produce the same MPs, although a careful examination shows
that the precise result of the loop (when it executes $x_{1}>0$ iterations) is
now given by $\langle
x_{1},x_{2}+x_{1}^{2},x_{2}+x_{1}(x_{1}-1),x_{1}\rangle$. This expression is
not a MP (since we only consider polynomials with non-negative coefficients),
but is tightly approximated by the MP we produced, as
$x_{1}(x_{1}-1)=\Theta(x_{1}^{2})$. The precise statement of what it means to
tightly approximate all possible results of a program by a finite set of MPs
is the essence of Theorem 1.

The next section describes the procedure Solve, and operates under the
assumption that all variables are polynomially bounded in the loop. However, a
loop can generate exponential growth. To cover this eventuality, we first
apply the algorithm of [BJK08] that identifies which variables are
polynomially bounded. If some $\texttt{X}_{i}$ is _not_ polynomially bounded
we replace the $i$th component of all the loop transitions with $x_{n}$ (we
assume $x_{n}$ to be a dedicated, unmodified variable). Clearly, after this
change, all variables are polynomially bounded; moreover, variables which are
genuinely polynomial are unaffected, because they cannot depend on a super-
polynomial quantity (given the restricted arithmetics in our language). In
reporting the results of the algorithm, we should display “super-polynomial”
instead of any expression that includes $x_{n}$.

##  5\. Simple Disjunctive Loop Analysis Algorithm

Intuitively, evaluating $\verb/loop E {C}/$ abstractly consists of simulating
any finite number of iterations, i.e., computing

$Q_{i}=\\{\mathit{Id}\\}\cup P\cup(P\circ P)\cup\dots\cup{P}^{(i)}$ (1)

where $P=\mbox{\mbox{$[[$}{\tt C}\mbox{$]]$}}^{S}\in\wp({\texttt{MPol}})$. The
question now is whether the sequence (1) reaches a fixed point. In fact, it
often doesn’t. However, it is quite easy to see that in the _multiplicative
fragment_ of the language, that is, where the addition operator is not used,
such non-convergence is associated with exponential growth. Indeed, since
there is no addition, all our polynomials are monomials with a leading
coefficient of 1 (_monic monomials_)—this is easy to verify. It follows that
if the sequence (1) does not converge, higher and higher exponents must
appear, which indicates that some variable cannot be bounded polynomially.
Taking the contrapositive, we conclude that if all variables are known to be
polynomially bounded the sequence will converge. Thus we have the following
easy (and not so satisfying) result:

For a SDL $P$ that does not use addition, the sequence $Q_{i}$ as in (1)
reaches a fixed point, and the fixed point provides tight bounds for all the
polynomially-bounded variables.

The following loop is in the multiplicative fragment, and has no exponential
behaviour:

$\verb/loop X/_{3}\verb/ { X/_{1}\verb/:= X/_{2}\verb/ * X/_{2}\verb/;
X/_{2}\verb/:= X/_{3}\verb/ }/$

The effect of an iteration is given by the multi-polynomial
${{\mathbf{p}}}=\langle x_{2}^{2},\ x_{3},\ x_{3}\rangle$. Let
$P=\\{{{\mathbf{p}}}\\}$. The accumulating effect of the loop is given by the
union of:

$\displaystyle\\{$ $\displaystyle\mathit{Id}\\}$ $\displaystyle P$
$\displaystyle=\\{\langle x_{2}^{2},\ x_{3},\ x_{3}\rangle\\}$ $\displaystyle
P\circ P$ $\displaystyle=\\{\langle x_{3}^{2},\ x_{3},\ x_{3}\rangle\\}$
$\displaystyle P^{(3)}$ $\displaystyle=P^{(2)}$ $\displaystyle\dots$

That is, the results are completely characterized by the three MPs above.

When we have addition, we find that knowing that all variables are
polynomially bounded does not imply convergence of the sequence (1). An
example is $\texttt{loop X}_{3}\texttt{ \\{ X}_{1}\texttt{:= X}_{1}\texttt{ +
X}_{2}\texttt{ \\}}$ yielding the infinite sequence of MPs $\langle
x_{1},x_{2},x_{3}\rangle$, $\langle x_{1}+x_{2},x_{2},x_{3}\rangle$, $\langle
x_{1}+2x_{2},x_{2},x_{3}\rangle$, … Our solution employs two means. One is the
introduction of $\tau$-polynomials, already presented. The other is a kind of
_abstraction_ —intuitively, ignoring the concrete values of (non-zero)
coefficients. Let us first define this abstraction:

APol, the set of abstract polynomials, consists of formal sums of distinct
monomials over $x_{1},\dots,x_{n}$, where the coefficient of every monomial
included is $1$. We extend the definition to an abstraction of
$\tau$-polynomials, denoted $\tau$APol.

The meaning of abstract polynomials is given by the following rules:

  1. (1)

The abstraction of a polynomial $p$, $\alpha(p)$, is obtained by modifying all
(non-zero) coefficients to 1.

  2. (2)

Addition and multiplication in $\tau$APol are defined in a natural way so that
$\alpha(p)+\alpha(q)=\alpha(p+q)$ and $\alpha(p)\cdot\alpha(q)=\alpha(p\cdot
q)$ (to carry these operations out, you just go through the motions of adding
or multiplying ordinary polynomials, ignoring the coefficient values).

  3. (3)

The _canonical concretization_ of an abstract polynomial,
$\gamma({{\mathbf{p}}})$ is obtained by simply regarding it as an ordinary
polynomial.

  4. (4)

These definitions extend to tuples of (abstract) polynomials in the natural
way.

  5. (5)

The set of abstract multi-polynomials AMPol and their extension with $\tau$
($\tau$AMPol) are defined as $n$-tuples over APol (respectively, $\tau$APol).
We use AMP as an abbreviation for abstract multi-polynomial.

  6. (6)

Composition ${{\mathbf{p}}}\mathop{\bullet}{{\mathbf{q}}}$, for
${{\mathbf{p}}},{{\mathbf{q}}}\in{\texttt{AMPol}}$ (or $\tau$AMPol) is defined
as $\alpha(\gamma({{\mathbf{p}}})\circ\gamma({{\mathbf{q}}}))$; it is easy to
see that one can perform the calculation without the detour through
polynomials with coefficients. The different operator symbol
(“$\mathop{\bullet}$” versus “$\circ$”) helps in disambiguating expressions.

An abstract polynomial can be reduced by deleting dominated monomials (e.g.,
$x^{2}+x\to x^{2}$); which clearly preserves its meaning when viewed in “big
Theta” terms. We expect that the combinatorial explosion in the algorithm can
be attenuated by reducing every abstract polynomial, but in this paper, we
ignore this optimization to alleviate the description and proof of the
algorithm. Another useful optimization (which we also ignore in our analysis)
is to delete dominated _multi-polynomials_ in a set of MPs.

##### Analysing a SDL

To analyse a SDL specified by a set of MPs $\mathcal{S}$, we start by
computing $\alpha(\mathcal{S})$. The rest of the algorithm computes within
$\tau$AMPol. We define two operations that are combined in the analysis of
loops. The first, which we call _closure_ , is simply the fixed point of
accumulated iterations as in the multiplicative case. It is introduced by the
following two definitions.

[iterated composition] Let ${\mathbf{t}}$ be any abstract $\tau$-MP. We define
${{\mathbf{t}}}^{\mathop{\bullet}(k)}$, for $k\geq 0$, by:

$\displaystyle{{\mathbf{t}}}^{\mathop{\bullet}(0)}$
$\displaystyle=\mathit{Id}$
$\displaystyle{{\mathbf{t}}}^{\mathop{\bullet}(k+1)}$
$\displaystyle={{\mathbf{t}}}\mathop{\bullet}{{\mathbf{t}}}^{\mathop{\bullet}(k)}.$

For a set $\mathcal{T}$ of abstract $\tau$-MPs, we define, for $k\geq 0$:

$\displaystyle\mathcal{T}^{\mathop{\bullet}(0)}$
$\displaystyle=\\{\mathit{Id}\\}$
$\displaystyle\mathcal{T}^{\mathop{\bullet}(k+1)}$
$\displaystyle=\mathcal{T}^{\mathop{\bullet}(k)}\cup\
\bigcup_{{\mathbf{q}}\in\mathcal{T},\
{\mathbf{p}}\in\mathcal{T}^{\mathop{\bullet}(k)}}{{\mathbf{q}}}\mathop{\bullet}{{\mathbf{p}}}\,.$

Note that
${{\mathbf{t}}}^{\mathop{\bullet}(k)}=\alpha({\gamma({\mathbf{t}})}^{(k)})$,
where ${{\mathbf{p}}}^{(k)}$ is defined using ordinary composition.

Let ${\mathbf{p}}=\langle x_{1},x_{1}+x_{2}\rangle$; clearly its $k$th iterate
(for $k\geq 1$) is ${{\mathbf{p}}}^{(k)}=\langle x_{1},x_{1}+kx_{2}\rangle$.
However, with abstract polynomials, we get
${\alpha({{\mathbf{p}}})}^{\mathop{\bullet}(k)}=\langle
x_{1},x_{1}+x_{2}\rangle$; the growth in the coefficient is abstracted away.
Similarly, we have
${\\{\alpha({\mathbf{p}})\\}}^{\mathop{\bullet}(k)}=\\{\mathit{Id},\alpha({{\mathbf{p}}})\\}$
for all $k\geq 1$.

[abstract closure] For finite $P\subset{\texttt{$\tau$AMPol}}$, we define:

${Cl(P)}=\bigcup_{i=0}^{\infty}P^{\mathop{\bullet}(i)}\,.$

In the correctness proof, we argue that when all variables are polynomially
bounded in a loop $\mathcal{S}$, the closure of $\alpha(\mathcal{S})$ can be
computed in finite time; equivalently, it equals
$\bigcup_{i=0}^{k}{(\alpha({\mathcal{S}}))}^{\mathop{\bullet}(i)}$ for some
$k$. The argument for finiteness is essentially the same as in the
multiplicative case.

The second operation is called _generalization_ and its role is to capture the
behaviour of accumulator variables, meaning variables that grow by
accumulating increments in the loop, and make explicit the dependence on the
number of iterations. The identification of which additive terms in a MP
should be considered as increments that accumulate is at the heart of our
problem.

Consider the following loop:

$\texttt{loop \ldots\ \\{ X}_{1}\texttt{:= X}_{1}\texttt{ + X}_{3}\texttt{;
X}_{2}\texttt{:= X}_{2}\texttt{ + X}_{3}\texttt{ + X}_{4}\texttt{;
X}_{4}\texttt{:= X}_{3}\texttt{\\}}$

We have omitted the loop bound in order to emphasize that we are now analyzing
the _growth of values as the loop progresses_ rather than its final result.
The generalization construction below introduces $\tau$’s into the AMPs,
obtained from the loop body, in order to express this growth in terms of the
number of iterations. Informally, consider the assignment to $\texttt{X}_{1}$:
it adds $x_{3}$ (the initial value of variable $\texttt{X}_{3}$), and does so
on every iteration: so we have an arithmetic series with an increment of
$x_{3}$. After $\tau$ iterations, $\texttt{X}_{1}$ will have grown by $\tau
x_{3}$. The assignment to $\texttt{X}_{2}$ similarly adds the values of two
other variables, $\texttt{X}_{3}$ and $\texttt{X}_{4}$, but as
$\texttt{X}_{4}$ is rewritten with $x_{3}$ already at the end of the first
iteration, subsequent iterations add $2x_{3}$ (not $x_{3}+x_{4}$). This will
be expressed by introducing the term $\tau x_{3}$ (the coefficient 2 is
abstracted away). We return to this example, and the issue it illustrates,
further below.

The definition of ${{\mathbf{p}}}^{\tau}$ will is greatly simplified by
concentrating on idempotent AMPs, defined next. We will later give an example
that shows that our definition does not work for AMPs which are not
idempotent; while the fact that a complete solution can be obtained by
generalizing only idempotent elements comes out of a Ramsey-like property of
finite monoids [Sim90], as will be seen in Section 7.2.

${\mathbf{p}}\in{\texttt{$\tau$AMPol}}$ is called _idempotent_ if
${\mathbf{p}}\mathop{\bullet}{\mathbf{p}}={\mathbf{p}}$. Note that this is
composition in the abstract domain. So, for instance, $\langle
x_{1},x_{2}\rangle$ is idempotent, and so is $\langle
x_{1}+x_{2},x_{2}\rangle$, while $\langle x_{1}x_{2},x_{2}\rangle$ and
$\langle x_{1}+x_{2},x_{1}\rangle$ are not.

For ${\mathbf{p}}$ an (abstract) multi-polynomial, we say that $x_{i}$ is
_self-dependent_ in ${\mathbf{p}}$ if ${\mathbf{p}}[i]$ depends on $x_{i}$. We
also say that the entry ${\mathbf{p}}[i]$ is self-dependent; the choice of
term depends on context and the meaning should be clear either way. We call a
monomial self-dependent if all the variables appearing in it are. We denote by
${{\textsc{SD}}({\mathbf{p}})}$ the set $\\{i\,:\,x_{i}\text{ is self-
dependent in }{\mathbf{p}}\\}$.

We later show that in polynomially-bounded loops, if $x_{i}$ is self-dependent
then ${\mathbf{p}}[i]$ must include the monomial $x_{i}$. To illustrate the
significance of self-dependent monomials, let us consider an example where
${{\mathbf{p}}}[1]=x_{1}+\dots$ and ${{\mathbf{p}}}[2]=x_{2}+\dots$, and
further ${{\mathbf{p}}}[3]=x_{1}x_{2}+\dots$. Then the monomial $x_{1}x_{2}$
reappears in every iterate ${{\mathbf{p}}}^{\mathop{\bullet}(k)}$. This is
because all the variables in it are self-dependent.

We define a notational convention for $\tau$-MPs, specifically for self-
dependent entries of the MP. Assuming that $x_{i}$ appears in
${{\mathbf{p}}}[i]$, we write:

${{\mathbf{p}}}[i]=x_{i}+\tau{{\mathbf{p}}}[i]^{\prime}+{{\mathbf{p}}}[i]^{\prime\prime}+{{\mathbf{p}}}[i]^{\prime\prime\prime}\,,$

where ${{\mathbf{p}}}[i]^{\prime\prime\prime}$ includes all the non-self-
dependent monomials of ${{\mathbf{p}}}[i]$, while the self-dependent monomials
(other than $x_{i}$) are grouped into two sums:
$\tau{{\mathbf{p}}}[i]^{\prime}$, including all monomials with a positive
degree of $\tau$, and ${{\mathbf{p}}}[i]^{\prime\prime}$ which includes all
the $\tau$-free monomials.

Let ${\mathbf{p}}=\langle x_{1}+\tau x_{2}+\tau x_{3}+x_{3}x_{4},\ x_{3},\
x_{3},\ x_{4}\rangle$. Then ${{\textsc{SD}}({\mathbf{p}})}=\\{1,3,4\\}$. Since
$x_{1}$ is self-dependent, we will apply the above definition to
${{\mathbf{p}}}[1]$, so that ${{\mathbf{p}}}[1]^{\prime}=x_{3}$,
${{\mathbf{p}}}[1]^{\prime\prime}=x_{3}x_{4}$ and
${{\mathbf{p}}}[1]^{\prime\prime\prime}=\tau x_{2}$. Note that a factor of
$\tau$ is stripped in ${{\mathbf{p}}}[1]^{\prime}$. Had the monomial been
$\tau^{2}x_{3}$, we would have ${{\mathbf{p}}}[1]^{\prime}=\tau x_{3}$.

[generalization] Let ${\mathbf{p}}$ be idempotent in $\tau$AMPol; define
${{\mathbf{p}}}^{\tau}$ by:

${{\mathbf{p}}}^{\tau}[i]=\begin{cases}x_{i}+\tau{{\mathbf{p}}}[i]^{\prime}+\tau{{\mathbf{p}}}[i]^{\prime\prime}+{{\mathbf{p}}}[i]^{\prime\prime\prime}&\text{if
$i\in{{\textsc{SD}}({\mathbf{p}})}$}\\\
{{\mathbf{p}}}[i]&\text{otherwise.}\end{cases}$

Note that the arithmetic here is abstract (see examples below). Note also that
in the term $\tau{{\mathbf{p}}}[i]^{\prime}$ the $\tau$ is already present in
${\mathbf{p}}$, while in $\tau{{\mathbf{p}}}[i]^{\prime\prime}$ it is added to
existing monomials. In this definition, the monomials of
${{\mathbf{p}}}[i]^{\prime\prime\prime}$ are treated like those of
$\tau{{\mathbf{p}}}[i]^{\prime}$; however, in certain steps of the proofs we
will treat them differently, which is why the notation separates them. We next
give a couple of examples, just to illustrate the definition; we later (Page
5) motivate the definition in the context of the loop analysis.

Let ${\mathbf{p}}=\langle x_{1}+x_{3},\ x_{2}+x_{3}+x_{4},\ x_{3},\
x_{3}\rangle$. Note that it corresponds to the loop body from Example 5.
Further note that
${{\mathbf{p}}}\mathop{\bullet}{{\mathbf{p}}}={{\mathbf{p}}}$, i.e.,
${\mathbf{p}}$ is idempotent. We have ${{\mathbf{p}}}^{\tau}=\langle
x_{1}+\tau x_{3},\ x_{2}+\tau x_{3}+x_{4},\ x_{3},\ x_{3}\rangle$.

Let ${\mathbf{p}}=\langle x_{1}+\tau x_{2}+\tau x_{3}+\tau x_{3}x_{4},\
x_{3},\ x_{3},\ x_{4}\rangle$. Note that
${{\mathbf{p}}}\mathop{\bullet}{{\mathbf{p}}}={{\mathbf{p}}}$. The self-
dependent variables are all but $x_{2}$. We have
${{\mathbf{p}}}^{\tau}=\langle x_{1}+\tau x_{2}+\tau x_{3}+\tau x_{3}x_{4},\
x_{3},\ x_{3},\ x_{4}\rangle={{\mathbf{p}}}$.

Finally we can present the analysis of the loop command. Solve$(\mathcal{S})$
Input: $\mathcal{S}$, a polynomially-bounded disjunctive simple loop.
Output: a set of $\tau$-MPs that tightly approximates the effect of $\tau$
iterations of loop $\mathcal{S}$.

  1. (1)

Set $T=\alpha(\mathcal{S})$.

  2. (2)

Repeat the following steps until $T$ remains fixed:

    1. (a)

Closure: Set $T$ to ${Cl(T)}$.

    2. (b)

Generalization: For all ${{\mathbf{p}}}\in T$ such that
${{\mathbf{p}}}\mathop{\bullet}{{\mathbf{p}}}={{\mathbf{p}}}$, add
${{\mathbf{p}}}^{\tau}$ to $T$.

Consider the following loop:

$\texttt{loop \ldots\ \\{ X}_{1}\texttt{:= X}_{1}\texttt{ + X}_{2}\texttt{;
X}_{2}\texttt{:= X}_{2}\texttt{ + X}_{3}\texttt{; X}_{4}\texttt{:=
X}_{3}\texttt{ \\}}$

The body of the loop is evaluated symbolically and yields the multi-
polynomial:

${\mathbf{p}}=\langle x_{1}+x_{2},\ x_{2}+x_{3},\ x_{3},\ x_{3}\rangle$

Now, computing within AMPol,

$\displaystyle{\alpha({{\mathbf{p}}})}^{\mathop{\bullet}(2)}$
$\displaystyle=\alpha({{\mathbf{p}}})\mathop{\bullet}\alpha({{\mathbf{p}}})=\langle
x_{1}+x_{2}+x_{3},\ x_{2}+x_{3},\ x_{3},\ x_{3}\rangle;$
$\displaystyle{\alpha({{\mathbf{p}}})}^{\mathop{\bullet}(3)}$
$\displaystyle={\alpha({{\mathbf{p}}})}^{\mathop{\bullet}(2)}\,.$

Here the closure computation stops. Since
$\alpha({{\mathbf{p}}}^{\mathop{\bullet}(2)})$ is idempotent, we compute

${{\mathbf{q}}}={({\alpha({{\mathbf{p}}})}^{\mathop{\bullet}(2)})}^{\tau}=\langle
x_{1}+\tau x_{2}+\tau x_{3},\ x_{2}+\tau x_{3},\ x_{3},\ x_{3}\rangle$

and applying closure again, we obtain

$\begin{array}[]{ll}{{\mathbf{q}}}\mathop{\bullet}{\alpha({{\mathbf{p}}})}&=\langle
x_{1}+x_{2}+x_{3}+\tau x_{2}+\tau x_{3},\ x_{2}+x_{3}+\tau x_{3},\ x_{3},\
x_{3}\rangle\\\ {({{\mathbf{q}}})}^{\mathop{\bullet}(2)}&=\langle x_{1}+\tau
x_{2}+\tau x_{3}+\tau^{2}x_{3},\ x_{2}+\tau x_{3},\ x_{3},\ x_{3}\rangle\\\
\end{array}$

where the first one simplifies to ${\mathbf{q}}$ by deleting dominated terms,
and the second to $\langle x_{1}+\tau x_{2}+\tau^{2}x_{3},\ x_{2}+\tau x_{3},\
x_{3},\ x_{3}\rangle$. The last element is idempotent but applying
generalization does not generate anything new. Thus the algorithm ends. The
reader may reconsider the source code to verify that we have indeed obtained
tight bounds for the loop.

Note that when a program contains nested loops, innermost loops will be
processed first and result in a set of abstract polynomials, so we might
actually analyze any enclosing commands entirely in the abstract domain. This
means rephrasing our definition of SDL by defining the input set as a set of
AMPs rather than concrete polynomials; then the initial step above, where
$\mathcal{S}$ is abstracted, is skipped. In the forthcoming sections we ignore
this issue and continue to treat the input as being a set of concrete
polynomials; this is for convenience only. It is easy enough to restate the
results such that the input is understood as abstract, but known to tightly
describe the effect of some concrete piece of code.

##### Comments on generalization

The precise definition of the generalization operator has been one of the key
steps in the development of this algorithm (operators which are similar—but
insufficient for our purpose—appear in related work [KA80, KN04, NW06, JK09,
BJK08, BEF+16]). Let us attempt to give some intuition for its definition (not
a correctness proof, yet). Say $x_{i}$ is self-dependent. An important point
is the partition of the terms added to $x_{i}$ into
$\tau{{\mathbf{p}}}[i]^{\prime}$, ${{\mathbf{p}}}[i]^{\prime\prime}$ and
${{\mathbf{p}}}[i]^{\prime\prime\prime}$. To see why the non-self-dependent
monomials ${{\mathbf{p}}}[i]^{\prime\prime\prime}$ are not multiplied by
$\tau$, consider Example 5. Had we been too eager to insert $\tau$’s and do
this to non-self-dependent monomials as well, we would have got:

$\langle x_{1}+\tau x_{3},\ x_{2}+\tau x_{3}+\tau x_{4},\ x_{3},\
x_{3}\rangle\,$

(differing from the correct result in the second component). This would give a
sound, but loose (overestimated) upper bound: as already discussed, when the
transition represented by ${\mathbf{p}}$ is iterated, copies of the initial
value $x_{4}$ do _not_ accumulate. Next, the distinction of
${{\mathbf{p}}}[i]^{\prime\prime}$ from $\tau{{\mathbf{p}}}[i]^{\prime}$
prevents $\tau$’s from being added where they already appear; this is
important because we reapply generalization to results of previous steps while
analyzing a given loop. Finally, an important aspect particular to our
algorithm (compared to the above-cited) is the application of the
generalization operator only to idempotent elements. Again, we can illustrate
with an example that applying it too eagerly (to all AMPs in the closure)
would be incorrect. Consider the following AMP:

${\mathbf{p}}=\langle x_{1}+x_{2}+x_{3}+x_{4},\ x_{3},\ x_{4},\ x_{4}\rangle$

Generalization (incorrectly applied to ${\mathbf{p}}$, since it is not
idempotent) would yield:

$\langle x_{1}+x_{2}+x_{3}+\tau x_{4},\ x_{3},\ x_{4},\ x_{4}\rangle$

This is bad because if ${\mathbf{p}}$ is iterated to accumulate copies of
$x_{4}$ in $\texttt{X}_{1}$ (a behaviour represented by the term $\tau
x_{4}$), the value of $\texttt{X}_{2}$ will no longer be $x_{3}$ (but
$x_{4}$). Hence, this AMP describes a result that is not realizable (and when
we substitute the loop bound for $\tau$, we will get a loose upper bound).

##### A comment on linear bounds

When values accumulate in a loop, a non-linear result is obtained. Stated
contrapositively: linear results do not involve accumulation. Indeed, it is
not hard to verify that if for linear polynomials (only) we maintain precise
numeric coefficients, our algorithm would still converge. Therefore, if we
wish, we can modify our algorithm so that _for linear results we have bounds
in which the coefficients are explicit and precise_. This is not a strong
result as might seem at first, since it is due to the weakness of our
language: linear results can only be built up by a finite number of additions.
Still, if the algorithm is employed as a brick in a larger system, this
property might possibly be useful.

##  6\. Correctness Statement for Simple Disjunctive Loops

We claim that our algorithm obtains a description of the worst-case results of
the program that is precise up to constant factors. That is, we claim that the
set of MPs returned provides a “big O” upper bound (on all executions) which
is also tight; tightness means that every MP returned is also a lower bound
(up to a constant factor) on an infinite sequence of possible executions. The
main, non-trivial part of the algorithm is of course the solution of a simple
disjunctive loop, procedure Solve. Completing this to show correctness for an
arbitrary program is not difficult.

In this section we formulate the _correctness statement for Simple Disjunctive
Loops_ , in other words, we state the contract for procedure Solve, which,
when satisfied, justifies its proper functioning within the whole algorithm.
This formulation forces us to step up the level of detail; specifically, we
introduce _traces_ , to give a more concrete semantics to loops (compared to
Section 2.2).

Let $\mathcal{S}$ be a set of polynomial transitions. An _(abstract) trace_
over $\mathcal{S}$ is a finite sequence
$\sigma={{\mathbf{p}}}_{1};\dots;{{\mathbf{p}}}_{|\sigma|}$ of elements of
$\mathcal{S}$. Thus $|\sigma|$ denotes the _length_ of the trace. The set of
all traces is denoted ${\mathcal{S}}^{*}$. We write
$\mbox{$[[$}{\sigma}\mbox{$]]$}$ for the composed relation
${{\mathbf{p}}}_{|\sigma|}\circ\dots\circ{{\mathbf{p}}}_{1}$ (for the empty
trace, ${\varepsilon}$, we have
$\mbox{$[[$}{{\varepsilon}}\mbox{$]]$}=\mathit{Id}$).

Using the following definition we will be able to give the desired correctness
statement for Solve.

Let $p({\mathbf{x}})$ be a (concrete or abstract) $\tau$-polynomial. We write
$\dot{p}$ for the _linear monomials_ of $p$, namely any one of the form
$ax_{i}$ for a constant coefficient $a$. We write $\ddot{p}$ for the rest.
Thus $p=\dot{p}+\ddot{p}$.

######  Theorem 2 (Solution of disjunctive loop problem).

Given a polynomially-bounded SDL represented as a set $\mathcal{S}$ of MPs,
procedure Solve finds a finite set $\mathcal{B}$ of $\tau$-MPs which _tightly
bound_ all traces over $\mathcal{S}$. More precisely, it guarantees:

  1. (1)

(Bounding) There is a constant $c_{{\mathbf{p}}}>0$ associated with each
${{\mathbf{p}}}\in\mathcal{B}$, such that

$\forall{\mathbf{x}},{\mathbf{y}},\sigma\ .\
{\mathbf{x}}\mbox{$[[$}\sigma\mbox{$]]$}{\mathbf{y}}\Longrightarrow\exists{{\mathbf{p}}}\in\mathcal{B}\,.\,{{\mathbf{y}}}\leq
c_{{\mathbf{p}}}{{\mathbf{p}}}({\mathbf{x}},|\sigma|)$

  2. (2)

(Tightness) For every ${{\mathbf{p}}}\in\mathcal{B}$ there are constants
$d_{{\mathbf{p}}}>0$, ${{\mathbf{x}}}_{0}$ such that for all
${{\mathbf{x}}}\geq{{\mathbf{x}}}_{0}$ there are a trace $\sigma$ and a state
vector ${\mathbf{y}}$ such that

${\mathbf{x}}\mbox{$[[$}\sigma\mbox{$]]$}{\mathbf{y}}\,\land\,{{\mathbf{y}}}\geq\dot{{\mathbf{p}}}({{\mathbf{x}}},|\sigma|)+d_{{\mathbf{p}}}\ddot{{\mathbf{p}}}({{\mathbf{x}}},|\sigma|)\,.$

Note that in the lower-bound clause (2), the linear monomials of $p$ are not
multiplied by the constant $d_{{\mathbf{p}}}$; this sets, in a sense, a
stricter requirement for them: if the trace maps $x$ to $x^{2}$ then the bound
$2x^{2}$ is acceptable, but if it maps $x$ to $x$, the bound $2x$ is not
accepted. The reader may understand this technicality by considering the
effect of iteration: it is important to distinguish the transition
$x^{\prime}_{1}=x_{1}$, which can be iterated ad libitum, from the transition
$x^{\prime}_{1}=2x_{1}$, which produces exponential growth on iteration.
Distinguishing $x^{\prime}_{1}=x_{1}^{2}$ from $x^{\prime}_{1}=2x_{1}^{2}$ is
not as important. We remark that $c_{{\mathbf{p}}},d_{{\mathbf{p}}}$ range
over real numbers. However, our data and the coefficients of polynomials
remain integers, it is only such comparisons that are performed with real
numbers (specifically, to allow $d_{{\mathbf{p}}}$ to be smaller than one; in
the upper bounds, it is possible to stick to integers). Note also that
polynomial boundedness is ensured by our algorithm before applying the
procedure (Section 4.3), so the precondition of the correctness theorem is
satisfied.

##  7\. Correctness Proofs

In this section we prove the correctness of the main, non-trivial part of our
algorithm, namely the solution of a simple disjunctive loop, showing that it
satisfies the requirements set forth in the last section.

##### Overview of the proof

Intuitively, what we want to prove is that the multi-polynomials we compute
cover all “behaviors” of the loop. More precisely, in the upper-bound part of
the proof we want to cover all behaviors: upper-bounding is a universal
statement. To prove that bounds are tight, we show that each such bound
constitutes a _lower bound_ on a certain “worst-case behavior”: tightness is
an existential statement. The main aspects of these proofs are as follows:

  * •

A key notion in our proofs is that of _realizability_. Intuitively, when we
come up with a bound, we want to show that there are traces that achieve
(realize) this bound for arbitrarily large input values.

  * •

In the lower-bound proof, we describe a set of traces by a _pattern_. A
pattern is constructed like a regular expression with concatenation and
Kleene-star. However, they allow no nested iteration constructs, and when
expanding a pattern into a concrete trace, the starred sub-expressions have to
be repeated the same number of times; for example, the pattern
${{\mathbf{p}}}^{*}{{\mathbf{q}}}^{*}$ generates the traces
$\\{{{\mathbf{p}}}^{t}{{\mathbf{q}}}^{t},\ t\geq 0\\}$. The proof constructs a
pattern for every multi-polynomial computed, showing that it is realizable. It
is interesting that such simple patterns suffice to establish tight lower
bounds for all loops in our class.

  * •

In the upper-bound proof, we describe all traces by a finite set of _well-
typed regular expressions_ [Boj09]. This elegant tool channels the power of
the Factorization Forest Theorem [Sim90]; this theorem exposes the role of
idempotent elements, which is key in our algorithm.

  * •

Interestingly, the lower-bound proof not only justifies the tightness of our
upper bounds, it also justifies the termination of the algorithm and the
application of the Factorization Forest Theorem in the upper-bound proof,
because it shows that our abstract multi-polynomials generate a finite monoid.

Recall that traces are just sequences of polynomial transitions (Definition
6). Next, we define _concrete traces_ , which represent executions on concrete
data. The following definition assumes that the steps of the trace are
specified by $\tau$-free multi-polynomials; it suffices for the first part of
the proof (Section 7.1).

[Concrete traces (unweighted)] A _concrete trace_ corresponding to
$\sigma\in{\mathcal{S}}^{*}$ is a path of labeled arcs in the state space
$\mathbb{N}^{n}$:

${\widetilde{\sigma}}={s_{0}\xrightarrow{{{\mathbf{p}}}_{1}}s_{1}}\dots
s_{t-1}\xrightarrow{{{\mathbf{p}}}_{t}}s_{t},$

where $s_{i+1}={{\mathbf{p}}}_{i+1}(s_{i})$. We write
${{s_{0}}\stackrel{{\scriptstyle{\sigma}}}{{\leadsto}}{s_{t}}}$ to indicate
just the initial and final states of a trace (as a special case, the empty
trace ${\varepsilon}$ corresponds to a path with no arcs:
${s_{0}\stackrel{{\scriptstyle{\varepsilon}}}{{\leadsto}}s_{0}}$). The set of
all concrete traces is denoted ${\widetilde{{\mathcal{S}}^{*}}}$.

Note that the semantics of polynomial transitions never block a state. That
is, given $\sigma$ and $s_{0}$ there always is a ${\widetilde{\sigma}}$
starting with $s_{0}$.

##### Notations

  * •

Concatenation of traces $\sigma,\rho$ is written as $\sigma\rho$. For concrete
traces, concatenation requires the final state of $\sigma$ to be the initial
state of $\rho$, assuming both are non-empty.

  * •

In the proofs, we handle the abstract polynomials computed by the algorithm as
if they were concrete polynomials. This should be understood as an “implicit
cast,” applying the $\gamma$ conversion function (see Page 3). In fact, it is
useful to bear in mind that the correctness claim—namely, Theorem 2—is a claim
about concrete MPs, relating their numeric values to values generated by
program executions. We mostly omit $\alpha$’s and $\gamma$’s and the reader
should interpret a MP as concrete or abstract according to context. For
example, comparison of value $p\geq q$ applies to concrete polynomials, while
the statement that ${\mathbf{p}}$ is idempotent indicates that ${\mathbf{p}}$
is (or should be “cast” into) an abstract MP.

  * •

We call a $\tau$-MP ${\mathbf{p}}$ $\tau$-closed if
${{\mathbf{p}}}^{\tau}={{\mathbf{p}}}$.

###  7.1. Lower-Bound Correctness for Simple Loops

The key notion in proving that the upper bounds that we compute are
tight—equivalently, that they provide lower bounds (up to constant factors) on
the worst-case results—is that of _realizability_. Intuitively, when we come
up with a bound, we want to show that there are traces which achieve (realize)
this bound. Importantly, with asymptotic analysis, a bound is not justified,
in general, by showing a _single_ trace; what we need is a _pattern_ that
generates arbitrarily long traces.

Formally, we define the class of _patterns_ (over a given set of polynomial
transitions, $\mathcal{S}$) and their associated languages (sets of traces).
The following statements define patterns $\pi$ along with corresponding sets
of languages, $L(\pi,t)$. The role of $t$ is related to loop counts; it tells
how many times to repeat ${\mathbf{a}}$ in a pattern ${{\mathbf{a}}}^{*}$.

  * •

The empty string ${\varepsilon}$ is also a pattern. It generates the language
$L({\varepsilon},t)=\\{{\varepsilon}\\}$, consisting of the empty trace.

  * •

A single MP, ${{\mathbf{p}}}\in\mathcal{S}$, is a pattern. It generates the
language $L({{\mathbf{p}}},t)=\\{{{\mathbf{p}}}\\}$, consisting of a single
trace.

  * •

A concatenation of patterns is a pattern, and
$L(\pi_{1}\pi_{2},t)\stackrel{{\scriptstyle
def}}{{=\;}}L(\pi_{1},t)L(\pi_{2},t)$, where the right-hand side applies
concatenation to traces.
We define concatenation of patterns to be associative, so
${{\mathbf{p}}}({{\mathbf{q}}}{{\mathbf{r}}})$ and
$({{\mathbf{p}}}{{\mathbf{q}}}){{\mathbf{r}}}$ are the same pattern, which may
be written ${{\mathbf{p}}}{{\mathbf{q}}}{{\mathbf{r}}}$ (this works because
concatenation of traces is also associative).

  * •

If $\pi$ is a pattern, $\pi^{*}$ is a pattern. However, nested application of
the star is not allowed; in other words, $\pi$ is required to be star-free. We
define $L(\pi^{*},t)={L(\pi)}^{t}$, where $L^{0}=\\{{\varepsilon}\\}$ and
$L^{t+1}=L^{t}\cdot L$.
Parentheses are used for syntactic disambiguation of the operand of the star,
e.g., ${{\mathbf{p}}}{({{\mathbf{q}}}{{\mathbf{r}}})}^{*}$.

We use the notation $\pi^{n}$ as a shorthand for a concatenation of $n$ copies
of $\pi$. The set of traces corresponding to pattern $\pi$, denoted $L(\pi)$,
is defined by $L(\pi)=\bigcup_{t\geq 0}L(\pi,t)$. E.g.,
$L(a^{*}b^{*})=\\{a^{n}b^{n}\mid n\geq 1\\}$. We denote by $\pi(n)$ the result
of substituting $n$ for all the stars in $\pi$ (obtaining a star-free
pattern). In particular, $\pi(1)$ is the result of substituting 1 for all the
stars in $\pi$. Since nesting of iterative expressions is not allowed,
$|\pi(t)|=\Theta(t)$.

[Realizability] A polynomial transition (PT)
${{\mathbf{p}}}\in{\texttt{$\tau$MPol}}$ is said to be _realizable_ over the
given set $\mathcal{S}\subset{\texttt{MPol}}$ if there is a pattern $\pi$ and
a constant $0<c\leq 1$, such that for all $t\geq 1$, for all $\sigma\in
L(\pi(t))$, if
${{\mathbf{x}}\stackrel{{\scriptstyle{\sigma}}}{{\leadsto}}{\mathbf{y}}}$,
then

${\mathbf{y}}\geq\dot{{\mathbf{p}}}({{\mathbf{x}}},t)+c\ddot{{\mathbf{p}}}({{\mathbf{x}}},t)\,.$
(2)

We say that ${\mathbf{p}}$ is realized by $\pi;c$, or that it is
$c$-realizable. For $\tau$-free MPs, we use the same definition but $\pi$
should not include a star, so $t$ may be omitted. Thus a $\tau$-free MP is to
be realized by a single abstract trace. A set of MPs is called realizable if
all its members are.

We reconsider the loop in Example 5. In Example 5 we have computed from its
body the $\tau$-MP ${{\mathbf{q}}}={{\mathbf{p}}}^{\tau}=\langle x_{1}+\tau
x_{3},\ x_{2}+\tau x_{3}+x_{4},\ x_{3},\ x_{3}\rangle$. We claim that it is
realizable. We use the simple pattern $\pi={{\mathbf{p}}}^{*}$. The final
state after $t\geq 1$ iterations (a trace in $L(\pi(t))$) is

${{\mathbf{y}}}=\langle x_{1}+tx_{3},\ x_{2}+(2t-1)x_{3}+x_{4},\ x_{3},\
x_{3}\rangle,$

which is easy to verify by inspection of the program. We now verify that

${{\mathbf{y}}}\geq\dot{{{\mathbf{q}}}}({{\mathbf{x}}},t)+c\ddot{{{\mathbf{q}}}}({{\mathbf{x}}},t),$

where $c=1$.

Note that realizability is a monotone property in the sense that if
${{\mathbf{p}}}\geq{{\mathbf{q}}}$ and ${\mathbf{p}}$ is realizable, then
${\mathbf{q}}$ is. This is natural, since we are arguing that ${\mathbf{p}}$
is a _lower bound_. Note also that in contrast to Clause 2 of Theorem 2, we
pass $t$ rather than $|\sigma|$ as the $\tau$ parameter to the polynomial
bound. However, since $|\pi(t)|=\Theta(t)$, the inequality in the theorem will
be satisfied, just with a different constant factor.222This consideration only
applies to the non-linear part $\ddot{{\mathbf{p}}}$, since
$\dot{{\mathbf{p}}}$ is $\tau$-free anyway.

We introduce a short form that makes inequalities such as (2) easier to
manipulate: For any $\tau$-polynomial $p$, and real number $c\leq 1$,

$c{:}p({{\mathbf{x}}},t)\stackrel{{\scriptstyle
def}}{{=\;}}\dot{p}({{\mathbf{x}}},t)+c\ddot{p}({{\mathbf{x}}},t)\,.$

We also write $c{:}{{\mathbf{p}}}$ for component-wise application of “$c{:}$”
to a multi-polynomial ${\mathbf{p}}$. It is useful to be aware of properties
of this operation. We leave the verification of the next lemma to the reader.

######  Lemma 3.

Let $r\in{\texttt{$\tau$Pol}}$, ${{\mathbf{p}}}\in{\texttt{$\tau$MPol}}$, and
$c\leq 1$. Then we have

$\displaystyle(c{:}r)\circ{{\mathbf{p}}}$ $\displaystyle\geq
c{:}(r\circ{{\mathbf{p}}})$ $\displaystyle r\circ(c{:}{{\mathbf{p}}})$
$\displaystyle\geq c^{\deg r}{:}(r\circ{{\mathbf{p}}})\,.$

######  Lemma 4.

Let ${{\mathbf{p}}},{{\mathbf{q}}}\in{\texttt{$\tau$AMPol}}$. Then
${{\mathbf{p}}}\circ{{\mathbf{q}}}\geq{{\mathbf{p}}}\mathop{\bullet}{{\mathbf{q}}}$.

Note that on the left-hand side of the inequality, we compose in $\tau$MPol,
while on the right-hand side, we compose in $\tau$AMPol. A more explicit
expression of this claim would be:

$\gamma({{\mathbf{p}}})\circ\gamma({{\mathbf{q}}})\geq\gamma({{\mathbf{p}}}\mathop{\bullet}{{\mathbf{q}}}).$

Now this becomes obvious, since both sides of the equality have the same
monomials (they are abstractly the same), and the coefficients on the right-
hand side are all 1, while on the left-hand side they are integers. The fact
that both sides have corresponding monomials allows us to strengthen the
statement to the following:

######  Lemma 5.

Let ${{\mathbf{p}}},{{\mathbf{q}}}\in{\texttt{$\tau$AMPol}}$ and $c\leq 1$.
Then $c{:}({{\mathbf{p}}}\circ{{\mathbf{q}}})\geq
c{:}({{\mathbf{p}}}\mathop{\bullet}{{\mathbf{q}}})$.

Recall that we aim to prove that all PTs computed by our algorithm are
realizable. We do this by a series of lemmas which shows that realizability is
preserved by the various constructions in our algorithm. Note that our
algorithm produces abstract MPs; so, let us clarify that when we say that
${{\mathbf{p}}}\in{\texttt{AMPol}}$ is realizable, Definition 7.1 is actually
applied to $\gamma({{\mathbf{p}}})$.

####  7.1.1. Realizability without generalization

The realizability of PTs computed in the closure step will follow quite easily
using a few simple lemmas.

######  Lemma 6.

$\mathit{Id}$ is realizable.

######  Proof 7.1.

$\mathit{Id}$ is realized by the empty pattern.

######  Lemma 7.

Every member of $\mathcal{S}$ is realizable.

######  Proof 7.2.

${{\mathbf{p}}}\in\mathcal{S}$ is realized by the pattern ${\mathbf{p}}$.

######  Lemma 8.

Let ${\mathbf{p}}$, ${\mathbf{q}}$ be realizable $\tau$-MPs. Then
${{\mathbf{q}}}\circ{{\mathbf{p}}}$ is realizable.

######  Proof 7.3.

Suppose that ${\mathbf{p}}$ is realized by $\pi_{1};c_{1}$ and ${\mathbf{q}}$
by $\pi_{2};c_{2}$. We claim that ${{\mathbf{q}}}\circ{{\mathbf{p}}}$ is
realized by $\pi_{1}\pi_{2};c^{\prime}$ for some $c^{\prime}$. Consider a
concrete transition sequence $\widetilde{\sigma}$ with $\sigma\in
L((\pi_{1}\pi_{2})(t))$, it has the form
${{\mathbf{x}}\stackrel{{\scriptstyle\sigma_{1}}}{{\leadsto}}{\mathbf{y}}}{\>\stackrel{{\scriptstyle\sigma_{2}}}{{\leadsto}}{\mathbf{z}}}$
with $\sigma_{i}\in L(\pi_{i}(t))$. We have:

$\displaystyle{\mathbf{y}}$ $\displaystyle\geq
c_{1}{:}{{\mathbf{p}}}({{\mathbf{x}}},t)$ $\displaystyle{\mathbf{z}}$
$\displaystyle\geq c_{2}{:}{{\mathbf{q}}}({{\mathbf{y}}},t),$

consequently, using Lemma 3:

${\mathbf{z}}\geq
c_{1}^{d}c_{2}{:}({{{\mathbf{q}}}\circ{{\mathbf{p}}}})({{\mathbf{x}}},t)$

where $d$ is the highest degree of any component of ${\mathbf{q}}$.

######  Lemma 9.

Let ${{\mathbf{p}}},{{\mathbf{q}}}\in{\texttt{$\tau$AMPol}}$ be realizable.
Then ${{\mathbf{q}}}\mathop{\bullet}{{\mathbf{p}}}$ is realizable.

######  Proof 7.4.

This follows from the previous lemma and Lemma 5.

######  Corollary 10.

Let $T$ be a set of realizable abstract $\tau$-MPs. Then every member of
${Cl(T)}$ is realizable.

####  7.1.2. Dependence graphs and neat MPs

We are still missing a realizability lemma for the generalization operation.
As a preparation for this proof, we introduce the dependence graph of a PT and
state an important structural property of dependency graphs associated with
idempotent transitions. This leads to the definition of the class we call neat
MPs.

Let ${{\mathbf{p}}}\in{\texttt{$\tau$MPol}}$. Its _dependency graph_
$G({{\mathbf{p}}})$ is a directed graph with node set $[n]$. The graph
includes an arc $i\to j$ if and only if ${{\mathbf{p}}}[j]$ depends on
$x_{i}$.

Intuitively, $G({{\mathbf{p}}})$ shows the data flow in the transition
${\mathbf{p}}$. It is easy to see that paths in the graph correspond to data-
flow effected by a sequence of transitions. For instance, if we have a path
$i\to j\to k$ in $G({{\mathbf{p}}})$, then $x_{i}$ will appear in the
expression $({{\mathbf{p}}}\circ{{\mathbf{p}}})[k]$.

######  Lemma 11.

Suppose that the SDL $\mathcal{S}$ is polynomially bounded. Then for all
${{\mathbf{p}}}\in{\texttt{$\tau$MPol}}$ which is realizable over
$\mathcal{S}$, ${{\mathbf{p}}}[i]$ has no monomial divisible by $x_{i}$ other
than $x_{i}$.

######  Proof 7.5.

Suppose that ${\mathbf{p}}$ has such a monomial, then it has the form
${\mathfrak{m}}x_{i}$. If $\mathfrak{m}$ is $\tau$-free, then starting with a
state in which all variables have values greater than 1, and repeatedly
executing a trace that realizes ${\mathbf{p}}$, we clearly obtain an
exponential growth of the value in $\texttt{X}_{i}$, contradicting the
assumption. In the case that $\tau$ occurs in $\mathfrak{m}$, suppose that
${\mathbf{p}}$ is realized by $\pi;c$. Choose $t\geq\max(c^{-1},2)$. Then
repeating the trace $\pi(t)$ creates an exponential growth in
$\texttt{X}_{i}$.

######  Lemma 12.

Suppose that ${{\mathbf{p}}}\in{\texttt{$\tau$MPol}}$ is realizable, and
$\alpha({{\mathbf{p}}})$ is idempotent. Assuming that the loop under analysis
is polynomially bounded, $G({{\mathbf{p}}})$ does not have any simple cycle
longer than one arc. In other words, it consists of a directed acyclic graph
(DAG) plus some self-loops.

######  Proof 7.6.

Assume, to the contrary, that $G({{\mathbf{p}}})$ does have a cycle
$i\to\dots\to k\to i$, where $k\neq i$. Let $r$ be the length of the cycle.
Then

  1. (1)

${{\mathbf{p}}}^{(r)}[i]$ depends on $x_{i}$; we can write
${{\mathbf{p}}}^{(r)}[i]=x_{i}+p({\mathbf{x}},\tau)$ (the occurrence of
$x_{i}$ must be in a linear monomial with a concrete coefficient of 1,
otherwise iteration would cause exponential growth). By the remark after
Definition 5,
$\alpha({{\mathbf{p}}}^{(r)})[i]=({(\alpha({{\mathbf{p}}}))}^{\mathop{\bullet}(r)})[i]$,
which, by idempotence, equals $\alpha({{\mathbf{p}}})[i]$. Reading backwards,
$\alpha({{\mathbf{p}}}[i])=\alpha({{\mathbf{p}}}^{(r)})[i]=\alpha(x_{i})+p({\mathbf{x}},\tau)$,
so ${{\mathbf{p}}}[i]$ also has the form $x_{i}+q(x,\tau)$ (where $q$ may
differ from $p$).

  2. (2)

By assumption, ${{\mathbf{p}}}[i]$ depends on $x_{k}$. Since $k\neq i$, we
conclude that $q$ depends on $x_{k}$. Also by the assumption of the cycle in
$G({{\mathbf{p}}})$, ${{\mathbf{p}}}^{(r-1)}[k]$ depends on $x_{i}$. This
shows that $q\circ{{\mathbf{p}}}^{(r-1)}$ depends on $x_{i}$.

  3. (3)

Now,

${{\mathbf{p}}}^{(r)}[i]=({{\mathbf{p}}}\circ{{\mathbf{p}}}^{(r-1)})[i]={{\mathbf{p}}}[i]\circ{{\mathbf{p}}}^{(r-1)}=(x_{i}+q)\circ{{\mathbf{p}}}^{(r-1)}={{\mathbf{p}}}^{(r-1)}[i]+(q\circ{{\mathbf{p}}}^{(r-1)})\,.$

We argue that the last expression has at least _two_ occurrences of $x_{i}$.
First, by the same token as (1), ${{\mathbf{p}}}^{(r-1)}[i]$ has an occurrence
of $x_{i}$. Secondly, $q\circ{{\mathbf{p}}}^{(r-1)}$ also has one.

  4. (4)

Thus ${{\mathbf{p}}}^{(r)}$ generates exponential growth when iterated, after
all.

We conclude that a cycle as assumed cannot exist.

The realizability lemmas are intended to be applied under the assumption of
Theorem 2, namely that our loop is polynomially bounded; therefore we can rely
on the properties guaranteed by Lemmas 11 and 12. We focus on a particular
idempotent realizable AMP ${\mathbf{p}}$. Then $G({{\mathbf{p}}})$, with self-
loops removed, is a DAG. We assume, w.l.o.g., that the variables are indexed
in an order consistent with $G({{\mathbf{p}}})$, so that if $x_{i}$ depends on
$x_{j}$ then $j\leq i$. We shall refer to an (abstract) MP satisfying the
properties in Lemma 11, Lemma 12 and with variables so re-indexed (if
necessary) as being _neat_.333Readers who like linear algebra may draw some
intuition about neat MPs from thinking about triangular matrices whose
diagonal elements are in $\\{0,1\\}$.

${{\mathbf{p}}}\in{\texttt{$\tau$MPol}}$ is called _neat_ if (a)
$G({{\mathbf{p}}})$, with self-loops removed, is a DAG; (b) for all $i$,
${{\mathbf{p}}}[i]$ has no monomial divisible by $x_{i}$ except (possibly)
$x_{i}$.

Note that ${\mathbf{p}}$ is not required to be idempotent; neat MPs that are
not necessarily idempotent come up in the upper-bound proof. In the rest of
this subsection we study neat idempotent AMPs, establishing (as Corollary 15
below) a property important for the subsequent realizability lemma. This
property involves the $n$th iterate ${{\mathbf{p}}}^{(n)}$. It is not hard to
prove that $({{\mathbf{p}}}^{(n)})(s^{\prime})\geq{{\mathbf{p}}}(s)$ if
$s^{\prime}[i]\geq s[i]$ for all $i$. We skip the proof, however, since we can
establish a sharper result, for states $s$, $s^{\prime}$ where
$s^{\prime}[i]\geq s[i]$ is only asserted for
$i\in{{\textsc{SD}}({\mathbf{p}})}$ (i.e., $x_{i}$ is self-dependent in
${\mathbf{p}}$).

We introduce the following notation: for
${{\mathbf{p}}}\in{\texttt{$\tau$AMPol}}$, $\chi_{{\mathbf{p}}}(i)$ is $1$ if
$i\in{{\textsc{SD}}({\mathbf{p}})}$ and $0$ otherwise.

######  Lemma 13.

Let ${{\mathbf{p}}}\in{\texttt{$\tau$AMPol}}$ be idempotent and neat. Let
$s,s^{\prime}\in\mathbb{N}^{n}$ be any state vectors such that for
$i\in{{\textsc{SD}}({\mathbf{p}})}$, $s^{\prime}[i]\geq s[i]$ (while for
$i\notin{{\textsc{SD}}({\mathbf{p}})}$ no relation is asserted). Then for all
$\ell\leq n$, ${{\mathbf{q}}}_{\ell}\stackrel{{\scriptstyle
def}}{{=\;}}{(c{:}{{\mathbf{p}}})}^{(\ell)}$ has the following property: for
all $i\leq\ell$, for all $t\geq 0$,

${{\mathbf{q}}}_{\ell}[i](s^{\prime},t)\geq(c^{{(d+1)}^{i}}{:}{{\mathbf{p}}})[i](s,t)+(s^{\prime}[i]-s[i])\cdot\chi_{{\mathbf{p}}}(i),$

where $d$ is the maximum degree in ${\mathbf{p}}$.

The following fact is useful for proving the lemma; it follows from Lemma 3.

######  Fact 14.

Let ${{\mathbf{p}}}\in{\texttt{$\tau$MPol}}$,
${{\mathbf{q}}}\in{\texttt{$\tau$MPol}}$. Suppose that for all $i<\ell$, we
have ${{\mathbf{q}}}[i]\geq c^{{(d+1)}^{i}}{:}{{\mathbf{p}}}[i]$, were $d$ is
the maximum degree in ${\mathbf{p}}$. And suppose that $r$ is a
$\tau$-polynomial depending only on $x_{1},\dots,x_{\ell-1}$, also of degree
at most $d$. Then $(c{:}r)\circ{{\mathbf{q}}}\geq
c^{{(d+1)}^{\ell}}{:}(r\circ{{\mathbf{p}}})$.

######  Proof 7.7 (Proof of Lemma 13).

We use induction on $\ell$. Since ${\mathbf{p}}$ is neat we know that
${{\mathbf{p}}}[1]=x_{1}$. Thus

$(c{:}{{\mathbf{p}}})[1](s^{\prime},t)=s^{\prime}[1]=s[1]+(s^{\prime}[1]-s[1])\cdot\chi_{{\mathbf{p}}}(1)=c^{d+1}{:}{{\mathbf{p}}}[1](s,t)+(s^{\prime}[1]-s[1])\cdot\chi_{{\mathbf{p}}}(1).$

Next, for $\ell>1$, consider
${{\mathbf{q}}}_{\ell}=(c{:}{{\mathbf{p}}})\circ{{{\mathbf{q}}}_{\ell-1}}$. If
$i\leq\ell$ and $x_{i}$ is not self-dependent in ${\mathbf{p}}$, then
${{\mathbf{p}}}[i]$ only depends on variables $x_{j}$ with $j<i$, so:

$\displaystyle{{\mathbf{q}}}_{\ell}[i](s^{\prime},t)$
$\displaystyle=(c{:}{{\mathbf{p}}}[i]\circ{{{\mathbf{q}}}_{\ell-1}})(s^{\prime},t)$
$\displaystyle\geq(c{:}{{\mathbf{p}}}[i]\circ
c^{{(d+1)}^{i-1}}{:}{{\mathbf{p}}})(s,t)$ by IH
$\displaystyle\geq(c^{{(d+1)}^{i}}{:}({{\mathbf{p}}}[i]\circ{{\mathbf{p}}}))(s,t)$
by Fact 14 $\displaystyle\geq(c^{{(d+1)}^{i}}{:}{{\mathbf{p}}}[i])(s,t)$ by
idempotence
$\displaystyle=(c^{{(d+1)}^{i}}{:}{{\mathbf{p}}}[i])(s,t)+(s^{\prime}[i]-s[i])\cdot\chi_{{\mathbf{p}}}(i)$

where the next-to-last step uses the idempotence of ${\mathbf{p}}$ in
$\tau$AMPol and Lemma 5.

If $x_{i}$ is self-dependent in ${\mathbf{p}}$, then
${{\mathbf{p}}}[i]=x_{i}+r({\mathbf{x}},\tau)$ where $r$ only depends on
variables $x_{j}$ with $j<i$. Now by IH, and Fact 14:

$\displaystyle{{\mathbf{q}}}_{\ell}[i](s^{\prime},t)$
$\displaystyle=(c{:}{{\mathbf{p}}}[i]\circ{{{\mathbf{q}}}_{\ell-1}})(s^{\prime},t)$
$\displaystyle={{{\mathbf{q}}}_{\ell-1}}[i](s^{\prime},t)+(c{:}r\circ{{{\mathbf{q}}}_{\ell-1}})(s^{\prime},t)\geq
s^{\prime}[i]+(c{:}r\circ(c^{{(d+1)}^{i-1}}{:}{{\mathbf{p}}}))(s,t)$
$\displaystyle=s[i]+(s^{\prime}[i]-s[i])\cdot\chi_{{\mathbf{p}}}(i)+(c{:}r\circ(c^{{(d+1)}^{i-1}}{:}{{\mathbf{p}}}))(s,t)$
$\displaystyle=(c{:}{{\mathbf{p}}}[i]\circ(c^{{(d+1)}^{i-1}}{:}{{\mathbf{p}}}))(s,t)+(s^{\prime}[i]-s[i])\cdot\chi_{{\mathbf{p}}}(i)$
$\displaystyle\geq
c^{{(d+1)}^{i}}{:}({{\mathbf{p}}}[i]\circ{{\mathbf{p}}})(s,t)+(s^{\prime}[i]-s[i])\cdot\chi_{{\mathbf{p}}}(i)$
$\displaystyle\geq(c^{{(d+1)}^{i}}{:}{{\mathbf{p}}}[i])(s,t)+(s^{\prime}[i]-s[i])\cdot\chi_{{\mathbf{p}}}(i)\,.$

Letting $\ell=n$ in this lemma we obtain:

######  Corollary 15.

Let ${{\mathbf{p}}}\in{\texttt{$\tau$AMPol}}$ be idempotent and neat. Let
$s,s^{\prime}\in\mathbb{N}^{n}$ be any state vectors such that for
$i\in{{\textsc{SD}}({\mathbf{p}})}$, $s^{\prime}[i]\geq s[i]$. Then, for all
$i\leq n$ and all $t$,
${(c{:}{{\mathbf{p}}})}^{(n)}[i](s^{\prime},t)\geq(c^{{(d+1)}^{n}}{:}{{\mathbf{p}}})[i](s,t)+(s^{\prime}[i]-s[i])\cdot\chi_{{\mathbf{p}}}(i)$.

####  7.1.3. Realizability lemma for generalization

This is what we have been preparing for.

######  Lemma 16.

Let ${\mathbf{p}}$ be a realizable, idempotent and neat abstract $\tau$-MP.
Then ${{\mathbf{p}}}^{\tau}$ is realizable.

Note that if ${\mathbf{p}}$ is $\tau$-closed, then
${{\mathbf{p}}}^{\tau}={{\mathbf{p}}}$ and the statement is trivial. But if
${\mathbf{p}}$ is not $\tau$-closed, then we have to construct a pattern that
causes additive terms to accumulate in the self-dependent variables in order
to justify the replacement of sums $x_{i}+{{\mathbf{p}}}[i]^{\prime\prime}$ by
$x_{i}+\tau{{\mathbf{p}}}[i]^{\prime\prime}$. The interesting case is when
${\mathbf{p}}$ is not $\tau$-free: then $\pi$ already has stars, however
nested stars are not allowed in a pattern, so we cannot iterate $\pi$. The
solution is to use ${(\pi(1))}^{*}$. However, in reducing $\pi$ to the star-
free $\pi(1)$ we pull the rug under $\tau$-monomials already present in
${\mathbf{p}}$. Therefore we use a pattern that includes both ${(\pi(1))}^{*}$
and $\pi$; actually, not $\pi$ but ${\pi}^{n}$, in order to use Corollary 15.
Note that realizability of ${\mathbf{p}}$ by $\pi$ means that $\pi(1)$
realizes ${{\mathbf{p}}}[1/\tau]$ (which is ${\mathbf{p}}$ with all $\tau$’s
erased). The following observation is useful: If
${{\mathbf{p}}}\in{\texttt{$\tau$AMPol}}$ is idempotent, so is
${{\mathbf{p}}}[1/\tau]$; and similarly for neat.

######  Proof 7.8 (Proof of Lemma 16).

Let $\pi;c$ realize ${\mathbf{p}}$. Note that $\pi$ will include stars iff
${\mathbf{p}}$ includes $\tau$’s. We are handling the general case so we treat
${\mathbf{p}}$ as a $\tau$-MP; the arguments also apply to the case that it is
$\tau$-free. So, our assumption is that:

$\text{if
}{{\mathbf{x}}\stackrel{{\scriptstyle{\pi(t)}}}{{\leadsto}}{\mathbf{y}}}\text{
then }{\mathbf{y}}\geq c{:}{{\mathbf{p}}}({\mathbf{x}},t)\,.$ (3)

We will show that ${{\mathbf{p}}}^{\tau}$ is realized by the pattern
${(\pi(1))}^{*}\pi^{n}$. Now, traces in $L({(\pi(1))}^{*}\pi^{n})$ have the
form $\sigma_{t}={(\pi(1))}^{t}\pi^{n}(t)$. We look at concrete traces

${s_{0}\stackrel{{\scriptstyle\pi(1)}}{{\leadsto}}s_{1}}{\cdots\stackrel{{\scriptstyle\pi(1)}}{{\leadsto}}s_{t}}{\>\stackrel{{\scriptstyle\pi^{n}(t)}}{{\leadsto}}s_{t+1}}\,.$

We first prove by induction on $t$, for $x_{i}$ self-dependent in
${\mathbf{p}}$, and $t\geq 0$,

$s_{t}[i]\geq s_{0}[i]+t(c{:}{{\mathbf{p}}}[i]^{\prime\prime}(s_{0}))$ (4)

(note that the omission of the $\tau$ parameter in
${{\mathbf{p}}}[i]^{\prime\prime}(s_{0})$ reminds us that
${{\mathbf{p}}}[i]^{\prime\prime}$ is $\tau$-free). For $t=0$, the statement
is trivial. For the inductive case,

$\displaystyle s_{t}[i]$ $\displaystyle\geq c{:}{{\mathbf{p}}}[i](s_{t-1},1)$
$\displaystyle\geq
s_{t-1}[i]+c{:}({{\mathbf{p}}}[i]^{\prime}(s_{t-1},1)+{{\mathbf{p}}}[i]^{\prime\prime}(s_{t-1})+{{\mathbf{p}}}[i]^{\prime\prime\prime}(s_{t-1},1))$
by structure of ${\mathbf{p}}[i]$ $\displaystyle\geq
s_{t-1}[i]+c{:}{{\mathbf{p}}}[i]^{\prime\prime}(s_{t-1})$ $\displaystyle\geq
s_{0}[i]+(t-1)(c{:}{{\mathbf{p}}}[i]^{\prime\prime}(s_{0}))+c{:}{{\mathbf{p}}}[i]^{\prime\prime}(s_{t-1})$
by IH $\displaystyle\geq
s_{0}[i]+(t-1)(c{:}{{\mathbf{p}}}[i]^{\prime\prime}(s_{0}))+c{:}{{\mathbf{p}}}[i]^{\prime\prime}(s_{0})$
(s.d. variables are non-decreasing) $\displaystyle\geq
s_{0}[i]+t{{\mathbf{p}}}[i]^{\prime\prime}(s_{0})$

Now, for $i\in{{\textsc{SD}}({\mathbf{p}})}$,

$\displaystyle s_{t+1}[i]$
$\displaystyle\geq{(c{:}{{\mathbf{p}}})}^{(n)}[i](s_{t},t)$
$\displaystyle\geq(c^{{(d+1)}^{n}}{:}{{\mathbf{p}}})[i](s_{0},t)+(s_{t}[i]-s_{0}[i])$
by Cor. 15
$\displaystyle=s_{0}[i]+c^{{(d+1)}^{n}}{:}(t{{\mathbf{p}}}[i]^{\prime}(s_{0},t)+{{\mathbf{p}}}[i]^{\prime\prime}(s_{0})+{{\mathbf{p}}}[i]^{\prime\prime\prime}(s_{0},t))+(s_{t}[i]-s_{0}[i])$
by Def. 5 $\displaystyle\geq
s_{0}[i]+c^{{(d+1)}^{n}}{:}(t{{\mathbf{p}}}[i]^{\prime}(s_{0},t)+{{\mathbf{p}}}[i]^{\prime\prime}(s_{0})+{{\mathbf{p}}}[i]^{\prime\prime\prime}(s_{0},t))+t{{\mathbf{p}}}[i]^{\prime\prime}(s_{0})$
by (4) $\displaystyle\geq
s_{0}[i]+c^{{(d+1)}^{n}}{:}(t{{\mathbf{p}}}[i]^{\prime}(s_{0},t)+t{{\mathbf{p}}}[i]^{\prime\prime}(s_{0})+{{\mathbf{p}}}[i]^{\prime\prime\prime}(s_{0},t))$
$\displaystyle=c^{{(d+1)}^{n}}{:}{{\mathbf{p}}}^{\tau}[i](s_{0},t)\,.$

For $i\notin{{\textsc{SD}}({\mathbf{p}})}$,

$\displaystyle s_{t+1}[i]$
$\displaystyle\geq{(c{:}{{\mathbf{p}}})}^{(n)}[i](s_{t},t)$
$\displaystyle\geq(c^{{(d+1)}^{n}}{:}{{\mathbf{p}}})[i](s_{0},t)+(s_{t}[i]-s_{0}[i])\cdot\chi_{{\mathbf{p}}}(i)$
by Cor. 15 $\displaystyle=(c^{{(d+1)}^{n}}{:}{{\mathbf{p}}})[i](s_{0},t)\,.$

We conclude that the pattern ${(\pi(1))}^{*}\pi^{n}$ realizes
${{\mathbf{p}}}^{\tau}$.

We can now complete our lower-bound correctness proof:

######  Theorem 17.

Consider any set of MPs $\mathcal{S}$. Then the set of $\tau$-MPs returned by
Solve$(\mathcal{S})$ is realizable over $\mathcal{S}$.

######  Proof 7.9.

This follows by induction on the number of operations used to construct each
resulting $\tau$-MP, being either composition steps or generalization steps
(justified, respectively, by Lemma 8 or Lemma 16).

This has a crucial corollary:

######  Corollary 18.

Consider any set of MPs $\mathcal{S}$, that represent a SDL in which all
variables are polynomially bounded. Then the set of $\tau$-MPs generated by
Solve$(\mathcal{S})$ is finite, and therefore obtained in a finite number of
steps.

######  Proof 7.10.

Since we are working within $\tau$AMPol, it is clear that if the set of
$\tau$-MPs computed by the algorithm is infinite, unbounded exponents must
appear. Since all these MPs are realizable, this indicates that some variable
cannot be bounded polynomially over all executions of the loop. Taking the
contrapositive, we conclude that if all variables are known to be polynomially
bounded, the set is finite.

###  7.2. Upper-Bound Correctness

The upper-bound correctness establishes a correspondence between the set of
AMPs computed by our algorithm and a set of concrete polynomials that actually
provide upper bounds for all loop executions (as in Theorem 2, Clause 1).
Implicitly, this proof provides _an algorithm to compute concrete upper
bounds_ , while ensuring that the abstractions of these bounds remain within
our set of AMPs. But we do not attempt to explicate the algorithm as such,
since our main contribution is the algorithm already given. Firstly, we have
to provide a finer definition of “upper bound” in terms of _weighted traces_.
The main technical part of the section defines a special class of $\tau$-MPs,
called _iterative_ , and shows some properties of the class. Finally, the main
part of the proof uses a corollary of Simon’s _Forest Factorization Theorem_
to construct the desired upper bounds. The application of this theorem is
justified by Corollary 18. Before diving into upper bounds, we give a useful
definition and some related lemmas.

For multiivariate polynomials $p,q$ we define their _join_ $p\sqcup q$ as the
polynomial obtained by setting the coefficient of every monomial to the
largest of its coefficients in $p$ and in $q$.

For example:
$(2x_{1}+x_{1}x_{2})\sqcup(x_{1}+x_{2}+3x_{1}x_{2})=2x_{1}+x_{2}+3x_{1}x_{2}\,$.

It is easy to see that $\sqcup$ is the join (least upper bound) operation in a
natural partial order on polynomials, which we denote by $\sqsubset$. Note
that this order is “syntactic” and is a part of the “semantic” relation $p\leq
q$ defined by treating them as functions over $\mathbb{N}^{n}$. To see that
the relations do not coincide, consider $xy$ versus $x^{2}+y^{2}$. With multi-
polynomials, we apply the relation component-wise.

######  Lemma 19.

Suppose that ${{\mathbf{p}}}\sqsubset{{\mathbf{q}}}$ and
${{\mathbf{r}}}\sqsubset{{\mathbf{s}}}$. Then
${{\mathbf{p}}}\circ{{\mathbf{r}}}\sqsubset{{\mathbf{q}}}\circ{{\mathbf{s}}}$.

######  Proof 7.11.

Every monomial $\mathfrak{m}$ of ${{\mathbf{p}}}\circ{{\mathbf{r}}}$ is the
result of substituting a certain monomial of ${{\mathbf{r}}}[i]$ for every
occurrence of $x_{i}$ in ${\mathbf{p}}$ (where $x_{i}^{d}$ counts as $d$
occurrences). As the same monomials (up to coefficients) appear in,
respectively, ${{\mathbf{s}}}[i]$ and ${\mathbf{q}}$, we conclude that
$\mathfrak{m}$ (times some constant) appears in
${{\mathbf{q}}}\circ{{\mathbf{s}}}$.

Using the join operator, we thus have:
${{\mathbf{p}}}\circ({{\mathbf{r}}}\sqcup{{\mathbf{s}}})\sqsupset({{\mathbf{p}}}\circ{{\mathbf{r}}})\sqcup({{\mathbf{p}}}\circ{{\mathbf{s}}})$.

######  Lemma 20.

For any pair of polynomials $f,g$, and numbers $a,b\geq 0$,

$af+bg\leq(a+b)(f\sqcup g)\,.$

######  Proof 7.12.

Partition the monomials of $f$ $\sqcup$ $g$ into three groups: those that
appear only in $f$; they are multiplied by $a$ on the LHS and by $(a+b)$ on
the RHS. Those that appear only in $g$; they are multiplied by $b$ on the LHS
and by $(a+b)$ on the RHS. For a monomial $\mathfrak{m}$ that appears in both
polynomials—possibly with different coefficients, say $c$ in $f$ and $d$ in
$g$, we find $ac{\mathfrak{m}}+bd{\mathfrak{m}}$ in the LHS, and
$(a+b)\max(c,d){\mathfrak{m}}$ in the RHS.

##### Weighted traces and upper bounds

We extend our notion of traces by defining _weighted traces_. The need for
this definition arises because, in the proof, we argue about a decomposition
of an actual trace into segments, and we need to abstract from the
intermediate states within a segment. The number of actual transitions in the
segment matters, however, and will be represented by its weight. Thus a
weighted step, denoted ${s\xrightarrow{{{\mathbf{p}}}|w}s^{\prime}}$,
indicates that state $s$ has evolved into step
$s^{\prime}={{\mathbf{p}}}(s,w)$ in $w$ actual transitions, for an integer
$w\geq 1$. A weighted concrete trace $\sigma$ is composed of such steps in the
same way as an ordinary trace is; a weighted abstract trace specifies the
bounds and weights but leaves the states unspecified, e.g.,
$({{\mathbf{p}}}_{1}|w_{1})({{\mathbf{p}}}_{2}|w_{2})({{\mathbf{p}}_{3}}|w_{3})$.
The total weight of a trace $\sigma$ is denoted by ${\|\sigma\|}$ and
calculated by adding up the weights of the steps. Thus we have
${\|\sigma\rho\|}={\|\sigma\|}+{\|\rho\|}$. Note that since the MPs that label
a weighted step are, in general, upper bounds obtained in previous analysis
steps, the value $s^{\prime}={{\mathbf{p}}}(s,w)$ represents, in general, a
bound and not a state that is actually reachable; however, we argue that due
to the monotonicity of the functions computable in our language, we do not
lose soundness by considering $s^{\prime}$ instead of a set of values bounded
by $s^{\prime}$.

We denote the set of weighted traces over $\mathcal{S}$ by
$\mathcal{W}{\mathcal{S}}^{*}$. Note that weights are associated with abstract
transitions and all concretizations of a weighted trace have the same weight.

[bound for a trace] Let $\sigma\in{\widetilde{\mathcal{W}{\mathcal{S}}^{*}}}$.
We say that $\sigma$ admits a $\tau$-polynomial $p$ as an upper bound on
variable $j$, or that $p$ bounds variable $j$ in $\sigma$, if the following
holds:

${{\mathbf{x}}\stackrel{{\scriptstyle\sigma}}{{\leadsto}}{\mathbf{y}}}\land{t\geq{\|\sigma\|}}\
\Longrightarrow\ y_{j}\leq p({\mathbf{x}},t)\,.$ (5)

If ${\mathbf{p}}$ bounds _all_ variables in a concrete weighted trace
${{\mathbf{x}}\stackrel{{\scriptstyle\sigma}}{{\leadsto}}{\mathbf{y}}}$, we
say that ${\mathbf{p}}$ bounds this trace. If ${\mathbf{p}}$ bounds all
concretizations of $\sigma$, we say it bounds $\sigma$.

The following lemma follows from the monotonicity of all our polynomials.

######  Lemma 21.

If ${\mathbf{p}}$ bounds $\sigma$ and ${\mathbf{q}}$ bounds $\rho$, then
${{\mathbf{q}}}\circ{{\mathbf{p}}}$ bounds $\sigma\rho$.

######  Proof 7.13.

Let $t_{s}={\|\sigma\|}$, $t_{r}={\|\rho\|}$. Consider a concrete run of
$\sigma\rho$ and name the states thus:
${{\mathbf{x}}\stackrel{{\scriptstyle\sigma}}{{\leadsto}}{\mathbf{y}}}{\>\stackrel{{\scriptstyle\rho}}{{\leadsto}}{\mathbf{z}}}$.
Then $z_{i}\leq{{\mathbf{q}}}[i]({\mathbf{y}},t_{r})$ (by assumption) and for
any $j$, $y_{j}\leq{{\mathbf{p}}}[j]({\mathbf{x}},t_{s})$. It clearly follows
that
$z_{i}\leq({{\mathbf{q}}}[i]\circ{\mathbf{p}})({\mathbf{x}},t_{s}+t_{r})$.
Note that $t_{s}+t_{r}$ is precisely ${\|\sigma\rho\|}$.

##### Iterative MPs and upper bounds for sequences of similar MPs

${\mathbf{p}}\in{\texttt{$\tau$MPol}}$ is called _iterative_ if all its
entries depend only on self-dependent variables. Moreover, each
${{\mathbf{p}}}[i]$ depends only on variables with indices $j\leq i$.

$\langle x_{1},x_{2}+x_{1},x_{2}x_{1}\rangle$ is iterative, while $\langle
x_{1},x_{1},x_{3}+x_{2}+x_{1}\rangle$ is not (note that the last MP is
idempotent when abstracted to AMPol, which demonstrates that this property
does not imply iterativity; the converse does not hold, either). We abbreviate
“iterative multi-polynomial” to IMP. We next give some technical definitions
and results regarding IMPs. The upshot of this part is the computation of
tight upper bounds for the end-state of certain traces composed of IMPs. We
now attempt to give some intuition. Consider a sequence of MPs which are
idempotent in their abstract form. Thus if we compose their abstractions in
AMPol we just get the same AMP again. This is a nice situation which suggests
that we can extrapolate the bounds for a single step to bounds for any number
of steps. But there may be some values that grow and we will have to account
for this in our upper bounds. Consider the following MP:

$\langle x_{1}+x_{2}+x_{3},\ x_{3},\ x_{3}\rangle$

Note that it is idempotent in AMPol. However, in concrete computation, the
increments accumulate. But hastily changing the first component to
$x_{1}+\tau(x_{2}+x_{3})$ overshoots the upper bound. The correct result is
$x_{1}+x_{2}+x_{3}+\tau(2x_{3})$. We find this result by extracting an
iterative MP from the given set of MPs. In the above example, the extracted
IMP will be $\langle x_{1}+2x_{3},\ x_{3},\ x_{3}\rangle$; we will see later
why.

Moving to more precise details, we are going to consider sequences of
_similar_ MPs, where similarity means that we get the same MP if we ignore the
coefficients as well as $\tau$ symbols, as expressed by the following set of
definitions.

Let ${\mathbf{p}}\in{\texttt{$\tau$MPol}}$. We define
$\alpha!({{\mathbf{p}}})$ to be $\alpha({{\mathbf{p}}}[1/\tau])$.

For example, $\alpha!({\langle x_{1}+\tau x_{2},x_{1}^{2}+\tau
x_{1}^{2}\rangle})=\langle x_{1}+x_{2},x_{1}^{2}\rangle$.

We call ${{\mathbf{p}}}$, ${\mathbf{q}}$ _similar_ if
$\alpha!({{\mathbf{p}}})=\alpha!({{\mathbf{q}}})$.

Suppose that $\alpha!({{\mathbf{p}}})=\alpha!({{\mathbf{q}}})$. Then for any
${\mathbf{t}}$,
$\alpha!({{{\mathbf{p}}}\circ{{\mathbf{t}}}})=\alpha!({{{\mathbf{q}}}\circ{{\mathbf{t}}}})=\alpha!({{\mathbf{p}}})\mathop{\bullet}\alpha!({{\mathbf{t}}})$.

Whenever an idempotent MP is considered, we also assume it is realizable,
which in turn allows us to assume that its variables are indexed in
topological order, as in the previous section, making it neat. One could worry
that the assumptions of topological order might contradict each other in an
argument that involves several different idempotents, but this is not a
problem since all the development below only concerns a set of similar MPs, so
they agree on the topological indexing. In such a discussion we may say, for
example, that some $x_{i}$ is self-dependent, without specifying which MP of
the set is concerned.

Let ${\mathbf{p}}\in{\texttt{$\tau$MPol}}$ be such that
$\alpha!({{\mathbf{p}}})$ is neat. Define its _self-dependent cut_
${\lfloor{\mathbf{p}}\rfloor}$ as follows: for all $i$ self-dependent in
${\mathbf{p}}$, ${\lfloor{\mathbf{p}}\rfloor}[i]=x_{i}$. For all other $i$,
${\lfloor{\mathbf{p}}\rfloor}[i]={{\mathbf{p}}}[i]$.

######  Lemma 22.

Let ${{\mathbf{p}}}_{1},\dots,{{\mathbf{p}}}_{n}$ be similar $\tau$-MPs such
that $\alpha!({{{\mathbf{p}}}_{1}})=\alpha!({{{\mathbf{p}}}_{2}})=\dots$ is
neat. Then for all $\ell\leq n$, ${{\mathbf{q}}}_{\ell}\stackrel{{\scriptstyle
def}}{{=\;}}{{\mathbf{p}}}_{1}\circ{\lfloor{{\mathbf{p}}}_{2}\rfloor}\cdots\circ{\lfloor{{\mathbf{p}}}_{\ell}\rfloor}$
has the following property: for all $i$, ${{\mathbf{q}}}_{\ell}[i]$ only
depends on variables $x_{j}$ which are either self-dependent or else $j\leq
i-\ell$.

######  Proof 7.14.

We use induction on $\ell$. For $\ell=1$, the result is immediate, by virtue
of the topological indexing. Next, for $\ell>1$, consider
${{\mathbf{q}}}_{\ell-1}={{\mathbf{p}}}_{1}\circ\cdots\circ{\lfloor{{\mathbf{p}}}_{\ell-1}\rfloor}$.
Now
${{\mathbf{q}}}_{\ell}={{\mathbf{q}}}_{\ell-1}\circ{\lfloor{{\mathbf{p}}}_{\ell}\rfloor}$.
By IH, ${{\mathbf{q}}}_{\ell-1}[i]$ only depends on variables $x_{j}$ which
are either self-dependent or have $j\leq i-\ell+1$. In the case that $x_{j}$
is self-dependent, then ${\lfloor{{\mathbf{p}}}_{\ell}\rfloor}[j]=x_{j}$, so
${{\mathbf{q}}}_{\ell}[i]$ also depends on $x_{j}$ which agrees with the
lemma. In the case that $x_{j}$ is not self-dependent,
${\lfloor{{\mathbf{p}}}_{\ell}\rfloor}[j]$ must depend on variables $x_{k}$
with $k\leq j-1\leq i-\ell$.

This lemma is actually formulated for induction; what we are really interested
in is the MP denoted by ${{\mathbf{q}}}_{n}$, for which we introduce a special
notation while enunciating the following corollary:

######  Corollary 23.

Let ${{\mathbf{p}}}_{1},\dots,{{\mathbf{p}}}_{n}$ be similar $\tau$-MPs such
that $\alpha!({{{\mathbf{p}}}_{1}})=\alpha!({{{\mathbf{p}}}_{2}})=\dots$ is
neat. Then
${\lfloor\\!\lfloor{{\mathbf{p}}}_{1}\cdots{{\mathbf{p}}}_{n}\rfloor\\!\rfloor}\stackrel{{\scriptstyle
def}}{{=\;}}{{\mathbf{p}}}_{1}\circ{\lfloor{{\mathbf{p}}}_{2}\rfloor}\cdots\circ{\lfloor{{\mathbf{p}}}_{n}\rfloor}$
is iterative.

_Notation_ : if $S$ is a set of neat, similar $\tau$-MPs as above, we let

${{\lfloor\\!\lfloor S\rfloor\\!\rfloor}}\stackrel{{\scriptstyle
def}}{{=\;}}\\{{\lfloor\\!\lfloor{{\mathbf{p}}}_{1}\>\dots\>{{\mathbf{p}}}_{n}\rfloor\\!\rfloor}\,\mid\,{{\mathbf{p}}}_{1},\dots,{{\mathbf{p}}}_{n}\in
S\\}\,.$

Note that the set ${{\lfloor\\!\lfloor S\rfloor\\!\rfloor}}$ consists of IMPs
(by the above corollary) and it is easy to see that they are neat and similar
to each other. Thus, we have a way to extract a set of IMPs from a certain set
of similar MPs. We will next move to the way in which we compute upper bounds
for sequences of similar MPs using these IMPs. Recall that a $\tau$-MP is
_$\tau$ -closed_ if ${{\mathbf{p}}}^{\tau}={{\mathbf{p}}}$. In particular,
$\tau$-MPs that result directly from generalization (i.e.,
${{\mathbf{q}}}^{\tau}$ for some ${\mathbf{q}}$) are $\tau$-closed. We next
define a special composition operator for $\tau$-closed IMPs, and show an
interesting property that it has. Note that, using the notation of Definition
5 (Page 5), if ${{\mathbf{p}}}$ is a $\tau$-closed IMP then its self-dependent
entries have the form
${{\mathbf{p}}}[i]=x_{i}+\tau{{\mathbf{p}}}[i]^{\prime}$.

[$\tau$-absorbing composition] We introduce a non-standard composition
operation on similar, $\tau$-closed IMPs, denoted by the operator
$\mathop{\star}$ (differing from both ordinary composition $\circ$ and
abstract composition $\mathop{\bullet}$). Specifically,
$({{\mathbf{q}}}\mathop{\star}{{\mathbf{p}}})[i]$ is defined as follows:

  1. (1)

If $i\in{{\textsc{SD}}({\mathbf{q}})}={{\textsc{SD}}({\mathbf{p}})}$, then
$({{\mathbf{q}}}\mathop{\star}{{\mathbf{p}}})[i]\stackrel{{\scriptstyle
def}}{{=\;}}{{\mathbf{p}}}[i]\sqcup\tau({{\mathbf{q}}}[i]^{\prime}\circ{{\mathbf{p}}})=x_{i}+\tau({{\mathbf{p}}}[i]^{\prime}\sqcup({{\mathbf{q}}}[i]^{\prime}\circ{{\mathbf{p}}}))$.

  2. (2)

Otherwise,
$({{\mathbf{q}}}\mathop{\star}{{\mathbf{p}}})[i]\stackrel{{\scriptstyle
def}}{{=\;}}({{\mathbf{q}}}[i]\circ{{\mathbf{p}}})$.

Observe that the difference between
${{\mathbf{q}}}\mathop{\star}{{\mathbf{p}}}$ and
${{\mathbf{q}}}\circ{{\mathbf{p}}}$ is only in the numeric coefficient of some
monomials. In particular, they have the same abstraction:
$\alpha({{\mathbf{q}}}\mathop{\star}{{\mathbf{p}}})=\alpha({{\mathbf{q}}}\circ{{\mathbf{p}}})=\alpha({{\mathbf{q}}})\mathop{\bullet}\alpha({{\mathbf{p}}})$.

Consider the following $\tau$-polynomial:

$\begin{array}[]{lrlllll}&{{\mathbf{p}}}=\langle&x_{1},&x_{2}+\tau
x_{1},&x_{3}+\tau x_{2}+\tau^{2}x_{1},&x_{4}\rangle\\\\[3.0pt] \hbox
to0.0pt{\hss\text{Then:}}\\\
&{{\mathbf{p}}}\mathop{\star}{{\mathbf{p}}}=\langle&x_{1},&x_{2}+\tau
x_{1},&x_{3}+\tau x_{2}+\tau^{2}x_{1},&x_{4}\rangle&={{\mathbf{p}}}\\\\[3.0pt]
\hbox to0.0pt{\hss\text{while:}}\\\
&{{\mathbf{p}}}\circ{{\mathbf{p}}}=\langle&x_{1},&x_{2}+2\tau
x_{1},&x_{3}+2\tau x_{2}+3\tau^{2}x_{1},&x_{4}\rangle.\end{array}$

Thus, the operation keeps (some) coefficients from growing when we compose
$\tau$-MPs. We will see next that this has the desirable result that a
sequence of “$\mathop{\star}$ powers” $\mathcal{T}^{\mathop{\star}(i)}$
(defined analogously to Definition 5 on Page 5) only includes a finite number
of MPs. On the other hand we will prove that it gives a sound upper bound for
a sequence of transitions.

######  Lemma 24.

Let ${\mathbf{p}}$, ${\mathbf{q}}$ be $\tau$-closed, similar IMPs and let
$\sigma$, $\rho$ be weighted traces such that ${\mathbf{p}}$ bounds $\sigma$
and ${\mathbf{q}}$ bounds $\rho$. Then
${{\mathbf{q}}}\mathop{\star}{{\mathbf{p}}}$ bounds $\sigma\rho$.

Compared to Lemma 21, this lemma poses stronger conditions, but has a stronger
conclusion since ${{\mathbf{q}}}\mathop{\star}{{\mathbf{p}}}$ is, in general,
lower than ${{\mathbf{q}}}\circ{{\mathbf{p}}}$.

######  Proof 7.15.

The definition of ${{\mathbf{q}}}\mathop{\star}{{\mathbf{p}}}$ makes the
statement trivial for variables that are not self-dependent. So, let $x_{i}$
be self-dependent. Suppose that
${{\mathbf{x}}\stackrel{{\scriptstyle\sigma}}{{\leadsto}}{\mathbf{y}}}{\>\stackrel{{\scriptstyle\rho}}{{\leadsto}}{\mathbf{z}}}$.
Let $t_{s}={\|\sigma\|}$, $t_{r}={\|\rho\|}$. By assumption,

$\displaystyle z_{i}$ $\displaystyle\leq{{\mathbf{q}}}({\mathbf{y}},t_{r})$
$\displaystyle=y_{i}+t_{r}{{\mathbf{q}}}[i]^{\prime}({\mathbf{y}},t_{r})$
$\displaystyle\leq\left(x_{i}+t_{s}{{\mathbf{p}}}[i]^{\prime}({\mathbf{x}},t_{s})\right)+t_{r}{{\mathbf{q}}}[i]^{\prime}({\mathbf{y}},t_{r})$
$\displaystyle\leq\left(x_{i}+t_{s}{{\mathbf{p}}}[i]^{\prime}({\mathbf{x}},t_{s}+t_{r})\right)+t_{r}({{\mathbf{q}}}[i]^{\prime}\circ{\mathbf{p}})({\mathbf{x}},t_{s}+t_{r})$
$\displaystyle\leq
x_{i}+(t_{s}+t_{r})({{\mathbf{p}}}[i]^{\prime}\sqcup({{\mathbf{q}}}[i]^{\prime}\circ{\mathbf{p}}))({\mathbf{x}},t_{s}+t_{r})$
(by Lemma 20)
$\displaystyle=({{\mathbf{q}}}\mathop{\star}{{\mathbf{p}}})[i](t_{s}+t_{r})\,.$

######  Lemma 25 (The Finite Closure Lemma).

Let $\mathcal{T}$ be a finite set of $\tau$-closed, similar IMPs. Then the set

$\mathcal{T}^{\bigstar}=\bigcup_{k=1}^{\infty}\mathcal{T}^{\mathop{\star}(k)}$

is finite. Hence, there is a number $\ell$ such that
$\mathcal{T}^{\bigstar}=\mathcal{T}^{\mathop{\star}(\ell)}$.

Consider $\mathcal{T}=\\{{{\mathbf{p}}},{{\mathbf{q}}}\\}$ with ${\mathbf{p}}$
from Example 7.2 and

$\begin{array}[]{lrlllll}&{{\mathbf{q}}}=\langle&x_{1}+\tau
x_{4},&x_{2},&x_{3}+\tau x_{4},&x_{4}\rangle.\end{array}$

Then

$\begin{array}[]{lrlllll}&{(\mathcal{T})}^{\mathop{\star}(2)}=&\mathcal{T}\mathop{\star}\mathcal{T}=&\\{{{\mathbf{p}}}\mathop{\star}{{\mathbf{p}}},&{{\mathbf{q}}}\mathop{\star}{{\mathbf{p}}},&{{\mathbf{q}}}\mathop{\star}{{\mathbf{q}}},&{{\mathbf{p}}}\mathop{\star}{{\mathbf{q}}}\\}=\\\
&&&\\{{{\mathbf{p}}},&{{\mathbf{r}}},&{{\mathbf{q}}},&{{\mathbf{r}}}\\}\end{array}$

Where

$\begin{array}[]{lrlllll}&{{\mathbf{r}}}=\langle&x_{1}+\tau x_{4},&x_{2}+\tau
x_{1},&x_{3}+\tau x_{2}+\tau^{2}x_{1}+\tau x_{4},&x_{4}\rangle.\end{array}$

Next, ${(\mathcal{T})}^{\mathop{\star}(3)}$ consists of 8 products, which
contribute only one new element to the accumulated union, namely

$\begin{array}[]{lrlllll}&{{\mathbf{p}}}\mathop{\star}{{\mathbf{r}}}=\langle&x_{1}+\tau
x_{4},&x_{2}+\tau x_{1},&x_{3}+\tau x_{2}+2\tau^{2}x_{1}+\tau x_{1}+\tau
x_{4},&x_{4}\rangle.\end{array}$

Adding ${(\mathcal{T})}^{\mathop{\star}(4)}$ to the union, we only have to
check ${{\mathbf{p}}}\mathop{\star}{{\mathbf{p}}}\mathop{\star}{{\mathbf{r}}}$
and ${{\mathbf{q}}}\mathop{\star}{{\mathbf{p}}}\mathop{\star}{{\mathbf{r}}}$.
It turns out that these $\tau$-MPs have appeared already. Therefore, we have
reached $\mathcal{T}^{\bigstar}$.

######  Proof 7.16.

Define the following sequence:

$\displaystyle T_{(0)}$ $\displaystyle=\mathit{Id}$ $\displaystyle T_{(k+1)}$
$\displaystyle=T_{(k)}\sqcup\ (\bigsqcup\mathcal{T})\circ T_{(k)}\,.$

We prove the following statement by complete induction on $k$:

${{\mathbf{r}}}\in\mathcal{T}^{\bigstar},\ i\leq k\
\Rightarrow{{\mathbf{r}}}[i]\sqsubset T_{(k)}[i]\,.$ (6)

This implies the desired result because it shows that for any $i\leq n$, the
set of values assumed by ${{\mathbf{r}}}[i]$, when ${\mathbf{r}}$ ranges over
$\mathcal{T}^{\bigstar}$, is finite, because it is contained in the down-set
of a single polynomial, namely $T_{(i)}[i]$, and such a down-set is always
finite. Hence, $\mathcal{T}^{\bigstar}$ is finite. It is worthwhile to observe
that since the members of $\mathcal{T}$ are similar IMPs, then, whenever $i$
is a self-dependent variable (in any of them—and then in all),
$\bigsqcup\mathcal{T}$ also has the form $x_{i}+\text{(function of lower
variables)}$ and, consequently, so do the $T_{(k)}$.

To prove (6), fix $k$ and $i\leq k$. We now employ induction on the number $t$
of compositions used to construct ${\mathbf{r}}$ (following the definition of
$\mathcal{T}^{\bigstar}$). The base case is $t=1$, i.e.,
${{\mathbf{r}}}\in\mathcal{T}$ where the result is immediate. In the general
case,

${{\mathbf{r}}}={{\mathbf{q}}}\mathop{\star}{{\mathbf{f}}}$

where ${{\mathbf{q}}}\in\mathcal{T}$ and
${{\mathbf{f}}}\in\mathcal{T}^{\mathop{\star}(t-1)}$.

_Case_ 1: we consider ${{\mathbf{r}}}[i]$ when
$i\in{{\textsc{SD}}({\mathbf{q}})}$. Write

${{\mathbf{q}}}[i]=x_{i}+\tau{{\mathbf{q}}}[i]^{\prime}$

then

${{\mathbf{r}}}[i]=(x_{i}+\tau{{\mathbf{f}}}[i]^{\prime})\sqcup\tau({{\mathbf{q}}}[i]^{\prime}\circ{{\mathbf{f}}})$

Note that ${{\mathbf{q}}}[i]^{\prime}$ only depends on variables $x_{j}$ with
$j<i\leq k$. By the induction hypothesis (of the induction on $k$) we have

${{\mathbf{f}}}[j]\sqsubset T_{(k-1)}[j]$

Consequently

$\tau({{\mathbf{q}}}[i]^{\prime}\circ{{\mathbf{f}}})\sqsubset\left({{\mathbf{q}}}\circ
T_{(k-1)}\right)[i]\sqsubset T_{(k)}[i]\,.$

By the induction hypothesis on $t$,

${{\mathbf{f}}}[i]=x_{i}+\tau{{\mathbf{f}}}[i]^{\prime}\sqsubset T_{(k)}[i]$

and we conclude that

$(x_{i}+\tau{{\mathbf{f}}}[i]^{\prime})\sqcup\tau({{\mathbf{q}}}[i]^{\prime}\circ{{\mathbf{f}}})\sqsubset
T_{(k)}[i]\,\sqcup\,T_{(k)}[i]=T_{(k)}[i]\,.$

_Case_ 2: consider $i\notin{{\textsc{SD}}({\mathbf{q}})}$. Then
${{\mathbf{q}}}[i]$ only depends on self-dependent variables lower than $i$,
hence lower than $k$. By the induction hypothesis on $k$, when $j<k$ we have

${{\mathbf{f}}}[j]\sqsubset T_{(k-1)}[j]$

Consequently

${{\mathbf{r}}}[i]={{\mathbf{q}}}[i]\circ{{\mathbf{f}}}\sqsubset
T_{(k)}[i]\,.$

We are heading towards a central part of the proof, where we construct upper
bounds for sequences of MPs taken from a set $\mathcal{S}$ of similar
$\tau$-MPs. Moreover, we restrict attention to MPs ${\mathbf{p}}$ such that
$\alpha!({{\mathbf{p}}})$ is idempotent. Lemma 25 is used to show that a
finite set of upper bounds covers such traces of any length. However, it
requires the MPs to be $\tau$-closed IMPs. We close this gap by demonstrating
that we can obtain upper bounds for such traces using
${\lfloor\\!\lfloor\mathcal{S}\rfloor\\!\rfloor}^{\tau}$ instead of
$\mathcal{S}$ (the $\tau$ superscript over a set name means that we apply
generalization to all members of the set).

######  Lemma 26.

Let $\mathcal{S}$ be a set of similar $\tau$-MPs such that
$\alpha!({{\mathbf{p}}})$, for ${{\mathbf{p}}}\in\mathcal{S}$, is neat. For
any $t>n$, consider a concrete trace

${{\widetilde{\sigma}}}={s_{0}\xrightarrow{{{\mathbf{p}}}_{1}|w_{1}}s_{1}}\dots
s_{t-1}\xrightarrow{{{\mathbf{p}}}_{t}|w_{t}}s_{t}\,.$

Let
${{\mathbf{r}}}={\lfloor\\!\lfloor{{\mathbf{p}}}_{t}\>\dots\>{{\mathbf{p}}}_{t-n+1}\rfloor\\!\rfloor}$.
Then $s_{t}\leq{{\mathbf{r}}}(s_{t-1},w^{\prime})$ where
$w^{\prime}=\sum_{z=t-n+1}^{t}w_{z}$. In other words, ${{\mathbf{r}}}$ bounds
the last step of $\sigma$ provided that its weight is suitably increased.

The point is to replace ${{\mathbf{p}}}_{t}$ by ${\mathbf{r}}$ as a bound on
the last step, the gain being the convenient form of ${\mathbf{r}}$, namely an
IMP.

######  Proof 7.17.

We use induction on $d$ to prove the following claim for all $0<d\leq n$:

Let
${{\mathbf{r}}}_{d}={\lfloor\\!\lfloor{{\mathbf{p}}}_{t-n+d}\>\dots\>{{\mathbf{p}}}_{t-n+1}\rfloor\\!\rfloor}$
and let $w^{\prime}_{d}=\sum_{z=t-n+1}^{t-n+d}w_{z}$.

Then for $i\leq d$,
$s_{t-n+d}[i]\leq{{\mathbf{r}}}_{d}(s_{t-n+d-1},w^{\prime}_{d})$.

Note that this claim implies the lemma’s statement (setting $d=n$). We now
move to its proof.

_Base case_ : $d=1$. Hence ${{\mathbf{r}}}_{d}={{\mathbf{p}}}_{t-n+1}$. The
claim only concerns $i=1$, and
$s_{t-n+1}[i]\leq{{\mathbf{p}}}_{t-n}(s_{t-n+1},w^{\prime}_{1})[i]$ by
definition.

_Inductive case_ : $d>1$. Then

${{\mathbf{r}}}_{d}={{\mathbf{p}}}_{t-n+d}\circ{\lfloor{{\mathbf{p}}}_{t-n+d-1}\rfloor}\circ\dots\circ{\lfloor{{\mathbf{p}}}_{t-n+1}\rfloor}\,.$

Consider $s_{t-n+d}[i]$, for some $i\leq d$. By assumption,

$s_{t-n+d}[i]={{\mathbf{p}}}_{t-n+d}[i](s_{t-n+d-1},w_{t-n+d})\,.$ (7)

Let us consider the entries $s_{t-n+d-1}[j]$ on which the above expression may
depend; thus $j\leq i$. Let us focus first on the case that $x_{j}$ is self-
dependent. We observe that

$s_{t-n+d-1}[j]=({\lfloor{{\mathbf{p}}}_{t-n+d-1}\rfloor}\circ\dots\circ{\lfloor{{\mathbf{p}}}_{t-n+1}\rfloor})[j](s_{t-n+d-1},w)$
(8)

for any $w$, since ${\lfloor{\mathbf{p}}\rfloor}[j]=x_{j}$ for all
${{\mathbf{p}}}\in\mathcal{S}$ (note that both sides of the equation refer to
$s_{t-n+d-1}$).

When $x_{j}$ is not self-dependent, we have (using the induction hypothesis,
and the definition of self-dependent cut)

$\displaystyle s_{t-n+d-1}[j]$
$\displaystyle\leq({{\mathbf{p}}}_{t-n+d-1}\circ{\lfloor{{\mathbf{p}}}_{t-n+d-2}\rfloor}\circ\dots\circ{\lfloor{{\mathbf{p}}}_{t-n+1}\rfloor})[j](s_{t-n+d-2},w^{\prime}_{d-1})$
(9)
$\displaystyle=({\lfloor{{\mathbf{p}}}_{t-n+d-1}\rfloor}\circ\dots\circ{\lfloor{{\mathbf{p}}}_{t-n+1}\rfloor})[j](s_{t-n+d-2},w^{\prime}_{d-1})$

We now wish to replace $s_{t-n+d-2}$ in the last expression by $s_{t-n+d-1}$.
To this end we apply Lemma 22, establishing that the entries $s_{t-n+d-2}[e]$
that influence the last expression are either self-dependent or have index
$e\leq j-d+1\leq 1$. But in the latter case $e=1$ and $x_{1}$ is certainly
self-dependent. We conclude that ${{\mathbf{p}}}_{t-n+d-1}[e]\geq x_{e}$,
hence $s_{t-n+d-1}[e]\geq s_{t-n+d-2}[e]$. We now obtain from (9) that

$\displaystyle s_{t-n+d-1}[j]$
$\displaystyle\leq({\lfloor{{\mathbf{p}}}_{t-n+d-1}\rfloor}\circ\dots\circ{\lfloor{{\mathbf{p}}}_{t-n+1}\rfloor})[j](s_{t-n+d-2},w^{\prime}_{d-1})$
$\displaystyle\leq({\lfloor{{\mathbf{p}}}_{t-n+d-1}\rfloor}\circ\dots\circ{\lfloor{{\mathbf{p}}}_{t-n+1}\rfloor})[j](s_{t-n+d-1},w^{\prime}_{d-1})\,.$

We substitute this in (7) to obtain

$\displaystyle s_{t-n+d}[i]$
$\displaystyle\leq({{\mathbf{p}}}_{t-n+d}[i]\circ({\lfloor{{\mathbf{p}}}_{t-n+d-1}\rfloor}\circ\dots\circ{\lfloor{{\mathbf{p}}}_{t-n+1}\rfloor}))(s_{t-n+d-1},w^{\prime}_{d-1}+w_{t-n+d})$
$\displaystyle={{\mathbf{r}}}_{d}(s_{t-n+d-1},w^{\prime}_{d})\,.$

######  Lemma 27.

Let $\mathcal{S}$ be a set of similar $\tau$-MPs such that
$\alpha!({{\mathbf{p}}})$, for all ${{\mathbf{p}}}\in\mathcal{S}$, is neat.
Then every weighted trace over $\mathcal{S}$ of length greater than $n$ has an
upper bound in the set
$\left(\left.({{\lfloor\\!\lfloor\mathcal{S}\rfloor\\!\rfloor}}^{\tau})\right.^{\bigstar}\circ{\mathcal{S}}^{(n)}\right)[n\tau/\tau]$.

######  Proof 7.18.

Write such a trace as
$\sigma={s_{0}\xrightarrow{{{\mathbf{p}}}_{1}|w_{1}}s_{1}}\dots
s_{t-1}\xrightarrow{{{\mathbf{p}}}_{t}|w_{t}}s_{t}$. Let $\sigma_{i}$ be the
$i$th step, namely ${s_{i-1}\xrightarrow{{{\mathbf{p}}}_{i}|w_{i}}s_{i}}$. For
each $i>n$, by the last lemma, the $i$th transition is bounded by a $\tau$-MP
${{\mathbf{r}}}\in{{\lfloor\\!\lfloor\mathcal{S}\rfloor\\!\rfloor}}$, with
modified weight. If ${\mathbf{r}}$ bounds a certain transition, then
${{\mathbf{r}}}^{\tau}$ certainly does. Consequently, by Lemmas 21 and 24,
$\sigma_{1}\dots\sigma_{n}\sigma_{n+1}^{\prime}\dots\sigma_{t}^{\prime}$
(where the primed transitions use modified weights) is bounded by a $\tau$-MP
${{\mathbf{q}}}\in\left.({{\lfloor\\!\lfloor\mathcal{S}\rfloor\\!\rfloor}}^{\tau})\right.^{\bigstar}\circ{\mathcal{S}}^{n}$.
In order to get rid of the modified weight, we note that

$\displaystyle{\|\sigma_{1}\dots\sigma_{n}\sigma_{n+1}^{\prime}\dots\sigma_{t}^{\prime}\|}$
$\displaystyle={\|\sigma_{1}\dots\sigma_{n}\|}+\sum_{i=n+1}^{t}{\|\sigma_{i}^{\prime}\|}$
$\displaystyle=\sum_{i=1}^{n}w_{i}+\sum_{i=n+1}^{t}\,\sum_{z=i-n+1}^{i}w_{z}$
$\displaystyle\leq n{\|\sigma\|}$

Thus we see that ${{\mathbf{q}}}[n\tau/\tau]$ bounds $\sigma$ using its
original weight.

Let $\mathcal{S}$ be the SDL under analysis, and $\alpha(\mathcal{S})$ map it
into AMPol. The latter is a monoid with respect to the composition operation,
and we obtain a monoid homomorphism
$\alpha:{\mathcal{S}}^{*}\to{\texttt{AMPol}}$ from abstract traces to AMPol.
The _Factorization Forest Theorem_ of Imre Simon [Sim90] shows that such a
homomorphism induces a useful structure on the traces, provided that the
codomain is a _finite_ monoid. Now, AMPol is, of course, infinite; but if we
assume that the loop under analysis is polynomially bounded, then, as argued
in the proof of termination (Corollary 18), the closure
${Cl(\alpha(\mathcal{S}))}$ is finite. Note that it is a sub-monoid of AMPol.
Thus, Simon’s theorem can be applied. Instead of the original formulation, we
can use a convenient corollary of Simon’s theorem, stated by Bojańczyk [Boj09]
(actually we will not use his formulation but a simplified one, as we do not
need its full power).

In the statement of this result, we refer to $\alpha(\sigma)$, with
$\sigma\in{\mathcal{S}}^{*}$, as the _type_ of $\sigma$. We consider regular
expressions constructed using the operators: concatenation, union and Kleene-
plus (where $E^{+}$ generates the union of all languages generated by $E^{i}$
for $i>0$). A regular expression $E$ over the alphabet $\mathcal{S}$ is _well-
typed_ if for each of its sub-expressions $F$ (including $E$), all words
(traces) generated by $F$ have the same type, which is then the type of the
expression.

######  Theorem 28 (Bojańczyk).

The existence of a homomorphism $\alpha:{\mathcal{S}}^{*}\to M$, where $M$ is
a finite monoid, implies that $\mathcal{S}^{*}$ can be generated by a finite
union of well-typed regular expressions.

Now, all we have to do is prove that the set of AMPs returned by our algorithm
provides upper bounds for all the traces generated by each of these regular
expressions. Note that this theorem highlights the role of _idempotence_ in
AMPol, since for an expression $E^{+}$ to be well-typed, $\alpha(\sigma)$ has
to be the same for all words $\sigma$ generated by $E^{+}$, which implies that
it is an idempotent element.

######  Theorem 29.

Let $\mathcal{S}$ be a polynomially-bounded SDL. Let $\mathcal{A}$ be the set
of abstract $\tau$-MPs returned by Algorithm Solve. Then there is a finite set
$\mathcal{B}\subset{\texttt{$\tau$MPol}}$ such that
$\alpha(\mathcal{B})\subseteq\mathcal{A}$ and for any trace
$\sigma\in{\mathcal{S}}^{*}$ there exists ${{\mathbf{p}}}\in\mathcal{B}$ that
bounds $\sigma$.

######  Proof 7.19.

We consider the regular expressions established by Theorem 28 and all their
sub-expressions: this is a finite set. We construct a set of bounds
${\mathcal{B}}_{E}$, with $\alpha({\mathcal{B}}_{E})\subseteq\mathcal{A}$, for
each such sub-expression $E$, by structural induction on the expressions.
Clearly, this proves the theorem. Importantly, the construction maintains
these properties:

  * •

If expression $E$ has type ${{\mathbf{a}}}\in{\texttt{AMPol}}$ then every
${{\mathbf{p}}}\in{\mathcal{B}}_{E}$ has
$\alpha!({{\mathbf{p}}})={{\mathbf{a}}}$ (intuitively, the algorithm does not
change the shape of the multi-polynomials except by adding $\tau$’s).

  * •

Moreover, ${\mathbf{p}}$ is realizable (this is not hard but requires a bit of
attention since Theorem 17 does not refer to the bounds constructed in the
current proof, but only to $\mathcal{A}$).

If $E$ is a single transition ${\mathbf{p}}$ we set
$\mathcal{B}=\\{{\mathbf{p}}\\}$.

If $E$ is $FG$ we compose ${\mathcal{B}}_{F}$ with ${\mathcal{B}}_{G}$. Note
that
$\alpha({\mathcal{B}}_{G}\circ{\mathcal{B}}_{F})=\alpha({\mathcal{B}}_{G})\mathop{\bullet}\alpha({\mathcal{B}}_{F})\subseteq\mathcal{A}$
thanks to the closure computation. Realizability follows from Lemma 8.

If $E$ is $F+G$ we unite ${\mathcal{B}}_{F}$ with ${\mathcal{B}}_{G}$. Again,
the abstraction of the result is in $\mathcal{A}$.

It remains to consider an expression of the form $F^{+}$. Consider
${\mathcal{B}}_{F}$. By IH, it consists of realizable $\tau$-MPs and are all
similar to a single idempotent AMP, so the requirements of Lemma 27 are
satisfied. Let $\Phi$ be the set of traces generated by $F$. Then every
$\sigma\in\Phi$ has a bound in ${\mathcal{B}}_{F}$. For a concatenation of
$i\leq n$ such traces we have a bound in ${({\mathcal{B}}_{F})}^{(i)}$. For a
concatenation of more than $n$ traces, consider each of these traces as a
weighted transition where the weight represents the trace’s length. By Lemma
27, the concatenation of the traces has a bound in

$\left(\left.({{\lfloor\\!\lfloor\mathcal{B}_{F}\rfloor\\!\rfloor}}^{\tau})\right.^{\bigstar}\circ{\mathcal{B}_{F}}^{(n)}\right)[n\tau/\tau]\,.$
(10)

By Lemma 25, we can replace
$\left.({{\lfloor\\!\lfloor\mathcal{B}_{F}\rfloor\\!\rfloor}}^{\tau})\right.^{\bigstar}$
with
$\left.({{\lfloor\\!\lfloor\mathcal{B}_{F}\rfloor\\!\rfloor}}^{\tau})\right.^{\mathop{\star}(\ell)}$
for some $\ell>0$. Moreover, it is sound to relax the upper bound to
$\left.({\mathcal{B}_{F}}^{\tau})\right.^{\mathop{\star}(\ell)}$. Now (10)
becomes

$\left(\left.({\mathcal{B}_{F}}^{\tau})\right.^{\mathop{\star}(\ell)}\circ{\mathcal{B}_{F}}^{(n)}\right)[n\tau/\tau]\,.$

We claim that this set of upper bounds satisfies all our requirements. For
realizability, all we need is the observation that substituting $n\tau$ for
$\tau$ does not affect realizability; plus Lemma 8 and the fact
${{\mathbf{q}}}\mathop{\star}{{\mathbf{p}}}\leq{{\mathbf{q}}}\circ{{\mathbf{p}}}$.

Finally we look at the abstractions of these $\tau$-MPs, namely the set

$\alpha\left(\left(\left.({\mathcal{B}_{F}}^{\tau})\right.^{\mathop{\star}(\ell)}\circ{\mathcal{B}_{F}}^{(n)}\right)[n\tau/\tau]\right)=\left.({\alpha({\mathcal{B}_{F}})}^{\tau})\right.^{\mathop{\bullet}(\ell)}\mathop{\bullet}{(\alpha({\mathcal{B}_{F}}))}^{\mathop{\bullet}(n)}\,.$

These AMPs are included in the result of Solve, since they they are produced
by closure, generalization and closure again. Note also that the bounds
conform with the type of $F$ (when $\tau$’s are ignored).

##  8\. On the Computational Complexity of our Problem

Our main goal in this research was to establish that the problem of computing
tight bounds is solvable. However, once proved solvable, the question of its
complexity arises. For simplicity we assume that we are only dealing with
programs where all variables are polynomially bounded. We consider the
complexity in terms of three parameters: $|P|$, the size of the program; $n$,
the number of variables; and $d$, the highest degree reached. We note that if
the user wishes to verify a desired degree bound $d$, say check that a program
is at most of cubic time complexity, it is possible to use an abstraction that
truncates exponents higher than $d$ and the complexity will be reduced
accordingly. First, we give an upper bound.444To avoid any confusion, we are
obliged to point out that in the preliminary version (proceedings of FoSSaCS
2019) a wrong expression for the upper bound was given.

######  Theorem 30.

Our algorithm runs in time polynomial in $|P|\cdot{2^{n^{d+1}}}$.

######  Proof 8.1.

We estimate the complexity of our algorithm, based on bounding the number of
different AMPs that may be encountered. The number of monomials over $n$
variables is bounded (for $n>2$) by $n^{d}$ (think of a monomial as a product
of at most $d$ variables. For uniqueness list the indices in descending order.
The number of descending lists of length at most $d$ is bounded by $n^{d}$).
Since a MP is an $n$-tuple of sets of monomials, the number of possible AMPs
is less than ${(2^{n^{d}})}^{n}=2^{n^{d+1}}$.

Next, we consider the running time of the analysis of a loop (independent of
the position of the loop in the program, so we can later just multiply this
time bound by the number of loops in the program). In procedure Solve, a set
of AMPs is maintained and repeatedly enlarged (by applying closure and
generalization), until stable. The time to perform each round of enlargement
is polynomial in the size of the resulting set (more precisely its
representation, but with any reasonable implementation this does not change
much) and the number of rounds is clearly bounded by the size of the final
set. So we deduce that the total time is polynomial in $2^{n^{d+1}}$.

Finally we should add the time to represent non-looping code as a set of AMPs,
and other “book-keeping” operations, but clearly they contribute at most a
polynomial in $|P|$ and the number of AMPs.

Is this a satisfactory upper bound? It seems high, and is probably not tight.
We know, however, that a solution to our problem must use at least exponential
time in the worst case, because it has a potentially high _output size_. There
is a command, of size polynomial in $n$ and $d$, which requires

${(\lfloor n/(2d)\rfloor)}^{\lfloor nd/2\rfloor}$

AMPs to describe its result.

######  Proof 8.2.

We assume that $n$ is even and a multiple of $d$, so we can avoid the “floor”
signs. We use $m=n/2$ variables called $\texttt{X}_{1},\dots,\texttt{X}_{m}$
and $m$ variables called $\texttt{Y}_{1},\dots,\texttt{Y}_{m}$. As usual let
$x_{i}$ denote the initial value in $\texttt{X}_{i}$. For each $j\leq m$ we
write a piece of code that computes

$(x_{1}\lor x_{2}\lor\dots\lor
x_{m/d})\ast\cdots\ast(x_{m-(m/d)+1}\lor\dots\lor x_{m}),$

where the disjunction operator represents a non-deterministic choice. Hence we
choose $d$ values and multiply them together. It should be clear that this
produces one of ${(m/d)}^{d}$ uncomparable monomials, and the result of
analysing this command will have to list all of them. We assign the product to
$\texttt{Y}_{j}$. Since the non-deterministic choices are made independently
for each $j$, to describe the outcome in $\texttt{Y}_{1},\dots,\texttt{Y}_{m}$
we need ${({(m/d)}^{d})}^{m}={(m/d)}^{md}$ uncomparable AMPs.

Thus, as long as we use an explicit AMP representation for the output of our
algorithm, worst-case complexity exponential in $nd$ is unavoidable—at least
for $d$ smaller than $n$. This does not necessarily rule out the applicability
of the algorithm, as some algorithms susceptible to combinatorial explosion
still prove usable in static analysis applications (consider the closure-based
algorithm for Size-Change Termination). At any rate, we intend to complement
the work presented in this article by further research into improving the
algorithm, which we consider only a starting point, being the first complete
algorithm for this problem. We now list some speculations about this future
work. The reader may have noticed that for the “bad” example we used above,
the description would be very compact if we were allowed to use the max
operator and embed it in expressions (for our output bound for each
$\texttt{Y}_{j}$ is just a product of $d$ “max” expressions). But this does
not seem to be a panacea, and we suspect that exponential output size—and
running time, for sure—may be necessary even with max. We leave this as an
open problem; of course, the central problem is to identify the complexity
class of the analysis problem. We can also ask what happens if we redefine our
problem so that the output size is small—a natural example is the case of a
univariate bound; or ask for an output-size dependent complexity function. In
these cases the output-size excuse for exponential complexity does not apply.
Another open problem that is raised by the above considerations is: what is
the best bound on $d$ in terms of $|P|$ and $n$ alone?

##  9\. Algorithm Extensions and Open Problems

In this section we list some ideas about how this research might be extended,