Andreas Abel, Thorsten Altenkirch
February 1st, 1999
We are developing a system (MuTTI - Munich Type Theory Implementation) with dependent types which can be used for the development of provably correct programs in Type Theory. Inspired by Coquand's pattern matching for dependent types [Coq92] as implemented in the ALF system [Alf94] and its successors, we define a total language as a subset of a partial one. Hence, we are faced with the problem of verifying termination.
We restrict ourselves to structural recursion, where by structural recursion we mean that the only termination orderings we consider are lexical products of the natural structural ordering on a strictly positive datatype. We also allow mutual recursion. A further restriction is that smaller terms are only generated by primitive operators like case-analysis, projection and application.
In the type-theoretic context this is sufficient, since general terminating recursion can be represented by adding additional (computationally irrelevant) parameters. We are not sure whether structural recursive without the afore mentioned restriction is actually decidable.
Abel implemented a termination checker for a simply typed sublanguage of MuTTI (called foetus), this system allows mutual recursive definitions on general strict positive datatypes and returns a lexical ordering on the arguments of the function if one exists.
In the work we want to present here, we show that from foetus output we can actually conclude that the function terminates. We define a semantic interpretation of each type and formally define the structural ordering on semantic values of possibly different types. A central result is that the structural ordering is wellfounded at each type. A general soundness theorem allows us to conclude that each term accepted by the foetus system actually terminates.
Our approach is related to the work by Telford & Turner, who are interested in a total functional programming language (ESFP). In a recent (unpublished) article [TTu98b] they present also a termination analysis based on abstract interpretation. It seems that they accept a larger set of functions but that our analysis of the output of the termination checker is more detailed.
Our next goal is to extend our termination checker to coinductively defined types [Coq93,TTu97b] and dependent types, including the definition of universes. We also hope to be able to answer the question whether the restriction of structural recursive function is actually necessary.