Une étude des sommes fortes : isomorphismes et formes normales

JUSTE APRÈS avoir appris à compter, à l’école primaire, les enfants apprennent l’addition. Ce n’est que bien après qu’est introduite la notion plus abstraite de multiplication. La somme et le produit réapparaissent ensuite sous de multiples formes dans l’étude des nombres à virgule, des nombres négatifs, des groupes et anneaux, des espaces vectoriels… En logique, ce sont respectivement les connecteurs « ou » et « et » ; en théorie des ensembles, l’union disjointe et le produit cartésien ; en théorie des catégories, le co-produit et le produit. . Mais très souvent, contrairement à l’école primaire, la somme est définie comme la notion « duale » duproduit. Définie après le produit… Souvent même, dans les livres, dans les cours de DEA, on n’en parle pas, ou très peu. C’est la notion duale. Elle doit se comporter de la même façon..

Malheureusement ce n’est pas si simple. Dans bien des domaines, les systèmes avec somme posent des problèmes. En λ-calcul typé, la somme a de très mauvaises propriétés de confluence. Ce n’est que récemment qu’ont été prouvées deux propriétés fondamentales de la théorie équationnelle du λ-calcul avec somme, à savoir sa décidabilité, par Neil Ghani [47, 48], et sa complétude par rapport aux égalités de la catégorie des ensembles (Dougherty et Subrahmanyam [43]). En évaluation partielle dirigée par les types, nous verrons que la somme oblige à introduire des opérateurs de contrôle. Nous verrons aussi que même en arithmétique, elle n’a pas toujours des propriétés aussi simples que le produit. La somme vient avec un objet étrange, son élément neutre, le zéro, l’ensemble vide, l’objet initial… Historiquement, il n’est apparu qu’au deuxième ou troisième siècle avant Jésus-Christ, à Babylone et en Grèce, puis fut adopté par les Arabes au huitième siècle, et en Europe au douzième siècle seulement ! Il n’est réellement devenu un nombre à part entière qu’au sixième siècle, en Inde. Cette notion aujourd’hui courante n’est donc pas si naturelle. En programmation, le zéro est un type mystérieux, quasiment jamais utilisé, qui n’a aucun élément… En logique, c’est une formule toujours fausse .

Le λ-calcu

Le λ-calcul est un modèle de représentation du calcul qui a donné naissance à un nouveau style de langages, dits fonctionnels (on peut citer Lisp, Scheme, Haskell, ou les dialectes de ML comme SML ou Caml). Sa syntaxe repose sur les notions de variable, d’abstraction (λx. t) et d’application (t u).

Les isomorphismes de types 

L’étude des isomorphismes dans les catégories trouve une application pratique particulièrement intéressante en programmation, où elle permet de considérer les types « à isomorphisme près », c’est-à-dire sans se préoccuper de détails sans importance dans la représentation de données, comme par exemple l’ordre des paramètres d’une fonction. De nombreux travaux ont par exemple porté sur la recherche de fonctions dans une bibliothèque en utilisant le type comme clef de recherche [34, 35, 36, 71, 72, 73, 75] (par exemple l’outil CamlSearch écrit par Jérôme Vouillon, Julien Jalon et Roberto Di Cosmo pour le langage Caml Light) ou bien sur la recherche d’un module d’après une spécification [15, 33, 5], ou encore dans un assistant de preuve pour trouver des preuves dans des bibliothèques [33]. Une autre application est l’inter-opérabilité entre langages, dans le but par exemple d’utiliser une bibliothèque écrite dans un langage pour programmer dans un autre, qui ne dispose pas forcément des mêmes types. Cette idée a été utilisée en 1997 par IBM pour le projet Mocking Bird. Si ces deux applications peuvent paraître anecdotiques au premier abord, elles deviennent primordiales pour des fonctions au type très complexe ou bien pour les programmeurs de grands logiciels, qui doivent gérer des bibliothèques gigantesques de fonctions.

Formes normales 

Pour un λ-calcul simplement typé sans type produit ni somme ni les constantes associées, les propriétés de la β-réduction sont très simples. Il suffit d’appliquer la réduction autant de fois qu’il est possible et dans un ordre quelconque. Le processus termine toujours et le résultat, appelé forme normale, est unique. Avec les types produits et sommes, ces propriétés ne sont pas toujours vérifiées.

Dans certains cas cependant, il serait intéressant de pouvoir trouver un représentant unique d’une classe de termes. Par exemple le travail sur les isomorphismes de types mentionné cidessus a conduit à utiliser des λ-termes compliqués dont il fallait prouver qu’ils étaient des isomorphismes. Il fallait donc les composer avec leur inverse supposé et montrer qu’ils étaient βη-équivalents à l’identité. La β-réduction associée à l’η-réduction ne permettent plus d’obtenir une forme normale unique. Il a donc fallu trouver une autre méthode.

La première étape a consisté à définir extensionnellement une notion de forme normale « canonique » pour le λ-calcul simplement typé avec somme, produit et constantes. En fait, nous ne pouvons pas parvenir à un représentant unique d’une classe d’équivalence modulo ηet β, essentiellement à causes de certaines équations dites « conversions commutatives » que l’on peut difficilement éviter. Cependant la forme que nous obtenons doit respecter des contraintes structurelles très fortes qui limitent de manière drastique les possibilités de formations des termes. Ce travail a été effectué grâce à une étude des modèles catégoriques du λ-calcul, et en particulier grâce aux relations logiques de Grothendieck. Il vient à la suite de plusieurs articles sur le sujet. Tout d’abord, en 1993, Achim Jung et Jerzy Tiuryn ont donné une preuve de λ-définissabilité grâce aux relations logiques de Kripke dans les catégories cartésiennes fermées [58]. Marcelo Fiore a ensuite montré dans le premier cas que ce résultat de définissabilité pouvait être adapté pour donner un résultat de normalisation extensionnelle [45]. Le résultat de définissabilité a été étendu aux catégories bi-cartésiennes fermées par Marcelo Fiore et Alex Simpson en 1999 au cas des catégories bi-cartésiennes fermées grâce aux relations logiques de Grothendieck [46]. Le travail présenté ici étend le résultat de normalisation à ce cas.

Dans son article sur les formes normales du λ-calcul sans somme [45], Marcelo Fiore montre ensuite que l’algorithme de normalisation par évaluation est une version « intentionnelle » de ce résultat, c’est-à-dire qu’il donne une méthode effective de normalisation. La normalisation par évaluation est une technique très astucieuse inventée par Ulrich Berger et Helmut Schwichtenberg [17] en 1991 permettant « d’inverser » la fonction d’évaluation pour obtenir la syntaxe d’un terme en forme normale à partir de sa sémantique. En 1996, Olivier Danvy redécouvrait cet algorithme pour faire de la normalisation de programme ML de manière très élégante [27]. Cette méthode est connue sous le nom d’évaluation partielle dirigée par les types.  Les deux derniers chapitres montrent une utilisation originale de cet algorithme : nous allons l’appliquer au problème de la vérification des isomorphismes de types. Malheureusement l’algorithme existant ne produit pas les termes dans notre forme normale canonique. De plus, deux termes βη-équivalents peuvent donner des résultats complètement différents, et nous verrons même que dans la cas des isomorphismes de la suite de Gurevic,ˇ on obtient des termes βη-équivalents à l’identité dont la normalisation produit des résultats de plusieurs milliers de lignes.

Heureusement, ce problème a été résolu. Le dernier chapitre montre comment on peut modifier l’algorithme d’évaluation partielle dirigée par les types pour qu’il produise un résultat répondant à la définition de nos formes normales, notamment grâce à un travail sur les opérateurs de contrôle. Cela aboutira dans les cas mentionnés ci-dessus à une drastique optimisation en taille et en temps de normalisation .

Table des matières

Introduction
I Modèles du λ-calcul
1 Introduction aux isomorphismes dans les catégories
1.1 Définitions de base
1.2 Catégories bi-cartésiennes fermées
1.2.1 Constructions de base
1.2.2 Limites
1.3 Foncteurs et catégories de foncteurs
1.3.1 Définitions
1.3.2 Pré-faisceaux
1.3.3 Catégories bi-cartésiennes fermées et transformations naturelles
1.4 Isomorphismes dans les biCCC
2 Modèles du λ-calcul
2.1 Le λ-calcul avec type somme
2.1.1 Le λ-calcul pur
2.1.2 Le λ-calcul simplement typé
2.2 Sémantique du λ-calcul simplement typé
2.2.1 Modèle des λ-termes
2.2.2 Les biCCC modèles du λ-calcul avec somme
2.3 Isomorphisme entre Λ×+10βη et la biCCC libre
2.3.1 Sans co-produit
2.3.2 Avec co-produit
2.3.3 Note sur la règle d’élimination du 0
II Isomorphismes de types avec somme
3 Isomorphismes linéaires en logique linéaire
3.1 La logique linéaire
3.1.1 Les règles de la logique linéaire
3.1.2 Les réseaux de preuves
3.2 Définitions et présentation des résultats
3.3 Réduction aux réseaux de preuves simples bipartites
3.4 Réduction à des formules non-ambiguës
3.5 Complétude pour les isomorphismes dans MLL
3.6 Prise en compte des constantes
3.6.1 Expansions des axiomes avec constantes : les réseaux simples identité revus
et corrigés
3.6.2 Réduction aux isomorphismes entre formules simplifiées
3.6.3 Complétude avec constantes
3.7 Conclusions
4 Isomorphismes pour le λ-calcul avec type somme et type vide
4.1 Mise en relation des différentes théories
4.2 Le problème des égalités du lycée et les isomorphismes de types
4.2.1 Types produit et somme
4.2.2 Types produit, flèche, et somme
4.2.3 Type vide et type somme
4.3 Preuve du lemme 4.9
4.4 Remarques conclusives
III Normalisation en présence du type somme
5 Formes normales extensionnelles du λ-calcul avec somme
5.1 Survol de la preuve
5.2 Sémantique dans la biCCC des relations de Grothendieck
5.3 Normalisation dans les biCCC
5.3.1 Lemme de base
5.3.2 Termes neutres, termes normaux
5.3.3 Contextes contraints
5.3.4 Formes normales
5.4 Lemmes utilisés
6 Normalisation par évaluation du λ-calcul avec somme
6.1 Normalisation par évaluation
6.2 Évaluation partielle dirigée par les types
6.2.1 Introduction à l’évaluation partielle
6.2.2 De NBE à TDPE
6.2.3 TDPE et les types sommes
6.3 Implantation de TDPE en Objective Caml
6.3.1 Le problème
6.3.2 La solution de Filinski/Yang
6.3.3 La solution avec génération de bytecode
6.3.4 Normalisation in situ
6.4 Conclusion
Conclusion

Télécharger le rapport complet