I'm working with the size-change termination principle to show program termination. In the system I work with, there is a so-called bit-vector ordering that goes as follows:

Given two sequences of arguments $s_1,s_2$.

  1. Filter the bitvector arguments (long/int/short/byte)

  2. Divide each sequence of arguments $s$ according to length (so one group is int, other short and so on). Denote the arguments of type $t$ in sequence $s$ as $s.t$.

  3. If $s.t$ is defined for $s_1,s_2$, compare $s_1.t$ with $s_2.t$ lexicographically.

We define $s_1 < s_2$ when there exists a type $t$ such that $s_1.t < s_2.t$.

I have confirmed that this behaviour is wrong. Indeed, if one has two sequences $s_1,s_2$ that contain ints and shorts where $s_1.int < s_2.int$ and $s_2.short < s_1.short$ we would deduce that $s_1 < s_2$ and $s_2 < s_1$.

What is the standard orders for lists of bitvectors while using the size-change termination principle?

  • $\begingroup$ In general, there is no single order that suits all needs for termination. What kinds of applications are you imagining? Are the bit-vectors representing numbers? $\endgroup$ – cody Aug 16 '18 at 14:24
  • $\begingroup$ @cody the bit-vectors have the same semantics as in the Java programming language (so they do represent numbers right? with special overflow conditions and so on...). Regarding the order, I have changed to plural, so I would be looking for standard orders instead $\endgroup$ – Rodrigo Aug 16 '18 at 15:17

Surely, you want $s_1 < s_2$ if there is a $t$ such that $s_1.t < s_2.t$ and $s_1.u \leq s_2.u$ for every other field $u$. That, at least, gives you a well-founded order.

But there are many other well-founded orders on tuples, e.g. lexicographical order for some order of the fields (though you might need a heuristic to find the order), and various arithmetic combinations of the sizes of each field.

Modern termination checkers will actually simultaneously search for some order that works among a large family of such orders, by generating constraints of the form "There is some lexicographic order, or some polynomial order that shows termination" and trying to satisfy this constraint all at once.

A couple of papers that address termination analysis for bit-vectors and Java, respectively, are:

Termination and Complexity Analysis for Programs with Bitvector Arithmetic by Symbolic Execution


Automated Termination Proofs for Java Programs with Cyclic Data

by Giesl & al.


Your Answer

