On Reasonable Space and Time Cost Models for the λ-Calculus

Description

Slot and van Emde Boas Invariance Thesis states that a time (respectively, space) cost model is reasonable for a computational model C if there are mutual simulations between Turing machines and C such that the overhead is polynomial in time (respectively, linear in space). The rationale is that under the Invariance Thesis, complexity classes such as LOGSPACE, P, PSPACE, become robust, i.e. machine independent. In this dissertation, we want to find out if it possible to define a reasonable space cost model for the lambda-calculus, the paradigmatic model for functional programming languages. We start by considering an unusual evaluation mechanism for the lambda-calculus, based on Girard's Geometry of Interaction, that was conjectured to be the key ingredient to obtain a space reasonable cost model. By a fine complexity analysis of this schema, based on new variants of non-idempotent intersection types, we disprove this conjecture. Then, we change the target of our analysis. We consider a variant over Krivine's abstract machine, a standard evaluation mechanism for the call-by-name lambda-calculus, optimized for space complexity, and implemented without any pointer. A fine analysis of the execution of (a refined version of) the encoding of Turing machines into the lambda-calculus allows us to conclude that the space consumed by this machine is indeed a reasonable space cost model. In particular, for the first time we are able to measure also sub-linear space complexities. Moreover, we transfer this result to the call-by-value case. Finally, we provide also an intersection type system that characterizes compositionally this new reasonable space measure. This is done through a minimal, yet non trivial, modification of the original de Carvalho type system.

Abstract (French)

La thèse d'invariance de Slot et van Emde Boas stipule qu'un modèle de coût temporel (respectivement spatial) est raisonnable pour un modèle informatique C s'il existe des simulations mutuelles entre les machines de Turing et C telles que la surcharge est polynomiale dans le temps (respectivement linéaire dans l'espace) . La logique est que sous la thèse de l'invariance, les classes de complexité telles que LOGSPACE, P, PSPACE, deviennent robustes, c'est-à-dire indépendantes de la machine. Dans cette thèse, nous voulons savoir s'il est possible de définir un modèle de coût spatial raisonnable pour le lambda-calcul, le modèle paradigmatique des langages de programmation fonctionnels. Nous commençons par considérer un mécanisme d'évaluation inhabituel pour le lambda-calcul, basé sur la géométrie de l'interaction de Girard, qui a été supposé être l'ingrédient clé pour obtenir un modèle de coût raisonnable en espace. Par une analyse fine de la complexité de ce schéma, basée sur de nouvelles variantes de types d'intersections non idempotentes, nous réfutons cette conjecture. Ensuite, nous changeons la cible de notre analyse. Nous considérons une variante de la machine abstraite de Krivine, un mécanisme d'évaluation standard pour le lambda-calcul d'appel par nom, optimisé pour la complexité de l'espace et implémenté sans aucun pointeur. Une analyse fine de l'exécution de (une version raffinée de) l'encodage des machines de Turing dans le lambda-calcul nous permet de conclure que l'espace consommé par cette machine est bien un modèle de coût d'espace raisonnable. En particulier, pour la première fois, nous sommes capables de mesurer également des complexités spatiales sous-linéaires. De plus, nous transférons ce résultat au cas d'appel par valeur. Enfin, nous fournissons également un système de type intersection qui caractérise la composition de cette nouvelle mesure d'espace raisonnable. Cela se fait par une modification minimale, mais non triviale, du système de type original de Carvalho.

Additional details