The authors consider proving two programs “fully equivalent” (that is, either both do not terminate or both terminate with the same value). Both compute the Collatz sequence starting with a natural number n, which replaces in each iteration n > 1 by 3n+1 if n is odd, and by n/2 if n is even. It is not known whether this sequence is finite for all n.

Conventional program equivalence techniques split this problem into a case where the sequence terminates or a case where it does not. In this situation, this approach cannot work since there is no termination proof. The authors’ technique is to match formulas for selected configurations of the programs and build a logical relation between them, as a bisimulation is built between states of transition systems.

Logical relations were developed in the work of Jean-Yves Girard, Gordon Plotkin, and John Reynolds on the lambda calculus around 1973. The Collatz sequence programs give a nice example of the logical relation technique within standard Hoare logic. Only a few earlier examples are known; they occur in the study of fairness, for terminating [1,2] and for nonterminating [3] programs. The paper will be of interest to the program semantics and verification community.