Abstract of Paper

The minimal graph model of lambda calculus
by Antonio Bucciarelli and Antonino Salibra

Abstract:

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.