The Size-Change Termination Principle for Constructor Based Languages

TL;DR

This paper introduces an automatic termination checker for ML-style languages that leverages size-change principles to analyze recursive call arguments, including subvalues, enhancing termination detection.

Contribution

It extends the size-change termination principle to handle subvalue size changes in constructor-based languages, with an easy-to-implement algorithm.

Findings

Effective detection of termination in constructor-based languages.

Extension of size-change principle to subvalues.

Algorithm suitable for practical experimentation.

Abstract

This paper describes an automatic termination checker for a generic first-order call-by-value language in ML style. We use the fact that value are built from variants and tuples to keep some information about how arguments of recursive call evolve during evaluation. The result is a criterion for termination extending the size-change termination principle of Lee, Jones and Ben-Amram that can detect size changes inside subvalues of arguments. Moreover the corresponding algorithm is easy to implement, making it a good candidate for experimentation.