Dissecting call-by-need by customizing multi type systems - Département d'informatique Accéder directement au contenu
Thèse Année : 2021

Dissecting call-by-need by customizing multi type systems

Une dissection de l'appel-par-nécessité par la personnalisation des systèmes de multi types

Résumé

In this thesis, we present a quantitative study of the call-by-need lambda-calculus, both from type-theoretical and operational standpoints.Type-theoretically speaking, we derive several multi type systems—a non-idempotent variant of intersection types. Each of them targets a certain (increasingly more complex) notion of call-by-need reduction, in such a way that typability in the type system is equivalent to normalization in the corresponding version of call-by-need. In each case, the characterization of normalization is tailored to such an extent that we are capable of extracting significant quantitative information on different aspects of the normalization processes—typically, the number of reduction steps to the normal form and the size of the normal form.Operationally speaking, we follow an incremental approach, starting with the weak and closed version of call-by-need, formalized in a calculus with explicit substitutions. Aiming at more general settings, we extend it to the weak and open setting—where terms are potentially open but reduction remains weak—calling it Open CbNeed. Finally, we derive a useful variant of Open CbNeed, called Useful Open CbNeed.The interest in this useful version of call-by-need comes from the complexity theory of the lambda-calculus. It is known that proving the existence of a reasonable time cost model for the strong lambda-calculus—where reduction is allowed under lambda-abstractions—requires the implementation of useful substitutions, consisting in reducing expressions up to a shared normal form while holding back substitutions that do not contribute to its obtention.The literature only contains implementations of useful substitutions in the leftmost-outermost evaluation strategy, the standard evaluation strategy of the lambda-calculus which performs call-by-name reduction. Therefore, Useful Open CbNeed is the first-ever implementation of (all the kinds of) useful substitutions required in a strong call-by-need lambda-calculus. First introduced as a key element in Useful Open CbNeed, useful substitutions are then represented within the Useful Open CbNeed multi type system.Lastly, we derive an evaluation strategy implementing a strong call-by-value lambda-calculus, and further extend the quantitative results concerning the strong setting by deriving a multi type system for this call-by-value strategy. This concerns the quantitative theory of call-by-need in that it is a necessary step towards the development of a strong variant of Useful Open CbNeed, as well as a multi type system for it with the desired quantitative properties.
Dans cette thèse, on présente une étude quantitative du lambda calcul en appel-par-nécessité, du côté de la théorie de types ainsi que de celui de la sémantique opérationnelle.En ce qui concerne la théorie de types, on dérive plusieurs systèmes de multi types — un variant non-idempotent des types d’intersection. Chacun de ces systèmes cible une certaine notion de l’appel-par-nécessité, de telle façon que le typage équivaut à la normalisation dans la version correspondante de l’appel-par-nécessité. Dans chaque cas, la caractérisation de la normalisation est tellement raffinée que l’on est capable d’extraire d’informations quantitatives concernant plusieurs aspects du processus de normalisation — typiquement, le nombre de pas de réduction vers la forme normale et la taille de la forme normale.En ce qui concerne la sémantique opérationnelle, on suit une approche incrémentale, en partant de la version faible et fermée de l’appel-par-nécessité, formalisée dans un calcul avec des substitutions explicites. En visant le cas le plus général, on l’étend vers le cadre de la réduction faible et ouverte — où les termes sont potentiellement ouverts mais la réduction reste faible — et on appelle cette stratégie l’Open CbNeed. Enfin, on obtient un variant utile de l’Open CbNeed, appelé Useful Open CbNeed.L’interêt de ce variant utile de l’appel-par-nécessité provient de la théorie de la complexité du lambda calcul. On sait que la preuve de l’existence d’un modèle de coût de temps raisonnable pour le lambda calcul fort — où la réduction peut aller au-dessous des abstractions lambdas — requiert la mise en œuvre des substitutions dites utiles. Ces dernières consistent à réduire les expressions jusqu’à l’obtention d’une forme normale partagée, tandis que l’on n’effectue les substitutions ne contribuant pas a son obtention.La literature ne contient d’analyses sur les substitutions utiles que pour la stratégie d’évaluation leftmost-outermost, la stratégie d’évaluation standard du lambda calcul, appartenant à la famille de l’appel-par-nom. La présentation de l’Useful Open CbNeed est donc la toute première analyse des substitutions utiles pour l’appel-par-nécessité dans le cadre du lambda calcul fort. Présentées comme un élément clé dans la sémantique opérationnelle de l’Useful Open CbNeed, les substitutions utiles sont en suite représentées dans le système de multi types de l’Useful Open CbNeed.Finalement, on dérive une stratégie d’évaluation pour le lambda calcul fort en appel-par-valeur, et puis on étend les résultats quantitatives du cadre fort du lambda calcul en dérivant un système de multi types pour cette stratégie de l’appel-par-valeur. Ceci concerne la théorie quantitative de l’appel-par-nécessité en tant qu’il est un pas nécessaire pour la mise en œuvre d’un variant fort de l’Useful Open CbNeed, ainsi que d’un système de multi types le caractérisant et ayant les propriétés quantitatives désirées.
Fichier principal
Vignette du fichier
97510_LEBERLE_2021_archivage.pdf (2.34 Mo) Télécharger le fichier
Origine : Version validée par le jury (STAR)

Dates et versions

tel-03284370 , version 1 (12-07-2021)

Identifiants

  • HAL Id : tel-03284370 , version 1

Citer

Maico Leberle. Dissecting call-by-need by customizing multi type systems. Symbolic Computation [cs.SC]. Institut Polytechnique de Paris, 2021. English. ⟨NNT : 2021IPPAX023⟩. ⟨tel-03284370⟩
132 Consultations
71 Téléchargements

Partager

Gmail Facebook X LinkedIn More