Type-based termination of recursive definitions

Abstract

This article The purpose of this paper is to introduce b, a simply typed -calculus that supports type-based recursive denitions. Although heavily inspired from previous work by Gimenez (Gimenez 1998) and closely related to recent work by Amadio and Coupet (Amadio and Coupet-Grimal 1998), the technical machinery behind our system puts a slightly dierent emphasis on the interpretation of types. More precisely, we formalize the notion of type-based termination using a restricted form of type dependency (a.k.a. indexed types), as popularized by (Xi and Pfenning 1998; Xi and Pfenning 1999). This leads to a simple and intuitive system which is robust under several extensions, such as mutually inductive datatypes and mutually recursive function denitions; however, such extensions are not treated in the paper. The basic idea is to proceed as follows: | First, every datatype d is replaced by a family of approximations indexed over a set of stages, which are used to record a bound on the \\depth" of values. Here, we adopt a simple minded approach and let stages range over the syntax s := { j b s j 1 where { ranges over stage variables, the hat operator b is a function mapping a stage to its \\successor" and 1 is the stage at which the iterative approximation process converges to the datatype itself