Types inductifs, isomorphismes et récriture extensionnelle
Institution:
Toulouse 3Disciplines:
Directors:
Abstract EN:
This PhD thesis copes with extensions of the simply-typed lambda-calculus by various rewrite relations preserving termination and confluence. Our first purpose is to ensure that some types become isomorphic. As far as inductive types are concerned, this problem is undecidable: therefore, we added some particular reductions solving it only in peculiar cases, namely the inductive encoding of the product and unit types and, more importantly, the notion of parameterised copy. Next, leaving isomorphims, we consider new reductions enabling to set up some algebraic structures on finite types: firstly, we deal with the definition of a category on a fragment of the calculus; and, secondly, with the representation of the symmetric group by factorisation of permutations as products of disjoint cycles. These results are obtained using techniques from abstract rewriting theory, some of which we have specifically developped for this thesis.
Abstract FR:
Cette thèse étudie l'extension du lambda-calcul simplement typé par diverses relations de récriture préservant la terminaison et la confluence. Il s'agit d'assurer, dans un premier temps, que certains types sont isomorphes. Or le problème est indécidable pour les types inductifs : nous avons donc ajouté au calcul des réductions spécifiques résolvant la question dans certains cas, à savoir le codage des types produits et unité et surtout la notion de copie paramétrée. Délaissant ensuite les isomorphismes, nous considérons de nouvelles réductions permettant d'établir des structures algébriques sur les types finis : nous envisageons d'une part la définition d'une catégorie sur un fragment du calcul ; et, d'autre part, la représentation du groupe symétrique par décomposition des permutations en produits de cycles disjoints. Ces résultats sont obtenus par des techniques de récriture abstraite, dont certaines développées spécifiquement pour la thèse.