Path: utzoo!attcan!uunet!mcsun!ukc!inmos!geoffb@butcombe.inmos.co.uk
From: geoffb@butcombe.inmos.co.uk (Geoff Barrett)
Newsgroups: comp.lang.functional
Subject: Re: Purity and Laziness
Message-ID: <7100@ganymede.inmos.co.uk>
Date: 29 May 90 10:07:51 GMT
References: <14531@dime.cs.umass.edu> <2535@skye.ed.ac.uk> <8691@cs.utexas.edu> <4170@castle.ed.ac.uk> <7044@ganymede.inmos.co.uk> <BJORNL.90Jul26211631@tarpon.tds.kth.se>
Sender: news@inmos.co.uk
Reply-To: geoffb@inmos.co.uk (Geoff Barrett)
Organization: INMOS Limited, Bristol, UK.
Lines: 112

In article <BJORNL.90Jul26211631@tarpon.tds.kth.se> bjornl@tds.kth.se (Bj|rn Lisper) writes:
]In article <7044@ganymede.inmos.co.uk> geoffb@butcombe.inmos.co.uk (Geoff
]Barrett) writes:
]%I believe there is an Oxford DPhil thesis by a man called David Turner
]%which pointed out that strict languages are not referentially
]%transparent because of the fact that conditionals are not strict, so
]%that the equality symbol in the definition
]
]%	fun iiff (b,x,y) = if b then x else y
]
]%is not equality.  Lazy evaluation languages are referentially
]%transparent.
]
]Hmmm. How would a lazy language treat a call
]
]if(b,x,x)
]
]where the evaluation of b is non-terminating but the evaluation of x
]terminates? If "naive" left-to-right evaluation order is assumed, the
]computation will not terminate. On the other hand, it is reasonable to
]define the semantics of the if-function so that such a call returns the
]value of x. (After all, the value of x will be the answer regardless of what
]b evaluates to). What about "referential transparency" here?

I think I need a good deal of convincing that it would be "reasonable"
to define the semantics of "if(b,x,x)" to be "x".  But, even so, so long
as "iiff (b,x,x)" and "if b then x else x" evaluate to the same thing
then the language is still referentially transparent.  All I want to be
able to do is to substitute equals.

]This problem is akin to left-to-right evaluation sensitivity of goals in
]Prolog; the order of goals that are ANDed together in a Horn clause can
]affect termination even though AND, considered as a "mathematical" binary
]operation, is commutative.

One would hope that it is commutative on proper values and obeys the
same rules as the "mathematical" operator there.  The functions

   f x = 2*x; g x = x/2

satisfy the rule "f.g = id = g.f" if their domains are restricted to the
non-zero real numbers, but not on the whole of the real numbers.
Sometimes different functions do satisfy different laws.  I think this
is what the French might call a "hering rouge".

]Bjorn Lisper

						Geoff Barrett
Newsgroups: comp.lang.functional
Subject: Re: Purity and Laziness
Summary: 
Expires: 
References: <14531@dime.cs.umass.edu> <2535@skye.ed.ac.uk> <8691@cs.utexas.edu> <4170@castle.ed.ac.uk> <7044@ganymede.inmos.co.uk> <BJORNL.90Jul26211631@tarpon.tds.kth.se>
Sender: 
Reply-To: geoffb@inmos.co.uk (Geoff Barrett)
Followup-To: 
Distribution: 
Organization: INMOS Limited, Bristol, UK.
Keywords: 

In article <BJORNL.90Jul26211631@tarpon.tds.kth.se> bjornl@tds.kth.se (Bj|rn Lisper) writes:
]In article <7044@ganymede.inmos.co.uk> geoffb@butcombe.inmos.co.uk (Geoff
]Barrett) writes:
]%I believe there is an Oxford DPhil thesis by a man called David Turner
]%which pointed out that strict languages are not referentially
]%transparent because of the fact that conditionals are not strict, so
]%that the equality symbol in the definition
]
]%	fun iiff (b,x,y) = if b then x else y
]
]%is not equality.  Lazy evaluation languages are referentially
]%transparent.
]
]Hmmm. How would a lazy language treat a call
]
]if(b,x,x)
]
]where the evaluation of b is non-terminating but the evaluation of x
]terminates? If "naive" left-to-right evaluation order is assumed, the
]computation will not terminate. On the other hand, it is reasonable to
]define the semantics of the if-function so that such a call returns the
]value of x. (After all, the value of x will be the answer regardless of what
]b evaluates to). What about "referential transparency" here?

I think I need a good deal of convincing that it would be "reasonable"
to define the semantics of "if(b,x,x)" to be "x".  But, even so, so long
as "iiff (b,x,x)" and "if b then x else x" evaluate to the same thing
then the language is still referentially transparent.  All I want to be
able to do is to substitute equals.

]This problem is akin to left-to-right evaluation sensitivity of goals in
]Prolog; the order of goals that are ANDed together in a Horn clause can
]affect termination even though AND, considered as a "mathematical" binary
]operation, is commutative.

One would hope that it is commutative on proper values and obeys the
same rules as the "mathematical" operator there.  The functions

   f x = 2*x; g x = x/2

satisfy the rule "f.g = id = g.f" if their domains are restricted to the
non-zero real numbers, but not on the whole of the real numbers.
Sometimes different functions do satisfy different laws.  I think this
is what the French might call a "hering rouge".

]Bjorn Lisper

						Geoff Barrett
vvv|       |vvv-------------------------------------
    \ o o /
     \   /           Wot! No Queen's Award logo?
      \_/