Egalité et filtrage avec types dépendants dans le calcul des constructions inductives / Nicolas Oury ; sous la direction de [Christine Paulin]

Date :

Editeur / Publisher : [s.l.] : [s.n.] , 2006

Type : Livre / Book

Type : Thèse / Thesis

Langue / Language : français / French

Paulin-Mohring, Christine (1962-....) (Directeur de thèse / thesis advisor)

Université de Paris-Sud. Faculté des sciences d'Orsay (Essonne) (Autre partenaire associé à la thèse / thesis associated third party)

Université Paris-Sud (1970-2019) (Organisme de soutenance / degree-grantor)

Relation : Egalité et filtrage avec types dépendants dans le calcul des constructions inductives / Nicolas Oury ; sous la direction de [Christine Paulin] / Grenoble : Atelier national de reproduction des thèses , 2006

Résumé / Abstract : La théorie des types autorise l'utilisation de types dépendants. Les types peuvent dépendre des valeurs du système. Ainsi, il est possible de manipuler l'ensemble des listes d'une taille n donnée. Il apparait alors des types équivalents mais syntaxiquement différents. Par exemple, les listes de longueur 2+2 et celles de longueur 4 sont les mêmes ensembles. La conversion du systeme assure la verification de ces équivalences. Dans le Calcul des Constructions Inductives, elle est réduite à des règles de calcul élémentaires. Ainsi, le type des listes de longueur n+0 et celui des listes de longueur n sont distincts. Nous introduisons un système extensionnel : dans un tel système, toutes les égalités prouvables sont incluses dans la conversion. Nous exhibons une traduction de ce système vers une extension raisonnable du Calcul des Constructions Inductives. Cette traduction peut servir à la fois de base theorique et de base pratique pour l'implantation d'un tel système. Par ailleurs, les types dépendants rendent parfois certains cas inutiles dans un filtrage. Par exemple, le cas de la liste vide est inutile dans la définition d'une fonction attendant une liste de longueur non nulle. Nous introduisons une méthode pour éliminer certains cas inutiles dans une définition par filtrage de motifs. Cette méthode se base sur l'approximation des ensembles de termes habitant un types ou un contexte. Elle est parametrée par le type d'approximation utilisée. Nous fournissons une preuve de correction de cette méthode et introduisons deux exemples d'implantation d'approximation utilisables en pratique.

Résumé / Abstract : Type Theory allows the use of dependent types. Types can depend upon values of the system. It is possible, for example, to define the set of lists of a given size n. Some types are equivalent and syntactically different. For example, lists of size 2+2 are the same objects as list of size 4. The conversion process of the system checks for these equivalencies. In the Calculus of Inductive Constructions, this process is reduced to a small set of elementary rules of calculus. For example, lists of size n+0 and lists of size n are distinct types. We introduce an extensional system : in such a system, every provable equality is added to the conversion. We exhibit a translation from this system to a slight extension of the Calculus of Inductive Constructions. This process can be used both as a theorical justification and a practical basis for the implementation of such a system. In the presence of dependent types, some cases can be useless in a definition by pattern matching. For example, the case of the empty list in a function taking lists of non zero size as argument is useless. We introduce a method to eliminate some useless cases in a pattern matching with dependent types. This method relies on approximations of the set of terms inhabiting a type or a context. It is parametred by the approximation used to represent such sets. we show the correction of this method and we introduce to implementations of set approximation that can be used in practice.