La plein paresse, une certain optimalité : partage de sous-termes et stratégies de réduction en réécriture d'ordre supérieur
Institution:
Paris 7Disciplines:
Directors:
Abstract EN:
This dissertation investigates efficient evaluation strategies for functional programming languages and higher-order rewriting, with two constraints: no early evaluation of non-instantiated function bodies, and a restriction of sharing mechanisms to complete subterms. In the lambda-calculus, as well as in the more general framework of orthogonal second-order rewriting, three evaluation models are considered: optimal reduction without sharing, fully lazy reduction à la Wadsworth, and optimal family reduction à la Levy. This defines a unified notion of weak optimality, that teaches us that Levy-optimality in weak reduction can be implemented by a fully lazy strategy as well as a strategy without sharing. It is however also proved that such an optimal strategy without sharing cannot be computable, while sharing allows in a number of cases the definition of very simple optimal strategies. To reach these conclusions, this dissertation makes good use of the contraints to reduce the discussion to simpler well-known Systems. On the one hand the graphs modelling the sharing of subterms are represented by labelled terms, thanks to the axiomatic framework of Sharing-via-Labelling Systems (SLS) developped for the occasion. On the other hand, a transformation process inspired from lambda-lifting defines a bisimulation between any weak second-order System and some first-order System, said bisimulation preserving in particular the length of reduction sequences, the possible orthogonality of the Systems, and sharing. Thus graphs for higher-order rewriting are formalized and studied, without graphs nor higher-order.
Abstract FR:
Cette thèse explore des stratégies d'évaluation efficaces pour les langages de programmation fonctionnelle et la récriture d'ordre supérieur, avec deux contraintes : pas d'évaluation anticipée du corps non-instancié d'une fonction, et une restriction des mécanismes de partage à des sous-termes complets Dans le cas du lambda-calcul et dans la plus générale récriture du second ordre orthogonale, trois modèles d'évaluation sont prouvés équivalents en réduction faible : la réduction optimale sans partage, la réduction pleinement paresseuse à la Wadsworth, et la réduction optimale de familles à la Lévy. Cette notion unifiée d'optimalité faible montre que l'optimalité à la Lévy en réduction faible peut être réalisée aussi bien par une stratégie paresseuse que par une stratégie sans partage. Toutefois, une telle stratégie optimale sans partage ne peut être calculable, alors que le partage permet dans de nombreux cas une stratégie optimale très simple. Ces résultats sont établis en tirant parti des restrictions imposées pour se ramener à des systèmes plus simples et bien maîtrisés. D'une part les graphes modélisant le partage de sous-termes sont systématiquement représentés par des termes étiquetés, grâce à un cadre axiomatique (Sharing-via-Labelling Systems, SLS) développé pour l'occasion. D'autre part, une transformation inspirée du lambda-lifting établit une bisimulation forte entre tout système du second ordre faible et un système du premier ordre, bisimulation qui préserve la longueur des séquences de réduction, l'orthogonalité des systèmes et le partage. Des graphes pour la récriture d'ordre supérieur sont ainsi formalisés et étudiés, sans graphes ni ordre supérieur.