13/05/2004
Antonino Salibra (Università Ca'Foscari di Venezia)
Lambda theories via graph models

The set of lambda theories is naturally equipped with a structure of complete lattice, where the meet of a family of lambda theories is their intersection, and the join is the least lambda theory containing their union. Many longstanding open problems of lambda calculus (as, for example, the order-incompleteness problem) can be restated in terms of properties of this lattice (hereafter denoted by LT). In this talk, I will present some results aiming to clarify the structure of the lattice LT. In one of these results (obtained in collaboration with Chantal Berline) the existence of an infinite distributive sublattice of LT shows, against the common belief, that the lambda calculus can satisfy strong algebraic properties.

Some of the presented results were obtained via a model-theoretic argument based on graph models, which are simple and natural set-theoretic models of pure lambda-calculus. If time permits, I'll present also some recent work characterizing the set of lambda-theories of graph models. In one of these results, obtained in collaboration with Antonio Bucciarelli, it is shown the non-existence of a graph model whose equational theory is exactly the minimal lambda theory lambda-beta. This answers a longstanding open question for the restricted class of graph models.