[Haskell-cafe] Deciding equality of functions.
Edward Z. Yang
ezyang at MIT.EDU
Sat Apr 9 23:24:53 CEST 2011
Excerpts from Grigory Sarnitskiy's message of Sat Apr 09 13:26:28 -0400 2011:
> 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?
In the case of functions where the domain and range are finite, function
equality is decidable but not usually feasible. If your function is a
combinatorial circuit, you can apply technology like SAT solvers to
hopefully decide equality in faster than exponential time (this is what
Cryptol does; you may find it interesting.)
More information about the Haskell-Cafe