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

• To: types@dcs.gla.ac.uk
• Subject: in which models of untyped lambda calculus are terms with no whnf
• From: Thomas Streicher <streiche@informatik.uni-muenchen.de>
• Date: Tue, 28 Jun 94 15:26:22 +0200
• Approved: types@dcs.gla.ac.uk

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

• Prev: Full affine logic is decidable
• Next: Krivine's book in Engl?
• Index(es):
  • Main
  • Thread