Etude théorique des fonctions
Antonia Balaa
Projet Lemme -- INRIA Sophia-Antipolis
Abstract:
La combinaison de la théorie des types et des structures inductives permet de
définir des fonctions récursives et de raisonner sur ces fonctions.
La répétition des calculs est effectuée en utilisant des fonctions
récursives. Les termes mis en jeu sont simplifiés par des règles de
réduction existant dans le système (entre autres la $iota$-réduction).
Nous avons étudiés deux familles de fonctions récursives:
-
Les fonctions définies par ordre bien fondée:
La méthodologie usuelle consiste à montrer
que les arguments récursifs successifs sont décroissants par rapport à un
ordre bien fondé.
-
Les fonctions définies par récursion limitée:
Le principe consiste à passer par l'intermédiaire
d'une fonction qui prend comme argument supplémentaire le nombre d'itérations
autorisé pour la fonction.
Pour ces deux types de méthodes, le système Coq ne fournit pas de règles de
réduction associées, d'où l'intérêt de disposer d'une équation de point fixe
qui représente cette règle de réduction.
Notre travail consiste à générer la preuve de cette équation de point fixe afin
de pouvoir l'utiliser systématiquement dans le système.
Nous détaillerons dans cet exposé ces deux solutions.
Back to schedule.
Nicolas Magaud
Last modified: Tue Apr 3 16:32:05 MEST 2001