Termination of algorithms over non-freely generated data types

Abstract

Termination proofs for recursively defined operations serve several purposes: On the one hand, of course, they ensure the termination of the respective algorithms which is an essential topic in software verification. On the other hand, a successful termination proof allows to use the termination ordering as an induction ordering for future inductive proofs. So far, in the area of explicit inductive theorem proving only data types were admitted whose objects possess a unique syntactical representation. These data types include nat1, lists, and trees. However, there are data types that do not possess this property, as, for instance, finite sets and finite arrays, which are frequently used for specifications in software verification. In this paper we are concerned with these data types. We admit them to explicit inductive theorem proving and, furthermore, we present an approach for an automated termination analysis of recursively defined algorithms over these data types.