9 Apr
2011
9 Apr
'11
5:24 p.m.
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.) Cheers, Edward