How do you check if two algorithms return the same result for any input? - Computer Science Stack Exchange most recent 30 from cs.stackexchange.com 2019-11-11T22:45:14Z https://cs.stackexchange.com/feeds/question/2059 https://creativecommons.org/licenses/by-sa/4.0/rdf https://cs.stackexchange.com/q/2059 17 How do you check if two algorithms return the same result for any input? Andres Riofrio https://cs.stackexchange.com/users/1638 2012-05-25T00:03:21Z 2012-05-25T20:16:22Z <p>How do you check if two algorithms (say, Merge sort and Naïve sort) return the same result for any input, when the set of all inputs is infinite?</p> <p><strong>Update:</strong> Thank you <a href="https://cs.stackexchange.com/a/2062/1638">Ben</a> for describing how this is impossible to do algorithmically in the general case. <a href="https://cs.stackexchange.com/a/2063/1638">Dave's answer</a> is a great summary of both algorithmic and manual (subject to human wit and metaphor) methods that don't always work, but are quite effective.</p> https://cs.stackexchange.com/questions/2059/-/2060#2060 1 Answer by Yuval Filmus for How do you check if two algorithms return the same result for any input? Yuval Filmus https://cs.stackexchange.com/users/683 2012-05-25T00:36:04Z 2012-05-25T10:04:58Z <p>It is impossible to devise an algorithm that does prove this equality in general. Hint: reduction from the Halting problem.</p> https://cs.stackexchange.com/questions/2059/-/2061#2061 2 Answer by James Koppel for How do you check if two algorithms return the same result for any input? James Koppel https://cs.stackexchange.com/users/1640 2012-05-25T01:27:25Z 2012-05-25T01:27:25Z <p>It's impossible in general, but many constraints can make it possible. For example, you can check the equivalence of two straight-line code programs using BDDs. Symbolic execution can handle many other cases.</p> https://cs.stackexchange.com/questions/2059/-/2062#2062 10 Answer by Ben for How do you check if two algorithms return the same result for any input? Ben https://cs.stackexchange.com/users/116 2012-05-25T02:38:52Z 2012-05-25T04:36:18Z <p>To elaborate slightly on the "it's impossible" statements, here's a simple proof sketch.</p> <p>We can model algorithms with output by Turing Machines which halt with their output on their tape. If you want to have machines that can halt by either accepting with output on their tape or rejecting (in which case there's no output) you can easily come up with an encoding that allows you to model these machines with the "halt or halt not, there is no reject" machines.</p> <p>Now, assume I have an algorithm <strong>P</strong> for determining whether two such TMs have the same output for every input. Then, given a TM <strong>A</strong> and an input <strong>X</strong>, I can construct a new TM <strong>B</strong> that operates as follows:</p> <ol> <li>Check whether the input is exactly <strong>X</strong></li> <li>If yes, then enter an infinite loop</li> <li>If no, then run <strong>A</strong> on the input</li> </ol> <p>Now I can run <strong>P</strong> on <strong>A</strong> and <strong>B</strong>. <strong>B</strong> does not halt on <strong>X</strong>, but has the same output as <strong>A</strong> for all other input, so if and only if <strong>A</strong> doesn't halt on <strong>X</strong> then these two algorithms have the same output for every input. But <strong>P</strong> was assumed to be able to tell whether two algorithms have the same output for every input, so if we had <strong>P</strong> we could tell whether an arbitrary machine halts on an arbitrary input, which is the Halting Problem. Since the Halting Problem is known to be undecidable, <strong>P</strong> cannot exist.</p> <p>This means there is no general (computable) approach to determining whether two algorithms have the same output that always works, so you have to apply reasoning particular to the pair of algorithms you're analysing. However in practice there may be computable approaches that work for large classes of algorithms, and there are certainly techniques you can use to try to work out a proof for any particular case. Dave Clarke's answer gives you some relevant things to look at here. The "impossibility" result only applies to devising a generic method that will solve the problem once and for all, for all pairs of algorithms.</p> https://cs.stackexchange.com/questions/2059/-/2063#2063 16 Answer by Dave Clarke for How do you check if two algorithms return the same result for any input? Dave Clarke https://cs.stackexchange.com/users/31 2012-05-25T02:54:03Z 2012-05-25T04:10:21Z <p>In contrast to what the nay-sayers say, there are many effective techniques for doing this.</p> <ul> <li><p>Bisimulation is one approach. See for example, Gordon's paper on <a href="http://research.microsoft.com/pubs/68298/fp94.ps.gz">Coinduction and Functional Programming</a>.</p></li> <li><p>Another approach is to use operational theories of program equivalence, such as the work of <a href="http://www.cs.tau.ac.il/~nachumd/formal/exam/pitts.pdf">Pitts</a>.</p></li> <li><p>A third approach is to <a href="http://en.wikipedia.org/wiki/Formal_verification">verify</a> that both programs satisfy the same functional specification. There are thousands of papers on this approach.</p></li> <li><p>A fourth approach is to show that one program can be rewritten into the other using sound <a href="http://www.program-transformation.org/">program transformations</a>.</p></li> </ul> <p>Of course none of these methods is complete due undecidability, but volumes and volumes of work has been produced to address the problem.</p>