|Abstract of Paper|
The minimal graph model of lambda calculus
by Antonio Bucciarelli and Antonino Salibra
Among the set-theoretical models of the untyped lambda calculus the graph models, introduced by Plotkin, Scott and Engeler within the continuous semantics, are particularly easy to describe. They have been proven useful for giving proof of consistency of extensions of $\lambda$-calculus and for studying operational features of $\lambda$-calculus. In this paper we show that there exists a graph model whose equational theory is included in the equational theory of any other graph model. This result solves an open question stated by Berline. Another interesting question arises: what equations between $\lambda$-terms are equated by this minimal lambda theory? The answer to this difficult question is still unknown; we conjecture that the right answer is the minimal lambda theory $\lambda\beta$. We give a sketch of the technicalities used in the proof of the main result. For any equation not belonging to the intersection of all $\lambda$-theories of graph models, we choose a particular model where the equation fails. Then we use a technique of completion for gluing together all these models in a unique graph model. Finally, we show that the equational theory of this completion is minimal. The technique used to prove the minimality of the completion seems general enough to be applied to other classes of models.