[Haskell-cafe] Deciding equality of functions.

[Claus Reinke]

>> It is a common situation when one has two implementations of 
>> the same function, one being straightforward but slow, and the 
>> other being fast but complex. It would be nice to be able to check 
>> if these two versions are equal to catch bugs in the more complex 
>> implementation.
> 
> This common situation is often actually one of the harder ones 
> to prove, I say coming from proving a few of them in Coq. The 
> thing is that a lot of the common optimizations (e.g., TCO) 
> completely wreck the inductive structure of the function which, 
> in turn, makes it difficult to say interesting things about them.[1]

The traditional approach is to derive the efficient version from
the simple, obviously correct version, by a series of small code
transformations. The steps would include meaning-preserving
equivalences as well as refinements (where implementation
decisions come in to narrow down the set of equivalent code).

Advantages: codes are equivalent by construction (modulo 
implementation decisions), and the relationship is documented
(so you can replay it in case requirements changes make you
want to revisit some implementation decisions).

Even with modern provers/assistants, this should be easier
than trying to relate two separately developed pieces of code,
though I can't speak from experience on this last point. But 
there have been derivations of tail-recursive code from the 
general form (don't have any reference at hand right now).

Claus