Termination Casts: A Flexible Approach to Termination with General Recursion

TL;DR

This paper introduces Teqt, a type-and-effect system that explicitly distinguishes terminating from diverging terms in a lambda calculus with general recursion, enabling safe termination proofs and recursive definitions.

Contribution

The paper presents Teqt, a novel type-and-effect system with primitive termination types and casts, allowing flexible and safe handling of termination in general recursive functions.

Findings

Teqt can express and verify termination properties of recursive functions.

Termination casts enable safe coercion from possibly diverging to terminating terms.

The system is sound and can be translated into a logical theory of termination.

Abstract

This paper proposes a type-and-effect system called Teqt, which distinguishes terminating terms and total functions from possibly diverging terms and partial functions, for a lambda calculus with general recursion and equality types. The central idea is to include a primitive type-form "Terminates t", expressing that term t is terminating; and then allow terms t to be coerced from possibly diverging to total, using a proof of Terminates t. We call such coercions termination casts, and show how to implement terminating recursion using them. For the meta-theory of the system, we describe a translation from Teqt to a logical theory of termination for general recursive, simply typed functions. Every typing judgment of Teqt is translated to a theorem expressing the appropriate termination property of the computational part of the Teqt term.