“Does a given program halt?” is perhaps the simplest question that one could ask of programs. It has fascinated computer scientists and has been at the root of a number of deep results ever since the earliest undecidability results by Turing. This paper carries on in this tradition and illuminates yet another part of this inexhaustible space of problems.

Since we know that the problem of termination in general is undecidable, it is only natural to analyze the space of programs and identify subclasses where the problem is decidable. This line of thought has led to some elegant results showing the decidability of certain linear loops [1,2]. This leads to the question of how tight these results are.

The authors present some extensions of linear loops and prove undecidability results for them. They also investigate variants of the termination problem, considering termination on given inputs in contrast with termination on all inputs, and prove undecidability results for these variants.

One extension introduces an instruction for testing the sign of a number. This instruction does not have the expressive power of a general conditional statement, but termination for even this is shown to be undecidable by a reduction to the problem of termination of a two-counter machine, which is known to be undecidable.

The other extension is motivated by practical applications in program analysis and introduces the notion of an integer constraint loop that could be used to represent an abstraction of a program. Though the paper is not able to construct a simulation of a two-counter machine, it demonstrates a simulation of Petri nets, thereby establishing a lower bound on the termination problem for integer constraint loops.

The paper contains a number of interesting and even curious results. For example, the introduction of at least a single irrational constant in linear constraint loops is necessary to encode a simulation of two-counter programs. The authors use an expressibility result from mixed integer programming to prove this result!

The paper opens up a number of interesting follow-up questions of both theoretical and practical interest, which can provide fodder for future research in this area.