Models and theories of pure and resource lambda calculas
Institution:
Paris 7Disciplines:
Directors:
Abstract EN:
Part I: A longstanding open problem is whether there exists a model of the untyped lambda calculus in the category CPO of complete partial orderings and Scott continuous fonctions, whose theory is exactly the least lambda-theory λß or the least extensional lambda-theory λβπ: it is Problem 22 in the TLCA list of open problems (http://tlca. Di. Unito. It/opltlca/problem22. Pdf). In this thesis we analyze the class of reflexive Scott domains, the models of lambda calculus living in the category of Scott domains (a full subcategory of CPO). We isolate, among the reflexive Scott domains, a class of webbed models arising from Scott's information Systems, that we call i-models. The class of i-models includes, for example, all preordered coherent models, al filter models living in CPO and ail extensional reflexive Scott domains. By performing a fine-grained study o an "effective" version of Scott's information Systems and i-models we obtain the following main results: there is an important class of i-models which is not complete for the extensional calculus and whose members never have a recursively enumerable order theory. A closed lambda-term M is easy if, for any other closed term N, the lambda-theory generated by the equation M = N is consistent, while it is simple easy if, given an arbitrary intersection type τ, one can find a suitable pre-order on types which allows to derive τ for M. Simple easiness implies easiness. The question whether easiness implies simple easiness constitutes Problem 19 in the TLCA list of open problems (http://tlca. Di. Unito. It/opltlca/probleml9. Pdf). As a byproduct of our work on i-models, we are in the position of solving this problem: we answer negatively, providing a nonempty set of easy, but non simple easy, lambda-terms. Part II: Given a semi-ring with unit which satisfies some conditions, we define an exponential functor on the category of sets and relations which allows to define a denotational model of Differential Linear Logic and of the lambda-calculus with resources. We show that, when the semi-ring has an element which is "infinitary", this model does not validate the Taylor formula and that it is possible to build, in the associated Kleisli cartesian closed category, a model of the pure lambda-calculus which is not sensible. This is a quantitative analogue of the Park's graph model construction in the category of Scott domains. We initiate a purely algebraic study of Ehrhard and Regnier's resource lambda-calculus, by introducing three algebraic varieties: resource combinatory algebras, resource lambda-algebras and resource lambda- abstraction algebras. We establish the relations between them, laying down foundations for a model theory of resource lambda calculus. We also show that the ideal completion of a resource combinatory algebra (resp. Lambda-algebra, lambda-abstraction algebra) induces a "classical" combinatory algebra (resp. Lambda-algebra, lambda-abstraction algebra), and that any model of the pure lambda calculus raising from a resource lambda- algebra determines a lambda-theory which equates ail terms having the same Böhm tree.
Abstract FR:
Partie I: Un problème ouvert depuis longtemps est de savoir s'il existe un modèle du lambda calcul non typé dans la catégorie CPO des ordres partiels complètes et fonctions Scott continues, dont la théorie équationnelk soit exactement la plus petite lambda-théorie λß ou la plus petite lambda-théorie extensionnnelle λβπ: c'est le Problème 22 dans la liste de problèmes ouverts TLCA (http://tlca. Di. Unito. It/opltlca/problem22. Pdf). Dans cette thèse, nous analysons la classe des domaines de Scott réflexifs, les modèles du lambda calcul vivants dans la catégorie des domaines de Scott (une sous-catégorie pleine de CPO). Nous isolons, parmi les domaines de Scott réflexifs, une classe de modèles à trame découlant des systèmes d'information de Scott, que nous appelons i-modèles. La classe des i-modèles comprend, par exemple, tous les modèles préordonnées cohérentes, tous les modèles de filtre vivants dans CPO et tous les domaines de Scott réflexifs extensionnels. En réalisant une étude fine d'une version "effective" des systèmes d'information de Scott et des i-modèles, nous obtenons les résultats suivants: il y a une important classe de i-modèles qui n'est pas complète pour le lambda calcul extensionnel et tel que tous ces membres ne ont pas une théorie d'ordre récursivement énumérable. Un lambda-terme clos M est dit facile si, pour tout autre terme clos N, la lambda-théorie engendrée par l'équation M-N est cohérente, alors qu'il est simple facile si, étant donné un type intersection quelconque τ, or peut trouver un pré-ordre sur les types qui permet de dériver le type τ pour M. La facilité simple implique la facilité. La question de savoir si la facilité implique la facilité simple constitue le Problème 19 dans la liste de problèmes ouverts TLCA (http://tlca. Di. Unito. It/opltlca/probleml9. Pdf). Comme sous-produit de notre travail sur les i-modèles, nous sommes en position de résoudre ce problème: nous répondons négativement, en fournissant un ensemble non vide de lambda-termes faciles mais non simple faciles. Partie II: Etant donné un semi-anneau avec unité qui satisfait certaines conditions, nous définissons un foncteur exponentiel sur la catégorie des ensembles et des relations qui permet de définir un modèle dénotationnel de la Logique Linéaire Différentielle et du lambda-calcul avec ressources. Nous montrons que, lorsque le semi-anneau contient un élément qui est "infinitaire", ce modèle ne satisfait pas la formule de Taylor et qu'il est possible de construire, dans la catégorie Cartésienne fermée de Kleisli associée, un modèle du lambda calcul pur qui n'est pas sensible. Il s'agit d'un analogue quantitative de la construction du graphe modèle de Park dans la catégorie des domaines de Scott. Nous commençons une étude purement algébrique du lambda calcul avec ressources de Ehrhard et Régnier, ei introduisant trois variétés algébriques: les algèbres combinatoires avec ressources, les lambda-algèbres avec ressources et les algèbres de lambda-abstraction avec ressources. Nous établissons les relations entre elles, et jetons les bases d'une théorie des modèles du lambda-calcul avec ressources. Nous montrons également que la complétion par idéaux d'une algèbre combinatoire (resp. Lambda-algèbre, algèbre de lambda-abstraction) avec ressources induit une algèbre combinatoire (resp. Lambda-algèbre, algèbre de lambda-abstraction) "classique", et que tout modèle du lambda calcul classique provenant d'une lambda-algèbre avec ressources détermine une lambda-théorie qui égalise tous les termes ayant le même arbre de Bôhm.