[Prev][Next][Index][Thread]
in which models of untyped lambda calculus are terms with no whnf
Although it is a question about untyped lambda calculus I hope to
receive an answer to the following 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.
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.
Thanks for all answers in advance,
Thomas Streicher