16

Q1. When can we say that two programs (written in some programming language like C++) are different?

The first extreme is to say that two programs are equivalent iff they are identical. The other extreme is to say two programs are equivalent iff they compute the same function (or show the same observable behavior in similar environments). But these are not good: not all programs checking primality are the same. We can add a line of code with no effect on the result and we would still consider it the same program.

Q2. Are programs and algorithms the same kind of object? If not, what is the definition of an algorithm and how does it differ from the definition of a program? When can we say two algorithms are equivalent?

Anonymous
  • 4,041
  • 19
  • 43
  • The program isomorphism problem? Can't one ask "is this program isomorphic to the program that always halts?" and recover the Halting Problem? If we restrict ourselves to the Bounded Halting Program Problem isn't this just graph isomorphism? – user834 Dec 13 '11 at 19:53
  • 5
    When are two algorithms the same? http://arxiv.org/abs/0811.0811 – sdcvvc Dec 14 '11 at 01:51
  • 1
    Wouldn't it depend entirely on the context? Getting a bit philosophical here, but a bolted-down chair and an upside-down bolted-down chair are the same thing physically but not the same in terms of the idea of a chair. – Rei Miyasaka Dec 14 '11 at 06:16
  • Slightly off-topic, but, since proofs are programs ... http://gowers.wordpress.com/2007/10/04/when-are-two-proofs-essentially-the-same/ – Radu GRIGore Jan 03 '12 at 13:44
  • theoretically this is basically the question of whether two recursive languages [eg specified by TMs] are equivalent which (as user834 points out) is undecidable. however it is also connected to the field of automated theorem proving and program termination analysis. – vzn Nov 16 '13 at 17:13
  • 1
    The following article is very related. I have only skimmed through it some time ago, but Blass and Gurevic usually write really well (I just don't recall reading anything else by Dershowitz, not saying it usually isn't very readable). http://research.microsoft.com/en-us/um/people/gurevich/Opera/192.pdf WHEN ARE TWO ALGORITHMS THE SAME? ANDREAS BLASS, NACHUM DERSHOWITZ, AND YURI GUREVICH – kasterma Nov 17 '13 at 13:00
  • @kasterma: I have read that paper. – Anonymous Dec 02 '13 at 20:28

3 Answers3

19

Q1: There are many notions of program equivalence (trace equivalence, contextual equivalence, observational equivalence, bisimilarity) which may or may not take into account things such as time, resource usage, nondeterminism, termination. A lot of work has been done on finding usable notions of program equivalence. For example: Operationally-Based Theories of Program Equivalence by Andy Pitts. But this barely scratches the surface. This should be useful even if you are interested in when two programs are not equivalent. One can even reason about non-halting programs (using bisimulation and coinduction).

Q2: One possible answer to part of this question is that interactive programs are not algorithms (assuming that one considers an algorithm to take all of its input at once, but this narrow definition excludes online algorithms). A program could be a collection of interacting processes that also interact with their environment. This certainly doesn't match with the Turing-machine/Recursion theory notion of algorithm.

Dave Clarke
  • 16,666
  • 3
  • 60
  • 106
15

The other extreme is to say two programs are equivalent iff they compute the same function (or show the same observable behavior in similar environments). But these are not good: not all programs checking primality are the same. We can add a line of code with no effect on the result and we would still consider it the same program.

This is not an extreme: program equivalence must be defined relative to a notion of observation.

The most common definition in PL research is contextual equivalence. In contextual equivalence, the idea is that we observe programs by using them as components of larger programs (the context). So if two programs compute the same final value for all contexts, then they are judged to be equal. Since this definition quantifies over all possible program contexts, it is difficult to work with directly. So a typical research program in PL is to find compositional reasoning principles which imply contextual equivalence.

However, this is not the only possible notion of observation. For example, we can easily say that the memory, time, or power behavior of a program is observable. In this case, fewer program equivalences hold, since we can distinguish more programs (eg, mergesort is now distinguishable from quicksort). If you want to (say) design languages immune to timing channel attacks, or to design space-bounded programming languages, then this is the sort of thing you have to do.

Also, we may choose to judge some of the intermediate states of a computation as observable. This always happens for concurrent languages, due to the possibility of interference. But you might want to take this view even for sequential languages --- for example, if you want to ensure that no computations store unencrypted data in main memory, then you have to regard writes to main memory as observable.

Basically, there is no single notion of program equivalence; it is always relative to the notion of observation you pick, and that depends on the application you have in mind.

Neel Krishnaswami
  • 32,528
  • 1
  • 100
  • 165
  • 1
    It's worth pointing out that there is no unique notion of contextual equivalence (or contextual congruence) either, for example if the programming language in question is interactive (i.e. does not yield a value). – Martin Berger Dec 14 '11 at 14:52
  • While the rest of your answer is excellent, I think that I disagree with this: "program equivalence must be defined relative to a notion of observation". That's only true for observational notions of equivalence. $\alpha$-equivalence isn't such a notion, but it's very much a kind of program equivalence. – Sam Tobin-Hochstadt Dec 14 '11 at 15:19
  • @ Sam, that's an interesting comment. One way to rescue observations would be to say that programs are syntax already quotiented by $\alpha$-equivalence. – Martin Berger Dec 15 '11 at 00:10
  • @Sam: only closed terms are ever substituted for variables in the (cbn or cbv) operational semantics of the lambda calculus. The $\alpha$-equivalence relation can then be seen as part of the equational theory of the language, which is justified in terms of soundness with respect to contextual equivalence. IIUC, you only need to take $\alpha$ as a primitive equivalence only when the reduction of open terms happens for real, like in the definitional equality of type theories. – Neel Krishnaswami Dec 15 '11 at 13:04
  • 1
    @NeelKrishnaswami, I think this is just begging the question. $\alpha$ is an equivalence, and there are programming languages where it doesn't respect observational equivalence. See Wand's "The Theory of Fexprs is Trivial". Other times, it's not an equivalence that you can use for optimization, for example if debugging is important. Both of these add observations that violate $\alpha$. – Sam Tobin-Hochstadt Dec 15 '11 at 18:01
  • @SamTobin-Hochstadt, I am not sure what point you are making. If I say two programs are equivalent if they have the same length, it is an equivalence (by the definition of the set-theorist), but a programmer wouldn't bother to call it an equivalence. Are you saying a programmer should care about equivalences even if they are not observational equivalences? – Uday Reddy Mar 01 '12 at 23:57
  • @UdayReddy, yes, I'm saying that equivalences (like $\alpha$) that aren't necessarily related to observation are important. Of course, if we take as the set of observations "all possible things you could ask about a program", then everything falls under observational equivalence, but only by eliminating all equivalences. For example, normally inlining a function call (ie, $\beta$-reduction) is observationally equivalent, but we might care about doing it or not doing it for performance/debugging/security checks/etc. – Sam Tobin-Hochstadt Mar 04 '12 at 17:54
  • @SamTobin-Hochstadt. You haven't defined what you mean by "equivalence" and what equivalences you are labelling as "important equivalences". "Observational equivalence" is at least a defined concept and it makes sense. What you are possibly after is that there is a range of observations that one might subject a program component to, and there is a range of observational equivalences corresponding to such observations. But you need to define what these are if we are to have any understanding of what you are saying. – Uday Reddy Mar 05 '12 at 08:07
  • @UdayReddy By "equivalence", I just mean the usual notion of an equivalence relation on program. Obviously "important" is in the eye of the beholder. Like I said, if we extend our notion of observation to include, for example, examining the timestamp of the source code of the program, then we can express everything in terms of observational equivalence. I think this perspective isn't that useful, though, and it's better to reserve "observational equivalence" for what we usually mean, and talk about other equivalences (such as $\alpha$) when needed. – Sam Tobin-Hochstadt Mar 06 '12 at 01:10
  • @SamTobin-Hochstadt. I don't know what you mean by "usual" notion of equivalence. That is what the original question was about! If there was something called a "usual" notion of equivalence, then the question would have been unnecessary. As far as I am aware, there isn't anything that could be called the "usual" notion. If you know one, define it please! – Uday Reddy Mar 06 '12 at 09:12
  • @UdayReddy, I used "usual" twice in that comment. In the first case, I just meant that the "usual notion of an equivalence relation" is a binary relation that is reflexive, symmetric, and transitive. I think the "usual" meaning of observational equivalence is just that two programs are equivalent iff in all program contexts, they either both converge or both diverge. Obviously that's an equivalence relation on programs, but it's far from the only one. – Sam Tobin-Hochstadt Mar 06 '12 at 22:54
  • 1
    @SamTobin-Hochstadt. Ok, let us forget "usual". The feeling I get is that you are saying the same thing that Neel said, which was quite well-thought out in my opinion. Your idea, which is still vague to me, can be formalized in Neel's framework by picking the right kind of observations and the right kind of program contexts. – Uday Reddy Mar 06 '12 at 23:41
  • 1
    @UdayReddy Consider the $\lambda$-calculus. What context can distinguish $\lambda x.x$ from $\lambda y.y$? None. We could change the language so that we can make this distinction, but then we lost the concept we had before -- observational equivalence in the lambda-calculus is a useful tool. Instead, we should recognize that in the LC, we can't distinguish the terms with in-language observations, even though they're different terms. – Sam Tobin-Hochstadt Mar 09 '12 at 01:35
2

Q2: I think usual theoretical definitions don't really distinguish between algorithms and programs, but "algorithm" as commonly used is more like a class of programs. For me an algorithm is sort of like a program with some subroutines left not fully specified (i.e. their desired behavior is defined but not their implementation). For example, the Gaussian elimination algorithm doesn't really specify how integer multiplication is to be performed.

I am sorry if this is naive. I don't do PL research.

Sasho Nikolov
  • 18,189
  • 2
  • 67
  • 115
  • The idea is probably that there are multiple implementations for those subroutines and you don't care which is chosen as long as it performs according to your specification. – Raphael Dec 15 '11 at 13:05