Computer Science Stack Exchange is a question and answer site for students, researchers and practitioners of computer science. It only takes a minute to sign up.
Sign up to join this community
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?
Update: Thank you Ben for describing how this is impossible to do algorithmically in the general case. Dave's answer 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.
In contrast to what the nay-sayers say, there are many effective techniques for doing this.
Bisimulation is one approach. See for example, Gordon's paper on Coinduction and Functional Programming.
Another approach is to use operational theories of program equivalence, such as the work of Pitts.
A third approach is to verify that both programs satisfy the same functional specification. There are thousands of papers on this approach.
A fourth approach is to show that one program can be rewritten into the other using sound program transformations.
Of course none of these methods is complete due undecidability, but volumes and volumes of work has been produced to address the problem.
To elaborate slightly on the "it's impossible" statements, here's a simple proof sketch.
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.
Now, assume I have an algorithm P for determining whether two such TMs have the same output for every input. Then, given a TM A and an input X, I can construct a new TM B that operates as follows:
Now I can run P on A and B. B does not halt on X, but has the same output as A for all other input, so if and only if A doesn't halt on X then these two algorithms have the same output for every input. But P was assumed to be able to tell whether two algorithms have the same output for every input, so if we had P 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, P cannot exist.
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.
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.
It is impossible to devise an algorithm that does prove this equality in general. Hint: reduction from the Halting problem.
