Re: in which models of untyped lambda calculus are terms with no whnf

In correction and partial answer to
Thomas Streicher's question:

> Let  D  be a domain theoretic model of the untyped lambda calculus,  
> i.e. let  D  be a cpo containing D->D  as a retract.
> Under which conditions is it guaranteed that a term has no weak head  
> normal form iff its interpretation in D is bottom ?!

> There is a partial answer to this as much as I know. A result of  
> Hyland tells us that two lambda terms have the same Boehm tree iff  
> their interpretation in Plotkin's T^omega is the the same.

As stated, this is not a result of  Hyland's but it appears, in a  
stronger form (Boehm tree inclusion corresponds exactly to the p.o in  
T^omega), in:

	AUTHOR = {Henk Barendregt and Giuseppe Longo},
	TITLE = {Equality of lambda-terms in the model {T}omega},
	JOURNAL = {To H.B. Curry: essays in Combinatory Logic, Lambda  
Calculus and Formalism}, YEAR = {1980},

> My question now precisely is the following : consider
>   C = D x C   D = C -> R    (R say Sierpinsky space)
> is it then the case that for the model  D  that a term is interpreted  
> as bottom iff it has no weak head normal form.

> Maybe the answer is already well known BUT if the answer is yes then  
> this would provide us with an ADEQUACY theorem for Krivin's machine.

A partial answer to a related (less general ?) question is in:

	AUTHOR = {Giuseppe Longo},
	TITLE = {Set-Theoretical Models of Lambda-calculus: Theories, 

Expansions, Isomorphisms},
	JOURNAL = {Annals of Pure and Applied Logic },
	YEAR = {1983}, VOLUME = {24}, PAGES = {153-188},

However, as the answer is not what required, this does not seem to  
give an ADEQUACY theorem for Krivine's machine.