Typing and Optimal reduction for λ-calculus in variants of Linear logic for Implicit computational complexity
Institution:
Paris 13Disciplines:
Directors:
Abstract EN:
Lambda-calculus has been introduced to study the mathematical functions from a computational point of view. It has then been used as a basis for the design of functional programming languages. Knowing whether there exists a provably most efficient method to reduce lambda-terms, and evaluate the complexity of this operation in general are still open questions. In this thesis, we use the tools of typing, of Linear logic, of type inference and of Optimal reduction to explore those questions. We present a type inference algorithm for Dual light affine logic (dlal), a type system which characterises the polynomial time complexity class. The algorithm takes in input a system F typed lambda-term, and outputs a typing in dlal if there exists one. An implementation is provided. Then, we extend a type system based on Elementary affine logic with subtyping, in order to automatise the cœrcions placement. We show that subtyping captures indeed the cœrcions, and we give a fully-fledged type inference algorithm for this extended system. Finally, we adapt Lamping’s Optimal reduction algorithm to the lambdaterms typable in Soft linear logic (sll), also characterising polynomial time. We prove a complexity bound on the reduction of any Sharing graph, and that lambda-terms typable in sll can be correctly reduced with our ad-hoc Optimal reduction algorithm.
Abstract FR:
Le lambda-calcul a été introduit pour étudier les fonctions mathématiques d’un point de vue calculatoire. Il a ensuite servi de fondement au développement des langages de prgrammation fonctionnels. Savoir si il existe une méthode prouvablement la plus efficace pour réduire les lambda-termes, et connaître la complexité intrinsèque de cette opération en général sont toujours des questions ouvertes. Dans cette thèse, nous utilisons les outils du typage, de l’inférence de type, de la Logique linéaire et de la Réduction optimale pour explorer ces questions. Nous présentons un algorithme d’inférence de type pour Dual light affine logic (dlal), un système de type qui caractérise la classe de complexité polynomiale. L’algorithme prend en entrée un lambda-terme typé dans le système F et renvoie un typage dans dlal si il en existe un. Une implémentation est fournie. Puis, nous étendons un système de type fondé sur Elementary affine logic avec du sous-typage, afin d’automatiser le placement des cœrcicions. Nous montrons que le sous-typage capture bien les cœrcicions, et nous donnons un algorithme d’inférence complet pour ce système étendu. Enfin, nous adaptons l’algorithme de Réduction optimale de Lamping pour les lambda-termes typables dans Soft linear logic (sll), une logique qui caractérise le temps polynomial. Nous montrons qu’une borne polynomiale existe pour tous les graphes de partage ainsi réduits, et que les lambda termes typables dans sll sont réduits correctement.