Fonctions récursives générales dans le calcul des constructions
Institution:
NiceDisciplines:
Directors:
Abstract EN:
Inductive type theories provide a systematic approach to program and reason about recursive functions. Intuitively, these functions are described such that recursive calls are performed only on terms that are smaller than the initial argument for some well-founded order. Using the fix-point theorem, we show two approaches to formalise recursive functions. The first one, quite complex, is based on the notion of dependent types. Specification of the recursive function and its termination proof are treated simultaneously. In the second, recursive functions are constructed by iteration. Our contribution is interesting as we could separate the main difficulties: function definition and its termination proof. As a result we considerably reduce the programmer's effort. For each approach, a tool is generated which allows us to program general recursive functions in Coq, as naturally as in functional programming languages. We believe that our techniques can be adapted for any type theory based system.
Abstract FR:
Notre objectif est la définition des fonctions récursives générales en théorie des types, où la méthodologie consiste à montrer que les arguments des appels récursifs sont décroissants pour un ordre bien fondé. Basées sur le théorème du point fixe nos recherches ont été menées suivant deux directions. La première, complexe, repose fortement sur la notion de type dépendant et mélange le problème de terminaison de la fonction avec celui de son adéquation à sa spécification. La deuxième, vise à réduire la complexité des données à fournir par le programmeur:la construction de la fonction récursive s'effectue par itération. Notre contribution est intéressante en ce qu'elle sépare les problématiques:définir la fonction et prouver sa terminaison. Ces travaux ont permis le développement de deux outils automatiques pour la programmation en Coq de fonctions récursives générales. Ces techniques s'appliqueront avec des variations mineures dans tout système de démonstration basé sur la théorie des types.