Submitted by Furio Honsell
Date: April 20 2007
Statement. Is there a continuously complete CPO model of the -calculus whose theory is precisely or ?
Problem Origin. I asked myself this question in 1983. In 1984, on different occasions I asked it to Dana Scott and Gordon Plotkin. Both told me that they had already thought about it.
A CPO model is continuously complete if all Scott-continuous self-maps are represented by a point in the model. Continuously complete models are sometimes called retract models or reﬂexive models.
The theory of a model is the set of all equations between closed -terms which hold in the model. The problem can be phrased equivalently as:
There are many related results, e.g.:
There exists a -continuously complete -CPO model whose theory is precisely [Di Gianantonio et al., 1995].
There exist theories which do not have continuously complete CPO-models [Honsell and Ronchi Della Rocca, 1992].
[Honsell and Ronchi Della Rocca, 1992] Honsell, F. and Ronchi Della Rocca, S. (1992). An approximation theorem for topological lambda models and the topological incompleteness of lambda calculus. Journal of Computer and System Sciences, 45(1):49–75.