# The 2-Dimensional Constraint Loop Problem Is Decidable

Quentin Guilmant, Engel Lefaucheux, Joël Ouaknine, James Worrell

► To cite this version:

Quentin Guilmant, Engel Lefaucheux, Joël Ouaknine, James Worrell. The 2-Dimensional Con-
straint Loop Problem Is Decidable. 51st International Colloquium on Automata, Languages, and
Programming (ICALP 2024), Tallinn University of Technology, Jul 2024, Tallin, Estonia. pp.21,
10.4230/LIPIcs.ICALP.2024.140 . hal-04644417

HAL Id: hal-04644417

https://inria.hal.science/hal-04644417v1

Submitted on 11 Jul 2024

**HAL** is a multi-disciplinary open access
archive for the deposit and dissemination of sci-
entific research documents, whether they are pub-
lished or not. The documents may come from
teaching and research institutions in France or
abroad, or from public or private research centers.

L'archive ouverte pluridisciplinaire HAL, est
destinée au dépôt et à la diffusion de documents
scientifiques de niveau recherche, publiés ou non,
émanant des établissements d'enseignement et de
recherche français ou étrangers, des laboratoires
publics ou privés.

<figure><img src="image_1.png" /></figure>
# The 2-Dimensional Constraint Loop Problem Is Decidable

Quentin Guilmant

<figure><img src="image_2.png" /></figure>

<figure><img src="image_3.png" /></figure>

<figure><img src="image_4.png" /></figure>

Max Planck Institute for Software Systems, Saarland Informatics Campus, Saarbrücken, Germany

Engel Lefaucheux

<figure><img src="image_5.png" /></figure>

<figure><img src="image_6.png" /></figure>

<figure><img src="image_7.png" /></figure>

Loria, Nancy, France

Joël Ouaknine

<figure><img src="image_8.png" /></figure>

<figure><img src="image_9.png" /></figure>

Max Planck Institute for Software Systems, Saarland Informatics Campus, Saarbrücken, Germany

James Worrell

<figure><img src="image_10.png" /></figure>

<figure><img src="image_11.png" /></figure>

Department of Computer Science, University of Oxford, UK

## Abstract

A linear constraint loop is specified by a system of linear inequalities that define the relation between the values of the program variables before and after a single execution of the loop body. In this paper we consider the problem of determining whether such a loop terminates, i.e., whether all maximal executions are finite, regardless of how the loop is initialised and how the non-determinism in the loop body is resolved. We focus on the variant of the termination problem in which the loop variables range over $ℝ$. Our main result is that the termination problem is decidable over the reals in dimension 2. A more abstract formulation of our main result is that it is decidable whether a binary relation on $ℝ²$ that is given as a conjunction of linear constraints is well-founded.

**2012 ACM Subject Classification** Theory of computation → Program verification

**Keywords and phrases** Linear Constraints Loops, Minkowski-Weyl, Convex Sets, Asymptotic Expansions

**Digital Object Identifier** 10.4230/LIPIcs.ICALP.2024.140

**Category** Track B: Automata, Logic, Semantics, and Theory of Programming

**Related Version** Full Version: https://arxiv.org/abs/2405.12992 [6]

**Funding** Engel Lefaucheux: ANR BisoUS (ANR-22-CE48-0012).

Joël Ouaknine: Also affiliated with Keble College, Oxford as emmy.network Fellow, and supported by DFG grant 389792660 as part of TRR 248 (see https://perspicuous-computing.science).

James Worrell: Work supported by UKRI Frontier Research Grant EP/X033813/1.

## 1 Introduction

The problem of deciding loop termination is of fundamental importance in software verification. Deciding termination is already challenging for very simple classes of programs. One such class consists of *linear constraint loops*. These are single-path loops in which both the loop guard and the loop update are given by conjunctions of linear inequalities over the program variables. Such a loop can be written as follows, where $A, B$ are matrices of rational numbers, $a, b$ are vectors of rational numbers, and $x, x'$ represent the respective values of the program variables before and after the loop update:

$$P: \text{ while } (Bx \geq b) \text{ do } A(x') \geq a,$$

Such loops are inherently non-deterministic, since the effect of the loop body is described by a collection of constraints. Note in passing that the loop guard can be folded into the constraints that describe the loop body and so, without loss of generality, the guard can

<figure><img src="image_12.png" /></figure>

© Quentin Guilmant, Engel Lefaucheux, Joël Ouaknine, and James Worrell;
licensed under Creative Commons License CC-BY 4.0

51st International Colloquium on Automata, Languages, and Programming (ICALP 2024).

Editors: Karl Bringmann, Martin Grohe, Gabriele Puppis, and Ola Svensson;
Article No. 140; pp. 140:1–140:21

<figure><img src="image_13.png" /></figure>

Leibniz International Proceedings in Informatics
LIPICS Schloss Dagstuhl – Leibniz-Zentrum für Informatik, Dagstuhl Publishing, Germany

<figure><img src="image_14.png" /></figure>
140:2 The 2-Dimensional Constraint Loop Problem Is Decidable

be assumed to be trivial. Linear constraint loops naturally arise as abstractions of other
programs. For example, linear constraints can be used to model size changes in program
variables, data structures, or terms in a logic program (see, e.g. [9]).

A linear constraint loop is said to *terminate* if there is no initial value of the loop variables
from which the loop has an infinite execution. The Termination Problem asks to decide
whether a given loop terminates. As such, the Termination Problem depends on the numerical
domain that the program variables range over: typically one considers either $\mathbb{Z}$, $\mathbb{Q}$, or $\mathbb{R}$.

One approach to proving termination of linear constraint loops involves synthesizing
linear ranking functions [2]. However, it is well-known that there are terminating loops that
admit no linear ranking function. In the special case of deterministic linear constraint loops
(i.e., where the loop body applies an affine function to the program variables) decidability
of termination over $\mathbb{R}$ was shown by Tiwari [10], decidability of termination over $\mathbb{Q}$ was
shown by Braverman [5], and decidability of termination over $\mathbb{Z}$ was established in [7].<fnref n="1" /> All
three papers build on an analysis of the spectrum of the matrix that determines the update
function in the loop body. To the best of our knowledge, decidability of termination of linear
constraint loops over $\mathbb{R}$, $\mathbb{Q}$, and $\mathbb{Z}$ remains open. It is known however that termination for
multi-path constraint loops is undecidable (i.e., where disjunctions are allowed in the linear
constraints that define the update map). It is moreover known that termination of single-path
constraint loops is undecidable if irrational constants are allowed in the constraints [3]. One
of the few known positive results is the restricted case that all the constraints are octagonal,
in which case termination is decidable over integers [4]. (Recall that a constraint is said to
be *octagonal* if it is a conjunction of propositions of the form $\pm x_i \pm x_j \le a$, for variables
$x_i, x_j$ and constant $a \in \mathbb{Z}$.)

In this paper we study the termination of linear constraint loops over the reals in dimension
at most 2. We give a sufficient and necessary condition that such a loop be non-terminating
in the form of a *witness of non-termination*. This is given in Definition 1. Here one should
think of $K$ as the transition relation of a linear constraint loop, while $\text{rec}(K)$ is the *recession
cone* of $K$, i.e., the set of vectors $v$ such that $w + \lambda v \in K$ for all $w \in K$ and $\lambda \ge 0$. The
witness of non-termination is essentially a finite representation of an infinite execution of the
loop in the spirit of the geometric non-termination arguments of [8] and the recurrent sets
of [1].

**Definition 1.** Let $E$ be a Euclidean space. Let $K \subseteq E^2$ be a convex set. A witness $W(K)$ consists of a linear map $M : E \to E$, a closed cone $C \subseteq E$, and $v, w \in E$, such that
$$ (\exists u1) \; MC \subseteq C $$
$$ (\exists u2) \; \forall x \in C \quad (x, Mx) \in \text{rec}(K) $$
$$ (\exists u3) \; (v, w) \in K $$
$$ (\exists u4) \; w - v \in C. $$

If $E$ has dimension at most 2 and $K$ is a polyhedron, then the existence of such a witness
can be expressed in the theory of real closed fields. (The restriction to dimension 2 entails
that every cone is generated by a most 3 vectors, whereas there is no such upper bound in
dimension 3.) Thus we obtain a polynomial-time reduction of the Termination Problem for
constraint loops to the decision problem for the theory of real closed fields with a bounded
number of quantifier, which is decidable in polynomial space.

<footnote n="1">¹ These works in fact consider loop guards that feature a mix of strict and non-strict inequalities, whereas in the present paper we consider only non-strict inequalities.</footnote>
The following is our main result, which characterises non-termination in terms of the above notion of witness. We refer to Section 2.3 for the notion of MW-convex set, suffice to say here that this class includes all polyhedra and that the main property of MW-convex sets used in the proof is that for every linear projection $\pi$ and MW-convex set $K$ we have $\pi(\mathrm{rec}(K)) = \mathrm{rec}(\pi(K))$. Further background about convex sets is contained in Section 2.2.

**Theorem 2.** Let $E$ be a Euclidean space of dimension at most 2. Let $K \subseteq E^2$ be MW-convex. There is a sequence $(u_n)_{n \in \mathbb{N}} \in E^\mathbb{N}$ such that $(u_n, u_{n+1}) \in K$ for all $n \in \mathbb{N}$ if and only if there exists a witness $W(K)$.

# 2 Preliminaries

## 2.1 Notation

A superscript `*` removes 0 from a set. Namely, $\mathbb{R}^* = \mathbb{R} \setminus \{0\}$, $\mathbb{N}^* = \mathbb{N} \setminus \{0\}$ and so on. $\mathbb{R}_+$ stands for all non-negative real numbers and $\mathbb{R}_+^*$ for all the positive real numbers. Also, for $n, m \in \mathbb{N}$ such that $n \le m$, we let $[[n; m]]$ be the set of integers between $n$ and $m$ inclusive, namely $[[n; m]] = \{n, n+1, \dots, m\}$.

**Landau Notations.** We use the Landau notations. Let $d \in \mathbb{N}^*$. Let $\|\cdot\|$ be any norm over $\mathbb{R}^d$ (recall that all norms on $\mathbb{R}^d$ are equivalent). Let $u: \mathbb{N} \to \mathbb{R}^d$, $w: \mathbb{N} \to \mathbb{R}^d$ and $v: \mathbb{N} \to \mathbb{R}$ be sequences. We then have the following notations:

- $u_n = \mathop{\mathrm{o}}_{n \to +\infty} (v_n)$ when for all $\varepsilon \in \mathbb{R}_+^*$ there is some $N \in \mathbb{N}$ such that for all $n \ge N$, we have $\|u_n\| \le \varepsilon|v_n|$.

- $u_n = \mathop{\mathrm{O}}_{n \to +\infty} (v_n)$ when there is some $M \in \mathbb{R}_+^*$ and some some $N \in \mathbb{N}$ such that for all $n \ge N$, we have $\|u_n\| \le M|v_n|$.

- $u_n = \mathop{\mathrm{\Omega}}_{n \to +\infty} (v_n)$ when there is some $M \in \mathbb{R}_+^*$ and some some $N \in \mathbb{N}$ such that for all $n \ge N$, we have $\|u_n\| \ge M|v_n|$.

- $u_n \stackrel{\sim}{\to}_{n \to +\infty} w_n$ if $u_n - w_n = \mathop{\mathrm{o}}_{n \to +\infty} (\|w_n\|)$.

- $u_n = w_n + \mathop{\mathrm{o}}_{n \to +\infty} (v_n)$ if $u_n - w_n = \mathop{\mathrm{o}}_{n \to +\infty} (v_n)$.

- $u_n = w_n + \mathop{\mathrm{O}}_{n \to +\infty} (v_n)$ if $u_n - w_n = \mathop{\mathrm{O}}_{n \to +\infty} (v_n)$.

We keep the same notations if the sequences are undefined at a finite number of points in $\mathbb{N}$.

## 2.2 Convex Sets

Throughout this section $E$ is an arbitrary Euclidean space.

These results are already known but for the sake of completeness, some proofs are written here anyway.
140:4 The 2-Dimensional Constraint Loop Problem Is Decidable

**Definition 3.** Let $S \subseteq E$. The affine hull of $S$, denoted $\text{AffHull}(S)$, the convex hull of $S$, denoted $\text{ConvHull}(S)$, and the vector space spanned by $S$, denoted $\text{Vect}(S)$, are defined by

$$ \text{AffHull}(S) = \left\{ \sum_{i=1}^{k} \alpha_i x_i \mid \alpha_i \in \mathbb{R}, x_i \in S, \sum_{i=1}^{k} \alpha_i = 1 \right\} $$

$$ \text{ConvHull}(S) = \left\{ \sum_{i=1}^{k} \alpha_i x_i \mid \alpha_i \in [0; 1], x_i \in S, \sum_{i=1}^{k} \alpha_i = 1 \right\} $$

$$ \text{Vect}(S) = \left\{ \sum_{i=1}^{k} \alpha_i x_i \mid \alpha_i \in \mathbb{R}, x_i \in S \right\} $$

**Definition 4.** Let $K \subseteq E$ be a convex set. The relative interior of $K$, denoted $\text{ri}(K)$, is defined by:

$$ \text{ri}(K) = \{ x \in K \mid \exists U \in \mathcal{O}(E), (x \in U) \wedge (U \cap \text{AffHull}(K) \subseteq K) \} $$

where $\mathcal{O}(E)$ stands for the set of open subsets of $E$.

In other words, the relative interior of a convex set $C$ is its interior with respect to the induced topology on the affine subspace spanned by $C$.

We have the following properties for the relative interior:

**Proposition 5.** Let $K \subseteq E$ be a non-empty convex set. Denoting as usual by $\bar{K}$ the smallest closed subset of $E$ containing $K$, we have:

(i) $\text{ri}(K)$ is a non-empty convex set

(ii) $\text{ri}(K) \subseteq K \subseteq \bar{K}$

(iii) $\text{AffHull}(\text{ri}(K)) = \text{AffHull}(K)$

(iv) $\text{ri}(K) = \text{ri}(\bar{K})$

(v) $\text{ri}(\bar{K}) = \bar{K}$

**Proposition 6.** Let $K$ be a non-empty convex set and $x, y$ such that $x \in \text{ri}(K)$ and $y \in K \setminus \text{ri}(K)$. Then for all $\lambda \in (0; 1]$ we have $\lambda x + (1 - \lambda)y \in \text{ri}(K)$.

**Definition 7.** Let $K \subseteq E$ be a non-empty convex set. The recession cone of $K$, denoted $\text{rec}(K)$, is the set $\text{rec}(K) = \{z \in E \mid K + \mathbb{R}_+ z \subseteq K\}$.

Note that we always have $0 \in \text{rec}(K)$. Also, the recession cone is indeed a cone, as it is stable under positive scalar multiplication by definition.

**Lemma 8.** Let $K \subseteq E$ be a convex set. Let $\pi: E \to E$ be a linear projection. Then $\pi(\text{rec}(K)) \subseteq \text{rec}(\pi(K))$.

**Proof.** Let $x \in \pi(\text{rec}(K))$. There is $y \in \text{Ker } \pi$ such that $x + y \in \text{rec}(K)$. Let $a \in \pi(K)$ and $b \in \text{Ker } \pi$ such that $a + b \in K$. Then,

$$ \forall \lambda \in \mathbb{R}_+ \quad (a+b) + \lambda(x+y) \in K $$

$$ \text{Hence,} \quad \forall \lambda \in \mathbb{R}_+ \quad a + \lambda x \in \pi(K) $$

$$ \text{and} \quad x \in \text{rec}(\pi(K)). $$

◀

If $K$ is closed, we even have an alternative characterization of the recession cone which requires a seemingly weaker property but that turns out to be equivalent.
**► Proposition 9.** Let $K \subseteq E$ be a non-empty closed convex set. Then

$$ \mathrm{rec}(K) = \{z \in E \mid \exists x \in K \ x + \mathbb{R}_+ z \subseteq K\} $$

**Proof.** We proceed by double inclusion.

(⊆) This direction is easy: if for all $x \in K$, $x + \mathbb{R}_+ z \subseteq K$, since $K \neq \emptyset$, there is at least one $x$ such that $x + \mathbb{R}_+ z \subseteq K$.

(≥) Let $z \in \mathbb{R}^d$ such that there is some $x \in K$ such that $x + \mathbb{R}_+ z \subseteq K$. Let $y \in K$. We have to show that for any $t_0 \in \mathbb{R}_+$, $y + t_0 z \in K$. Note that, by convexity, for all $\lambda \in [0; 1]$, for all $t \in \mathbb{R}_+$ we have

$$ (1 - \lambda)y + \lambda(x + tz) \in K $$

$$ \begin{array}{ll} \text{We then define the function} & \lambda : \begin{cases} [t_0; +\infty) & \to [0; 1] \\ t & \mapsto \frac{t_0}{t} \end{cases} \\ \text{hence} & \forall t \ge t_0 \quad (1 - \lambda(t)) y + \lambda(t)x + t_0 z \in K \\ \text{We also have} & (1 - \lambda(t)) y + \lambda(t)x + t_0 z \underset{t \to +\infty}{\longrightarrow} y + t_0 z \end{array} $$

Since $K$ is closed, we then deduce that for all $y + t_0 z \in K$. Since this holds for any $y \in K$ and any $t_0 \in \mathbb{R}_+$ we end up with $z \in \mathrm{rec}(K)$. ◀

When considering a closed convex set, we can look at its relative interior to get the same recession cone.

**► Proposition 10.** Let $K \subseteq E$ be a non-empty closed convex set. Then $\mathrm{rec}(K) = \mathrm{rec}(\mathrm{ri}(K))$.

**Proof.** We proceed by double inclusion.

(⊆) Let $v \in \mathrm{rec}(K)$. Let $x \in \mathrm{ri}(K)$. In particular, $x \in K$. By definition, for any $\lambda \in \mathbb{R}_+$, $x + \lambda v \in K$. Let $S = \{\lambda \in \mathbb{R}_+ \mid x + \lambda v \in K \setminus \mathrm{ri}(K)\}$. We just have to show that $S = \emptyset$. Assume $S \neq \emptyset$ and consider $\mu \in S$. Let $\lambda > \mu$. Note that

$$ x + \mu v = \left(1 - \frac{\mu}{\lambda}\right) x + \frac{\mu}{\lambda} (x + \lambda v) $$

We have two cases:

- $\lambda \in S$, in this case, using Proposition 6, since $x \in \mathrm{ri}(K)$ and $x + \lambda v \in K \setminus \mathrm{ri}(K)$, we have $x + \mu v \in \mathrm{ri}(K)$, which is a contradiction.

- $\lambda \notin S$, since, by Proposition 5, $\mathrm{ri}(K)$ is convex, $x \in \mathrm{ri}(K)$ and $x + \lambda v \in \mathrm{ri}(K)$, we again reach $x + \mu v \in \mathrm{ri}(K)$, a contradiction.

Both cases are impossible. Therefore, $S = \emptyset$.

(≥) Let $v \in \mathrm{rec}(\mathrm{ri}(K))$. By Proposition 5, there is some $x \in \mathrm{ri}(K)$. Therefore, for all $\lambda \in \mathbb{R}_+$, $x + \lambda v \in \mathrm{ri}(K) \subseteq K$. By Proposition 9, we get that $v \in \mathrm{rec}(K)$. ◀

**► Remark 11.** Note that if $K$ is not closed we have, thanks to Proposition 5, $\mathrm{rec}(\overline{K}) = \mathrm{rec}(\mathrm{ri}(K))$ but we may have $\mathrm{rec}(K) \neq \mathrm{rec}(\mathrm{ri}(K))$.

**► Lemma 12.** Let $C$ be a closed convex cone in $E$. Let $u: E \to E$ be linear. Then $u(C)$ is a closed convex cone.

**Proof.** By definition of a cone,

$$ C = \{0\} \cup \mathbb{R}_+ \{x \in C \mid \|x\| = 1\}. $$
140:6 The 2-Dimensional Constraint Loop Problem Is Decidable

Since $C$ is closed, $\{x \in C \mid \|x\| = 1\}$ is bounded and closed in a vector space of finite dimension, hence it is compact. By linearity of $u$,

$$u(C) = \{0\} \cup \mathbb{R}_+ u(\{x \in C \mid \|x\| = 1\}).$$

Since $u$ is linear over a vector space of finite dimension, it is continuous. Thus, the set $u(\{x \in C \mid \|x\| = 1\})$ is also compact, hence closed. The continuity of the norm ensures that $u(C)$ is closed. By linearity of $u$, we also get that $u(C)$ is a convex cone. ◀

**Lemma 13.** Let $C$ be a non-trivial convex cone in $E$. Let $x \in \text{ri}(C) \setminus \{0\}$ and $u \in \text{Vect}(C)$. Then there is $\lambda \ge 0$ such that $u + \lambda x \in C$.

**Proof.** If $x = u$ then $\lambda = 0$ works. We then assume $x \ne u$. Since $u \in \text{Vect}(C)$, there is $\mu \in (0; 1)$ $\mu u + (1 - \mu)x \in \text{ri}(C)$. Therefore, for any $\lambda \in \mathbb{R}_+$, $\lambda(\mu u + (1 - \mu)x) \in \text{ri}(C)$. In particular, for $\lambda = \frac{1}{\mu}$ (which exists since $\mu \ne 0$),

$$u + \frac{1 - \mu}{\mu} x \in \text{ri}(C)$$

and we indeed have $\frac{1 - \mu}{\mu} \ge 0$. ◀

## 2.3 Minkowski-Weyl Convex Sets

**Definition 14.** A closed convex set $K$ is said to be *MW-convex* if there is a compact convex set $K'$ such that $K = K' + \text{rec}(K)$.

This property comes from the Minkowski-Weyl Theorem for polyhedra:

**Theorem 15 (Minkowski-Weyl).** Let $K \subseteq \mathbb{R}^d$. The following statements are equivalent:

(i) $K = \{x \in \mathbb{R}^d \mid Ax \le b\}$ for some matrix $A \in \mathbb{R}^{n \times d}$ and $b \in \mathbb{R}^n$.

(ii) There are finitely many points $x_1, \dots, x_k \in P$ and finitely many directions $v_1, \dots, v_p$ such that

$$K = \text{ConvHull}(\{x_1, \dots, x_k\}) + \sum_{i=1}^{p} \mathbb{R}_+ v_i.$$

Needing this property, we will assume that the sets $K$ we consider are MW-convex. Note that, among others, polyhedrons are MW-convex, and thus our results apply to a more general class of sets.

One of the main benefits of MW-convex sets is that they behave very nicely with linear projections. Unlike other convex sets, the projections “commute” with the operator $\text{rec}$, giving a reciprocal to Lemma 8.

**Lemma 16.** Let $K \subseteq \mathbb{R}^d$ be MW-convex. Let $\pi$ be a linear projection over $\mathbb{R}^d$. We have $\text{rec}(\pi(K)) \subseteq \pi(\text{rec}(K))$.

**Proof.** Let $x \in \text{rec}(\pi(K))$. If $x = 0$ then we immediately have $x \in \pi(\text{rec}(K))$. Therefore, we may assume $x \ne 0$. For $a \in \pi(K)$, we have $a + \mathbb{R}_+ x \subseteq \pi(K)$. Thus,

$$\forall \lambda \in \mathbb{R}_+ \quad \exists b(\lambda) \in \text{Ker} \pi \quad a + \lambda x + b(\lambda) \in K.$$
Let $K'$ convex compact such that $K = K' + \text{rec}(K)$. Therefore, for all $\lambda \in \mathbb{R}_+$ there are $a'(\lambda) \in \pi(K')$ and $x'(\lambda) \in \pi(\text{rec}(K))$ such that

$$a + \lambda x = a'(\lambda) + x'(\lambda).$$

Since $a'(\lambda) \in \pi(K')$ and that $\pi(K')$ is compact (as the continuous image of a compact), there is $a' \in \pi(K')$ and an increasing sequence $(\lambda_n)_{n \in \mathbb{N}}$ that tends to infinity such that

$$a'(\lambda_n) \underset{n \to +\infty}{\longrightarrow} a'.'$$

Thus

$$\lambda_n x - x'(\lambda_n) \underset{n \to +\infty}{\longrightarrow} a' - a.$$

We then get that

$$\frac{x'(\lambda_n)}{\lambda_n} = x + \frac{a - a'}{\lambda_n} + \underset{n \to +\infty}{o}\left(\frac{1}{\lambda_n}\right) \quad \text{and} \quad \frac{x'(\lambda_n)}{\lambda_n} \underset{n \to +\infty}{\longrightarrow} x.$$

Also $\frac{x'(\lambda_n)}{\lambda_n} \in \pi(\text{rec}(K))$. Moreover, using Lemma 12, $\pi(\text{rec}(K))$ is closed. Hence, we have $x \in \pi(\text{rec}(K))$ what concludes the proof. ◀

The converse inclusion is true for general convex sets (Lemma 8). Combining this to Lemma 16, we have:

**Corollary 17.** Let $K \subseteq \mathbb{R}^d$ be MW-convex. Let $\pi$ be a linear projection over $\mathbb{R}^d$. We have $\text{rec}(\pi(K)) = \pi(\text{rec}(K))$.

**Corollary 18.** Let $K \subseteq \mathbb{R}^d$ be MW-convex. Let $\pi: \mathbb{R}^d \to \mathbb{R}^d$ be a linear projection. Then $\pi(K)$ is MW-convex.

**Proof.** We write $K = K' + \text{rec}(K)$ where $K'$ is a convex compact set. Hence, since $\pi$ is continuous (linear in a finite dimensional space), $\pi(K')$ is also compact. Moreover, by linearity of $\pi$, we get that

$$\pi(K) = \pi(K') + \pi(\text{rec}(K)).$$

By Lemma 12, $\pi(\text{rec}(K))$ is a closed convex cone. Hence, $\pi(K)$ is closed convex as a sum of closed convex sets. By Corollary 17, we get

$$\pi(K) = \pi(K') + \text{rec}(\pi(K)).$$

## 2.4 Accumulation Expansions

We consider an arbitrary Euclidean space $E$ of dimension $d \in \mathbb{N}$. We denote $\langle \cdot, \cdot \rangle$ its scalar product and $\|\cdot\|$ the associated norm.

To study the sequences of the constraint loop problem, we need to identify the asymptotic directions these sequences are going towards, building a form of asymptotic expansion of those sequences. We thus introduce the concept of accumulation expansion. As sequences may point in several directions, we consider the expansion of a subsequence that has a single main direction.
140:8 The 2-Dimensional Constraint Loop Problem Is Decidable

**Definition 19.** Let $(u_n)_{n \in \mathbb{N}}$ be a sequence of $E$. An accumulation expansion of $(u_n)_{n \in \mathbb{N}}$ consists in an increasing function $\psi : \mathbb{N} \to \mathbb{N}$, an integer $p \in [0; d]$, some vectors $z_1, \dots, z_{p+1} \in E$ and sequences $(\alpha_{k,n})_{n \in \mathbb{N}}$ for $k \in [1; p]$ such that

$$
(\text{AE1}) \quad \forall k \in [1; p] \quad \|z_k\| = 1
$$

$$
(\text{AE2}) \quad \forall k, k' \in [1; p] \quad \langle z_k, z_{k'} \rangle = \begin{cases} 1 & \text{if } k = k' \\ 0 & \text{if } k \neq k' \end{cases}
$$

$$
(\text{AE3}) \quad \forall k \in [1; p] \quad \langle z_k, z_{p+1} \rangle = 0
$$

$$
(\text{AE4}) \quad \forall k \in [1; p] \quad \forall n \in \mathbb{N} \quad \alpha_{k,n} > 0
$$

$$
(\text{AE5}) \quad \forall k \in [1; p] \quad \alpha_{k,n} \underset{n \to +\infty}{\longrightarrow} +\infty
$$

$$
(\text{AE6}) \quad \forall m \in [1; p] \quad \alpha_{m,n} \underset{n \to +\infty}{\sim} \left\| u_{\psi(n)} - \sum_{k=1}^{m-1} \alpha_{k,n} z_k \right\|
$$

$$
(\text{AE7}) \quad \forall k \in [1; p-1] \quad \alpha_{k+1,n} = \mathop{\mathrm{o}}\limits_{n \to +\infty} (\alpha_{k,n})
$$

$$
(\text{AE8}) \quad \forall n \in \mathbb{N} \quad \forall \ell \le m \in [1; p] \quad \left\langle z_{\ell}, u_{\psi(n)} - \sum_{k=1}^{m} \alpha_{k,n} z_k \right\rangle = 0
$$

$$
(\text{AE9}) \quad u_{\psi(n)} = \sum_{k=1}^{p} \alpha_{k,n} z_k + z_{p+1} + \mathop{\mathrm{o}}\limits_{n \to +\infty} (1).
$$

Abusing notations, we will say that $u_{\psi(n)} = \sum_{k=1}^{p} \alpha_{k,n}z_k + z_{p+1} + \mathop{\mathrm{o}}\limits_{n \to +\infty} (1)$ is an accumulation expansion of $(u_n)_{n \in \mathbb{N}}$.

**Definition 20.** Let $u = (u_n)_{n \in \mathbb{N}}$ be a sequence of $E$. The set $D_u$ of principal directions of $u$ is defined by

$$
D_u = \left\{ z \in E \left| \begin{array}{l} \displaystyle \sum_{k=1}^{p} \alpha_{k,n} z_k + z_{p+1} + \mathop{\mathrm{o}}\limits_{n \to +\infty} (1) \text{ is an accumulation expansion} \\[2ex] \qquad p \ge 1 \quad \text{and} \quad z = z_1 \end{array} \right. \right\}.
$$

In other words, $D_u$ is the set of directions that are in the dominant position of some accumulation expansion of $u$ such that $p \ge 1$. It also corresponds to the dominant directions of an unbounded sequence.

For $x \in E \setminus \{0\}$ we denote $\tilde{x} = \frac{x}{\|x\|}$ the associated normalized vector.

**Lemma 21.** Let $(u_n)_{n \in \mathbb{N}}$ be an unbounded sequence of $E$. There exist $z \in E$ a unit vector, an increasing function $\varphi : \mathbb{N} \to \mathbb{N}$ and a sequence $(\alpha_n)_{n \in \mathbb{N}}$ such that

$$
\begin{array}{l}
\text{■} \quad \forall n \in \mathbb{N} \quad \alpha_n > 0 \\
\text{■} \quad \alpha_n \xrightarrow{n \to +\infty} +\infty
\end{array}
$$

$$
\textcircled{2} \quad \alpha_n \xrightarrow{n \to +\infty} +\infty
$$

$$
\textcircled{3} \quad \alpha_n \xrightarrow{n \to +\infty} \|u_{\varphi(n)}\|
$$

$$
\textcircled{4} \quad u_{\varphi(n)} = \alpha_n z + \mathop{\mathrm{o}}\limits_{n \to +\infty} (\alpha_n)
$$

$$
\textcircled{5} \quad \forall n \in \mathbb{N} \quad u_{\varphi(n)} - \alpha_n z \in z^{\perp} \text{ where } z^{\perp} \text{ means the vector subspace of } E \text{ orthogonal to } \mathrm{Vect}(\{z\})
$$

**Proof.** Since $(u_n)_{n \in \mathbb{N}}$ is unbounded, we can assume that we have an increasing function $\varphi : \mathbb{N} \to \mathbb{N}$ such that for all $n \in \mathbb{N}$, $u_{\varphi(n)} \neq 0$ and $\|u_{\varphi(n)}\| \xrightarrow{n \to +\infty} +\infty$. Therefore the sequence $(\widetilde{u_{\varphi(n)}})_{n \in \mathbb{N}}$ is well defined. Moreover, as it is bounded by definition, up to refining $\varphi$, we can assume that it converges to some $z \in E$. Let $\pi$ be the orthogonal projection onto $\mathbb{R}z$. We define $\alpha_n$ to be the unique real number such that $\pi(u_{\varphi(n)}) = \alpha_n z$. As $\widetilde{u_{\varphi(n)}} \xrightarrow{n \to +\infty} z$, we have that $\alpha_n \xrightarrow{n \to +\infty} \|u_{\varphi(n)}\|$. Therefore, up to refining $\varphi$, we can assume that $\alpha_n \xrightarrow{n \to +\infty} +\infty$ and $\alpha_n > 0$. Moreover, we have $u_{\varphi(n)} = \alpha_n z + \mathop{\mathrm{o}}\limits_{n \to +\infty} (\alpha_n)$. Finally, by definition of $\pi$, for all $n \in \mathbb{N}$, $u_{\varphi(n)} - \alpha_n z \in z^{\perp}$.

$\blacksquare$
**► Proposition 22.** Any sequence $u = (u_n)_{n \in \mathbb{N}}$ of E admits accumulation expansions. Moreover, if u is unbounded, then $D_u$ is not empty.

**Proof.** If $(u_n)_{n \in \mathbb{N}}$ is bounded, then it has an accumulation point $z_1$. Hence, taking $p = 0$, all the points are trivially true except Point (AE9). Taking any $\psi$ given by the definition of accumulation point lead to $u_{\psi(n)} = z_1 + \mathfrak{o}(1)$.

Assume now that $(u_n)_{n \in \mathbb{N}}$ is unbounded. We proceed by induction on $d = \dim E$.

- If $d = 1$, consider $z_1$ and $(\alpha_{1,n})_{n \in \mathbb{N}}$ and $\psi$ given by Lemma 21. By definition, $\|z_1\| = 1$ and $u_{\psi(n)} - \alpha_{1,n}z_1 \in z_1^{\perp} = \{0\}$. Taking $p = 1$ and $z_2 = 0$ satisfies all the required properties. Moreover, $z_1 \in D_u$.

- Assume the proposition holds for any Euclidean space of dimension $d-1$. Consider $z_1$, $(\alpha'_{1,n})_{n \in \mathbb{N}}$ and $\varphi$ given by Lemma 21. By definition $\|z_1\| = 1$ and $u_{\varphi(n)} - \alpha'_{1,n}z_1 \in z_1^{\perp}$. Since $z_1 \neq 0$, dim $z_1^{\perp} = d-1$. We can thus apply the induction hypothesis on the sequence $(u_{\varphi(n)} - \alpha'_{1,n}z_1)_{n \in \mathbb{N}}$ in $z_1^{\perp}$. Let $\varphi'$ be the function given by the induction hypothesis. Let $\psi = \varphi \circ \varphi'$ and $\alpha_{1,n} = \alpha'_{1,\varphi'(n)}$.

Every point is immediately satisfied either by the induction hypothesis or the fact that $z_1$ is orthogonal to any point in $z_1^{\perp}$, except for Point (AE7): It remains to prove that if $p \ge 2$, then $\alpha_{2,n} = \mathfrak{o}(\alpha_{1,n})$. By induction hypothesis we know that

$$ \alpha_{2,n} \underset{n \to +\infty}{\sim} \|u_{\psi(n)} - \alpha_{1,n}z_1\|. $$

Moreover, by Lemma 21

$$ \|u_{\varphi(n)} - \alpha'_{1,n}z_1\| = \mathfrak{o}(\alpha'_{1,n}). $$

Since $(\alpha_{1,n})_{n \in \mathbb{N}}$ is a subsequence of $(\alpha'_{1,n})_{n \in \mathbb{N}}$, we have

$$ \alpha_{2,n} \underset{n \to +\infty}{\sim} \|u_{\psi(n)} - \alpha_{1,n}z_1\| = \mathfrak{o}(\alpha_{1,n}) $$

as required. Moreover, $z_1 \in D_u$.

<figure><img src="image_15.png" /></figure>

We now state a relation between the directions within the accumulation expansion and the set $\mathrm{rec}(K)$.

**► Proposition 23.** Let E be an Euclidean space. Let $K \subseteq E$ be MW-convex. Let $u = (u_n)_{n \in \mathbb{N}}$ be an unbounded sequence in K. Let $u_{\varphi(n)} = \sum_{k=1}^{p} \alpha_{k,n}z_k + z_{p+1} + \mathfrak{o}(1)$ be an accumulation expansion of $(u_n)_{n \in \mathbb{N}}$. Then, there are some positive real numbers $(\beta_{k,l})_{1 \le l < k \le p+1}$ such that

$$ \forall k \in [1; p] \quad z_k + \sum_{\ell=1}^{k-1} \beta_{k,\ell} z_\ell \in \mathrm{rec}(K) $$

$$ \text{and} \quad z_{p+1} + \sum_{\ell=1}^{p} \beta_{p+1,\ell} z_\ell \in K. $$

**Proof.** For $k \in [1; p]$, we consider $\pi_k : E \to E$ the orthogonal projection onto the vector space $\mathrm{Vect}((z_1, \dots, z_{k-1})^{\perp})$. Let us first show that $z_k \in \pi_k(\mathrm{rec}(K))$. Let $\lambda \in \mathbb{R}_+$ and define

$$ \lambda_{k,n} = \frac{\lambda}{\alpha_{k,n}}. $$
140:10 The 2-Dimensional Constraint Loop Problem Is Decidable

Note that for large enough $n$, $\lambda_{k,n} \in [0; 1]$. Without loss of generality, we assume $\lambda_{k,n} \in [0; 1]$. Then, by convexity,

$$ \lambda_{k,n}u_{\varphi(n)} + (1 - \lambda_{k,n})u_0 \in K. $$

Moreover,

$$ \pi_k(\lambda_{k,n}u_{\varphi(n)} + (1 - \lambda_{k,n})u_0) = \lambda z_k + \sum_{\ell=k+1}^{p} \lambda_{k,n} \alpha_{\ell,n} z_{\ell} \\ + \lambda_{k,n} z_{p+1} + (1 - \lambda_{k,n})\pi_k(u_0) + \mathop{\mathrm{o}}_{n \to +\infty} (\lambda_{k,n}) \\ \underset{n \to +\infty}{\longrightarrow} \lambda z_k + \pi_k(u_0). $$

Also, thanks to Corollary 18, we have $\overline{\pi_k(K)} = \pi_k(K)$. Using now Proposition 9, we then conclude that $z_k \in \mathrm{rec}(\pi_k(K))$. Finally, using Corollary 17,

$$ z_k \in \pi_k(\mathrm{rec}(K)). $$

We now prove the proposition by induction on $k$. For $k = 1$, our preliminary result gives in particular that $z_1 \in \mathrm{rec}(K)$.

Assume now that $(\beta_{q,\ell})_{1\le\ell<q<k}$ have been defined for some $k \in [1; p]$. Since $z_k \in \pi_k(\mathrm{rec}(K))$ as proven earlier, there are some real numbers $(\gamma_{k,\ell})_{\ell \in [1; k-1]}$ such that

$$ z_k + \sum_{\ell=1}^{k-1} \gamma_{k,\ell} z_{\ell} \in \mathrm{rec}(K). $$

If all the $\gamma_{k,\ell}$ are positive then fixing $\beta_{k,\ell} = \gamma_{k,\ell}$ satisfies the proposition. Let $\ell \in [1; k-1]$ maximum such that $\gamma_{k,\ell} \le 0$. Then, as by hypothesis we have that $z_\ell + \sum_{j=1}^{\ell-1} \beta_{\ell,j} z_j \in \mathrm{rec}(K)$, we can deduce that

$$ z_k + \sum_{j=1}^{k-1} \gamma_{k,j} z_j + (1 + |\gamma_{k,\ell}|) \left( z_\ell + \sum_{j=1}^{\ell-1} \beta_{\ell,j} z_j \right) \in \mathrm{rec}(K). $$

$$ \text{Considering } \gamma'_{k,j} = \begin{cases} \gamma_{k,j} & j > \ell \\ 1 & j = \ell, \\ \gamma_{k,j} + (1 + |\gamma_{k,\ell}|)\beta_{\ell,j} & j < \ell \end{cases} $$

we end up with $z_k + \sum_{\ell=1}^{k-1} \gamma'_{k,\ell} z_\ell \in \mathrm{rec}(K)$ with one less non-positive coefficient. Repeating this procedure until every coefficient is positive lead to a sum of the desired shape, thus establishing the induction hypothesis holds on $k$ and therefore concluding the induction.

Let $\pi_{p+1}: E \to E$ the orthogonal projection on $\mathrm{Vect}((z_1, \dots, z_p)^\perp)$. We have

$$ \pi_{p+1}(u_{\varphi(n)}) \underset{n \to +\infty}{\longrightarrow} z_{p+1}. $$

By Corollary 18,

$$ z_{p+1} \in \overline{\pi_{p+1}(K)} = \pi_{p+1}(K). $$

Thus, there are some real numbers $(\gamma_{p+1,\ell})_{\ell \in [1; k]}$ such that

$$ z_{p+1} + \sum_{\ell=1}^{p} \gamma_{p+1,\ell} z_{\ell} \in K. $$
Doing the same work as above, we can add some elements of $\mathrm{rec}(K)$ so that we end up with some positive $(\beta_{p+1,l})_{l \in [1; k]}$ such that

$$z_{p+1} + \sum_{l=1}^{p} \gamma_{p+1,l} z_l \in K. \quad \blacksquare$$

The two following corollaries specialise this result for some form of sequences.

**Corollary 24.** Let $E$ an Euclidean space. Let $\pi: E \to E$ be a linear projection. Let $K \subseteq E$ be MW-convex. Let $u = (u_n)_{n \in \mathbb{N}}$ be an unbounded sequence in $K$ and $x \in D_{\pi(u)}$. Let

$$f(\mathrm{id} - \pi)(u_{\varphi(n)}) \|\pi(u_{\varphi(n)})\| = \sum_{k=1}^{p} \alpha_{k,n} z_k + z_{p+1} + \mathfrak{o}_{n \to +\infty} (1)$$

be an accumulation expansion of $\left( \frac{(\mathrm{id} - \pi)(u_n)}{\|\pi(u_n)\|} \right)_{n \in \mathbb{N}}$ such that

$$\pi(\widetilde{u_{\varphi(n)}}) \xrightarrow{n \to +\infty} x.$$

Then, there are some positive real numbers $(\beta_{k,l})_{1 \le l < k \le p+1}$ such that

$$\forall k \in [1; p+1] \quad z_k + \sum_{l=1}^{k-1} \beta_{k,l} z_l \in \mathrm{rec}(K) \quad \text{and} \quad x + z_{p+1} + \sum_{l=1}^{p} \beta_{p+1,l} z_l \in \mathrm{rec}(K)$$

**Proof.** We have

$$(\mathrm{id} - \pi)(u_{\varphi(n)}) = \sum_{k=1}^{p} \|\pi(u_{\varphi(n)})\| \alpha_{k,n} z_k + \|\pi(u_{\varphi(n)})\| z_{p+1} + \mathfrak{o}_{n \to +\infty} (\|\pi(u_{\varphi(n)})\|)$$

Also, provided $\widetilde{u_{\varphi(n)}} \xrightarrow{n \to +\infty} x$, we have

$$\pi(u_{\varphi(n)}) = \|\pi(u_{\varphi(n)})\| x + \mathfrak{o}_{n \to +\infty} (\|\pi(u_{\varphi(n)})\|).$$

Therefore

$$u_{\varphi(n)} = \sum_{k=1}^{p} \|\pi(u_{\varphi(n)})\| \alpha_{k,n} z_k + \|\pi(u_{\varphi(n)})\| (x + z_{p+1}) + \mathfrak{o}_{n \to +\infty} (\|\pi(u_{\varphi(n)})\|).$$

The result is obtained by applying Proposition 23 to this accumulation expansion of $(u_n)_{n \in \mathbb{N}}$. Note that in this case we in fact have a truncated accumulation expansion so the case $p+1$ is not the last element of an actual accumulation expansion. That is why we get $\mathrm{rec}(K)$ instead of $K$ even for $p+1$. ◀

**Corollary 25.** Let $E$ an Euclidean space. Let $K \subseteq E^2$ be MW-convex. Let $\pi: E \to E$ be a linear projection. Let $u = (u_n)_{n \in \mathbb{N}}$ be an unbounded sequence in $E$ such that

$$\forall n \in \mathbb{N} \quad (u_n, u_{n+1}) \in K$$

and $x \in D_u$. Let

$$\frac{u_{\varphi(n)+1}}{\|u_{\varphi(n)}\|} = \sum_{k=1}^{p} \alpha_{k,n} z_k + z_{p+1} + \mathfrak{o}_{n \to +\infty} (1)$$
be an accumulation expansion of $(\frac{u_{n+1}}{\|u_n\|})_{n \in \mathbb{N}}$ such that
$$ \widetilde{u_{\varphi(n)}} \underset{n \to +\infty}{\longrightarrow} x. $$

Then, there are some positive real numbers $(\beta_{k,l})_{1\le l<k\le p+1}$ such that

$$ \forall k \in [1; p] \quad \left( 0, z_k + \sum_{\ell=1}^{k-1} \beta_{k,\ell} z_\ell \right) \in \mathrm{rec}(K) \quad \text{and} \quad \left( x, z_{p+1} + \sum_{\ell=1}^{p} \beta_{p+1,\ell} z_\ell \right) \in \mathrm{rec}(K) $$

and such that for sufficiently large $n$,

$$ \left\langle \pi \left( z_{p+1} + \sum_{\ell=1}^{p} \beta_{p+1,\ell} z_{\ell} \right), \pi \left( z_{p+1} + \sum_{k=1}^{p} \alpha_{k,n} z_k \right) \right\rangle \ge 0. $$

Moreover, there is some $i \in [1; p+1]$ such that $\pi(z_i) \notin \mathrm{Ker}(\pi)$, this inequality can be taken to be strict.

**Proof.** We first apply Corollary 24 to the sequence $((u_n, u_{n+1}))_{n \in \mathbb{N}}$ and the projection on the first component to get some positive real numbers $(\beta_{k,l})_{1\le l<k\le p+1}$ such that

$$ \forall k \in [1; p] \quad \left( 0, z_k + \sum_{\ell=1}^{k-1} \beta_{k,\ell} z_\ell \right) \in \mathrm{rec}(K) \quad \text{and} \quad \left( x, z_{p+1} + \sum_{\ell=1}^{p} \beta_{p+1,\ell} z_\ell \right) \in \mathrm{rec}(K). $$

Let $k_0 \in [1; p+1]$ minimum such that $z_k \notin \mathrm{Ker} \pi$.

■ If there is no such $k_0$, then

$$ \left\langle \pi \left( z_{p+1} + \sum_{\ell=1}^{p} \beta_{p+1,\ell} z_{\ell} \right), \pi \left( z_{p+1} + \sum_{k=1}^{p} \alpha_{k,n} z_k \right) \right\rangle = 0 $$

and the proof is complete.

■ If $k_0 = p+1$, then

$$ \left\langle \pi \left( z_{p+1} + \sum_{\ell=1}^{p} \beta_{p+1,\ell} z_{\ell} \right), \pi \left( z_{p+1} + \sum_{k=1}^{p} \alpha_{k,n} z_k \right) \right\rangle = \langle \pi(z_{p+1}), \pi(z_{p+1}) \rangle > 0. $$

■ Otherwise, $k_0 \in [1; p]$ and $\|\pi(z_{k_0})\| \ne 0$. Let

$$ S_n(\lambda) = \left\langle \pi \left( z_{p+1} + \sum_{\ell=1}^{p} \beta_{p+1,\ell} z_{\ell} \right) + \lambda \pi \left( z_{k_0} + \sum_{\ell=1}^{k_0-1} \beta_{k_0,\ell} z_{\ell} \right), \pi \left( \sum_{k=1}^{p} \alpha_{k,n} z_k + z_{p+1} \right) \right\rangle. $$

We have

$$
\begin{align*}
S_n(\lambda) &= \left\langle \pi(z_{p+1}) + \sum_{\ell=k_0}^{p} \beta_{p+1,\ell} \pi(z_\ell) + \lambda \pi(z_{k_0}), \sum_{k=k_0}^{p} \alpha_{k,n} \pi(z_k) + \pi(z_{p+1}) \right\rangle \\
&= \left\langle \pi(z_{p+1}) + \sum_{\ell=k_0}^{p} \beta_{p+1,\ell} \pi(z_\ell) + \lambda \pi(z_{k_0}), \pi(z_{p+1}) \right\rangle \\
&\quad + \sum_{k=k_0}^{p} \alpha_{k,n} \left\langle \pi(z_{p+1}) + \sum_{\ell=k_0}^{p} \beta_{p+1,\ell} \pi(z_\ell) + \lambda \pi(z_{k_0}), \pi(z_k) \right\rangle \\
&= \alpha_{k_0,n} \left\langle \pi(z_{p+1}) + \sum_{\ell=k_0}^{p} \beta_{p+1,\ell} \pi(z_\ell) + \lambda \pi(z_{k_0}), \pi(z_{k_0}) \right\rangle + \mathop{\mathrm{o}}_{n \to +\infty} (\alpha_{k_0,n}) \\
&= \alpha_{k_0,n} \left( \lambda \|\pi(z_{k_0})\|^2 + \left\langle \pi(z_{p+1}) + \sum_{\ell=k_0}^{p} \beta_{p+1,\ell} \pi(z_\ell), \pi(z_{k_0}) \right\rangle \right) + \mathop{\mathrm{o}}_{n \to +\infty} (\alpha_{k_0,n}).
\end{align*}
$$
Therefore, taking any $\lambda > 0$ such that

$$ \lambda > - \frac{\left\langle \pi(z_{p+1}) + \sum_{\ell=k_0}^{p} \beta_{p+1,\ell} \pi(z_\ell), \pi(z_{k_0}) \right\rangle}{\|\pi(z_{k_0})\|^2} $$

we get $S_n(\lambda) \underset{n \to +\infty}{\longrightarrow} +\infty$. Thus, for sufficiently large $n$,

$$ \left\langle \pi \left( z_{p+1} + \sum_{\ell=1}^{p} \beta_{p+1,\ell} z_{\ell} \right) + \lambda \pi \left( z_{k_0} + \sum_{\ell=1}^{k_0-1} \beta_{k_0,\ell} z_{\ell} \right), \pi \left( \sum_{k=1}^{p} \alpha_{k,n} z_k + z_{p+1} \right) \right\rangle > 0. $$

Also,

$$ \left( x, z_{p+1} + \sum_{\ell=1}^{p} \beta_{p+1,\ell} z_{\ell} + \lambda z_{k_0} + \lambda \sum_{\ell=1}^{k_0-1} \beta_{k_0,\ell} z_{\ell} \right) = \underbrace{\left( x, z_{p+1} + \sum_{\ell=1}^{p} \beta_{p+1,\ell} z_{\ell} \right)}_{\in \mathrm{rec}(K)} + \underbrace{\lambda \left( 0, z_{k_0} + \sum_{\ell=1}^{k_0-1} \beta_{k_0,\ell} z_{\ell} \right)}_{\in \mathrm{rec}(K)} $$

$$ \left( x, z_{p+1} + \sum_{\ell=1}^{p} \beta_{p+1,\ell} z_{\ell} + \lambda z_{k_0} + \lambda \sum_{\ell=1}^{k_0-1} \beta_{k_0,\ell} z_{\ell} \right) \in \mathrm{rec}(K). $$

Thus, considering

$$ \beta'_{p+1,\ell} = \begin{cases} \beta_{p+1,\ell} & \ell > k_0 \\ \beta_{p+1,\ell} + \lambda & \ell = k_0 \\ \beta_{p+1,\ell} + \lambda \beta_{k_0,\ell} & \ell < k_0 \end{cases} $$

instead of the $\beta_{k+1,\ell}$s, we get the desired result.

<figure><img src="image_16.png" /></figure>

### 3 Deciding the Constraint Loop Problem

The goal of this section is to establish Theorem 2. This will be done by showing equivalence between the existence of a witness of the form given by Definition 1 and the existence of an infinite run of a constraint loop. The easy direction in this argument – constructing an infinite execution from a witness – is the purpose of Proposition 27 in Subsection 3.2. In fact, there is an even easier case, namely certifying the existence of bounded infinite run, is dealt with in Section 3.1. It states that a bounded infinite run exists if an only if there is a fixed point. This proof holds in any dimension and relies on a simpler certificate. We will also reuse this result in the specific cases of dimension 1 and 2.

The main objective in this section is to construct a witness from an infinite execution. We provide the proof of sufficient condition in Subsection 3.2. This will help motivate the definition of witness. Subsection 3.3 deals with the simple 1-dimensional case, and Subsection 3.4 handles the dimension-2 case, which is more challenging. Because of the difficulty of this proof we only provide high level explanation here. For a complete proof, we refer to the full-version of this article [6].
## 3.1 Deciding the Existence of a Bounded Sequence

**Proposition 26.** Let $E$ be a vector space of dimension $d \in \mathbb{N}$. Let $K \subseteq E^2$ be closed convex. Denoting $\Delta_E = \{(x, x) | x \in E\} \subseteq E^2$, we have that $K \cap \Delta_E \neq \emptyset$ if and only if there is a bounded sequence $u = (u_n)_{n \in \mathbb{N}}$ of $E$ such that for all $n \in \mathbb{N}$, $(u_n, u_{n+1}) \in K$.

**Proof.**

(⇒) Let $(x, x) \in K \cap \Delta_E$. The sequence constantly equal to $x$ satisfy the proposition.

( ⇐ ) Assume now that there exists a bounded sequence $(u_n)_{n \in \mathbb{N}}$ such that for all $n \in \mathbb{N}$, $(u_n, u_{n+1}) \in K$. Let $n \in \mathbb{N}^*$ and define $x_n = \frac{1}{n} \sum_{p=0}^{n} (u_p, u_p)$ and $y_n = \frac{1}{n} \sum_{p=0}^{n-1} (u_p, u_{p+1})$.

We have

$$ \|x_n - y_n\| = \frac{1}{n} \|(u_n, u_0)\|. $$

Since the sequence $(u_n)_{n \in \mathbb{N}}$ is bounded, there is a positive real number $M$ such that

$$ \forall n \in \mathbb{N}^* \quad \|x_n - y_n\| \le \frac{M}{n}. $$

In particular, both sequences $(x_n)_{n \in \mathbb{N}^*}$ and $(y_n)_{n \in \mathbb{N}^*}$ must have the same accumulation points. As these sequences are bounded (and since they are in a vector space of finite dimension), such a point exists. Let us denote it $x$. Notice that since $K$ is closed and convex, for all positive integer $n$, $y_n \in K$ and thus $x \in K$. Moreover, by definition, for all positive integer $n$, $x_n \in \Delta_E$. This set is again closed, thus $x \in \Delta_E$. This proves that

$$ x \in K \cap \Delta_E \neq \emptyset. $$

<figure><img src="image_17.png" /></figure>

## 3.2 A Sufficient Condition for the Existence of a Sequence

**Proposition 27.** Let $E$ be an Euclidean space of dimension $d$. Let $K \subseteq E^2$ be MW-convex. If there exists a witness $W(K)$, then, there is a sequence $(u_n)_{n \in \mathbb{N}} \in E^N$ such that

$$ \forall n \in \mathbb{N} \quad (u_n, u_{n+1}) \in K. $$

**Proof.** Assume we have a witness $W(K)$. We then take $M, v, w, C$ as given by the witness and define the following sequence:

$$ u_0 = v \quad \text{and} \quad u_1 = w $$

$$ \forall n \in \mathbb{N} \quad u_{n+2} - u_{n+1} = M(u_{n+1} - u_n) $$

Remark first that for all $n \in \mathbb{N}$, $u_{n+1} - u_n \in C$. This can be proven by induction, noting that the initialisation is given by Point $(\exists u4)$ and the induction step comes from Point $(\exists u1)$.

We now prove by induction that $\forall n \in \mathbb{N} \quad (u_n, u_{n+1}) \in K$.

■ By Point $(\exists u3)$, $(u_0, u_1) \in K$.

■ Assume that for some $n \in \mathbb{N}$, $(u_n, u_{n+1}) \in K$. As $u_{n+1} - u_n \in C$ as shown before, by Point $(\exists u2)$

$$ (u_{n+1} - u_n, u_{n+2} - u_{n+1}) \in \mathrm{rec}(K). $$

$$ \text{Thus } (u_{n+1}, u_{n+2}) = (u_n, u_{n+1}) + (u_{n+1} - u_n, u_{n+2} - u_{n+1}) \in K + \mathrm{rec}(K) = K. $$

By the induction principle we conclude that for all $n \in \mathbb{N}$, $(u_n, u_{n+1}) \in K$.

<figure><img src="image_18.png" /></figure>
## 3.3 Necessary Condition for the Existence of a 1-Dimensional Sequence

We establish the main result in the one dimensional case. Note that we prove a slightly stronger certificate here, which is not necessary in itself, but which we need for the 2 dimensional case.

**Proposition 28.** Let $E$ be an Euclidean space of dimension 1. Let $K \subseteq E^2$ be MW-convex. Let a sequence $(u_n)_{n \in \mathbb{N}} \in E^\mathbb{N}$ such that $(u_n, u_{n+1}) \in K$ for all $n \in \mathbb{N}$. Let $\gamma \in \text{cone}(D_u)$ such that $(0, \gamma) \in \text{rec}(K)$ (note that at least $\gamma = 0$ works). Then, there are $a \in \mathbb{R}^*$, a closed convex cone $C \subseteq E$ and $x, y \in E$ such that

(i) $aC \subseteq C$

(ii) $\forall x \in C \quad (x, ax) \in \text{rec}(K)$

(iii) $(x, y) \in K$

(iv) $y - x \in C$

(v) $\gamma \in C$

**Proof.** Without loss of generality, as $E$ is an Euclidean space of dimension 1, we assume $E = \mathbb{R}$. If $(u_n)_{n \in \mathbb{N}}$ is bounded, then, by Proposition 26 there exists $z \in \mathbb{R}$ such that $(z, z) \in K$. Then $\gamma = 0$ and we can select $y = x = z$, $C = \{0\}$ and $a \in \mathbb{R}^*$ arbitrary (e.g. 1) to produce the requested witness.

We now assume that $(u_n)_{n \in \mathbb{N}}$ is unbounded. By Proposition 22, it admits accumulation expansions and $D_u \neq \emptyset$. The only two possible accumulation directions are 1 and $-1$. We consider three cases:

- If $D_u = \{-1, 1\}$. Take $\varphi_1$ and $\varphi_{-1}$ such that $\widetilde{u_{\varphi_1(n)}} \xrightarrow{n \to +\infty} 1$ and $\widetilde{u_{\varphi_{-1}(n)}} \xrightarrow{n \to +\infty} -1$. Up to extracting a subsequence, we have the accumulation expansions

$$ \frac{u_{\varphi_1(n)+1}}{\|u_{\varphi_1(n)}\|} = \sum_{k=1}^{p} \alpha_{k,n} z_k + z_{p+1} + \mathbf{o}(1) $$

$$ \text{and} \quad \frac{u_{\varphi_{-1}(n)+1}}{\|u_{\varphi_{-1}(n)}\|} = \sum_{k=1}^{p'} \alpha'_{k,n} z'_{k} + z'_{p'+1} + \mathbf{o}(1). $$

Then, by Corollary 25, there are $\alpha, \beta \in \mathbb{R}$ such that

$$ (1, \alpha) \in \text{rec}(K) \quad \text{and} \quad (-1, \beta) \in \text{rec}(K). $$

$$ \text{Let } \delta = \begin{cases} \gamma & \text{if } \gamma \neq 0 \\ \alpha + \beta & \text{if } \gamma = 0. \end{cases} $$

Therefore, either $(0, \delta) = (0, \gamma) \in \text{rec}(K)$, or $(0, \delta) = (1, \alpha) + (-1, \beta)$ and $(0, \delta) \in \text{rec}(K)$ by conic combinations.

- If $\delta = 0$ then $\gamma = 0$ and $\alpha = -\beta$.

* If $\alpha = 0$, then $\beta = 0$, $(u_1, u_1) = \underbrace{(u_0, u_1)}_{\in K} + \underbrace{(u_1 - u_0, 0)}_{\in \text{rec}(K)} \in K$.

We then choose for instance $a \in \mathbb{R}^*$, $C = \{0\}$ and $x = y = u_1$.

* If $\alpha \neq 0$, then we just have to take $a = \alpha$, $C = \mathbb{R}$, $x = u_0$, $y = u_1$.

Note that in both these cases we trivially have $\gamma \in C$.

- If $\delta > 0$ then, for large enough $n$, $n\delta + \alpha > 0$. Moreover, as $\text{rec}(K)$ is a cone,

$$ (1, n\delta + \alpha) = \underbrace{n(0, \delta)}_{\in \text{rec}(K)} + \underbrace{(1, \alpha)}_{\in \text{rec}(K)} \in \text{rec}(K). $$
140:16 The 2-Dimensional Constraint Loop Problem Is Decidable

We then take $a = n\delta + \alpha > 0$, $C = \mathbb{R}_+$, $x = u_k$, $y = u_{k+1}$, for some $k$ such that $u_{k+1} - u_k > 0$. This exists since $1 \in \mathcal{D}_u$ and hence $(u_n)_{n \in \mathbb{N}}$ is not bounded from above. Note also that since $\delta > 0$ then $\gamma \ge 0$. Thus $\gamma \in C$.

- If $\delta < 0$ then, for large enough $n$, $n\delta + \beta < 0$. Moreover, as $\mathrm{rec}(K)$ is a cone,

$$(-1, n\delta + \beta) = \underbrace{n(0, \delta)}_{\in \mathrm{rec}(K)} + \underbrace{(-1, \beta)}_{\in \mathrm{rec}(K)} \in \mathrm{rec}(K).$$

We then take $a = -n\delta - \beta > 0$, $C = \mathbb{R}_-$, $x = u_k$, $y = u_{k+1}$ for some $k$ such that $u_{k+1} - u_k < 0$. This exists since $-1 \in \mathcal{D}_u$ and hence $(u_n)_{n \in \mathbb{N}}$ is not bounded from below. Note also that since $\delta < 0$ then $\gamma \le 0$. Thus $\gamma \in C$.

- If $\mathcal{D}_u = \{1\}$, then, similarly to the first case, using Corollary 25, there is some $\alpha \in \mathbb{R}_+$ such that $(1, \alpha) \in \mathrm{rec}(K)$. Note also that $\gamma \ge 0$ and that $(1, \alpha + \gamma) \in \mathrm{rec}(K)$. Let $k$ such that $u_{k+1} - u_k > 0$. This exists since $1 \in \mathcal{D}_u$ and hence $(u_n)_{n \in \mathbb{N}}$ is not bounded from above.

- If $\alpha + \gamma = 0$, then, $\alpha = \gamma = 0$ and

$$(u_{k+1}, u_{k+1}) = \underbrace{(u_k, u_{k+1})}_{\in K} + \underbrace{(u_{k+1} - u_k, 0)}_{\in \mathrm{rec}(K)} \in K.$$

We then choose for instance $a \in \mathbb{R}^*$, $C = \{0\}$ and $x = y = u_{k+1}$.

- If $\alpha + \gamma > 0$, then we just have to take $a = \alpha + \gamma$, $C = \mathbb{R}_+$, $x = u_k$ and $y = u_{k+1}$. Note that in both cases, $\gamma \in \mathbb{R}_+ = C$.

- The case $\mathcal{D}_u = \{-1\}$ can be made similarly to the previous point. ◀

<figure><img src="image_19.png" /></figure>

We are now ready to prove the special case of Theorem 2 in which $E$ has dimension 1 (see Section 1). Without loss of generality we just consider $E = \mathbb{R}$. The necessary condition is given by the application of Proposition 28 with $\gamma = 0$. The sufficient condition is given by Proposition 27.

3.4 Necessary Condition for the Existence of a 2-Dimensional Sequence

We now move to 2-dimensional Euclidean spaces and prove that the existence of a witness as given by Definition 1 is implied by the existence of an infinite sequence. This, combined with Proposition 27 will imply Theorem 2.

For the entire section, we thus fix $E$ to be an Euclidean space of dimension 2, $K \subseteq E^2$ to be MW-convex and thus satisfying $K = K' + \mathrm{rec}(K)$ where $K'$ is a compact convex set. We assume that there exists a sequence $(u_n)_{n \in \mathbb{N}} \in E^\mathbb{N}$ such that for all $n \in \mathbb{N}$, $(u_n, u_{n+1}) \in K$. We start by two technical lemmas to lighten the proof of the proposition.

**Lemma 29.** Assume that $\mathcal{D}_u$ is not empty and for all $x \in \mathrm{cone} \mathcal{D}_u$, if $(0, x) \in \mathrm{rec}(K)$, then $x = 0$. Denoting $\mathrm{cone} \mathcal{D}_u = \mathrm{cone} \mathcal{D}_u$, we have that for all $x \in \mathcal{C}_u$, there is $s(x) \in \mathcal{C}_u$ such that $(x, s(x)) \in \mathrm{rec}(K)$.

**Proof.** Let $x \in \mathcal{C}_u$. By definition, we can consider $x_1, \dots, x_m \in \mathcal{D}_u$ and $\lambda_1, \dots, \lambda_m \in \mathbb{R}_+$ such that $x = \sum_{i=1}^m \lambda_i x_i$. By definition of $\mathcal{D}_u$, for $i \in [1; m]$ there is an increasing function $\varphi_i : \mathbb{N} \to \mathbb{N}$ such that $\widetilde{u}_{\varphi_i(n)} \xrightarrow{n \to +\infty} x_i$. Using Proposition 22, the sequence $((u_{\varphi_i(n)}, u_{\varphi_i(n)+1}))_{n \in \mathbb{N}}$ admits an accumulation expansion

$$(u_{\varphi_i \circ \psi_i(n)}, u_{\varphi_i \circ \psi_i(n)+1}) = \sum_{k=1}^{p_i} \alpha_{i,k,n} (z_{i,k,1}, z_{i,k,2}) + (z_{i,p+1,1}, z_{i,p+1,2}) + \mathbf{o}_{n \to +\infty}(1).$$
In particular, for $k \in [1; p_i]$ minimum such that $z_{i,k,1} \neq 0$, we have $z_{i,k,1} \in \mathbb{R}_+^* x_i$. Since the first component is not bounded, such a $k$ exists. Let $\mu_i > 0$ such that $z_{i,k,1} = \mu_i x_i$. Now, applying Proposition 23, $(z_{i,1,1}, z_{i,1,2}) \in \text{rec}(K)$ and $\|(z_{i,1,1}, z_{i,1,2})\| = 1$. Therefore, if $k > 1$, then $z_{i,1,1} = 0$ and $\|z_{i,1,2}\| = 1$. Hence $z_{i,1,2} \in D_u$. This contradicts the hypothesis that for all $x \in C_u$, if $(0, x) \in \text{rec}(K)$, then $x = 0$. Thus, $k = 1$. Considering $s(x_i) = \frac{1}{\mu_i} z_{i,1,2}$ satisfies the claim for $x_i$. Thus, defining $s(x) = \sum_{i=1}^m \lambda_i s(x_i)$ establishes the lemma. ◀

**Lemma 30.** Assume that $D_u$ is not empty, that for all $x \in \text{cone } D_u$, if $(0, x) \in \text{rec}(K)$, then $x = 0$ and for all $x \in E$, $(x, x) \notin K$. Denoting $C_u = \text{cone } D_u$, for all $x \in D_u$, there are $\delta(x) \in E$ and $\lambda \in \mathbb{R}_+^*$ such that $(\delta(x), \lambda x + \delta(x)) \in K \cup \text{rec}(K)$.

**Proof.** Let $x \in D_u$ and the accumulation expansion

$$u_{\varphi(n)} = \sum_{k=1}^{p} \alpha_{k,n} z_k + z_{p+1} + \mathbf{o}_{n \to +\infty} (1)$$

with $p > 0$ and $z_1 = x$. By convexity, we have

$$\forall n \in \mathbb{N} \quad \frac{1}{\varphi(n)} \sum_{k=0}^{\varphi(n)-1} (u_k, u_{k+1}) \in K.$$

Up to refining $\varphi$, we can assume that we also have the accumulation expansion

$$\frac{1}{\varphi(n)} \sum_{k=0}^{\varphi(n)-1} (u_k, u_{k+1}) = \sum_{k=1}^{q} \beta_{k,n}(w_{k,1}, w_{k,2}) + (w_{q+1,1}, w_{q+1,2}) + \mathbf{o}_{n \to +\infty} (1).$$

Therefore

$$\begin{aligned} \sum_{k=1}^{q} \beta_{k,n}(w_{k,2} - w_{k,1}) + w_{q+1,2} - w_{q+1,1} &= \frac{1}{\varphi(n)} \sum_{k=0}^{\varphi(n)-1} (u_{k+1} - u_k) + \mathbf{o}_{n \to +\infty} (1) \\ &= \frac{u_{\varphi(n)} - u_0}{\varphi(n)} + \mathbf{o}_{n \to +\infty} (1) \\ &= \sum_{k=1}^{p} \frac{\alpha_{k,n}}{\varphi(n)} z_k + \mathbf{o}_{n \to +\infty} (1). \end{aligned}$$

If $(\frac{\alpha_{1,n}}{\varphi(n)})_{n \in \mathbb{N}}$ has an accumulation point, say $\lambda$, up to refining $\varphi$, we assume that it converges to it. By definition of an accumulation expansion, we then have for all $k \in [1; q]$, $w_{k,1} = w_{k,2}$. Therefore, $w_{q+1,2} - w_{q+1,1} = \lambda x$.

By Proposition 23, there are some positive real numbers $\gamma_1, \dots, \gamma_q$ such that

$$\sum_{k=1}^{q} \gamma_k (w_{k,1}, w_{k,2}) + (w_{q+1,1}, w_{q+1,2}) \in K.$$

The difference between the two coordinates of this vector is $\lambda x$. Since $\lambda$ is the limit of a positive sequence, $\lambda \ge 0$. Also, provided that there is no $a \in E$ such that $(a, a) \in K$ by hypothesis, we have $\lambda \ne 0$. Therefore, considering $\delta(x) = \sum_{k=1}^q \gamma_k w_{k,1} + w_{q+1,1}$ we get $(\delta(x), \lambda x + \delta(x)) \in K$.
140:18 The 2-Dimensional Constraint Loop Problem Is Decidable

Now suppose that $(\frac{\alpha_{1,n}}{\varphi(n)})_{n \in \mathbb{N}}$ has no accumulation point. Since it is positive, we have

$$ \frac{\alpha_{1,n}}{\varphi(n)} \xrightarrow{n \to +\infty} +\infty. $$

Thus, there is $k \in [1; q]$ minimum such that $w_{k,1} \neq w_{k,2}$ and for this $k$, we have

$$ \beta_{k,n}(w_{k,2} - w_{k,1}) \underset{n \to +\infty}{\sim} \frac{\alpha_{1,n}}{\varphi(n)}x. $$

Therefore, there is $\lambda > 0$ such that $w_{k,2} - w_{k,1} = \lambda x$. By Proposition 23, there are some positive real numbers $\gamma_1, \dots, \gamma_{k-1}$ such that

$$ \sum_{\ell=1}^{k-1} \gamma_{\ell}(w_{\ell,1}, w_{\ell,2}) + (w_{k,1}, w_{k,2}) \in \mathrm{rec}(K). $$

The difference between the two coordinates of this vector is $\lambda x$. Therefore, considering

$$ \delta(x) = \sum_{\ell=1}^{k-1} \gamma_{\ell} w_{\ell,1} + w_{k,1} \text{ we have } (\delta(x), \lambda x + \delta(x)) \in \mathrm{rec}(K). \quad \blacksquare $$

► **Proposition 31.** *There exists a witness W(K).*

For the detailed proof we refer to the full version [6]. Here we just give an overview of the proof.

**Proof sketch.** The proof is divided into several cases under the structure described in Figure 1. Among all these cases, Case 6 is by far the most difficult, followed by Cases 2 and 5, then Case 4 (quite easy) and finally the almost trivial Cases 1 and 3. In this proof we denote $C_u = \mathrm{cone}(D_u)$.

■ **Case 1:** There is a fixed point $(x, x)$ in $K$. In this case we just need to take $v = w = x$, $M$ arbitrary and $C = \{0\}$ to get a Witness. This just leads to a constant sequence.

■ **Case 2:** No fixed point but there is $x \in C_u \setminus \{0\}$ such that $(0, x) \in \mathrm{rec}(K)$. In this case we are going to try to make use of Proposition 28. Let $\pi: E \to E$ be the orthogonal projection onto $x^{\perp}$ and let $\hat{\pi}: E^2 \to E^2$ be such that

$$ \forall e, f \in E, \hat{\pi}(e, f) = (\pi(e), \pi(f)). $$

Assume that we have found some $x'$ such that $(x, x') \in \mathrm{rec}(K)$. We then can write $x' = \gamma x + y$ for some $y$ orthogonal to $x$ and some $\gamma \in \mathbb{R}$. Then we have $\hat{\pi}(x, x') = (0, y)$. Also $(0, y) \in \hat{\pi}(\mathrm{rec}(K)) = \mathrm{rec}(\hat{\pi}(K))$. Thus if we can build $x'$ such that $y \in \mathrm{cone}(D_{\pi(u)})$, we would be allowed to apply Proposition 28. This requires some work. The idea is to write $x = \sum_{i=1}^{n} a_i x_i$ with $x_i \in D_u$ and $a_i \ge 0$ then apply Corollary 25 for all $i \in [1; n]$ (see the full version [6] for details). Assume this is done. There are $a \in \mathbb{R}^*$, a closed convex cone $C \subseteq x^{\perp}$ and $v, w \in x^{\perp}$ such that

- $aC \subseteq C$

- $\forall c \in C \quad (c, ac) \in \mathrm{rec}(\hat{\pi}(K))$

- $(v, w) \in \hat{\pi}(K)$

- $w - v \in C$

- $y \in C$
<figure><img src="image_20.png" /><figcaption>Figure 1 The case disjunction structure.</figcaption></figure>

Again, since $\mathrm{rec}(\hat{\pi}K) = \hat{\pi}(\mathrm{rec}(K))$, for all $\xi \in C$, there are $b_{\xi}, c_{\xi} \in \mathbb{R}$ such that $(b_{\xi}x + \xi, c_{\xi}x + a\xi) \in \mathrm{rec}(K)$. For all $\xi \in C$, we fix $b_{\xi}$ and $c_{\xi}$ such that $(|b_{\xi}|, |c_{\xi}|)$ is minimal for the lexicographic order and among all these possibilities, such that $(b_{\xi}, c_{\xi})$ is maximal for the lexicographic order. We denote

$$ \gamma_0(\xi) = \max(1, \gamma, b_{\xi}) \quad \text{and} \quad \gamma_1(\xi) = \max(|a|, b_{a\xi}, c_{\xi}) $$

and for $n \ge 1$,

$$ \gamma_{2n}(\xi) = \max(a^{2n}, a^{2n}b_{\xi}, a^{2(n-1)}c_{a\xi}) $$

$$ \gamma_{2n+1}(\xi) = \max(|a|^{2n+1}, a^{2n}b_{a\xi}, a^{2n}c_{\xi}). $$

For $n \in \mathbb{N}$, let

$$ \chi_n(\xi) = \gamma_n(\xi)x + a^n\xi \quad \text{and} \quad b'_{n,\xi} = \begin{cases} a^{2n}b_{\xi} & n \in 2\mathbb{N} \\ a^{2n}b_{a\xi} & n \in 2\mathbb{N} + 1. \end{cases} $$

We some algebraic manipulations and intensively using that $(0, x) \in \mathrm{rec}(K)$ to add missing weight on $x$ in the second component, we get

$$ \forall n \in \mathbb{N} \quad (\chi_n(\xi), \chi_{n+1}(\xi) + (\gamma_n(\xi) - b'_{n,\xi}) \chi_0(y)) \in \mathrm{rec}(K). $$
Recalling that $w - v \in C$ we define $C' = \mathbb{R}_+x + \sum_{n \in \mathbb{N}} (\mathbb{R}_+\chi_n(w-v) + \mathbb{R}_+\chi_n(y))$ This is the cone we want to use. It is finitely generated. We can also see that it cannot contain line. Since all such two-dimensional cones are generated by at most two vectors we can find such generating vectors. $M$ will just be a matrix defined thanks to its behavior on these vectors and $C'$ is defined to get stability. Finally, up to add some component on $x$ again we can get our starting conditions thanks to $v$ and $w$ (See details in the full version [6]).

**Case 3:** No fixed point or $x \in C_u \setminus \{0\}$ such that $(0, x) \in \text{rec}(K)$. However there are $a \in E$, $x \in D_u$ and $\mu \in \mathbb{R}_+$ such that $(a, a+\mu x) \in K$. This means that their is a principle direction of $u$ along which it is possible to take a first step. In this case, we select $C = C_u$. $C$ is a non empty closed convex cone of $\mathbb{R}^2$, thus, there are two vectors $x_1, x_2 \in C \setminus \{0\}$ such that either $C = \mathbb{R}x_1 + \mathbb{R}_+x_2$ or $C = \mathbb{R}_+x_1 + \mathbb{R}_+x_2$ or $C = \mathbb{R}x_1 + \mathbb{R}x_2$. Let $I \subseteq \{1, 2\}$, $I \neq \emptyset$ the largest set such that $(x_i)_{i \in I}$ is a free family. Using the function $s$ defined by Lemma 29, we define $M$ such that $Mx_i = s(x_i)$ for all $i \in I$. Noting that since, for $i \in I$, $-x_i \in C$, $(0, s(x_i) + s(-x_i)) \in \text{rec}(K)$, we have that $s(-x_i) = -s(x_i)$, this choice of $M$ satisfies Points $(\exists u1)$ and $(\exists u2)$. We now choose $v = a$ and $w = a + \mu x$. By assumption, $(v, w) \in K$. Also, $w - v = \mu x \in C_u = C$. $C, v$ and $w$ thus satisfy Points $(\exists u3)$ and $(\exists u4)$.

**Case 4:** No fixed point, $x \in C_u \setminus \{0\}$ such that $(0, x) \in \text{rec}(K)$ or $a \in E$, $x \in D_u$, $\mu \in \mathbb{R}_+$ such that $(a, a + \mu x) \in K$. However $D_u$ spans the entire space $E$. Given that, take $(a, b) \in K$. Using Lemma 13 there is $\lambda \ge 0$ such that $y := b - a + \lambda x \in C_u$. Let $v = a + \lambda\delta(x)$ and $w = b + \lambda(x + \delta(x))$ with $\delta$ given by Lemma 30. We then have $(u, v) \in K$. Let $C = \text{cone} \{s^k(y) \mid k \in \mathbb{N}\}$ with $s$ being the function defined in Lemma 29. $C$ is a closed convex cone in a 2-dimensional vector space, therefore there are vectors $\zeta_1, \zeta_2 \in C \setminus \{0\}$ such that

$$C \in \{ \mathbb{R}_+\zeta_1 + \mathbb{R}_+\zeta_2, \mathbb{R}_1\zeta_1 + \mathbb{R}_+\zeta_2, \mathbb{R}_+\zeta_1 + \mathbb{R}_2\zeta_2, \mathbb{R}_1\zeta_2 + \mathbb{R}_2\zeta_2 \}.$$

Let $(\zeta_{i,n})_{n \in \mathbb{N}}$ be a sequence in cone $\{s^k(y) \mid k \in \mathbb{N}\}$ such that

$$\zeta_{i,n} \xrightarrow{n \to +\infty} \zeta_i.$$

If $(s(\zeta_{i,n}))_{n \in \mathbb{N}}$ is unbounded then Proposition 23 ensures that there is some $\zeta'_i \in D_{(s(\zeta_{i,n}))_{n \in \mathbb{N}}}$ such that $(0, \zeta'_i) \in \text{rec}(K)$ and $\zeta'_i \in C_u$. This is impossible by assumption on $C_u$. Therefore, it is bounded and we have an accumulation point $\zeta'_i \in C$. Since $\text{rec}(K)$ is closed, we also have $(\zeta_i, \zeta'_i) \in \text{rec}(K)$. Let $I \subseteq \{1, 2\}$ maximal such that $(\zeta_i)_{i \in I}$ is a free family. Let $M$ be a matrix such that

$$\forall i \in I \quad M\zeta_i = \zeta'_i.$$

**Case 5:** No fixed point, $x \in C_u \setminus \{0\}$ such that $(0, x) \in \text{rec}(K)$ or $a \in E$, $x \in D_u$, $\mu \in \mathbb{R}_+$ such that $(a, a + \mu x) \in K$ and $C_u$ is a line $C_u = \mathbb{R}x$. This case uses the induction hypothesis (Proposition 28) and similar techniques as in Case 2. The main change here is that we use the function $s$ defined by Lemma 29. Here $s(x)$ will have to be collinear with $x$. In stead of adding multiples of $(0, x)$, we have access to some $(x, \gamma x) \in \text{rec} K$ and are allowed negative coefficients which makes the case relatively easy. See details in the full version [6].

**Case 6:** No fixed point, $x \in C_u \setminus \{0\}$ such that $(0, x) \in \text{rec}(K)$ or $a \in E$, $x \in D_u$, $\mu \in \mathbb{R}_+$ such that $(a, a + \mu x) \in K$ and $C_u = \mathbb{R}_+x$ for some $x$. Let $y \in x^{\perp}$ such that $\|y\| = 1$. The main goal of this case is to find $a, b \ge 0$ and $c, d \in \mathbb{R}$ such that

$$(x, ax) \in \text{rec}(K) \quad \text{and} \quad (dx + y, cx + by) \in \text{rec}(K) \quad \text{and} \quad c \ge db.$$
This can be achieved by a very careful look at the asymptotic behavior of the $(u_n)_{n \in \mathbb{N}}$ and more precisely its components along $x$ and $y$. Namely, the component along $x$ must blow up significantly faster than the one along $y$. This is where the difficulty of this case lies. We refer to the full version [6] for the details. This naturally leads to choose $C$ and $M$ such that:

$$C = \mathbb{R}_+x + \mathbb{R}_+(dx + y) \quad \text{and} \quad Mx = ax \quad \text{and} \quad M(dx + y) = cx + by$$

immediately satisfying $(\exists u1)$ and $(\exists u2)$. With the same technics we can show that there is some $n \in \mathbb{N}$ such that

$$\langle u_{n+1} - u_n, x \rangle \geq d \langle u_{n+1} - u_n, y \rangle.$$

Then considering $v = u_n$ and $w = u_{n+1}$.

$$\begin{aligned} w - v &= u_{n+1} - u_n = \langle u_{n+1} - u_n, x \rangle x + \langle u_{n+1} - u_n, y \rangle y \\ &= (\langle u_{n+1} - u_n, x \rangle - d \langle u_{n+1} - u_n, y \rangle) x + \langle u_{n+1} - u_n, y \rangle (dx + y) \in C. \end{aligned}$$

Hence, Points $(\exists u3)$ and $(\exists u4)$ are satisfied by $C$, $v$, $w$.

<figure><img src="image_21.png" /></figure>

References

1. Amir M. Ben-Amram, Jesús J. Doménech, and Samir Genaim. Multiphase-linear ranking functions and their relation to recurrent sets. In *Static Analysis - 26th International Symposium, SAS 2019, Proceedings*, volume 11822 of *Lecture Notes in Computer Science*, pages 459–480. Springer, 2019.

2. Amir M. Ben-Amram and Samir Genaim. Ranking functions for linear-constraint loops. *Journal of the ACM*, 61(4):1–55, 2014. doi:10.1145/2629488.

3. Amir M. Ben-Amram, Samir Genaim, and Abu Naser Masud. On the termination of integer loops. *ACM Transactions on Programming Languages and Systems*, 34(4):1–24, 2012. doi:10.1145/2400676.2400679.

4. Marius Bozga, Radu Iosif, and Filip Konecný. Deciding conditional termination. *Log. Methods Comput. Sci.*, 10(3), 2014. doi:10.2168/LMCS-10(3:8)2014.

5. Mark Braverman. Termination of integer linear programs. In *Computer Aided Verification 2006*, volume 4144 of LNCS, pages 372–385. Springer Berlin Heidelberg, 2006. doi:10.1007/11817963_34.

6. Quentin Guilmant, Engel Lefaucheux, Joël Ouaknine, and James Worrell. The 2-dimensional constraint loop problem is decidable, 2024. arXiv:2405.12992.

7. Mehran Hosseini, Joël Ouaknine, and James Worrell. Termination of linear loops over the integers. In *ICALP 2019*, volume 132 of LIPIcs, pages 118:1–118:13. Schloss Dagstuhl – Leibniz-Zentrum für Informatik, Wadern/Saarbruecken, Germany, 2019. doi:10.4230/LIPICS.ICALP.2019.118.

8. Jan Leike and Matthias Heizmann. Geometric nontermination arguments. In *Tools and Algorithms for the Construction and Analysis of Systems - 24th International Conference, TACAS 2018*, volume 10806 of *Lecture Notes in Computer Science*, pages 266–283. Springer, 2018.

9. Naomi Lindenstrauss and Yehoshua Sagiv. Automatic termination analysis of logic programs. In Lee Naish, editor, *Logic Programming, Proceedings of the Fourteenth International Conference on Logic Programming*, 1997, pages 63–77. MIT Press, 1997.

10. Ashish Tiwari. Termination of linear programs. In *Computer Aided Verification 2004*, volume 3114 of LNCS, pages 70–82. Springer Berlin Heidelberg, 2004. doi:10.1007/978-3-540-27813-9_6.