Hi,
>>>>> "F" == Fergus Henderson <[EMAIL PROTECTED]> writes:
F> Well, it depends a bit on how you look at it. But I would say
F> that with normal equational reasoning, you _are_ constrained to
F> preserve strictness. To say that a function is strict in an
F> argument just means that when you apply that function to _|_, the
F> result is _|_. Using equational reasoning, transformations need
F> to preserve properties such as `f _|_ = _|_' just as much as they
F> need to preserve properties such as `f 0 = 42'.
I see a huge problem for equational reasoning due to preserving
strictness and that has nothing to do whether you are in a strict
language like ML or in a non-strict language like Haskell:
!!! You loose ability to expand functions.
Have a look at the following example: Assume
f :: Integer -> Integer
f x = x - x
and the expression (e + f n). Normally, you would like to simplify that
expression to e what you cannot do if you don't know that n/=_|_.
The use of Haskell can't help here, because '-' is strict anyway and,
in fact, termination behavior might change.
The problem is to introduce _|_ into your calculus, i.e., into the
integers, where it doesn't belong to. Mathematics says that for every
integer x, it holds that x-x=0. If you add _|_ to the integers,
this and many other theorems simply don't hold any longer,
because _|_ - _|_ must be _|_.
Therefore, I suggest to keep _|_ out of equational reasoning proofs and
consider termination behavior as a separate issue. Precisely, the
proof tells you, that if both programs terminate, they deliver the
same result, and that's better than having no proof at all (e.g., in
the case that a program you derived terminates more often, which
is obviously a good thing).
Cheers
--
Christoph Herrmann
E-mail: [EMAIL PROTECTED]
WWW: http://brahms.fmi.uni-passau.de/cl/staff/herrmann.html
