16
$\begingroup$

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.

$\endgroup$

migrated from cstheory.stackexchange.com May 25 '12 at 0:43

This question came from our site for theoretical computer scientists and researchers in related fields.

  • 5
    $\begingroup$ as yuval said, there is no procedure that can determine that for any two programs. but in a special case like your example you can prove it: for example if you prove that both your algorithms return a sorted sequence and are stable, you will be done. $\endgroup$ – Sasho Nikolov May 25 '12 at 0:41
  • 1
    $\begingroup$ Do you want an automatic technique/algorithm or a set of manual techniques? $\endgroup$ – Dave Clarke May 25 '12 at 3:55
  • $\begingroup$ @SashoNikolov, if performance is considered a part of output you'd also have to show they both operate in the same time/space complexity. $\endgroup$ – edA-qa mort-ora-y May 25 '12 at 5:23
  • 1
    $\begingroup$ Do you mean "check" or prove? Do mean "any input" or all inputs? What is the motivation and context for the question? $\endgroup$ – Kaveh May 25 '12 at 14:19
  • 2
    $\begingroup$ @AndresRiorio: Proof techniques are different from algorithms that solve the general problem. For example, the halting problem is undecidable but it is certainly possible to prove termination of many programs (by hand or automated heuristics). $\endgroup$ – Raphael May 25 '12 at 20:53
16
$\begingroup$

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.

$\endgroup$
  • $\begingroup$ heu·ris·tic. [Gr. εὑρίσκω "discover"] n. 1. A technique designed to solve a problem that ignores whether the solution can be proven to be correct, but which usually produces a good solution or solves a simpler problem that contains or intersects with the solution of the more complex problem. 2. (Theor.) An algorithm that doesn't work. $\endgroup$ – JeffE May 25 '12 at 4:27
  • 1
    $\begingroup$ Bart Simpson: "Can't win. Don't try." $\endgroup$ – Dave Clarke May 25 '12 at 6:15
  • 9
    $\begingroup$ @JeffE: If you want to check if two algorithms return the same result, you do a proof. There are plenty of good techniques for doing this. Sure, all the methods are incomplete, but who cares? Goedel's incompleteness theorem is not a reason to give up on mathematics! $\endgroup$ – Neel Krishnaswami May 25 '12 at 13:49
  • 3
    $\begingroup$ @JeffE Just because there is no computable function for determining whether two arbitrary algorithms return the same result doesn't mean that you can't answer the question for any two particular algorithms, especially as the process of searching for a proof is not a computable function. Similarly there are loads of papers that prove guaranteed termination for particular algorithms, irrespective of the fact that it's not possible to mechanically determined whether an arbitrary algorithm will always terminate. $\endgroup$ – Ben May 25 '12 at 15:56
  • 2
    $\begingroup$ In practice two algorithms that are supposed to compute the same function hardly ever allow for a bisimulation-based proof of equivalence. (In case of the above-mentioned sorting algorithms, the intermediate stages of the loops/recursion are different.) I'd say using good old Hoare-logic to show that they both implement the same specification of I/O behaviour is the way to go. $\endgroup$ – Kai May 26 '12 at 11:32
10
$\begingroup$

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:

  1. Check whether the input is exactly X
  2. If yes, then enter an infinite loop
  3. If no, then run A on the input

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.

$\endgroup$
  • $\begingroup$ Maybe my $P$ only works for sorting algorithms. (provocative question) $\endgroup$ – Raphael May 25 '12 at 10:10
  • $\begingroup$ @Raphael Yes, the argument I sketched says nothing about such a restricted P, only that a fully general one cannot exist. My instinct is that the halting problem is still undecidable even when you restrict it to "sorting algorithms" rather than general algorithms, in which case the impossibility proof still holds, though I've never heard such a claim. $\endgroup$ – Ben May 25 '12 at 15:43
  • 2
    $\begingroup$ More generally, Rice's theorem states that there is no computable way to prove something about an algorithm, as soon as there is at least one algorithm that has the property you're trying to prove and at least one that doesn't. For example, given an algorithm A, there is no computable function that takes an algorithm B as input and tests whether B is equivalent to A. $\endgroup$ – Gilles May 25 '12 at 23:06
  • $\begingroup$ It's important to note that Rice's theorem applies only to properties of languages, not of Turing Machines (when you're using those as your model of "algorithm"). If it's possible for two Turing Machines to exist that both recognise the same language but one has the property and the other doesn't, then Rice's theorem doesn't apply, and there might be a general computable method for testing the property. But Rice's theorem clearly applies to this case, yes. $\endgroup$ – Ben May 26 '12 at 1:33
2
$\begingroup$

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.

$\endgroup$
1
$\begingroup$

It is impossible to devise an algorithm that does prove this equality in general. Hint: reduction from the Halting problem.

$\endgroup$
  • $\begingroup$ Many techniques exist, though none are fully automatic. $\endgroup$ – Dave Clarke May 25 '12 at 2:56
  • $\begingroup$ I don't know is possible or not, by your answer is just a comment. not an answer. $\endgroup$ – user742 May 25 '12 at 5:53
  • $\begingroup$ @SaeedAmiri: I fleshed to context of the answer out a bit; I think it is complete enough, if maybe not particularly good. $\endgroup$ – Raphael May 25 '12 at 10:11
  • $\begingroup$ @Raphael, The reduction which is in Yuval mind is obvious, and I don't think OP is not aware of that, but IMO hard problem is finding some way for special cases, So this obvious reduction could be a comment to just reminding OP for general case. $\endgroup$ – user742 May 25 '12 at 10:16
  • 2
    $\begingroup$ @SaeedAmiri: That's for the OP and voters to decide then, not us. $\endgroup$ – Raphael May 25 '12 at 10:18

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.