On Tue, 27 Jul 1999, Andreas C. Doering wrote:
> >> let x=[1..] in x==x
> >> would not terminate in the first case but succeed in the second.
> >
> > But, much worse
> >
> > let x = (a,b) in x `req` x = True
> > but
> > (a,b) `req` (a,b) = False
> >
> > So referential transparency is lost. This is a high price to pay.
> > You are right that *something* is needed; but I don't yet know what.
One solution is nondeterminism.
req x y is False when x and y are not 'equal'
req x y is True | False when x and y are 'equal'
where 'equal' means the same as the built-in == operator for the type,
or structural equality for user-defined types and where
a | b
means a nondeterministic choice between a and b.
Now
let x=[1..] in x == x
can not be proved to terminate with Andreas's optimized definition
of List == (although it also can not be proved not to terminate).
It is valid to optimize
(a,b) `req` (a,b)
to
let x = (a,b) in x `req` x .
However, the inverse transformation increases nondeterminism and
thus would not be valid. So if you define referential transparency
as the saying that
E[ x / F]
and
let x = F in E
are equivalent, then referential transparency is still 'lost'.
But when nondeterminism is involved, this equivalence is usually
already an inequivalence.
In 'good' implementations, there would be a pragmatic understanding that
req x y will be True when x and y are the same reference.
Cheers,
Theo
----------------------------
Dr. Theodore Norvell, Assistant Professor [EMAIL PROTECTED]
Memorial University of Newfoundland http://www.engr.mun.ca/~theo
Vox: (709) 737-8962 Fax: (709) 737-4042
