[Prev][Next][Index][Thread]
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:
@article{BaLon80,
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:
@article{Lon83,
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.
GL