Consider the program Collatz, written in our core programming language:
c = n;
while (c != 1) {
if (c % 2 == 0) { c = c / 2; }
else { c = 3*c + 1; }
}
We write "c % 2" for the remained of n modulo 2. Thus, "c % 2 == 0" is
true if, and only if, c is even. We write "c / 2" for the division of
c by 2, modulo 2. For example, both 4 / 2 and 5 / 2 compute 2 as a
result. Here is a simple question: does the Hoare triple ( n >= 1 )
Collatz ( c = 1 ) hold with respect to total
correctness? The astonishing thing about this program is that nobody
seems to know this! If you want to find out more about the behaviour
of this curiuous program, check out Jeffrey C. Lagarias's tutorial
at AT&T Bell Labs, Murray Hill, New York.
From the perspective of our proof rules for total program correctness, it seems intractably hard to convert the boolean guard "c != 1" into some expression E (while still preserving the meaning of the original program) that would strictly DECREASE each time the body of the while loop is executed. This example may well require a more general orerding than that of the natural numbers. A well-founded ordering is a set P with a transitive relation "<", where no element is related to itself, and where one cannot have an infinite descending chain "e_1 > e_2 > e_3 > ...". The natural numbers with the usual "less than" relation are an example of a well-founded ordering. If the Hoare triple above holds under total correctness, then there must be an associated well-founded ordering to a proof of that fact.
We consider a few runs of this program:
nunk% java Collatz initial number n > 1: 57 172 86 43 130 65 196 98 49 148 74 37 112 56 28 14 7 22 11 34 17 52 26 13 40 20 10 5 16 8 4 2 1 The initial number 57 required 32 steps to reach 1.
If we change that program to print out "+" whenever the value of c increases, and "-" whenever it decreases, we obtain
nunk% java Collatz_ai initial number n > 1: 57 + - - + - + - - + - - + - - - - + - + - + - - + - - - + - - - - The initial number 57 required 32 steps to reach 1.
Running that same mode on a larger number:
nunk% java Collatz_ai initial number n > 1: 123456789 + - - - - - - + - - - + - + - - + - + - + - + - + - + - - + - - - - + - - - - + - - + - - + - - + - + - - - + - + - - - - - + - - + - + - - + - - - - + - - - - - - + - - + - + - - + - + - + - - + - + - + - + - - + - - - + - + - + - - + - + - - + - + - + - + - + - + - - - + - + - + - + - - - - + - - + - - + - - - - + - - - + - + - + - - - - - + - - - - The initial number 123456789 required 177 steps to reach 1.
Turning off all printouts but the final one, we work with a really big number:
nunk% java Collatz_ai initial number n > 1: 3249872346250973503456727965237642056304756345635634756396598734085384756074086560785607840745067340563457640875629845737563065378564056340562456345786928256235421357619519765129854122965424895465956457 The initial number 3249872346250973503456727965237642056304756345635634756396598734085384756074086560785607840745067340563457640875629845737563065378564056340562456345786928256235421357619519765129854122965424895465956457 required 4940 steps to reach 1.
If you want to play with this, here is the source code in Java. You need the KeyboardReader class from CIS200 for it to run; or change the input interface:
import java.math.*;
import java.util.*;
public class Collatz {
private static KeyboardReader keyboard = new KeyboardReader();
private static final BigInteger ZERO = new BigInteger("0");
private static final BigInteger ONE = new BigInteger("1");
private static final BigInteger TWO = new BigInteger("2");
private static final BigInteger THREE = new BigInteger("3");
public static void main(String[] args) {
BigInteger n;
String s = keyboard.readString("initial number n > 1: ");
n = new BigInteger(s);
BigInteger current = n;
BigInteger length = ZERO;
while (ONE.compareTo(current) != 0) {
if (ZERO.compareTo(current.mod(TWO)) == 0) {
current = current.divide(TWO); }
else { current = ONE.add(THREE.multiply(current)); }
length = length.add(ONE);
// System.out.print(current + " "); // optional printout
}
System.out.println("The initial number " + n + " required " + length + " steps to reach 1.");
}
}
If you find this program hard to read, here is the version for regular integers (with a maximal number of bits):
import java.math.*;
import java.util.*;
public class Collatz_Small {
private static KeyboardReader keyboard = new KeyboardReader();
public static void main(String[] args) {
int n = keyboard.readInt("starting number n > 1: ");
int length = 0;
int current = n;
while (current != 1) {
if ((current % 2) == 0) { current = current / 2; }
else { current = 3*current + 1; }
++length;
}
System.out.println("The initial value " + n + " required " + length + " steps to reach 1.");
}
}
Michael Huth (huth@cis.ksu.edu)