[Prev][Next][Index][Thread]
[mcvax!doc.ic.ac.uk!sa@uunet.UU.NET: Re: [meyer: TYPE:TYPE]]
From: mcvax!doc.ic.ac.uk!sa@uunet.UU.NET
Date: Mon, 9 Nov 87 15:10:26 GMT
To: meyer@theory.lcs.mit.edu
Subject: Re: [meyer: TYPE:TYPE]
I was interested in the discussion about computational adequacy, because
it seems to relate quite strongly to some work I have been doing recently
(and also work of my student Luke Ong).
We have been studying what I call the ``Lazy lambda-calculus'', where
one considers convergence to WEAK head normal form, i.e. to an
abstraction. This is in fact what all implementations of lazy functional
languages do (see e.g. Simon Peyton Jones' book on graph reduction).
Taking convergence to weak head normal form as the basic observable,
one can define a bisimulation-like preorder on terms (closed terms,
then extended to all terms via their closed instances). This gives
rise to a rather interesting--although of course non-sensible--
lambda theory, in which: Longo's POk terms are grouped into an
ascending chain; this chain's lub (the PO infinity terms) are the
global top element (represented e.g. by YK); (beta) holds, and (eta) holds in
the conditional form:
lambda x. Mx = M (M converges, x not free in M)
where ``converges'' means of course ``head reduces to an abstraction''.
The bisimulation preorder IS equivalent to the one obtained from
convergence by closing under all contexts, but this is by no means
trivial to prove; in fact, my proof of this purely syntactic fact
goes via the denotational semantics, and specifically the ``Domain logic''
version of it, in the sense of my LICS paper.
There IS a canonical model for this lazy lambda calculus, namely
D = lift (D -> D)
(the intital solution is not trivial).
One can carry out a similar programme as regards computational
adequacy AND full abstraction for this untyped pure lambda calculus
as Plotkin did for typed lambda calculus with base types; similar
results as his can be obtained, although the proofs are often
rather hairier.
All this is in a draft paper of which I can send copies to anyone interested;
a short version will apppear in the proceedings of the Austin Institute
of Declarative Programming.