Le lambda calcul avec constructeurs (de Arbiser, Miquel et Rios) est une extension du lambda calcul avec un mécanisme de filtrage. Le filtrage à la ML y est décomposé en deux étapes: une analyse de cas sur des constantes (telle l'instruction «case» de Pascal), et une commutation de l'application avec la construction de filtrage. Cette règle de commutation entre deux constructions de natures différentes induit une géométrie de calcul surprenante, a priori incompatible avec les intuitions habituelles de typage. Cependant il a été montré que ce calcul est confluent, et vérifie la propriété de séparation (à la Böhm). Cette thèse propose un système de types du polymorphique pour ce calcul, et décrit ensuite un modèle de réalisabilité, qui adapte les candidats de réductibilité de Girard au lambda calcul avec constructeurs. La normalisation forte du calcul typé et l'absence d'erreur de filtrage lors de l'évaluation en découlent immédiatement. Nous nous intéressons ensuite à la sémantique du lambda calcul avec constructeurs non typé. Une notion générique de modèle catégorique pour ce calcul est définie, puis un modèle particulier (le modèle syntaxique dans la catégorie des PERs) est construit. Nous en déduisons un résultat de complétude. Enfin, nous proposons une traduction CPS du lambda calcul avec constructeurs dans le lambda calcul simplement typé avec paires. Le lambda calcul avec constructeurs peut ainsi être simulé dans un calcul bien connu, et cette traduction nous permet aussi de transformer tout modèle par continuation en modèle du lambda calcul avec constructeurs. Une équation catégorique caractéristique de ces modèles apparait alors, qui permet de construire des modèles non syntaxiques (dans les domaines) de Scott du lambda calcul avec constructeurs. / The lambda calculus with constructors was introduced by Arbiser, Miquel and Rios in the early 2000's as an extension of lambda calculus with pattern matching features. It decomposes the pattern matching à la ML into a case-analysis on constant constructors (in the spirit of the case instruction in Pascal), and a commutation rule between case construction and application. This commutation rule between two different kinds of constructions designs a surprising computational behaviour, a priori} not compatible with usual typing intuitions. However the whole calculus was proved confluent, and it enjoys the separation property (a version of Böhm's lemma).In this thesis we propose a polymorphic type system for this calculus, and we develop a realisability model, based on Girard's reducibility candidates. This leads to a strong normalisation result for the typed calculus, and guaranties that the type system prevents match failure. Next we focus on semantics for the untyped calculus. We first define a generic notion of models for the lambda calculus with constructors in Cartesian closed categories. We then establish the syntactic model in the category of PERs, and deduce a completeness result from it.Finally, we consider a translation of the lambda calculus with constructors into the pure lambda lambda calculus relying on continuation passing style techniques. This enables the simulation of the lambda calculus with constructors by a well known calculus, and provides a transformation of every continuation model into a model of the lambda calculus with constructors. Thereby a categorical equation characteristic of these models appears, which enables the construction of non syntactic models in Scott's domains.
| Identifer | oai:union.ndltd.org:theses.fr/2011ENSL0628 |
| Date | 13 July 2011 |
| Creators | Petit, Barbara |
| Contributors | Lyon, École normale supérieure, Miquel, Alexandre |
| Source Sets | Dépôt national des thèses électroniques françaises |
| Language | English |
| Detected Language | French |
| Type | Electronic Thesis or Dissertation, Text |
Page generated in 0.0027 seconds