Unverified

Continuously Complete CPO Models with Minimal Theory

A CPO model is continuously complete if every Scott-continuous self-map is represented by a point of the model. Its theory is the set of equations between closed lambda terms valid in the model. Determine whether there exists

a continuously complete CPO model with theory exactly $\lambda\beta$ ; or
an extensional continuously complete CPO model with theory exactly $\lambda\beta\eta$ .

Equivalently, are retract models complete for the corresponding lambda calculus? The source also asks whether a filter model can realize either exact theory.

Download

Abstract

Does a continuously complete CPO model of lambda calculus have equational theory exactly lambda-beta, or, in the extensional case, exactly lambda-beta-eta?

Background and progress

Furio Honsell submitted this question in 2007 and traces it to discussions beginning in 1983--1984. The source reports an $\omega_1$ -continuous analogue with theory exactly $\lambda\beta\eta$ and theories admitting no continuously complete CPO model, but not a model answering the stated question. The status statements here follow the TLCA page's July 21, 2014 snapshot and have not been independently updated after that date [Honsell, 2007]. The original open problem appears at https://tlca.di.unito.it/opltlca/opltlcasu29.html.

Reference papers

Continuously Complete CPO Models with Minimal TheoryFurio HonsellTLCA Open Problem List · 2007 ↗

Continuously Complete CPO Models with Minimal Theory

Coming soon

Organizer