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 reflexive 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:
(or 
) the only equations which hold in all (extensional)
continuously complete CPO models of 
-calculus? I.e. Are retract
models complete for 
-calclulus?
or 
?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].
[Di Gianantonio et al., 1995] Di Gianantonio, P., Honsell, F., and Plotkin, G. (1995). Uncountable limits and the lambda calculus. Nordic Journal of Computing, 2(2):126–145.
[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.