Soutenance mémoire
Calcul et langage
L’informaticien considère que la notion de langage sous-tend celle de toute notion de calcul, car les calculs véritablement intéressants sont ceux dont on peut observer le résultat étant donné une configuration de départ que l’on peut fixer arbitrairement. On pourrait considérer qu’une montre analogique bien réglée effectue chaque seconde un calcul différent. On peut donc considérer la montre comme une machine à calculer. Même pour une machine aussi simple que celle-ci, le langage joue un rôle: il faut bien pouvoir lire le cadran de la montre pour que celle-ci ait une quelconque utilité. Plus encore, la montre est mue par un état interne (la tension d’un ressort, par exemple) qui guide le résultat du calcul à chaque instant. Cet état n’est pas arbitraire mais appartient à l’ensemble de tous le états possibles. Une grammaire génératrice de cet ensemble peut servir à le caractériser. Si d’aventure l’état interne de la montre échappait de cet ensemble, la montre ne serait plus en mesure de fonctionner. Ou tout du moins, les calculs successifs qu’elle effectuerait alors seraient a priori imprévisibles et incompréhensibles.
Mais les calculs effectués par cette montre bien réglée ne sont pas très intéressants pour deux raisons. La première est qu’à chaque instant t il n’est pas possible de changer la configuration de départ de la montre, c’est-à-dire l’heure courante, sauf à désynchroniser l’horaire affiché du temps réel ou savoir inverser ou accélérer la flèche du temps. La deuxième est que tous les calculs de la montre se suivent et se ressemblent beaucoup. Pour une observation donnée de l’état de la montre, chaque aiguille du cadran aura fait une rotation dont le signe et l’amplitude restent constants d’une seconde à l’autre. Il n’est pas possible de changer la montre pour lui demander d’effectuer un calcul autre que ceux pour lesquels elle a été conçue. À la racine du problème, on trouvera que le langage interne à la montre est bien trop pauvre pour paramétrer le calcul effectué de manière à en changer significativement la nature.
Notons que le langage interne de la montre analogique est de nature physique, mais les détails de ce langage importent peu. En lieu et place d’un ressort et un jeu de roues, nous pourrions installer un circuit électronique allié à un morceau de quartz finement taillé de manière à vibrer à une fréquence précise sous l’effet d’un potentiel électrique. Bien que le langage interne de la montre en serait alors changé, le calcul effectué et les résultats observés peuvent être mis en bijection avec ceux de la montre analogique. La montre digitale simule ainsi la montre analogique. Nous pouvons de surcroît nous affranchir du caractère physique des langages internes aux montres et passer à un langage de symboles qu’il est possible de retranscrire sur une feuille de papier. Les calculs successifs de la montre analogique peuvent tout autant qu’avec la montre digitale être simulés sur papier, ou mentalement, à l’aide de chiffres et autres symboles.
En théorie de la calculabilité, on considère le plus souvent des langages que l’on caractérise comme des ensembles de chaînes de symboles. Les symboles forment donc les éléments de base de tout langage dans ce cadre. À contrario, nous considérons dans la suite de ce chapitre plusieurs formalismes de langages. Tantôt des langages portant sur des arbres (que l’on qualifiera de formels), tantôt des langages de chaînes de codes machine qu’un processeur peut interpréter comme une suite d’instructions et d’octets. L’objet de ce chapitre est de rappeler comment simuler un calcul exprimé à l’aide d’un langage d’arbre, par un calcul équivalent exprimé comme une suite d’instructions et d’octets. Il est entendu que tous les calculs exprimé à l’aide de ces chaînes sont eux-mêmes des simulations de phénomènes physiques bien réels se produisant au coeur même de supercalculateurs et autres téléphones mobiles. Ainsi, passer d’un langage à un autre permet de simuler sur ordinateur un calcul formel.
Calcul par réécriture
La section précédente s’est bien gardée de définir précisément ce qu’est un calcul, puisque la forme que peut prendre celui-ci en mathématiques et plus encore dans la nature est diverse. Mais si l’on part du postulat que tous les calculs de la nature sont en principe simulables par d’autres calculs , choisissons un cadre très restreint de calculs plus amènes à l’analyse, sachant que ces calculs peuvent simuler bon nombre de calculs de la nature, si ce n’est tous.
Les notations suivantes concernant les relations binaires nous aideront par la suite. Nous supposons dans toute cette section l’existence d’un type A quelconque, pendant en théorie des types d’un ensemble en théorie des ensembles. Chacun des habitants de A est appellé terme. Définition 1.1 Soit (−→) une relation binaire sur A. Pour tout a,b : A, nous écrivons a −→ b pour (−→) a b. Nous noterons également (−→0,1) la clôture réflexive de (−→), (−→+) la clôture transitive, (−→∗ ) la clôture réflexive et transitive, et (≡−→) la clôture réflexive, symétrique et transitive. On peut aussi construire la réciproque de (−→), que nous noterons (←−). L’union de (−→) et de sa réciproque est notée par (←→).
L’énoncé du Entscheidungsproblem par Hilbert en 1928 requit la notion « d’algorithme » ou de « méthode effective de calcul ». Hilbert se demandait s’il existait une procédure mécanique pour distinguer les vérités mathématiques de l’ivraie. Le calcul énoncé comme un algorithme est un processus « mécanique » ou effectif d’exécution d’instructions les unes à la suite des autres. C’est cette notion de calcul pas à pas qui amène à énoncer le cadre formel suivant pour le calcul.
Définition 1.2 (Réduction) Nous dirons que a se réduit ou se réécrit en b si a −→∗ b. Une séquence finie de réductions pour (−→) est une suite finie (ai)0≤i≤n telle que pour tout 0 ≤ i ≤ n − 1, ai −→ ai+1. Une séquence infinie de réductions pour (−→) est une suite infinie (ai)i∈N telle que pour tout i ∈ N, ai −→ ai+1.
Définition 1.3 (Forme normale) Soit a : A et (−→) une relation binaire sur A. a est en forme normale pour (−→) si il n’existe pas de b : A tel que a −→ b. Pour tout c : A tel que c −→+ a, nous dirons que a est une forme normale de c.
Il est intéressant de savoir s’il est possible d’atteindre une forme normale à partir d’un élément quelconque a, et plus encore si toute les suites de réductions partant de a mènent vers une forme normale. On distingue donc deux formes de normalisation, la dernière étant plus forte que la première et souvent beaucoup plus difficile à établir.
Définition 1.4 (Normalisation faible) Pour tout a : A, a est faiblement normalisant (noté W N → a) pour une relation binaire (−→) si il existe une forme normale de a. Une relation (−→) est faiblement normalisante si ∀a : A, W N → a.
Définition 1.5 (Normalisation forte) Soit (−→) une relation binaire sur A et a : A. On définit le prédicat S N → a inductivement par :
− pour tout a, si a est en forme normale alors S N → a ;
− si pour tout a’ : A tel que a −→ a’ alors S N → a’ , alors S N → a.
Cette définition inductive du prédicat S N → correspond en théorie des ensemble au plus petit ensemble vérifiant les conditions énoncées.
On dira d’un système de réécriture défini comme une relation binaire (−→) sur A qu’il est faiblement normalisant si pour tout a : A est faiblement normalisant ; mutatis mutandis pour un système fortement normalisant. Un calcul par réécriture est une suite de réductions potentiellement infinie, commençant par un élément a’ : A. Dans le cas où cette suite est de taille finie, le résultat du calcul est une forme normale de a’. Le calcul à l’aide d’un automate (déterministe ou non), cadre formel plus usuel en informatique, est une instance de la réécriture où l’ensemble A est l’ensemble de tous les états de l’automate.
Confluence
Une instance particulièrement intéressante de la réécriture sont les calculs formels, où l’on voit souvent les termes comme des programmes. Chaque étape de réduction produit un nouveau programme. Le résultat final d’un programme est sa forme normale, si elle existe. Dans ce cadre, la confluence est une propriété particulièrement intéressante.
En effet, si un système de réécriture (−→) ne normalise que faiblement, alors il peut exister des termes à partir desquelles certaines suites de réductions arrivent à une forme normale alors que d’autres suites n’y parviennent pas. Même si (−→) est fortement normalisant, certains termes peuvent avoir plusieurs formes normales auxquelles on parvient par des suites de réductions distinctes. Il n’est pas aisé d’écrire des programmes en présence de ce non-déterminisme de la forme normale éventuellement atteinte. Dans la mesure où l’intérêt d’un calcul est son résultat final, ce non-déterminisme peut aussi être problématique pour la performance du calcul car il peut être nécessaire d’essayer toutes les suites de réductions avant de trouver une forme normale, ou la bonne forme normale.
|
Table des matières
Introduction
1 Le λ-calcul et la machine
1.1 Calcul et langage
1.2 Calcul par réécriture
1.3 Confluence
1.4 le λ-calcul
1.5 Des arbres au code machine
Étape 1 : des noms aux pointeurs
Étape 2 : des termes aux clôtures avec les substitution explicites
Étape 3 : fixer une stratégie de réduction
Étape 4 : machines abstraites
Étape 5 : de l’interprétation à la compilation
1.6 Extensions et optimisations
1.6.1 Le calcul monadique
1.6.2 Conversion de clôture
1.7 Conclusion
2 Systèmes de types et algorithmes
2.1 le λ-calcul simplement typé
2.2 Le λΠ-calcul
2.3 Les systèmes de types purs (PTS)
2.4 Le calcul des constructions inductives (CCI)
2.5 Types modulo
2.6 Algorithmes de vérification
3 Conversion par évaluation
3.1 Un algorithme de décision naïf
3.2 Normalisation par évaluation
3.3 La normalisation par évaluation est un auto-réduiseur
3.4 Normalisation multi-étage
3.5 Règles de réécriture
3.6 Optimisations
3.6.1 Décurryfication
3.6.2 Compilation du filtrage
3.7 Extension aux termes du calcul des constructions inductives
3.7.1 Interprétation du filtrage
3.7.2 Points fixes
3.8 Comparatif de performances
3.8.1 Micro-tests
3.8.2 Vérification d’une preuve réflexive dans Coq
3.9 Conclusion
4 Systèmes de types purs hors contexte
4.1 Les jugements de typage comme des clôtures
4.2 Typage hors contexte pour le λ-calcul simplement typé
4.2.1 Complétude du système de type hors contexte
4.2.2 Correction du système de type hors contexte
4.2.3 Un algorithme de typage pour les λ st xτ -termes
4.3 Du λ-calcul simplement typé aux termes de HOL
4.4 Vers une architecture à la LCF pour les PTS
4.4.1 Le choix du métalangage
4.4.2 Les preuves par réflexion
4.4.3 Vers des PTS hors contexte
4.5 Les PTS hors contexte
4.5.1 Variables annotées ou noms typés
4.5.2 Variables ordonnées
4.6 PTS hors contexte en HOAS
4.6.1 Formalisation dans Coq
4.6.2 Complétude
4.6.3 Correction
4.7 Vers un vérificateur de types
4.7.1 Inférence de types
4.7.2 Le typage est statique, le calcul est dynamique
4.7.3 Typage de formes monadiques
4.8 Typage de clôtures
4.9 Des petites aux grandes boîtes
4.9.1 Principes définitionnels
4.9.2 Élimination du contexte global
4.9.3 Commutation de la β-réduction sous les grandes boîtes
4.10 Conclusion
5 Usages et encodages
5.1 Compilation de preuves complètes
5.2 Plongement du CCI
5.2.1 Définitions globales et locales
5.2.2 Constantes opaques
Conclusion
Bibliographie
Télécharger le rapport complet
