<p>Surely, you want $s_1 &lt; s_2$ if there is a $t$ such that $s_1.t &lt; 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.</p>

<p>But there are many other well-founded orders on tuples, e.g. <a href="https://en.wikipedia.org/wiki/Lexicographical_order" rel="nofollow noreferrer">lexicographical</a> 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.</p>

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

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

<p><a href="https://www.researchgate.net/publication/323579576_Termination_and_Complexity_Analysis_for_Programs_with_Bitvector_Arithmetic_by_Symbolic_Execution" rel="nofollow noreferrer">Termination and Complexity Analysis for Programs with Bitvector Arithmetic by Symbolic Execution</a></p>

<p>and</p>

<p><a href="https://www.researchgate.net/publication/230554947_Automated_Termination_Proofs_for_Java_Programs_with_Cyclic_Data" rel="nofollow noreferrer">Automated Termination Proofs for Java Programs with Cyclic Data
</a></p>

<p>by Giesl <em>&amp; al</em>.</p>

CC BY-SA 4.0
2018-08-16T18:38:24.287Z
2018-08-16T18:38:24.287Z
cody
<p>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:</p>

<p>Given two sequences of arguments $s_1,s_2$.</p>

<ol>
<li><p>Filter the bitvector arguments (long/int/short/byte) </p></li>
<li><p>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$.</p></li>
<li><p>If $s.t$ is defined for $s_1,s_2$, compare $s_1.t$ with $s_2.t$ lexicographically. </p></li>
</ol>

<p>We define $s_1 &lt; s_2$ when there exists a type $t$ such that $s_1.t &lt; s_2.t$. </p>

<p>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 &lt; s_2.int$ and $s_2.short &lt; s_1.short$ we would deduce that $s_1 &lt; s_2$ and $s_2 &lt; s_1$.</p>

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

CC BY-SA 4.0
2018-08-16T14:24:06.070Z
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?
cody
CC BY-SA 4.0
2018-08-16T15:17:05.620Z
@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
user1868607
<program-verification><formal-methods><order-theory>
Ordering sequences containing bitvectors for size-change termination
user1868607
# Ordering sequences containing bitvectors for size-change termination

(Asked by: username_0 on 2018-08-16)

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?

**Tags:** program-verification, formal-methods, order-theory
> **Comments:**
> **username_1**: 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?  
> **username_0**: @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  

---

## 1 answers

### Answer by username_1 on 2018-08-16. Score: 4 | Accepted answer

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](https://en.wikipedia.org/wiki/Lexicographical_order) 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](https://www.researchgate.net/publication/323579576_Termination_and_Complexity_Analysis_for_Programs_with_Bitvector_Arithmetic_by_Symbolic_Execution)

and

[Automated Termination Proofs for Java Programs with Cyclic Data](https://www.researchgate.net/publication/230554947_Automated_Termination_Proofs_for_Java_Programs_with_Cyclic_Data)

by Giesl *& al*.


---

