Distilling Programs to Prove Termination

TL;DR

This paper introduces a novel method for proving program termination by applying a distillation transformation to programs, converting them into a simplified form, and analyzing their transition systems for infinite descent, advancing termination analysis techniques.

Contribution

The paper presents a new termination proof technique that leverages program distillation and transition system analysis, offering an alternative to existing ranking function methods.

Findings

Effective on various example programs

Comparable or improved success rate over previous methods

Provides a new perspective on termination proofs

Abstract

The problem of determining whether or not any program terminates was shown to be undecidable by Turing, but recent advances in the area have allowed this information to be determined for a large class of programs. The classic method for deciding whether a program terminates dates back to Turing himself and involves finding a ranking function that maps a program state to a well-order, and then proving that the result of this function decreases for every possible program transition. More recent approaches to proving termination have involved moving away from the search for a single ranking function and toward a search for a set of ranking functions; this set is a choice of ranking functions and a disjunctive termination argument is used. In this paper, we describe a new technique for determining whether programs terminate. Our technique is applied to the output of the distillation program transformation that converts programs into a simplified form called distilled form. Programs in distilled form are converted into a corresponding labelled transition system and termination can be demonstrated by showing that all possible infinite traces through this labelled transition system would result in an infinite descent of well-founded data values. We demonstrate our technique on a number of examples, and compare it to previous work.