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.