[Next]  [Previous]  [Up]  

Problem # 22

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:

There are many related results, e.g.:

There exists a ω1   -continuously complete ω1   -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].

References for # 22

[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.

[Next]  [Previous]  [Up]  
© 2006 Dip. Informatica - Universita di Torino
Last modified: July 21, 2014