Précédent : Fondements scientifiques Remonter : Fondements scientifiques Suivant : Autour de Coq
Précédent : Fondements scientifiques
Remonter : Fondements scientifiques
Suivant : Autour de Coq
Participants :
Frédéric Lang, Pierre Lescanne, Luigi Liquori, Kristoffer Rose, Daniel Dougherty.
Mots clés : Substitution explicite, transformation de programmes, normalisation des preuves, réécriture, programmation fonctionnelle, impérative et par objets, systèmes des types .
Nos travaux sur la modélisation des langages de programmation sont issus
entre autres de l'étude de la substitution en lambda-calcul, et en
particulier des travaux sur les substitutions explicites. Les
substitutions explicites, introduites par Abadi, Cardelli, Curien &
Lévy![[*]](../icons/foot_motif.gif){kind=icon}
, permettent une description du
lambda-calcul où substitution et élimination de beta-redex sont décrites
par les règles d'un même système de réécriture. Les calculs ainsi
obtenus permettent donc de décrire des stratégies de substitution,
lesquelles interagissent naturellement avec les stratégies du
lambda-calcul.
L'avantage principal des calculs de substitution explicite est de
permettre la modélisation et l'implantation d'outils dans lesquels la
substitution n'est pas systématiquement appliquée aux variables, mais
bloquée dans le terme, soit parce que sa propagation serait inefficace
(c'est le cas des implantations de langages fonctionnels), soit parce
qu'elle est impossible.
En démonstration automatique, une preuve incomplète est un lambda-terme
dont certains composants ne sont pas encore connus. De tels composants
sont modélisés par des variables instanciables par des termes
quelconques, nommées méta-variables. La substitution ne peut
généralement pas être définie sur un tel type de variables car on ne
connaît pas encore la structure du terme qui va l'instancier. Les
substitutions explicites sont donc une solution pour la normalisation
des preuves incomplètes. Il est par conséquent important de disposer
d'un calcul avec substitution explicite qui soit confluent sur les
méta-termes (ou termes avec méta-variables) et qui préserve la forte
normalisation du lambda-calcul. Ce problème est ouvert depuis plusieurs
années, mais des solutions sont en train d'émerger, émergence à laquelle
nous avons contribué.
Les substitutions explicites sont aussi au coeur des transformations de
programmes dans les logiciels, où les techniques de réécriture d'ordre
supérieur permettent d'exprimer des transformations complexes. Elles
fournissent des preuves élégantes et nouvelles sur l'évaluation partielle
et la programmation par continuations (continuation-passing
style).
Les langages à objets ont acquis une importance prépondérante dans les
applications informatiques à grande échelle. Cette utilisation a rendu
nécessaire l'étude formelle de ces langages pour à la fois mieux en
cerner les caractéristiques fondamentales et pour pouvoir définir de
nouveaux langages à objets capables de combiner une plus grande
expressivité avec une grande facilité d'utilisation. C'est dans ce
dernier cadre que cette veine de recherche se situe, et plus précisément
dans le contexte des calculs à objets où la création des nouveaux objets
est déléguée aux objets mêmes (à délégation ou delegation-based). Ces calculs paraissent à ce jour comme les plus
prometteurs pour une immersion dans un environnement de processus
parallèles afin d'obtenir un langage à objets concurrents. Parmi ces
calculs, ceux définis par Fisher, Honsell and Mitchell à l'Université de
Stanford,
et par Abadi et Cardelli au centre de recherche Digital de Palo
Alto,
en sont les représentants principaux. En particulier, les aspects de
typage et d'implantation des dits calculs ont été développés.
Dans les langages à délégation, les objets sont définis directement à
partir d'autres objets, en utilisant ces derniers comme prototypes. Les seules opérations sur les objets sont l'extension
d'un objet avec une une variable ou une méthode (object
extension), ou bien la surcharge d'une variable ou d'une méthode
(object override). L'adjonction ou la réécriture d'un objet
produit (dans un modèle fonctionnel) un nouvel objet qui hérite de
toutes les propriétés d'un objet original. Ces langages ont un
mécanisme d'héritage simple, le dynamic lookup des méthodes, et la
mytype specialization, c'est-à-dire la possibilité de spécialiser
les types des méthodes héritées. Les langages à délégation sont moins
étudiés que les langages fondés sur les classes. Ils ont une grande
capacité expressive, c'est à dire que les classes peuvent être vues
comme des objets capables de recevoir le message new de création
d'un objet.
Participants : D. Dougherty, F. Lang, P. Lescanne, K. Rose
Nous avons proposé les «systèmes de réécriture de termes à adresses» (ATRS) comme outil permettant la description du partage, des structures cycliques, et de la mutation, présents dans de nombreux langages de programmation. Les ATRS sont caractérisés par la combinaison de trois aspects : les objets manipulés sont des termes finis, ils permettent une représentation minimale des données cycliques par l'utilisation de pointeur en arrière, et ils assurent une complexité bornée de chaque pas de réécriture (relativement à une éventuelle implémentation) en éliminant les redirections explicites de pointeur de la réécriture de graphes de termes (Term graph rewriting). En ce sens, les ATRS sont un outil utile pour, par exemple, la définition de la sémantique opérationnelle de langages impératifs. La première phase de notre travail a consisté en la définition des ATRS, qui a donné lieu à un rapport de recherche []. Le projet est actuellement en cours de développement et devrait donner lieu ultérieurement à d'autres publications.
Cette branche d'études est aussi en relation avec le thème de recherche de la sous-section 3.1.2, puisque dans le rapport de recherche [] on a démontré que les ATRS peuvent être utilisés pour formaliser la sémantique opérationnelle des langages à objets.