Christopher Jefferson wrote:
On 8 Aug 2009, at 07:30, Scott McMurray wrote:
2009/8/7 Zachary Turner
: Out of curiosity, is it impossible due to technical limitations, or is it just not implemented because it's either difficult or nobody's ever gotten around to it?
Undecidable by reduction to the halting problem in general, though apparently possible for straight-line code (no loops/recursion) through the brute-force method of generate all paths and send them to a theorem prover to prove equivalence.
That sounds very unnecessary. Surely it would be sufficient, and what most people would expect, to check if the two function objects point to the same function (in the sense of location in memory), as opposed to logically equivalent functions?
I wrote some code that compares instances of the SAT problem, of course I didn't do the NP-hard job of checking if they had the same set of solutions, just if they were actually the same problem.
Chris
Comparing two SAT-instances actually is NP-hard, too. Given any SAT formula F, you could just check if (not F) is the same problem as the trivial formula (true). If (not F) is equivalent to (true), F is unsatisfiable and otherwise F is satisfiable. Tobi