Résumé:
On s'intéresse à la représentation des quotients dans le calcul des
constructions inductives(CIC). Un quotient est défini en théorie des
ensembles à partir d'un ensemble et d'une relation d'équivalence sur
ses éléments. Dans le cas de la théorie des types et du calcul des
constructions inductives en particulier cela signifie que ces
structures (dites non libres) sont telles que deux termes clos, en
forme normale et différents peuvent être égaux (et on aimerai qu'ils
soient convertible).
L'utilisation des types inductifs pour représenter les quotients n'est pas possible directement, en revanche une axiomatisation des quotients a été faite dans Coq (Samuel Boutin, Loïc Pottier). Mais l'axiomatisation n'est pas une solution satisfaisante car elle ne permet pas d'avoir de comportement calculatoire. Plusieurs solutions ont été proposées, notamment par Gilles Barthe et Hermann Geuvers, Martin Hofmann...
On présente une nouvelle solution consistant en une extension de CIC appelée calcul des constructions inductives avec types normalisés, dans laquelle il est possible de définir une certaine catégorie de quotient. La méthode est la suivante: un quotient sera représenté par un type normalisés, c'est à dire un type T associé à une fonction cl, noté Norm(T,cl), dont les éléments seront de la forme Class(T,cl,t) où t est de type T. Dans ce type, Class(T,cl,t) et Class(T,cl,u) seront convertible si (cl t) et (cl u) le sont.
Retour au sommaire / Back to schedule