The incompleteness problem for a semantics S of the untyped lambda
calculus can be stated as follows:
Is there a lambda theory that is not induced by any model of S?
In this talk we present a technique to prove in an uniform way the
incompleteness of a wide range of lambda calculus semantics,
including the strongly stable one, whose incompleteness had been
conjectured. The general technique used for proving that a semantics S is
incomplete is the following:
i) Find a topological property P satisfied by all models of the semantics S
ii) Find a lambda theory whose models do not satisfy P.
The main results are a topological incompleteness theorem and an order
incompleteness theorem. In the first one it is shown the incompleteness
of the lambda calculus semantics given in terms of topological models
whose topology satisfies a suitable property of connectedness.
In the second one it is shown the incompleteness of the lambda calculus
semantics given in terms of partially ordered models with finitely many
connected components (= minimal upper and lower sets)
w.r.t. the Alexandroff topology (the strongest topology whose
specialization order is the order of the considered model).