Path: utzoo!attcan!uunet!munnari.oz.au!bunyip!moondance!batserver.cs.uq.oz.au!paul
From: paul@batserver.cs.uq.oz.au (Paul Bailes)
Newsgroups: comp.lang.functional
Subject: Re: Laziness and Leftmost Rule
Message-ID: <3835@moondance.cs.uq.oz.au>
Date: 5 Jun 90 01:25:53 GMT
References: <BJORNL.90Jul30101627@tarpon.tds.kth.se> <3462@rex.cs.tulane.edu> <1990Jun2.123101.24421@sics.se> <3485@rex.cs.tulane.edu>
Sender: news@moondance.cs.uq.oz.au
Reply-To: paul@batserver.cs.uq.oz.au
Lines: 31

fs@rex.cs.tulane.edu (Frank Silbermann) writes:


> <lots of good stuff, but then ...>

>For instance, the pure untyped lambda calculus is fully abstract
>w.r.t. a domain isomorphic to its own function space
>(i.e. a universe D isomorphic to the universe of
>computable unary functions over D).

Not so, I think. As you appreciate at the start of your letter,
parallel-or is only (untyped-)lambda-definable through some
complex encoding/interpretation. However, parallel-or exists in the
Scott domain. Hence, lambda-calc's not fully-abstract. The detailed
support for this comes from Mulmuley (1987) and Plotkin (1977). While
they're working with typed lambda-calc., I can't see how that affects
the issue (ie the semantic domain's got something in it that the
programming language hasn't). Anyhow, I look forward to being corrected
if appropriate.

REFERENCES

Mulmuley, K. ``Full Abstraction and Semantic Equivalence'' MIT Press 1987.

Plotkin, G.D. ``LCF Considered as a Programming Language'' TCS vol 5 pp 223-
	255 1977.

Paul Bailes
Dept Comp Sci
Uni of Queensland QLD 4072
AUSTRALIA