[Haskell-cafe] Deciding equality of functions.

[wren ng thornton]

On 4/9/11 1:26 PM, Grigory Sarnitskiy wrote:
> I guess that deciding whether two functions are equal in most cases is algorithmically impossible. However maybe there exists quite a large domain of decidable cases? If so, how can I employ that in Haskell?
>
> 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 easy path forward for this situation is to demonstrate the 
correctness of the slow/obvious implementation and then use a 
combination of lazy SmallCheck, QuickCheck, and HUnit in order to show 
that the fast implementation produces equal outputs for all small 
inputs, randomly chosen inputs, and select manually chosen inputs.

Or, if you happen to be working with a nice well-behaved type, then you 
can use circuit SAT, SMT, and other domain solvers, or Martin Escardo's 
excellent work on compact spaces.


[1] Though if something as simple as TCO is so hard to prove 
equivalences with, maybe that says something about our current crop of 
proof assistants and theorem provers.

-- 
Live well,
~wren