The computability path ordering: the end of a quest

TL;DR

This paper introduces the Computability Path Ordering, an improved method for automated termination proofs in higher-order calculi, rooted in computability arguments by Tait and Girard.

Contribution

It provides a refined definition of the higher-order recursive path ordering that better captures computability arguments, advancing termination proof techniques.

Findings

The new ordering improves termination proof capabilities.

It aligns with classical computability arguments.

Provides a clearer theoretical foundation for termination methods.

Abstract

In this paper, we first briefly survey automated termination proof methods for higher-order calculi. We then concentrate on the higher-order recursive path ordering, for which we provide an improved definition, the Computability Path Ordering. This new definition appears indeed to capture the essence of computability arguments \`a la Tait and Girard, therefore explaining the name of the improved ordering.