On functions preserving levels of approximation: A refined model construction for various lambda calculi

In this paper dI-domains are enriched by a family of projections which assi gn to each point a sequence of canonical approximations. The morphisms are stable maps that preserve the levels of approximation generated by the proj ections. For the computation of an approximation of a given level of the ou tput they require, in addition, only information about the input of at most the same level of approximation. It is shown that the category of these do mains and maps is Cartesian closed. The set of morphisms between two such d omains is a domain of the same kind, but turns out not to be an exponent in the category. Domains D are constructed which are isomorphic to the exponent D-D. Moreove r, it is proved that the space of retractions in an exponent D-D is a retra ct of this. Both results together provide new models of Amadio-Longo's exte nsion lambda beta p of the lambda-calculus. As has been shown by Amadio and Longo, strong type theories which incorporate the Type: Type assumption ca n be syntactically interpreted in this calculus. (C) 1999-Elsevier Science B.V. All rights reserved.