Models and theories of pure and resource lambda calculi

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 functions, 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, all filter models living in CPO and all extensional reflexive Scott domains. By performing a fine-grained study of 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/problem19.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 all terms having the same Bohm tree.