Abstract: | We prove that the class of stable models is incomplete with respect to pure λ-calculus. More precisely, we show that no stable model has the same theory as the strongly stable version of Park's model. This incompleteness proof can be adapted to the continuous case, giving an incompleteness proof for this case which is much simpler than the original proof by Honsell and Ronchi della Rocca. Moreover, we isolate a very simple finite set,
, of equations and inequations, which has neither a stable nor a continuous model, and which is included in
and in
, the contextual theory induced by the set of essentially λI-closed terms. Finally, using an approximation theorem suitable for a large class of models (in particular stable and strongly stable non-sensible models like
and
), we prove that
and
are included in
, giving an operational meaning to the equality in these models. |