Path: utzoo!utgpu!watserv1!watmath!att!rutgers!tut.cis.ohio-state.edu!zaphod.mps.ohio-state.edu!samsung!rex!fs
From: fs@rex.cs.tulane.edu (Frank Silbermann)
Newsgroups: comp.lang.functional
Subject: Re: Laziness and Leftmost Rule
Message-ID: <3500@rex.cs.tulane.edu>
Date: 5 Jun 90 18:00:13 GMT
References: <1990Jun2.123101.24421@sics.se> <3485@rex.cs.tulane.edu> <3835@moondance.cs.uq.oz.au>
Organization: Computer Science Dept., Tulane Univ., New Orleans, LA
Lines: 44


>>		...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).

In article <3835@moondance.cs.uq.oz.au> paul@batserver.cs.uq.oz.au writes:

>	Not so, I think.  Parallel-or exists in the Scott domain.
>	But, parallel-or is only (untyped-)lambda-definable
>	through some complex encoding/interpretation.
>	Hence, lambda-calc's not fully-abstract.

Parallel-or exists in _which_ Scott domain?
There is no such thing as "fully-abstract",
except in relationship to some specified (or implied) domain.

The Scott domain D described by:
		D =~ (Int + Bools + D->D )_bot
does indeed contain a (curried) parallel-OR.
However, the Scott domain D described by:
		D =~ (D->D)
contains no Boolean functions at all.  In fact,
this domain lacks even the base Boolean values TRUE and FALSE!
So, please explain again why you don't believe
this domain D =~ (D->D) is not a fully abstract model
of the pure untyped lambda calculus.

>	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 ...  Paul Bailes

In programming languages, we usually assume the existence of
base atomic values (e.g. integers, booleans or other atoms),
so D =~ (D->D) is rarely the appropriate domain.
Therefore, the pure-untyped-lambda-calculus
is not the best basis for programming language design.
Mulmuley and Plotkin use typed lambda calculi,
whose fully abstract models (their corresponding domains)
contain the kinds of values desired.

	Frank Silbermann	fs@rex.cs.tulane.edu
	Tulane University, New Orleans, Louisianna  USA