foetus -- Termination Checker for Simple Functional Programs

TL;DR

This work addresses termination verification for simple functional programs by introducing foetus and a termination checker. The method gathers recursive calls, builds a call graph (including mutual recursion), and searches for a well-founded lexical order on function parameters to ensure that recursive calls are smaller in each step. Key contributions include the design of the foetus language, the implementation of a termination prover, and formal treatment of call extraction, call graph completion, and parameter-order analysis. The approach demonstrates how termination verification can be integrated into a small functional-language setting, contributing to practical program verification for structural, pattern-matching functional programs.

Abstract

We introduce a simple functional language foetus (lambda calculus with tuples, constructors and pattern matching) supplied with a termination checker. This checker tries to find a well-founded structural order on the parameters on the given function to prove termination. The components of the check algorithm are: function call extraction out of the program text, call graph completion and finding a lexical order for the function parameters.