On Multiphase-Linear Ranking Functions

Abstract

Multiphase ranking functions ($M\varPhi$RFs) were proposed as a means to prove the termination of a loop in which the computation progresses through a number of “phases”, and the progress of each phase is described by a different linear ranking function. Our work provides new insights regarding such functions for loops described by a conjunction of linear constraints (single-path loops). We provide a complete polynomial-time solution to the problem of existence and of synthesis of $M\varPhi$RF of bounded depth (number of phases), when variables range over rational or real numbers; a complete solution for the (harder) case that variables are integer, with a matching lower-bound proof, showing that the problem is coNP-complete; and a new theorem which bounds the number of iterations for loops with $M\varPhi$RFs. Surprisingly, the bound is linear, even when the variables involved change in non-linear way. We also consider a type of lexicographic ranking functions more expressive than types of lexicographic functions for which complete solutions have been given so far. We prove that for the above type of loops, lexicographic functions can be reduced to $M\varPhi$RFs, and thus the questions of complexity of detection, synthesis, and iteration bounds are also answered for this class.

This work was funded partially by the Spanish MINECO projects TIN2012-38137 and TIN2015-69175-C4-2-R, and by the CM project S2013/ICE-3006. We thank Mooly Sagiv for providing us with a working space at Tel-Aviv University, which was crucial for completing this work.

1 Introduction

Proving that a program will not go into an infinite loop is one of the most fundamental tasks of program verification, and has been the subject of voluminous research. Perhaps the best known, and often used, technique for proving termination is the ranking function. This is a function f that maps program states into the elements of a well-founded ordered set, such that $f(s) > f(s')$ holds whenever state $s'$ follows state s. This implies termination since infinite descent in a well-founded order is impossible.

Unlike termination of programs in general, which is the fundamental example of undecidability, the algorithmic problems of detection (deciding the existence) or generation (synthesis) of a ranking function can well be solvable, given certain choices of the program representation, and the class of ranking function. Numerous researchers have proposed such classes, with an eye towards decidability; in some cases the algorithmic problems have been completely settled, and efficient algorithms provided, while other cases remain as open problems. Thus, in designing ranking functions, we look for expressivity (to capture more program behaviors) but also want (efficient) computability. Besides proving termination, some classes of ranking functions also serve to bound the length of the computation (an iteration bound), useful in applications such as cost analysis (execution-time analysis, resource analysis) and loop optimization [1, 2, 7, 14].

We focus on single-path linear-constraint loops ($SLC$ loops for short), where a state is described by the values of a finite set of numerical variables, and the effect of a transition (one iteration of the loop) is described by a conjunction of linear constraints. We consider the setting of integer-valued variables, as well as rational-valued (or real-valued) variables¹. Here is an example of this loop representation (a formal definition is in Sect. 2); primed variables $x',y',\dots$ refer to the state following the transition.

$$\begin{aligned} \mathtt {while} ~(x \ge -z)~\mathtt {do} ~x'=x+y,\; y'=y+z,\; z'=z-1 \end{aligned}$$

(1)

Note that by $x'=x+y$ we mean an equation, not an assignment statement; it is a standard procedure to compile sequential code into such equations (if the operations used are linear), or to approximate it using various techniques.

This constraint representation may be extended to represent branching in the loop body, a so-called multiple-path loop; in the current work we do not consider such loops. However, $SLC$ loops are important, e.g., in approaches that reduce a question about a whole program to questions about simple loops [10, 11, 13, 16, 19]; see [21] for references that show the importance of such loops in other fields.

We assume the “constraint loop” to be given, and do not concern ourselves with the orthogonal topic of extracting such loops from general programs.

Types of Ranking Functions. Several types of ranking functions have been suggested; linear ranking functions ($LRFs$) are probably the most widely used and well-understood. In this case, we seek a function $f(x_1,\dots ,x_n) = a_1x_1+\dots +a_n x_n + a_0$, with the rationals as a co-domain, such that (i) $f(\bar{x}) \ge 0$ for any valuation $\bar{x}$ that satisfies the loop constraints (i.e., an enabled state); and (ii) $f(\bar{x})-f(\bar{x}') \ge 1$ for any transition leading from $\bar{x}$ to $\bar{x}'$. Technically, the rationals are not a well-founded set under the usual order, but we can refer to the partial order $a \succeq b$ if and only if $a\ge 0$ and $a\ge b+1$, which is well-founded. Given a linear-constraint loop, it is possible to find a linear ranking function (if one exists) using linear programming ($LP$). This method was found by multiple researchers in different contexts and in some alternative versions [9, 14, 22, 24]. Since $LP$ has a polynomial-time complexity, most of these methods yield polynomial-time algorithms. This method is sound (any ranking function produced is valid), and complete (if there is a ranking function, it will find one), when variables are assumed to range over the rationals. When variables range over the integers, treating the domain as $\mathbb Q$ is safe, but completeness is not guaranteed. Consider the following loop:

$$\begin{aligned} \mathtt {while} ~( x_2-x_1 \le 0,\, x_1+x_2 \ge 1 ) ~\mathtt {do} ~ x_2' = x_2-2x_1+1,\, x_1'=x_1 \end{aligned}$$

(2)

and observe that it does not terminate over the rationals at all (try $x_1=x_2=\frac{1}{2}$); but it has a $LRF$ that is valid for all integer valuations, e.g., $f(x_1,x_2) = x_1+x_2$. Several authors noted this issue, and finally the complexity of a complete solution for the integers was settled by [4], who proved that the detection problem is $\mathtt {coNP}$ -complete and gave matching algorithms.

However, not all terminating loops have a $LRF$; and to handle more loops, one may resort to an argument that combines several $LRFs$ to capture a more complex behavior. Two types of such behavior that re-occur in the literature on termination are lexicographic ranking and multiphase ranking.

Lexicographic Ranking. One can prove the termination of a loop by considering a tuple, say a pair $\langle f_1,f_2 \rangle$ of linear functions, such that either $f_1$ decreases, or $f_1$ does not change and $f_2$ decreases. There are some variants of the definition [2, 4, 5, 17] regarding whether both functions have to be non-negative at all times, or “just when necessary.” The most permissive definition [17] allows any component to be negative, and technically, it ranks states in the lexicographic extension of the order $\succeq$ mentioned above. We refer to this class as $LLRFs$. For example, the following loop

$$\begin{aligned} \mathtt {while} ~(x \ge 0, y \le 10, z \ge 0, z\le 1)~\mathtt {do} ~x'=x+y+z-10, y'=y+z, z'=1-z \end{aligned}$$

(3)

has the $LLRF$ $\langle 4y,4x-4z+1 \rangle$, which is valid only according to [17].

Multiphase Ranking. Consider loop (1) above. Clearly, the loop goes through three phases—in the first, z descends, while the other variables may increase; in the second (which begins once z becomes negative), y decreases; in the last phase (beginning when y becomes negative), x decreases. Note that since there is no lower bound on y or on z, they cannot be used in a $LRF$; however, each phase is clearly finite, as it is associated with a value that is non-negative and decreasing during that phase. In other words, each phase is linearly ranked. We shall say that this loop has the multiphase ranking function ($M\varPhi$RF) $\langle z+1,y+1,x \rangle$. The general definition (Sect. 2) allows for an arbitrary number d of linear components; we refer to d as depth, intuitively it is the number of phases.

Some loops have multiphase behavior which is not so evident as in the last example. Consider the following loop, that we will discuss further in Sect. 6, with $M\varPhi$RF $\langle x-4y, x-2y, x-y \rangle$

$$\begin{aligned} \mathtt {while} ~(x\ge 1,\; y\ge 1,\; x\ge y,\; 4 y\ge x)~\mathtt {do} ~x'=2x,\; y'=3y \end{aligned}$$

(4)

Technically, under which ordering is a $M\varPhi$RF a ranking function? It is quite easy to see that the pairs used in the examples above descend in the lexicographic extension of $\succeq$. This means that $M\varPhi$RFs are a sub-class of $LLRFs$. Note that, intuitively, a lexicographic ranking function also has “phases”, namely, steps where the first component decreases, steps where the second component decreases, etc.; but these phases may alternate an unbounded number of times.

Complete Solutions and Complexity. Complete solutions for $M\varPhi$RFs (over the rationals) appear in [18, 20]. Both use non-linear constraint solving, and therefore do not achieve a polynomial time complexity. [3] study “eventual linear ranking functions,” which are $M\varPhi$RFs of depth 2, and pose the questions of a polynomial-time solution and complete solution for the integers as open problems.

In this paper, we provide complete solutions to the existence and synthesis problems for both $M\varPhi$RFs and $LLRFs$, for rational and integer $SLC$ loops, where the algorithm is parameterized by a depth bound. Over the rationals, the decision problem is PTIME and the synthesis can be done in polynomial time; over the integers, the existence problem is $\mathtt {coNP}$-complete, and our synthesis procedure is deterministic exponential-time.

While such algorithms would be a contribution in itself, we find it even more interesting that our results are mostly based on discovering unexpected equivalences between classes of ranking functions. We prove two such results: Theorem 3 in Sect. 4 shows that $LLRFs$ are not stronger than $M\varPhi$RFs for $SLC$ loops. Thus, the complete solution for $LLRFs$ is just to solve for $M\varPhi$RFs (for the loop (3), we find the $M\varPhi$RF $\langle 4y+x-z,4x-4z+4 \rangle$). Theorem 1 in Sect. 3 shows that one can further reduce the search for $M\varPhi$RFs to a proper sub-class, called nested $M\varPhi$RFs. This class was introduced in [18] because its definition is simpler and allows for a polynomial-time solution (over $\mathbb Q$)².

Our complete solution for the integers is also a reduction—transforming the problem so that solving over the rationals cannot give false alarms. The transformation consists of computing the integer hull of the transition polyhedron. This transformation is well-known in the case of $LRFs$ [4, 12, 14], so it was a natural approach to try, however its proof in the case of $M\varPhi$RFs is more involved.

We also make a contribution towards the use of $M\varPhi$RFs in deriving iteration bounds. As the loop (1) demonstrates, it is possible for the variables that control subsequent phases to grow (at a polynomial rate) during the first phase. Nonetheless, we prove that any $M\varPhi$RF implies a linear bound on the number of iterations for a $SLC$ loop (in terms of the initial values of the variables). Thus, it is also the case that any $LLRF$ implies a linear bound.

An open problem raised by our work is whether one can precompute a bound on the depth of a $M\varPhi$RF for a given loop (if there is one); for example [4] prove a depth bound of n (the number of variables) on their notion of $LLRFs$ (which is more restrictive); however their class is known to be weaker than $M\varPhi$RFs and $LLRFs$. In Sect. 6 we discuss this problem.

The article is organized as follows. Section 2 gives precise definitions and necessary background. Sections 3 and 4 give our equivalence results for different types of ranking functions (over the rationals) and the algorithmic implications. Section 5 covers the integer setting, Sect. 6 discusses depth bounds, Sect. 7 discusses the iteration bound, and Sect. 8 concludes. For closely related work, see the above-mentioned references, while for further background on algorithmic and complexity aspects of linear/lexicographic ranking, we refer the reader to [4].

2 Preliminaries

In this section we define the class of loops we study, the type of ranking functions, and recall some definitions, and properties, regarding (integer) polyhedra.

Single-Path Linear-Constraint Loops. A single-path linear-constraint loop ($SLC$ for short) over n variables $x_1,\ldots ,x_n$ has the form

$$\begin{aligned} \mathtt {while} ~(B\mathbf {x} \le \mathbf {b})~\mathtt {do} ~A\bigl ({\begin{matrix}{\mathbf {x}}\\ {\mathbf {x}'}\end{matrix}}\bigr ) \le \mathbf {c} \end{aligned}$$

where $\mathbf {x}=(x_1,\ldots ,x_n)^{\tiny {\text{ T }}}$ and $\mathbf {x}'=(x_1',\ldots ,x_n')^{\tiny {\text{ T }}}$ are column vectors, and for some $p,q>0$, $B \in {\mathbb Q}^{p\times n}$, $A\in {\mathbb Q}^{q\times 2n}$, $\mathbf {b}\in {\mathbb Q}^p$, $\mathbf {c}\in {\mathbb Q}^q$. The constraint $B\mathbf {x} \le \mathbf {b}$ is called the loop condition (a.k.a. the loop guard) and the other constraint is called the update. We say that the loop is a rational loop if $\mathbf {x}$ and $\mathbf {x}'$ range over $\mathbb Q ^n$, and that it is an integer loop if they range over $\mathbb Z ^n$. One could also allow variables to take any real-number value, but as long as the constraints are expressed by rational numbers, our results for $\mathbb Q$ also apply to $\mathbb R$.

We say that there is a transition from a state $\mathbf {x}\in \mathbb Q ^n$ to a state $\mathbf {x}'\in \mathbb Q ^n$, if $\mathbf {x}$ satisfies the condition and $\mathbf {x}$ and $\mathbf {x}'$ satisfy the update. A transition can be seen as a point $\bigl ({\begin{matrix}{\mathbf {x}}\\ {\mathbf {x}'}\end{matrix}}\bigr ) \in \mathbb Q ^{2n}$, where its first n components correspond to $\mathbf {x}$ and its last n components to $\mathbf {x}'$. For ease of notation, we denote $\bigl ({\begin{matrix}{\mathbf {x}}\\ {\mathbf {x}'}\end{matrix}}\bigr )$ by $\mathbf {x}''$. The set of all transitions $\mathbf {x}''\in \mathbb Q ^{2n}$, of a given $SLC$ loop, will be denoted by ${\mathcal Q}$ and is specified by the constraints in the loop body and update. It is a polyhedron (see below), which we call the transition polyhedron. For the purpose of this article, the essence of the loop is this polyhedron, even if the loop is presented in a more readable form as above.

Multi-phase Ranking Functions. An affine function $f: \mathbb Q ^n \rightarrow \mathbb Q$ is of the form $f(\mathbf {x}) = \vec {a}\cdot \mathbf {x} + a_0$ where $\vec {a}\in \mathbb Q ^n$ is a row vector and $a_0\in \mathbb Q$. For a given function f, we define the function $\varDelta f:\mathbb Q ^{2n}\mapsto \mathbb Q$ as $\varDelta f(\mathbf {x}'')=f(\mathbf {x})-f(\mathbf {x}')$.

Definition 1

Given a set of transitions $T\subseteq \mathbb Q ^{2n}$, we say that $\tau =\langle f_1,\dots ,f_d \rangle$ is a $M\varPhi$RF (of depth d) for T if for every $\mathbf {x}'' \in T$ there is an index $i\in [1,d]$ such that:

$$\begin{aligned} \forall j \le i.\ \varDelta f_j(\mathbf {x}'')&\ge 1, \end{aligned}$$

(5)

$$\begin{aligned} f_i(\mathbf {x})&\ge 0, \end{aligned}$$

(6)

$$\begin{aligned} \forall j < i.\ f_j(\mathbf {x})&\le 0. \end{aligned}$$

(7)

We say that $\mathbf {x}''$ is ranked by $f_i$ (for the minimal such i).

It is not hard to see that this definition, for $d=1$, means that $f_1$ is a linear ranking function, and for $d>1$, it implies that as long as $f_1(\mathbf {x}) \ge 0$, transition $\mathbf {x}''$ must be ranked by $f_1$, and when $f_1(\mathbf {x}) < 0$, $\langle f_2,\dots ,f_d \rangle$ becomes a $M\varPhi$RF. This agrees with the intuitive notion of “phases.” We further note that, for loops specified by polyhedra, making the inequality (7) strict results in the same class of ranking functions (we chose the definition that is easier to work with), and, similarly, we can replace (5) by $\varDelta f_j(\mathbf {x}'') > 0$, obtaining an equivalent definition (up to multiplication of the $f_i$ by some constants). We say that $\tau$ is irredundant if removing any component invalidates the $M\varPhi$RF.

The decision problem Existence of a $M\varPhi RF$ asks to determine whether a given $SLC$ loop admits a $M\varPhi$RF. The bounded decision problem, denoted by $\text {BM}{\varPhi }\text {RF}(\mathbb Q)$ and $\text {BM}{\varPhi }\text {RF}(\mathbb Z)$, restricts the search to $M\varPhi$RFs of depth at most d, where the parameter d is part of the input.

Polyhedra. A rational convex polyhedron ${\mathcal P} \subseteq \mathbb Q ^n$ (polyhedron for short) is the set of solutions of a set of inequalities $A\mathbf {x} \le \mathbf {b}$, namely ${\mathcal P}=\{ \mathbf {x}\in \mathbb Q ^n \mid A\mathbf {x} \le \mathbf {b} \}$, where $A \in \mathbb Q ^{m \times n}$ is a rational matrix of n columns and m rows, $\mathbf {x}\in \mathbb Q ^n$ and $\mathbf {b} \in \mathbb Q ^m$ are column vectors of n and m rational values respectively. We say that ${\mathcal P}$ is specified by $A\mathbf {x} \le \mathbf {b}$. If $\mathbf {b}=\mathbf {0}$, then ${\mathcal P}$ is a cone. The set of recession directions of a polyhedron ${\mathcal P}$ specified by $A\mathbf {x} \le \mathbf {b}$, also know as its recession cone, is the set $\{ \mathbf {y}\in \mathbb Q ^n \mid A\mathbf {y} \le \mathbf {0}\}$. For a given polyhedron ${\mathcal P} \subseteq \mathbb Q ^n$ we let $I({{\mathcal P}})$ be ${\mathcal P} \cap \mathbb Z ^n$, i.e., the set of integer points of ${\mathcal P}$. The integer hull of ${\mathcal P}$, commonly denoted by ${{\mathcal P}}_I$, is defined as the convex hull of $I({{\mathcal P}})$, i.e., every rational point of ${{\mathcal P}}_I$ is a convex combination of integer points. It is known that ${{\mathcal P}}_I$ is also a polyhedron, and that ${\mathtt {rec.cone}}({\mathcal P})={\mathtt {rec.cone}}({{\mathcal P}}_I)$ [23, Theorem 16.1, p. 231]. An integer polyhedron is a polyhedron ${\mathcal P}$ such that ${\mathcal P} = {{\mathcal P}}_I$. We also say that ${\mathcal P}$ is integral.

Next we state a lemma that is fundamental for many proofs in this article. Given a polyhedron ${\mathcal P}$, the lemma shows that if a disjunction of constraints of the form $f_i > 0$, or $f_i \ge 0$, holds over ${\mathcal P}$, then a certain conic combination of these functions is non-negative over ${\mathcal P}$.

Lemma 1

Fix $\vartriangleright$ to be either > or $\ge$. Given a polyhedron ${\mathcal P}\ne \emptyset$, and linear functions $f_1,\ldots ,f_k$ such that  

(i):

$\mathbf {x}\in {\mathcal P} \rightarrow f_1(\mathbf {x}) \vartriangleright 0 \vee \cdots \vee f_{k-1}(\mathbf {x}) \vartriangleright 0 \vee f_k(\mathbf {x}) \ge 0$

(ii):

$\mathbf {x}\in {\mathcal P} \not \rightarrow f_1(\mathbf {x}) \vartriangleright 0 \vee \cdots \vee f_{k-1}(\mathbf {x}) \vartriangleright 0$

  There exist non-negative constants $\mu _1,\ldots ,\mu _{k-1}$ such that $\mathbf {x}\in {\mathcal P} \rightarrow \mu _1 f_1(\mathbf {x})+\cdots + \mu _{k-1} f_{k-1}(\mathbf {x})+ f_{k}(\mathbf {x}) \ge 0$.

Proof

We prove the lemma in one version; the other is very similar. Specifically, we assume:  

(i):

$\mathbf {x}\in {\mathcal P} \rightarrow f_1(\mathbf {x})> 0 \vee \cdots \vee f_{k-1}(\mathbf {x}) > 0 \vee f_k(\mathbf {x}) \ge 0$

(ii):

$\mathbf {x}\in {\mathcal P} \not \rightarrow f_1(\mathbf {x})> 0 \vee \cdots \vee f_{k-1}(\mathbf {x}) > 0$.

 

Let ${\mathcal P}$ be $B\mathbf {x} \le \mathbf {c}$, $f_i = \vec {a}_i\cdot \mathbf {x}-b_i$, then (i) is equivalent to infeasibility of

$$\begin{aligned} B\mathbf {x} \le \mathbf {c} \wedge A\mathbf {x} \le \mathbf {b} \wedge \vec {a}_k\cdot \mathbf {x} < b_k \end{aligned}$$

(8)

where A consists of the $k-1$ rows $\vec {a}_i$, and $\mathbf {b}$ of corresponding $b_i$. However, $B\mathbf {x}\le \mathbf {c} \wedge A\mathbf {x}\le \mathbf {b}$ is assumed to be feasible.

According to Motzkin’s transposition theorem [23, Corollary 7.1k, p. 94], this implies that there are row vectors $\vec {\lambda }, \vec {\lambda }' \ge 0$ and a constant $\mu \ge 0$ such that the following is true:

$$\begin{aligned} \vec {\lambda }B+\vec {\lambda }'A + \mu a_k = 0 \wedge \vec {\lambda }\mathbf {c} + \vec {\lambda }'\mathbf {b} + \mu b_k \le 0 \wedge ( \mu \ne 0 \vee \vec {\lambda }\mathbf {c} + \vec {\lambda }'\mathbf {b} + \mu {b_k} < 0 ) \end{aligned}$$

(9)

Now, if (9) is true, then for all $\mathbf {x}\in {\mathcal P}$,

$$\begin{aligned} (\sum _i \lambda '_i f_i (\mathbf {x}) ) + \mu f_k(\mathbf {x})&= \vec {\lambda }'A\mathbf {x} - \vec {\lambda }'\mathbf {b} + \mu a_k\mathbf {x} - \mu b_k \\&= -\vec {\lambda }B\mathbf {x} - \vec {\lambda }'\mathbf {b} -\mu b_k \ge -\vec {\lambda }\mathbf {c} - \vec {\lambda }' \mathbf {b} - \mu b_k \ge 0 \end{aligned}$$

where if $\mu = 0$, the last inequality must be strict. However, if $\mu = 0$, then $\vec {\lambda }B + \vec {\lambda }'A = 0$, so by feasibility of $B\mathbf {x}\le \mathbf {c}$ and $A\mathbf {x}\le \mathbf {b}$, this implies $\vec {\lambda }\mathbf {c} + \vec {\lambda }'\mathbf {b} \ge 0$, a contradiction. Thus, $(\sum _i \lambda '_i f_i ) + \mu f_k\ge 0$ on ${\mathcal P}$ and $\mu > 0$. Dividing by $\mu$ we obtain the conclusion of the lemma.    $\square$

3 Complexity of Synthesis of $M\varPhi$RFs  over the Rationals

In this section we study the complexity of deciding if a given rational $SLC$ loop has a $M\varPhi$RF of depth d, and show that this can be done in polynomial time. These results follow from an equivalence between $M\varPhi$RFs and a sub-class called nested ranking functions [18]. In the rest of this article we assume a given $SLC$ loop specified by a transition polyhedron ${\mathcal Q}$. The complexity results are in terms of the bit-size of the a constraint representation of ${\mathcal Q}$ (see Sect. 2 of [4]).

Definition 2

A d-tuple $\tau = \langle f_1,\dots ,f_d \rangle$ is a nested ranking function for ${\mathcal Q}$ if the following are satisfied for all $\mathbf {x}'' \in {\mathcal Q}$ (where $f_0 \equiv 0$ for uniformity)

$$\begin{aligned} f_d(\mathbf {x}) \ge 0 \end{aligned}$$

(10)

$$\begin{aligned} (\varDelta f_i(\mathbf {x}'') - 1) + f_{i-1}(\mathbf {x}) \ge 0&\quad \quad \quad&\text {for all } i=1,\dots ,d. \end{aligned}$$

(11)

It is easy to see that a nested ranking function is a $M\varPhi$RF. Indeed, $f_1$ is decreasing, and when it becomes negative $f_2$ starts to decrease, etc. Moreover, the loop must stop by the time that $f_d$ becomes negative, since $f_d$ is non-negative over ${\mathcal Q}$ (more precisely, on the projection of ${\mathcal Q}$ to its first n coordinates—as $f_i$ is a function of state).

Example 1

Consider loop (1) (at Page 2). It has the $M\varPhi$RF $\langle z+1,y+1,x \rangle$ which is not nested because, among other things, last component x might be negative, e.g., for the state $x=-1, y=0, z=1$. However, it has the nested ranking function $\langle z+1,y+1,z+x \rangle$, which is $M\varPhi$RF.

The above example shows that there are $M\varPhi$RFs which are not nested ranking functions, however, next we show that if a loop has a $M\varPhi$RF then it has a (possibly different) nested ranking function of the same depth. We first state an auxiliary lemma, and then prove the main result.

Lemma 2

Let $\tau =\langle f_1,\ldots ,f_d \rangle$ be an irredundant $M\varPhi$RF for ${\mathcal Q}$, such that $\langle f_2,\dots ,f_d \rangle$ is a nested ranking function for ${\mathcal Q}' = {\mathcal Q}\cap \{\mathbf {x}''\in \mathbb Q ^{2n} \mid f_1(\mathbf {x}) \le 0 \}$. Then there is a nested ranking function of depth d for ${\mathcal Q}$.

Proof

First recall that, by definition of $M\varPhi$RF, we have $\varDelta f_1(\mathbf {x}'')\ge 1$ for any $\mathbf {x}''\in {\mathcal Q}$, and since $\langle f_2,\dots ,f_d \rangle$ is a nested ranking function for ${\mathcal Q}'$ we have

$$\begin{aligned} \begin{aligned} \mathbf {x}''\in {\mathcal Q}' \rightarrow&f_d(\mathbf {x}) \ge 0\\ \mathbf {x}''\in {\mathcal Q}' \rightarrow&(\varDelta f_2(\mathbf {x}'')-1) \ge 0 \ \wedge \\&(\varDelta f_3(\mathbf {x}'')-1)+f_2(\mathbf {x}'') \ge 0 \ \wedge \\&\cdots \\&(\varDelta f_d(\mathbf {x}'')-1)+f_{d-1}(\mathbf {x}'') \ge 0 \end{aligned} \end{aligned}$$

(12)

Next we construct a nested ranking function $\langle f_1',\ldots ,f_d' \rangle$ for ${\mathcal Q}$, i.e., such that (10) is satisfied for $f_d'$, and (11) is satisfied for each $f'_i$ and $f'_{i-1}$ — we refer to the instance of (11) for a specific i as (11 $_{i}$).

We start with the condition (10). If $f_d$ is non-negative over ${\mathcal Q}$ we let $f_d'=f_d$, otherwise, clearly $\mathbf {x}''\in {\mathcal Q}\rightarrow f_d(\mathbf {x}) \ge 0 \vee f_1(\mathbf {x}) > 0 \,.$ Then, by Lemma 1 there is a constant $\mu _d>0$ such that $\mathbf {x}''\in {\mathcal Q}\rightarrow f_d(\mathbf {x})+ \mu _d f_1(\mathbf {x}) \ge 0$ and we define $f_d'(\mathbf {x}) = f_d(\mathbf {x}) + \mu _d f_1(\mathbf {x})$. Clearly (10) holds for $f_d'$.

Next, we handle the conditions (11 $_{i}$) for $i=d,\dots , 3$ in this order. When we handle (11 $_{i}$), we shall define $f'_{i-1}(\mathbf {x}) = f_{i-1}(\mathbf {x})+\mu _{i-1} f_1(\mathbf {x})$ for some $\mu _{i-1} \ge 0$. Note that $f'_d$ has this form. Suppose we have computed $f_d',\dots ,f_{i}'$. The construction of $f'_{i-1}$ will ensure that (11 $_{i}$) holds over ${\mathcal Q}$. From (12) we know that

$$\begin{aligned} \mathbf {x}''\in {\mathcal Q}' \rightarrow (\varDelta f_i(\mathbf {x}'')-1)+f_{i-1}(\mathbf {x}'') \ge 0. \end{aligned}$$

Now since $f'_{i}(\mathbf {x}) = f_i(\mathbf {x})+\mu _i f_1(\mathbf {x})$, and $\varDelta f_1(\mathbf {x}'') \ge 1$ over ${\mathcal Q}$, we have

$$\begin{aligned} \mathbf {x}''\in {\mathcal Q}' \rightarrow (\varDelta f'_i(\mathbf {x}'')-1)+f_{i-1}(\mathbf {x}'') \ge 0. \end{aligned}$$

Now if ($\varDelta f'_i(\mathbf {x}'')-1)+f_{i-1}(\mathbf {x}'') \ge 0$ holds over ${\mathcal Q}$ as well, we let $f_{i-1}'=f_{i-1}$. Otherwise, we have

$$\begin{aligned} \mathbf {x}''\in {\mathcal Q}\rightarrow (\varDelta f'_i(\mathbf {x}'') - 1) + f_{i-1}(\mathbf {x}) \ge 0 \vee f_1(\mathbf {x})>0, \end{aligned}$$

and by Lemma 1 there is $\mu _{i-1} > 0$ such that

$$\begin{aligned} \mathbf {x}''\in {\mathcal Q}\rightarrow (\varDelta f'_i(\mathbf {x}'') - 1) + f_{i-1}(\mathbf {x}) + \mu _{i-1} f_1(\mathbf {x}) \ge 0. \end{aligned}$$

In this case, we let $f'_{i-1}(\mathbf {x}) = f_{i-1}(\mathbf {x}) + \mu _{i-1} f_1(\mathbf {x})$. Clearly (11 $_{i}$) holds.

We proceed to (11 $_{2}$). From (12) we know that

$$\begin{aligned} \mathbf {x}''\in {\mathcal Q}' \rightarrow (\varDelta f_2(\mathbf {x}'')-1) \ge 0. \end{aligned}$$

Since $f_2'(\mathbf {x})=f_2(\mathbf {x})+\mu _2 f_1(\mathbf {x})$ and $\varDelta f_1(\mathbf {x}'') \ge 1$ we have

$$\begin{aligned} \mathbf {x}''\in {\mathcal Q}' \rightarrow (\varDelta f'_2(\mathbf {x}'') - 1) \ge 0. \end{aligned}$$

Next, by definition of ${\mathcal Q}'$ and the Lemma’s assumption we have

$$\begin{aligned} \mathbf {x}''\in {\mathcal Q}\rightarrow (\varDelta f'_2(\mathbf {x}'') - 1) \ge 0 \vee f_1(\mathbf {x}) > 0 \end{aligned}$$

and we also know that $(\varDelta f'_2(\mathbf {x}'') - 1) \ge 0$ does not hold over ${\mathcal Q}$, because then $f_1$ would be redundant. Now by Lemma 1 there is $\mu _1 > 0$ such that

$$\begin{aligned} \mathbf {x}''\in {\mathcal Q}\rightarrow (\varDelta f'_2(\mathbf {x}'') - 1) + \mu _1 f_1(\mathbf {x}) \ge 0. \end{aligned}$$

We let $f_1'(\mathbf {x})=\mu _1 f_1(\mathbf {x})$. For (11 $_{1}$) we need to show that $\varDelta f'_1(\mathbf {x}'') - 1 \ge 0$ holds over ${\mathcal Q}$, which clearly holds if $\mu _1\ge 1$ since $\varDelta f_1(\mathbf {x}'')\ge 1$; otherwise we multiply all $f_i'$ by $\frac{1}{\mu _1}$, which does not affect any (11 $_{i}$) and makes (11 $_{1}$) true.    $\square$

Theorem 1

If ${\mathcal Q}$ has a $M\varPhi$RF of depth d, then it has a nested ranking function of depth at most d.

Proof

The proof is by induction on d. We assume a $M\varPhi$RF $\langle f_1,\ldots ,f_d \rangle$ for ${\mathcal Q}$. For $d=1$ there is no difference between a general $M\varPhi$RF and a nested one. For $d>1$, we consider $\langle f_2,\dots ,f_d \rangle$ as a $M\varPhi$RF for ${\mathcal Q}' = {\mathcal Q}\cap \{ \mathbf {x}''\in \mathbb Q ^{2n} \mid f_1(\mathbf {x}) \le 0\}$, we apply the induction hypothesis to turn $\langle f_2,\dots ,f_d \rangle$ into a nested $M\varPhi$RF. Either $f_1$ becomes redundant, or we can apply Lemma 2.    $\square$

The above theorem gives us a complete algorithm for the synthesis of $M\varPhi$RFs of a given depth d for ${\mathcal Q}$, namely, just synthesize a nested $M\varPhi$RF.

Theorem 2

$\text {BM}{\varPhi }\text {RF}(\mathbb Q) \in \mathtt {PTIME}$.

Proof

We describe, concisely, how to determine if a nested $M\varPhi$RF exists, and then synthesize one, in polynomial time (this actually appears in [18]). Given ${\mathcal Q}$, our goal is to find $f_1,\ldots ,f_d$ such that (10), (11) hold. If we take just one of the conjuncts, our task is to find coefficients for the functions involved ($f_d$, or $f_i$ and $f_{i-1}$), such that the desired inequality is implied by ${\mathcal Q}$. Using Farkas’ lemma [23], this problem can be formulated as a $LP$ problem, where the coefficients we seek are unknowns. By conjoing all these $LP$ problems, we obtain a single $LP$ problem, of polynomial size, whose solution—if there is one—provides the coefficients of all the $f_i$; and if there is no solution, then no nested $M\varPhi$RF exists. Since $LP$ is polynomial-time, this procedure has polynomial time complexity.    $\square$

Clearly, if d is considered as constant, then $\text {BM}\varPhi {RF}(\mathbb {Q})$ is polynomial in the bit-size of ${\mathcal Q}$. When considering d as variable, then the complexity is polynomial in the bit-size of ${\mathcal Q}$ plus d—equivalently, it is polynomial in the bit-size of the input if we assume that d is given in unary representation (which is a reasonable assumption since d describes the number of components of the $M\varPhi$RF sought).

4 Multiphase vs Lexicographic-Linear Ranking Functions

$M\varPhi$RFs are similar to $LLRFs$, and a natural question is: which one is more powerful for proving termination of $SLC$ loops? In this section we show that they have the same power, by proving that an $SLC$ has a $M\varPhi$RF if and only if it has a $LLRF$. We first note that there are several definitions for $LLRFs$  [2, 4, 5, 17]. The following is the most general [17].

Definition 3

Given a set of transitions $T\subseteq \mathbb Q ^{2n}$, we say that $\langle f_1,\dots ,f_d \rangle$ is a $LLRF$ (of depth d) for T if for every $\mathbf {x}'' \in T$ there is an index i such that:

$$\begin{aligned} \forall j < i.\ \varDelta f_j(\mathbf {x}'')&\ge 0, \\ \end{aligned}$$

(13)

$$\begin{aligned} \varDelta f_i(\mathbf {x}'')&\ge 1, \\ \end{aligned}$$

(14)

$$\begin{aligned} f_i(\mathbf {x})&\ge 0, \end{aligned}$$

(15)

We say that $\mathbf {x}''$ is ranked by $f_i$ (for the minimal such i).

Regarding other definitions: [4] requires $f_j(\mathbf {x})\ge 0$ for all $f_j$ with $j\le i$, and [2] requires it for all components. Actually [2] shows that an $SLC$ loop has a $LLRF$ according to their definition if and only if it has a $LRF$, which is not the case of [4]. The definition in [5] (which do not present here) is equivalent to a $LRF$ when considering $SLC$ loops, as their main interest is in multipath loops.

It is easy to see that a $M\varPhi$RF is also a $LLRF$ as in Definition 3. Next we show that for $SLC$ loops any $LLRF$ can be converted to a $M\varPhi$RF, proving that these classes of ranking functions have the same power for $SLC$ loops. We start with an auxiliary lemma.

Lemma 3

Let f be a non-negative linear function over ${\mathcal Q}$. If ${\mathcal Q}' = {\mathcal Q}\cap \{\mathbf {x}''\mid {\varDelta f(\mathbf {x}'')\le 0}\}$ has a $M\varPhi$RF of depth d, then ${\mathcal Q}$ has one of depth at most $d+1$.

Proof

Note that appending f to a $M\varPhi$RF $\tau$ of ${\mathcal Q}'$ does not always produce a $M\varPhi$RF, since the components of $\tau$ are not guaranteed to decrease over ${\mathcal Q}\setminus {\mathcal Q}'$. Let $\tau =\langle g_1,\ldots ,g_d \rangle$ be a $M\varPhi$RF for ${\mathcal Q}'$, we construct a $M\varPhi$RF $\langle g_1',\ldots ,g_d',f \rangle$ for ${\mathcal Q}$. If $g_1$ is decreasing over ${\mathcal Q}$, we define $g_1'(\mathbf {x})=g_1(\mathbf {x})$. Otherwise, we have

$$\begin{aligned} \mathbf {x}''\in {\mathcal Q}\rightarrow \varDelta f(\mathbf {x}'')>0 \vee \varDelta g_1(\mathbf {x}'') \ge 1. \end{aligned}$$

Therefore, by Lemma 1, we can construct $g_1'(\mathbf {x})=g_1(\mathbf {x})+\mu f(\mathbf {x})$ such that $\mathbf {x}''\in {\mathcal Q}\rightarrow \varDelta g_1'(\mathbf {x}'') \ge 1$. Moreover, since f is non-negative, $g_1'$ is non-negative on the transitions on which $g_1$ is non-negative. If $d>1$, we proceed with ${\mathcal Q}^{(1)} = {\mathcal Q}\cap \{\mathbf {x}''\mid g_1'(\mathbf {x}) \le (-1)\}$. Note that these transitions must be ranked, in ${\mathcal Q}'$, by $\langle g_2,\dots ,g_d \rangle$. If $g_2$ is decreasing over ${\mathcal Q}^{(1)}$, let $g_2'=g_2$, otherwise

$$\begin{aligned} \mathbf {x}''\in {\mathcal Q}^{(1)} \rightarrow \varDelta f(\mathbf {x}'')>0 \vee \varDelta g_2(\mathbf {x}'') \ge 1, \end{aligned}$$

and again by Lemma 1 we can construct the desired $g_2'$. In general for any $j\le d$ we construct $g_{j+1}'$ such that $\varDelta g_{j+1}' \ge 1$ over

$$\begin{aligned} {\mathcal Q}^{(j)} = {\mathcal Q}\cap \{\mathbf {x}''\in \mathbb Q ^{2n}\mid g_1'(\mathbf {x}) \le (-1) \wedge \dots \wedge g_{j}'(\mathbf {x}) \le (-1) \} \end{aligned}$$

and $\mathbf {x}''\in {\mathcal Q}\wedge g_j(\mathbf {x}) \ge 0 \rightarrow g_j'(\mathbf {x}) \ge 0$. Finally we define

$$\begin{aligned} {\mathcal Q}^{(d)} = {\mathcal Q}\cap \{\mathbf {x}''\in \mathbb Q ^{2n}\mid g_1'(\mathbf {x}) \le (-1) \wedge g_d'(\mathbf {x}) \le (-1) \}, \end{aligned}$$

each transition $\mathbf {x}''\in {\mathcal Q}^{(d)}$ must satisfy $\varDelta f(\mathbf {x}'')>0$, and in such case $\varDelta f(\mathbf {x}'')$ must have a minimum $c > 0$ since ${\mathcal Q}^{(d)}$ is a polyhedron. Without loss of generality we assume $c \ge 1$, otherwise take $\frac{1}{c}f$ instead of f. Now $\tau '=\langle g_1'+1,\dots ,g_d'+1,f \rangle$ is a $M\varPhi$RF for ${\mathcal Q}$. Note that if we arrive to ${\mathcal Q}^{(j)}$ that is empty, we can stop since we already have a $M\varPhi$RF.    $\square$

In what follows, by a weak $LLRF$ we mean the class of ranking functions obtained by changing condition (14) to $\varDelta f_i(\mathbf {x}'') > 0$. Clearly it is more general than $LLRFs$, and as we will see next it suffices to guarantee termination, since we show how to convert them to $M\varPhi$RFs. We prefer to use this class as it simplifies the proof for the integer case that we present in Sect. 5.

Lemma 4

Let $\langle f_1,\ldots ,f_d \rangle$ be a weak $LLRF$ for ${\mathcal Q}$. There is a linear function g that is positive over ${\mathcal Q}$, and decreasing on (at least) the same transitions of $f_i$, for some $1\le i\le d$.

Proof

If any $f_i$ is positive over ${\mathcal Q}$, we take $g=f_i$. Otherwise, we have $\mathbf {x}''\in {\mathcal Q}\rightarrow f_1(\mathbf {x})\ge 0 \vee \cdots \vee f_d(\mathbf {x}) \ge 0$ since every transition is ranked by some $f_i$. If this implication satisfies the conditions of Lemma 1 then we can construct $g(\mathbf {x})=f_d(\mathbf {x})+\sum _{i=1}^{d-1}\mu _if_i(\mathbf {x})$ that is non-negative over ${\mathcal Q}$, and, moreover, decreases on the transitions ranked by $f_d$. If the conditions of Lemma 1 are not satisfied, then the second condition must be false, that is, $\mathbf {x}''\in {\mathcal Q}\rightarrow f_1(\mathbf {x})\ge 0 \vee \cdots \vee f_{d-1}(\mathbf {x})\ge 0$. Now we repeat the same reasoning as above for this implication. Eventually we either construct g that corresponds for some $f_i$ as above, or we arrive to $\mathbf {x}''\in {\mathcal Q}\rightarrow f_1(\mathbf {x})\ge 0$, and then take $g=f_1$.    $\square$

Theorem 3

If ${\mathcal Q}$ has a weak $LLRF$ of depth d, it has a $M\varPhi$RF of depth d.

Proof

Let $\langle f_1,\ldots ,f_d \rangle$ be a weak $LLRF$ for ${\mathcal Q}$. We construct a corresponding $M\varPhi$RF. The proof is by induction on the depth d of the $LLRF$. For $d=1$ it is clear since it is an $LRF$.³ Now let $d>1$, by Lemma 4 we can find g that is positive over ${\mathcal Q}$ and decreasing at least on the same transitions as $f_i$. Now $\langle f_1,\ldots ,f_{i-1},f_{i+1},\dots ,f_d \rangle$ is a weak $LLRF$ of depth $d-1$ for ${\mathcal Q}'= {\mathcal Q}\cap \{\mathbf {x}''\mid \varDelta g(\mathbf {x''})\le 0 \}$. By the induction hypothesis we can construct a weak $M\varPhi$RF for ${\mathcal Q}'$ of depth $d-1$, and by Lemma 3 we can lift it to one of depth d for ${\mathcal Q}$.    $\square$

Example 2

Let ${\mathcal Q}$ be the transition polyhedron of the loop (3) (on Page 3), which admits the $LLRF$ $\langle 4y,4x-4z+4 \rangle$, and note that it is not a $M\varPhi$RF. Following the proof of above theorem, we can convert it to the $M\varPhi$RF $\langle 4y+x-z,4x-4z+4 \rangle$.

5 $M\varPhi$RFs and $LLRFs$ over the Integers

The procedure of Sect. 3 for synthesizing $M\varPhi$RFs, i.e., use $LP$ to synthesize a nested ranking function, is complete for rational loops but not for integer loops. That is because it might be the case that $I({{\mathcal Q}})$ has a $M\varPhi$RF but ${\mathcal Q}$ does not.

Example 3

Consider the loop

$$\begin{aligned} \mathtt {while} ~( x_2-x_1 \le 0, x_1+x_2 \ge 1, x_3 \ge 0 ) ~\mathtt {do} ~ x_2' = x_2-2x_1+1; x_3' = x_3 + 10x_2+9 \end{aligned}$$

When interpreted over the integers, it has the $M\varPhi$RF $\langle 10x_2,x_3 \rangle$. However, when interpreted over the rationals, the loop does not even terminate, e.g., for $(\frac{1}{2}, \frac{1}{2}, 0)$.

For $LRFs$, completeness for the integer case was achieved by reducing the problem to the rational case, using the integer hull ${{\mathcal Q}}_I$ [4, 12]. In fact, it is quite easy to see why this reduction works for $LRFs$, as the requirements that a $LRF$ has to satisfy are a conjunction of linear inequalities and if they are satisfied by $I({{\mathcal Q}})$, they will be satisfied by convex combinations of such points, i.e., ${{\mathcal Q}}_I$.

Since we have reduced the problem of finding a $M\varPhi$RF to finding a nested ranking function, and the requirements from a nested ranking function are conjunctions of linear inequalities that should be implied by ${\mathcal Q}$, it is tempting to assume that this argument applies also for $M\varPhi$RFs. However, to justify the use of nested functions, specifically in proving Lemma 2, we relied on Lemma 1, which we applied to ${\mathcal Q}$ (it is quite easy to see that the lemma fails if instead of quantifying over a polyhedron, one quantifies only on its integer points). This means that we did not prove that the existence of a $M\varPhi$RF for $I({{\mathcal Q}})$ implies the existence of a nested ranking function over $I({{\mathcal Q}})$. A similar observation also holds for the results of Sect. 4, where we proved that any (weak) $LLRF$ can be converted to a $M\varPhi$RF. Those results are valid only for rational loops, since in the corresponding proofs we used Lemma 1.

In this section we show that reduction of the integer case to the rational one, via the integer hull, does work also for $M\varPhi$RFs, and for converting $LLRFs$ to $M\varPhi$RFs, thus extending our result to integer loops. We do so by showing that if $I({{\mathcal Q}})$ has a weak $LLRF$, then ${{\mathcal Q}}_I$ has a weak $LLRF$ (over the rationals).

Theorem 4

Let $\langle f_1,\dots ,f_d \rangle$ be a weak $LLRF$ for $I({{\mathcal Q}})$. There are constants $c_1,\dots ,c_d$ such that $\langle f_1+c_1,\dots ,f_d+c_d \rangle$ is a weak $LLRF$ for ${{\mathcal Q}}_I$.

Proof

The proof is by induction on d. The base case, $d=1$, concerns a $LRF$, and as already mentioned, is trivial (and $c_1=0$). For $d>1$, define:

Note that ${\mathcal Q}'$ includes only integer points of ${{\mathcal Q}}_I$ that are not ranked at the first component, due to violating $f_1(\mathbf {x}) \ge 0$. By changing the first component into $f_1+1$, we take care of points where $-1< f_1(\mathbf {x}) < 0$. Thus we will have that for every integer point $\mathbf {x}''\in {\mathcal Q}$, if it is not in ${\mathcal Q}'$, then the first component is non-negative, and otherwise $\mathbf {x}''$ is ranked by $\langle f_2,\dots ,f_d \rangle$. Similarly ${\mathcal Q}''$ includes all the integer points of ${{\mathcal Q}}_I$ that are not ranked by the first component due to violating $\varDelta f_1(\mathbf {x}'') > 0$. Note also that ${\mathcal Q}''$ is integral, since it is a face of ${{\mathcal Q}}_I$. On the other hand, ${\mathcal Q}'$ is not necessarily integral, so we have to distinguish ${{\mathcal Q}}_I'$ from ${\mathcal Q}'$. By the induction hypothesis there are

• $c'_2,\dots ,c'_d$ such that $\langle f_2+c'_2,\dots ,f_d+c'_d \rangle$ is a weak $LLRF$ for ${{\mathcal Q}}_I'$; and

• $c''_2,\dots ,c''_d$ such that $\langle f_2+c''_2,\dots ,f_d+c''_d \rangle$ is a weak $LLRF$ for ${{\mathcal Q}}_I''$.

Next we prove that $f_1$ has a lower bound on ${{\mathcal Q}}_I\setminus {{\mathcal Q}}_I'$, i.e., there is $c_1 \ge 1$ such that $f_1+c_1$ is non-negative on this set. Before proceeding to the proof, note that this implies that is a weak $LLRF$ for ${{\mathcal Q}}_I$. To see this, take any rational $\mathbf {x}''\in {{\mathcal Q}}_I$, then either $\mathbf {x}''$ is ranked by the first component, or $\mathbf {x}''\in {\mathcal Q}''$ or $\mathbf {x}''\in {{\mathcal Q}}_I'$; in the last two cases, it is ranked by a component $f_i+\max (c'_i,c''_i)$ for $i>1$.

It remains to prove that $f_1$ has a lower bound on ${{\mathcal Q}}_I\setminus {{\mathcal Q}}_I'$. We assume that ${{\mathcal Q}}_I'$ is non-empty, since otherwise, by the definition of ${\mathcal Q}'$, it is easy to see that $f_1 \ge -1$ over all of ${{\mathcal Q}}_I$. Thus, we consider ${{\mathcal Q}}_I'$ in an irredundant constraint representation: ${{\mathcal Q}}_I' = \{ \mathbf {x}'' \in \mathbb Q ^{2n} \mid \vec {a}_i \cdot \mathbf {x}'' \le b_i, \ i = 1,\dots ,m \}$, and define

for $i=1,\dots ,m$. Then, clearly, ${{\mathcal Q}}_I\setminus {{\mathcal Q}}_I' \subseteq \bigcup _{i=1}^m {\mathcal P}_i$. It suffices to prove that $f_1$ has a lower bound over ${\mathcal P}_i$, for every i. Fix i, such that ${\mathcal P}_i$ is not empty. It is important to note that, by construction, all integer points of ${\mathcal P}_i$ are in ${{\mathcal Q}}_I\setminus {{\mathcal Q}}_I'$.

Let H be the half-space $\{\mathbf {x}'' \!\mid \vec {a}_i\cdot \mathbf {x} \le b_i\}$. We first claim that ${\mathcal P}_i = {\mathcal P}'_i \setminus H$ contains an integer point. Equivalently, there is an integer point of ${{\mathcal Q}}_I$ not contained in H. There has to be such a point, for otherwise, ${{\mathcal Q}}_I$, being integral, would be contained in H, and ${\mathcal P}_i$ would be empty. Let $\mathbf {x}''_0$ be such a point.

Next, assume (by way of contradiction) that $f_1$ is not lower bounded on ${\mathcal P}_i$. Express $f_1$ as $f_1(\mathbf {x}) = \vec {\lambda }\cdot \mathbf {x} + \lambda _0$, then $\vec {\lambda }\cdot \mathbf {x}$ is not lower bounded on ${\mathcal P}_i$ and thus not on ${\mathcal P}_i'$. This means that ${\mathcal P}_i'$ is not a polytope, and thus can be expressed as ${\mathcal O} + {\mathcal C}$, where ${\mathcal O}$ is a polytope and ${\mathcal C}$ is a cone [23, Corollary 7.1b, p. 88]. There must be a rational $\mathbf {y}''\in {\mathcal C}$ such that $\vec {\lambda }\cdot \mathbf {y} < 0$, since otherwise $f_1$ would be bounded on ${\mathcal P}'_i$.

For $k\in \mathbb Z _+$, consider the point $\mathbf {x}''_0 +k\mathbf {y}''$. Clearly it is in $P_i'$. Since $\mathbf {y}'' \in {\mathcal C}$, we have $\vec {a}_i\cdot \mathbf {y}'' \ge 0$; Since $\mathbf {x}''_0 \in {\mathcal P}_i$, we have $\vec {a}_i\cdot \mathbf {x}''_0 > b_i$; adding up, we get $\vec {a}_i\cdot (\mathbf {x}''_0 + k\mathbf {y}'') > b_i$ for all k. We conclude that the set $S = \{\mathbf {x}''_0 + k\mathbf {y}'' \mid k\in \mathbb Z _+ \}$ is contained in ${\mathcal P}_i$. Clearly, it includes an infinite number of integer points. Moreover $f_1$ obtains arbitrarily negative values on S (the larger k, the smaller the value), in particular on its integer points. Recall that these points are included ${{\mathcal Q}}_I\setminus {{\mathcal Q}}_I'$, thus $f_1$ is not lower bounded on the integer points of ${{\mathcal Q}}_I\setminus {{\mathcal Q}}_I'$, a contradiction to the way ${{\mathcal Q}}_I'$ was defined.    $\square$

Corollary 1

If $I({{\mathcal Q}})$ has a weak $LLRF$ of depth d, then ${{\mathcal Q}}_I$ has a $M\varPhi$RF, of depth at most d.

Proof

By Theorem 4 we know that ${{\mathcal Q}}_I$ has a weak $LLRF$ (of the same depth), which in turn can be converted to a $M\varPhi$RF by Theorem 3.    $\square$

Since $M\varPhi$RFs are also weak $LLRF$, the above corollary provides a complete procedure for synthesizing $M\varPhi$RFs over the integers, simply by seeking a nested ranking function for ${{\mathcal Q}}_I$.

Example 4

For the loop of Example 3, computing the integer hull results in the addition of $x_1\ge 1$. Now seeking a $M\varPhi$RF as in Sect. 3 we find, for example, $\langle 10x_2+10,x_3 \rangle$. Note that $\langle 10x_2,x_3 \rangle$, which a $M\varPhi$RF for $I({{\mathcal Q}})$, is not a $M\varPhi$RF for ${Q}_I$ according to Definition 1, e.g., for any $0<\varepsilon <1$ the transition $(1+\varepsilon ,-\varepsilon ,0,1,-3\varepsilon -1,-10\varepsilon +9) \in {Q}_I$ is not ranked, since $10x_2<0$ and $x_3-x_3'=10\varepsilon -9 < 1$.

The procedure described above has exponential-time complexity, because computing the integer hull requires exponential time. However, it is polynomial for the cases in which the integer hull can be computed in polynomial time [4, Sect. 4]. The next theorem shows that the exponential time complexity is unavoidable for the general case (unless $\mathtt {P}=\mathtt {NP}$). The proof repeats the arguments in the $\mathtt {coNP}$-completes proof for $LRFs$  [4, Sect. 3]. We omit the details.

Theorem 5

$\text {BM}{\varPhi }\text {RF}(\mathbb Z)$ is $\mathtt {coNP}$-complete.

As in Sect. 3, we consider d as constant, or as input given in unary.

6 The Depth of a $M\varPhi$RF

A wishful thought: If we could pre-compute an upper bound on the depth of optimal $M\varPhi$RFs, and use it to bound the recursion, we would obtain a complete decision procedure for $M\varPhi$RFs in general, since we can seek a $M\varPhi$RF, as in Sect. 3, of this specific depth. This thought is motivated by results for lexicographic ranking functions, for example, [4] shows that the number of components in such functions is bounded by the number of variables in the loop. For $M\varPhi$RFs, we were not able to find a similar upper bound, and we can show that the problem is more complicated than in the lexicographic case as a bound, if one exists, must depend not only on the number of variables or constraints, but also on the values of the coefficients in the loop constraints.

Theorem 6

For integer $B>0$, the following loop ${\mathcal Q}_B$

$$\begin{aligned} \mathtt {while} ~(x\ge 1,\; y\ge 1,\; x\ge y,\; 2^{B} y\ge x)~\mathtt {do} ~x'=2x,\; y'=3y \end{aligned}$$

needs at least $B+1$ components in any $M\varPhi$RF.

Proof

Define $R_i=\{ (2^ic,c,2^{i+1}c,3c) \mid c \ge 1 \}$ and note that for $i=0\ldots B$, we have $R_i \subset {\mathcal Q}_B$. Moreover, $R_i \ne R_j$ for different i and j. Next we prove that in any $M\varPhi$RF $\langle f_1,\ldots ,f_d \rangle$ for ${\mathcal Q}_B$, and $R_i$ with $i=0\ldots B$, there must be a component $f_k$ such that $\mathbf {x}''\in R_i \rightarrow f_k(\mathbf {x}) - f(0,0) \ge 0 \wedge \varDelta f_k(\mathbf {x}'')>0.$ To prove this, fix i. We argue by the pigeonhole principle that, for some k, $f_k(2^ic,c) = c f_k(2^i,1) + (1-c)f_k(0,0)\ge 0$ and $f_k(2^ic,c)-f_k(2^{i+1}c,3c)=c(f_k(2^i,1)-f_k(2^{i+1},3))>0$ for infinite number of values of c, and thus $f_k(2^i,1) - f_k(0,0) \ge 0$, and $f_k(2^i,1)-f_k(2^{i+1},3)>0$, leading to the above statement. We say that $R_i$ is “ranked” by $f_k$.

If $d < B+1$, then, by the pigeonhole principle, there are different $R_i$ and $R_j$ that are “ranked” by the same $f_k$. We show that this leads to a contradiction. Consider $R_i$ and $R_j$, with $j>i$, and assume that they are “ranked” by $f_k(x,y)=a_1x+a_2y+a_0$. Applying the conclusion of the last paragraph to $R_i$ and $R_j$, we have:

$$\begin{aligned} f_k(2^i,1)-f_k(2^{i+1},3)&= \, -a_12^i-a_22&> 0 \end{aligned}$$

(16)

$$\begin{aligned} f_k(2^j,1)-f_k(2^{j+1},3)&= \, -a_12^j-a_22&> 0 \end{aligned}$$

(17)

$$\begin{aligned} f_k(2^i,1) - f_k(0,0)&= a_12^i+a_2&\ge 0 \end{aligned}$$

(18)

$$\begin{aligned} f_k(2^j,1) - f_k(0,0)&= a_12^j+a_2&\ge 0 \end{aligned}$$

(19)

Adding $\frac{1}{2}\cdot$(17) to (19) we get . Thus, $a_1$ must be positive. From the sum of $\frac{1}{2}\cdot$(17) and (18), we get $a_1(2^i-2^{j-1}) > 0$, which implies $j>i+1$, and $a_1<0$, a contradiction. Note that the bound $B+1$ is tight. This is confirmed by the $M\varPhi$RF $\langle x-2^By , x-2^{B-1}y, x-2^{B-2}y, \ldots , x-y \rangle$.    $\square$

7 Iteration Bounds from $M\varPhi$RFs

Automatic complexity analysis techniques are often based on bounding the number of iterations of loops, using ranking functions. Thus, it is natural to ask if a $M\varPhi$RF implies a bound on the number of iterations of a given $SLC$ loop. For $LRFs$, the implied bound is trivially linear, and in the case of $SLC$ loops, it is known to be linear also for a class of lexicographic ranking functions [4]. In this section we show that $M\varPhi$RFs, too, imply a linear iteration bound, despite the fact that the variables involved may grow non-linearly during the loop. Below we concentrate on its existence, but the bound can also be computed explicitly.

Example 5

Consider the following loop with the corresponding $M\varPhi$RF $\langle y+1,x \rangle$

$$ \mathtt {while} ~(x\ge 0)~\mathtt {do} ~x'=x+y,\; y'=y-1 $$

Let us consider an execution starting from positive values $x_0$ and $y_0$, and note that when $y+1$ reaches 0, i.e., when moving to the second phase, the value of x would be $x_0-1+\sum _{i=-1}^{y_0}i=x_0-1+\frac{y_0(y_0+1)}{2}$, which is polynomial in the input. It may seem that the next phase would be super-linear, since it is ranked by x, however, note that x decreases first by 1, then by 2, then by 3, etc. Therefore the quantity $\frac{y_0(y_0+1)}{2}$ is eliminated in $y_0$ iterations.

In what follows we generalize the observation of the above example. We consider an $SLC$ loop ${\mathcal Q}$, and a corresponding irredundant $M\varPhi$RF $\tau =\langle f_1,\dots ,f_d \rangle$. Let us start with an outline of the proof. We first define a function $F_k(t)$ that corresponds to the value of $f_k$ after iteration t. We then bound each $F_k$ by some expression $UB _k(t)$, and observe that for t greater than some number $T_k$, that depends linearly on the input, $UB _k(T_k)$ becomes negative. This means that $T_k$ is an upper bound on the time in which the k-th phase ends; the whole loop must terminate before $\max _k T_k$ iterations.

Let $\mathbf {x}_t$ be the state after iteration t, and define $F_k(t) = f_k(\mathbf {x}_t)$, i.e., the value of the k-th component $f_k$ after t iterations. For the initial state $\mathbf {x}_0$, we let $M = \max \{f_1(\mathbf {x}_0),\dots ,f_d(\mathbf {x}_0),1\}$. Note that M is linear in $\Vert \mathbf {x}_0 \Vert _{\infty }$ (i.e., in the maximum absolute value of the components of $\mathbf {x}_0$). We first state an auxiliary lemma, and then a lemma that bounds $F_k$.

Lemma 5

For all $1 < k \le d$, there are $\mu _1,\dots ,\mu _{k-2} \ge 0$ and $\mu _{k-1} > 0$ such that $\mathbf {x}''\in {\mathcal Q}\,\rightarrow \, \mu _1 f_1(\mathbf {x}) + \dots + \mu _{k-1} f_{k-1}(\mathbf {x}) + (\varDelta f_k(\mathbf {x}'')-1) \ge 0$.

Proof

From the definition of $M\varPhi$RF we have

$$\begin{aligned} \mathbf {x}''\in {\mathcal Q}\rightarrow f_1(\mathbf {x}) \ge 0 \vee \cdots \vee f_{k-1}(\mathbf {x}) \ge 0 \vee \varDelta f_k(\mathbf {x}'') \ge 1. \end{aligned}$$

Moreover the conditions of Lemma 1 hold since $f_k$ is not redundant, thus there are non-negative constants $\mu _1,\ldots ,\mu _{k-1}$ such that

$$\begin{aligned} \mathbf {x}''\in {\mathcal Q}\rightarrow \mu _1f_1(\mathbf {x})+\cdots + \mu _{k-1} f_{k-1}(\mathbf {x})+ (\varDelta f_{k}(\mathbf {x}'') - 1) \ge 0. \end{aligned}$$

Moreover, at least $\mu _{k-1}$ must be non-zero, otherwise it means that $\varDelta f_k(\mathbf {x}'')\ge 1$ holds already when $f_1,\dots ,f_{k-2}$ are negative, so $f_{k-1}$ would be redundant.    $\square$

Lemma 6

For all $1\le k\le d$, there are constants $c_k, d_k > 0$ such that $F_k(t) \le c_k M t^{k - 1} - d_k t^{k}$, for all $t \ge 1$.

Proof

The proof is by induction. For $k=1$ we let $c_1=d_1=1$ and get $F_1(t) \le M - t$, which is trivially true. For $k\ge 2$ we assume that the lemma holds for smaller indexes and show that it holds for k. Note that the change in the value of $F_k(t)$ in the i-th iteration is $f_k(\mathbf {x}_{i+1})-f_k(\mathbf {x}_{i}) = -\varDelta f_k(\mathbf {x}''_i)$. By Lemma 5 and the definition of $F_k$, we have $\mu _1,\dots ,\mu _{k-2} \ge 0$ and $\mu _{k-1}>0$ such that (over ${\mathcal Q}$)

$$\begin{aligned} f_k(\mathbf {x}_{i+1}) - f_k(\mathbf {x}_{i}) < \mu _1 F_1(i) + \dots + \mu _{k-1} F_{k-1}(i) \,. \end{aligned}$$

(20)

Now we bound $F_k$ (explanation follows):

$$\begin{aligned} F_k(t)&= f_k(\mathbf {x}_0) + \varSigma _{i=0}^{t-1} (f_k(\mathbf {x}_{i+1}) - f_k(\mathbf {x}_{i})) \end{aligned}$$

(21)

$$\begin{aligned}&< M + \varSigma _{i=0}^{t-1} \left( \mu _1 F_1(i) + \dots + \mu _{k-1} F_{k-1}(i) \right) \end{aligned}$$

(22)

$$\begin{aligned}&\le M(1+\mu ) + \varSigma _{i=1}^{t-1} \left( \mu _1 F_1(i) + \dots + \mu _{k-1} F_{k-1}(i) \right) \end{aligned}$$

(23)

$$\begin{aligned}&\le M(1+\mu ) + \varSigma _{i=1}^{t-1} \varSigma _{j=1}^{k-1} \left( \mu _j c_j M i^{j - 1} - \mu _j d_j i^{j} \right) \end{aligned}$$

(24)

$$\begin{aligned}&\le M(1+\mu ) + \varSigma _{i=1}^{t-1} \left( ( \varSigma _{j=1}^{k-1} \mu _j c_j M i^{j - 1} ) - \mu _{k-1} d_{k-1} i^{k-1} \right) \end{aligned}$$

(25)

$$\begin{aligned}&\le M(1+\mu ) + \varSigma _{i=1}^{t-1} \left( M ( \varSigma _{j=1}^{k-1} \mu _j c_j ) i^{k - 2} - \mu _{k-1} d_{k-1} i^{k-1} \right) \end{aligned}$$

(26)

$$\begin{aligned}&= M(1+\mu ) + M ( \varSigma _{j=1}^{k-1} \mu _j c_j ) ( \varSigma _{i=1}^{t-1} i^{k - 2} ) - \mu _{k-1} d_{k-1}\varSigma _{i=1}^{t-1} i^{k-1} \end{aligned}$$

(27)

$$\begin{aligned}&\le M(1+\mu ) + M ( \varSigma _{j=1}^{k-1} \mu _j c_j ) ( \frac{t^{k-1}}{k-1} ) - \mu _{k-1} d_{k-1} ( \frac{t^{k}}{k} - t^{k-1} ) \end{aligned}$$

(28)

$$\begin{aligned}&= c_k M t^{k-1} - d_k t^{k} \end{aligned}$$

(29)

Each step above is obtained from the previous one as follows: (22) by replacing $f_k(\mathbf {x}_0)$ by M, since $f_k(\mathbf {x}_0)\le M$, and applying (20); (23) by separating the term for $i=0$ from the sum; this term is bounded by $\mu M$, where $\mu =\sum _{j=1}^{k-1}\mu _j$, because $F_k(0)=f_k(\mathbf {x}_0)\le M$ by definition; (24) by applying the induction hypothesis; (25) by removing all negative values $- \mu _j d_j i^{j}$, except the last one $-\mu _{k-1} d_{k-1} i^{k-1}$; (26) by replacing $i^{j-1}$ by an upper bound $i^{k-2}$; (27) by opening parentheses; (28) replacing $\varSigma _{i=1}^{t-1} i^{k - 2}$ by an upper bound $\frac{t^{k-1}}{k-1}$, and $\varSigma _{i=1}^{t-1} i^{k-1}$ by a lower bound $\frac{t^{k}}{k} - t^{k-1}$; finally for (28), take $c_k=(1+\mu )+(\varSigma _{j=1}^{k-1} \mu _j c_j)/(k-1)+\mu _{k-1} d_{k-1}$, and $d_k=\mu _{k-1} d_{k-1}/k$ and note that both are positive.    $\square$

Theorem 7

An $SLC$ loop that has a $M\varPhi$RF terminates in a number of iterations bounded by $O(\Vert \mathbf {x}_0 \Vert _{\infty })$.

Proof

For $t > \max \{1, (c_k/d_k)M\}$, we have $F_k(t) < 0$, proving that the k-th phase terminates by this time (since it remains negative). Thus, by the time $\max \{1,(c_1/d_1)M,\ldots ,(c_d/d_d)M\}$, which is linear in $\Vert \mathbf {x}_0 \Vert _{\infty }$, all phases must have terminated. Note that $c_k$ and $d_k$ can be computed explicitly, if desired.    $\square$

We remark that the above result also holds for multi-path loops if they have a nested $M\varPhi$RF, but does not hold for any $M\varPhi$RF.

8 Conclusion

$LRFs$, $LLRFs$ and $M\varPhi$RFs have all been proposed in earlier work. The original purpose of this work has been to improve our understanding of $M\varPhi$RFs, and answer open problems regarding the complexity of obtaining such functions from linear-constraint loops, the difference between the integer case and the rational case, and the possibility of inferring an iteration bound from such ranking functions. Similarly, we wanted to understand a natural class of lexicographic ranking functions, which removes a restriction of previous definitions regarding negative values. Surprisingly, it turned out that our main results are equivalences which show that, for $SLC$ loops, both $M\varPhi$RFs and $LLRFs$ reduce to a simple kind of $M\varPhi$RFs, that has been known to allow polynomial-time solution (over $\mathbb Q$). Thus, our result collapsed, in essence, these above classes of ranking functions.

The implication of having a polynomial-time solution, which is hardly more complex than the standard algorithm to find $LRFs$, is that whenever one considers using $LRFs$ in one’s work, one should consider using $M\varPhi$RFs. By controlling the depth of the $M\varPhi$RFs one trades expressivity for processing cost. We believe that it would be sensible to start with depth 1 (i.e., seeking a $LRF$) and increase the depth upon failure. Similarly, since a complete solution for the integers is inherently more costly, it makes sense to begin with the solution that is complete over the rationals, since it is safe for the integer case. If this fail, one can also consider special cases in which the inherent hardness can be avoided [4, Sect. 4].

Table 1. Experiments on loops taken from [15]—loops (1–5) originate from [11] and (6–41) originate from [8].

Theoretically, some tantalizing open problems remain. Is it possible to decide whether a given loop admits a $M\varPhi$RF, without a depth bound? This is related to the question, discussed in Sect. 6, whether it is possible to precompute a depth bound. What is the complexity of the $M\varPhi$RF problems over multi-path loops? For such loops, the equivalence of $M\varPhi$RFs, nested r.f.s and $LLRFs$ does not hold. Finally (generalizing the first question), we think that there is need for further exploration of single-path loops and of the plethora of “termination witnesses” based on linear functions (a notable reference is [18]).

We have implemented the nested ranking function procedure of Sect. 3, and applied it on a set of terminating and non-terminating $SLC$ loops taken from [15]. Table 1 (at Page 18) summarizes these experiments. All loops marked with “None” have no $M\varPhi$RF, and they are mostly non-terminating: Loop 1 is terminating over the integers, but does not have $M\varPhi$RF, and Loop 21 is terminating over both integers and rationals but does not have $M\varPhi$RF. Note that loops 3–5 are multi-path, in such case we seek a nested $M\varPhi$RF that is valid for all paths. In all cases, a strict inequality $x>y$ was translated to $x\ge y+1$ before applying out procedure. Interestingly, all 25 terminating loops in this set have a $M\varPhi$RF. These experiments can be tried at http://loopkiller.com/irankfinder.