On 27-Sep-1999, Ch. A. Herrmann <[EMAIL PROTECTED]> wrote:
> >>>>> "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.
I agree with your main point, but I'd disagree on this detail.
You can expand functions just fine, so long as you do so by applying
their definitions.
> 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 _|_.
Right. But the problem here is not so much due to preserving strictness,
rather it is the presence of bottom in the Haskell type `Integer'
in the first place.
You can expand functions like `-' just fine in Haskell, so long as you
use the Haskell definition of `-', not the mathematical definition.
So equational reasoning works fine. The problem is that traditional
mathematical reasoning doesn't. The difference between Haskell's `Integer'
type and mathematical integers needs to be taken into account when
reasoning about or transforming programs. You can't treat Haskell's
`Integer' type as if it were just mathematical integers.
> 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).
I agree with this approach. That is the approach we took for Mercury.
Cheers,
Fergus.
--
Fergus Henderson <[EMAIL PROTECTED]> | "I have always known that the pursuit
WWW: <http://www.cs.mu.oz.au/~fjh> | of excellence is a lethal habit"
PGP: finger [EMAIL PROTECTED] | -- the last words of T. S. Garp.
