<p>The actual field you seem to be talking about is <em>formal methods</em>, and in particular, <em>formal semantics</em> of programming languages. The particular programming language you have (the machine language of the processor) seems to be without recursion and with some global state involved. This kind of <em>effectful</em> semantics has been well investigated in various forms and approaches.</p>

<p>The fields involved have developed so much that a full overview is out of the question. Also, these not only contain results, but tools employed to attack the difficulties inherent in establishing eqivalences. I will try to mentionsome keywords and topics.</p>

<p>One famous approach is that of <em>axiomatic semantics</em>. In this approach one interleaves the program with formulae from a prespecified logic, used to reason about the language. For example, in your case this logic might encode statements about the state of the processor's registers: $\exists n: r_1 =n \wedge r_2 &gt;n^2+n-5$. These combine to form a logic (rigorous reasoning system), where statements have the form $\{\phi\}C\{\psi\}$. $\phi$ is a formula in this logic representing a <em>precondition</em> known about the state of the world prior to the execution of the program phrase $C$. $\psi$ is a formula representing the <em>postcondition</em>, guaranteed to be valid in state of the world (under the assumption that the precondition held).</p>

<p>The semantics is then given axiomatically as a collection of pre/post-conditions and inference rules. For instance, the semantics of register addition may look like this:
$\{r_1 = n \wedge r_2 = m\} {\rm addi\ r3,r1,r2}\{r_3=m+n\}$. The inference rules may include rules for using intermediate formulae to compose smaller phrases into larger ones. </p>

<p>So in your case, you will need to show that for all preconditions and postconditions, the statement $\{\phi\}B_1\{\psi\}$ is valid iff $\{\phi\}B_2\{\psi\}$ is valid. There are several such systems, applied academically and industrially. The keywords are Hoare logic, separation logic, invariants.</p>

<p>Another approach is <em>operational semantics</em>. In this approach the meaning is given by an implementation of the language. It is desirable to give an abstract implementation, so that rigorous reasoning is possible. Nowadays it is also reasonable to expect this semantics to be <em>structural</em>: the operation of the machine is directed by the structure of the languages syntax, and the meaning of a composite program is given by the meaning of its components. </p>

<p>The implementation is commonly given as a transition system, where each state is a configuration containing the current program phrase that awaits execution. Some keywords and tools that are useful for your problem: structural operational semantics, structural induction, small-step and big-step semantics, observational equivalence, contextual equivalence.</p>

<p>A third approach is <em>denotational semantics</em>. In this, the meaning of a program phrase is given by a mathematical function of its components. This semantics tends to give a <em>global</em> understanding of the mathematical  structure of the semantics. As a consequence, their presentation is a lot less elementary, and tend to lag behind the other approaches. On the other hand, this global understanding may give rise to deep insights about the behaviour and structure of the language. Some keywords: domain theory, category theory, monads, call-by-push-value.</p>

<p>The bottom line is that program equivalence has been investigated quite a lot.  It is one of the most fundamental questions in semantics. In your case, determining algorithmically and tractably whether two such computations are equivalent will probably involve tools from <em>model checking</em>.  Indeed, if you have $n$ registers of $k$ bits then the state-space has at least $n2^k$ points. An exhaustive search of this space is then $\Omega(n2^km)$ where $k$ is the length of the program. Of course, it might even be much worse than this.  So I guess you'll need to employ some non-trivial reasoning to establish such equivalences. Some keywords: the state-space explosion, abstract and symbolic interpretation, normalization by evaluation.</p>

<p>Some places to start looking at things. The Handbook of Theoretical Computer Science (Volume B) has some chapters covering various topics in semantics (Chapters 7, 9, 11, 12, 15 and 19). By now these topics are taught to undergraduates in various universities, they usually concentrate on operational and axiomatic semantics (as they are more elementary).  There is a <a href="https://cstheory.stackexchange.com/questions/3670/formal-semantics-of-programming-languages/3674#3674">related question about that here at TCS@SE</a>.</p>

<p>I'm sorry for speaking in such broad terms, but the body of knowledge and tools underlying this problem is quite extensive. I hope that I at least given you somewhere to start looking!</p>

<p>It is a pet peeve of mine that the formal semantics community, who explores these  questions inherent to compiler theory, have drifted apart from the compiler community. This is not entirely the semantics' community fault: first, as usual in TCS, a big body of theory needs to be developed before a substantial application is possible. Also, Moore's law and other advances in computer science allowed compiler writers to concentrate on other problems, and dismiss formal semantics as abstract nonsense. Another observation I heard from Paul Levy is that people from outside the community take interest because of the usefulness of the problems, and then become so fascinated with the theory that they join the community.</p>

<p>Finally, i'll mention that the gap is closing. There are researchers around the world from both communities that take interest in each other and in closing the gap. A few local names in the semantics world: Nick Benton, Gordon Plotkin, Peter Sewell.</p>

CC BY-SA 3.0
2011-08-29T20:50:11.593Z
if it's true what you've wrote, that semantics community is not joining their efforts with compiler community - is a big shame that this happened... If someone knows examples of such cooperation, please make new answer.
Grzegorz Wierzowiecki
CC BY-SA 3.0
2011-08-29T20:51:04.883Z
Good, you've mentioned *model checking*. So far I mostly tried to apply some methods used for propositional and predicate calculus, automated theorem proving (resolution, etc). But still curious about more. :)
Grzegorz Wierzowiecki
CC BY-SA 3.0
2011-08-29T20:52:36.813Z
You've said it can be done in $O(n2^k)$ time, and mentioned about need of "non-trivial reasoning". That's what I'm looking for. I'd love to see how already people tried to deal with problem (approaches, heuristics - maybe approximations), and investigate it.
Grzegorz Wierzowiecki
CC BY-SA 3.0
2011-08-29T20:52:59.730Z
You've mentioned "well investigated in various forms and approaches" - I would love to see references to read (or watched if video).
Grzegorz Wierzowiecki
CC BY-SA 3.0
2011-08-29T20:53:09.187Z
Thank you @Ohad-Kammar. You've gave a great answer. Such answers I'm looking for. I'd like to investigate topic, and learn more about it. Broad terms are completely ok, I feel only lack of references to papers,books,algorithms.
Grzegorz Wierzowiecki
CC BY-SA 3.0
2011-08-29T23:55:41.353Z
I think I address now these comments in the text. Feel free to replace them with new ones. I'll see whether I can think of good references, but they are more in the form of textbooks than single papers and results!
Ohad Kammar
CC BY-SA 3.0
2011-08-30T12:20:45.827Z
Books are very good to me :). In free moment, I'll read carefully what you've wrote, if something will come to my mind I'll write. Thanks for all details, so far :).
Grzegorz Wierzowiecki
CC BY-SA 3.0
2011-08-29T19:01:11.363Z
2011-08-30T08:52:30.433Z
2017-04-13T12:32:28.080Z
Ohad Kammar
<p>The problem as you state it is extremely general and has been around in some form since the early days of computer science. For example, language equivalence of various kinds of machines is a kind of equivalence of computational devices. </p>

<p>That said, your question indicates you are interested in the equivalence of imperative programs. There are several ways and approaches to do this. One specific application of such work is to prove the correctness of compiler optimizations. Translation validation is another technical term you may want to look up. </p>

<p>The equivalence of two programs is a semantic property.  It is difficult to check directly. A core idea behind many techniques is to find a structural property of programs (or the transition graphs they generate) that is easier to check and implies equivalence. For example, one may use bisimulation, simulation or related notions in a proof. The challenge is to lift these ideas from transition systems to the program text. Here are a few recent proposals in this area.</p>

<ol>
<li><a href="http://cseweb.ucsd.edu/~lerner/papers/pldi09-pec.html" rel="nofollow">Proving Optimizations Correct using Parameterized Program Equivalence</a>, Sudipta Kundu, Zachary Tatlock, and Sorin Lerner , PLDI 2009</li>
<li><a href="http://www.informatik.uni-trier.de/~ley/db/indices/a-tree/l/Leroy%3aXavier.html" rel="nofollow">A Formally Verified Compiler Back-end</a>, Xavier Leroy, Journal of Automated Reasoning 2008.</li>
<li><a href="http://dl.acm.org/citation.cfm?id=349314" rel="nofollow">Translation validation for an optimizing compiler</a>, George Necula, PLDI 2000</li>
<li><a href="http://webcourse.cs.technion.ac.il/236803/Spring2006/ho/WCFiles/pnueli98translation-validation.pdf" rel="nofollow">Translation Validation</a>, A. Pnueli ,  M. Siegel ,  F. Singerman , TACAS 1998.</li>
</ol>

<p>There is much more. I am not an expert. I believe the third paper was an important position statement. The work of Xavier Leroy and Sorin Lerner would give you pointers to two different but very current approaches. </p>

CC BY-SA 3.0
2011-08-29T23:47:30.367Z
2011-08-29T23:47:30.367Z
Vijay D
<h2>My questions:</h2>

<ul>
<li>What are other names for this and similar problems and their fields? ("equivalence of varieties in universal algebra", "equivalence of algebraic structures", "rewriting systems for searching equivalence"?)</li>
<li>what algorithms do you know solving this kind of problems?</li>
<li>What papers/books do you recommend?</li>
</ul>

<h2>Problem</h2>

<p>I'm interested in approaches of finding, whether two computations are equivalent?</p>

<p>I try to find my way between rewriting systems, automated theorem proving, logic programming, <a href="http://en.wikipedia.org/wiki/Variety_(universal_algebra)" rel="nofollow noreferrer">varieties</a>, or just visiting graph of all possible basic block transformations (in order to find corresponding vertices (with some luck ;) ) ).</p>

<p>Of course. In finite domains, I could enumerate all possible inputs for all possible symbols permutations, check whether computations gives same results, and do this in finite time. I am looking for other approaches.</p>

<h3>Computations</h3>

<p>Computations are given as <a href="http://en.wikipedia.org/wiki/Control_flow_graph" rel="nofollow noreferrer">basic blocks</a> represented in <a href="http://en.wikipedia.org/wiki/Static_single_assignment_form" rel="nofollow noreferrer">SSA - static single assignment form</a>. We can assume finite number integer arithmetic (for example 64bit numbers). Computations run in RAM model.</p>

<p>For those not familiar with compilers theory and design, <em>Basic Block has no jumps, no loops, no function call, one exit, and one entry</em> etc. So we can say, that each execution of BB has O(1) complexity.</p>

<p><a href="http://en.wikipedia.org/wiki/Static_single_assignment_form" rel="nofollow noreferrer">SSA - static single assignment form</a> of <a href="http://en.wikipedia.org/wiki/Control_flow_graph" rel="nofollow noreferrer">basic block</a> is <a href="http://en.wikipedia.org/wiki/Directed_acyclic_graph" rel="nofollow noreferrer">DAG (Direct Acyclic Graph)</a>. In that sense, there is <a href="https://cstheory.stackexchange.com/questions/6842/questions-on-unification-theory-and-its-application-to-dag-isomorphism">similar question on TCS.SE about unification theory and DAG isomorphism</a>, while my context, focus, purpose and approach is different.</p>

<h3>Equivalence</h3>

<p>Let me be more specific what I mean by <em>equivalence of computations</em>. Let's take following setup:</p>

<ul>
<li>two computations $f$ and $g$ and treat them as functions.</li>
<li>$P$ is a vector of $f$'s parameters $p_1, p_2, \ldots, p_n$</li>
<li>$P' = \operatorname{perm}(P)$ is permutation of parameters.</li>
</ul>

<p>By equivalence, I mean, there exist permutation $P'$ that for any inputs $P$ , we have $f(P) = g(P')$ same (vector of) results in both computations.</p>

<h3>Another equivalence definition</h3>

<p>I've just found, definition of basic block equivalence, very similar to mine. I hope it might clarify, what I mean by that.</p>

<p>Let me cite from <a href="http://decompilation.info/wp-content/uploads/2011/03/iwpu09.pdf" rel="nofollow noreferrer">C Decompilation: Is It Possible? by Katerina Troshina, Alexander Chernov and Yegor Derevenets</a>:</p>

<blockquote>
  <p>Let $f$ be an object renaming transformation (...) $f(C_1) = C_2$ if there exists a renaming of named objects such as registers, labels, etc, preserving program semantics and making the programs $f(C_1)$ and $C_2$ syntactically indistinguishable. Existence of such an f transformation is a sufficient condition of program equivalence. (...) Equivalence of basic blocks may be checked by reducing them to a RISC-like representation. Let $h$ be a basic block reduction transformation. Let $B_1$ and $B_2$ be basic blocks, let $B'_1 = h(B_1)$ and $B'_2 = h(B_2)$ be the corresponding basic blocks in the RISC-like representation. Let $g$ be an instruction reordering transformation preserving the program semantics. If for the basic blocks $B_1$ and $B_2$ there exist transformations $f$ , $g$ and $h$ making $g(f(h(B_1))$ and $h(B_2)$ syntactically indistinguishable, basic blocks $B_1$ and $B_2$ are equivalent.</p>
</blockquote>

<p>Although, their approach is more focused on assembly code, my approach is more in direction of path-algebra for algorithm pattern matching. What it implies, I'd like to take into account, not only instruction reordering, but equations they represent as well. (Simple example : $(a + b) / 2$ is different to $a / 2 + b / 2$ on $k$-bits integer computations - <a href="http://en.wikipedia.org/wiki/Modular_arithmetic" rel="nofollow noreferrer">modular arithmetic</a>. When $a + b \ge 2^k$ results are different. While algorithms, authors/implementators intentions might be the same. That's why I'd like to mix approaches from different fields).</p>

CC BY-SA 3.0
2011-08-28T19:35:11.077Z
I fail to understand the question.  Do you say that a+b and 2*c are equivalent because you can map both a and b to c?
Tsuyoshi Ito
CC BY-SA 3.0
2011-08-28T20:11:39.690Z
Do you mean a bijective mapping when you say “mapping between symbols in X and symbols in Y”?
Tsuyoshi Ito
CC BY-SA 3.0
2011-08-28T20:16:38.943Z
Yes, bijective. Thanks for comment, I've added "bijective" to problem statement.
Grzegorz Wierzowiecki
CC BY-SA 3.0
2011-08-28T20:19:45.803Z
@Grzegorz: do you mean http://en.wikipedia.org/wiki/Rewriting ?  The general problem you seem to be describing would then be related to the word problem and would then be undecidable.
András Salamon
CC BY-SA 3.0
2011-08-28T21:19:52.913Z
@andras-salamon Yes, it includes rewriting systems :). I re-edit problem statement, and update specification.
Grzegorz Wierzowiecki
CC BY-SA 3.0
2011-08-28T22:12:38.180Z
I do not understand the problem at all. What do you mean by 'structures'? What do you mean by 'answer'? What do you mean by 'transformation'? Can you use rigorous mathematical definitions please? Usually an algebraic structure is a carrier set with some operations on it obeying (algebra for a signature). Are you talking about one of these?
Ohad Kammar
CC BY-SA 3.0
2011-08-28T22:51:43.090Z
Thank you for comment's. I've completly re-edited question. I hope it will be clearer now :).
Grzegorz Wierzowiecki
CC BY-SA 3.0
2011-08-29T12:37:02.490Z
(1) You removed the definition of equivalence.  Please do not expect that the reader reads old revisions to understand the question.
Tsuyoshi Ito
CC BY-SA 3.0
2011-08-29T12:38:14.890Z
(2) I do not like a complete rewriting of a question, although this might be a personal taste.
Tsuyoshi Ito
CC BY-SA 3.0
2011-08-29T12:49:03.750Z
Thanks @tsuyoshi-ito for comments. I've added previous version. I hope, now it's ok :).
Grzegorz Wierzowiecki
CC BY-SA 3.0
2011-08-29T13:06:33.957Z
I do not think that just listing the old and the new questions is a solution.  If you want to state both versions, you have to relate the two questions.  But obviously I do not know what you really want to know, and it is you who decides the best way to present your question.
Tsuyoshi Ito
CC BY-SA 3.0
2011-08-29T13:44:08.963Z
What do you think about making new question with this sorter -more concrete - one , and relating to this? Maybe closing this one?
Grzegorz Wierzowiecki
CC BY-SA 3.0
2011-08-29T14:35:15.663Z
In my opinion, you have to make up your mind about how to present your question.  I understand that it is sometimes difficult especially if you have many ways to choose from, but it is important.  Easily giving up one formulation and moving to another seems to me like you posted a problem without thinking about it carefully, and that is why I do not like a complete rewriting.  I do not have a strong opinion about edit vs repost, but keep in mind that usually posting the same question twice is frowned upon.  (more)
Tsuyoshi Ito
CC BY-SA 3.0
2011-08-29T14:37:45.940Z
(cond’d)  I do not know the answer to your question, but I hope that my comments might help you find a better way to pose your question.
Tsuyoshi Ito
CC BY-SA 3.0
2011-08-29T14:49:36.170Z
As far as I know, this is Q&A Wiki ! Wiki is about collaborating. Collaborating, also on forms of questions. If oyu have any suggestions about question, please let me know. As you see I try to satisfy people comments and improve question, also according to your needs. Thanks to your comments, I've found out, what was wrong, that's why I've made new version. I haven't found similar question here, so I couldn't follow any pattern, like question about proof,complexity,papers.
Grzegorz Wierzowiecki
CC BY-SA 3.0
2011-08-29T14:51:45.293Z
Yes, @tsuyoshi-ito , Your answers and other comment authors, helped me a lot in understanding, what to stress out in my question, what to take away. Please, don't mind, I will leave now, a new version, which I've created in collaboration with all of you - Thanks :). It's my second question here, I need practice to adjust customs and habits here in formulation of questions :).
Grzegorz Wierzowiecki
CC BY-SA 3.0
2011-08-29T15:50:44.197Z
1. It is not a Q&A Wiki. 2. This is your question, other cannot guess what you intend to ask. 3. I think the question is not still in a form that it can be answered, please read the FAQ, in particular entries about how to ask a good question. 4. I suggest you check the [this](http://www.youtube.com/watch?v=7XfA5EhH7Bc), it might help you in formulating your question.
Kaveh
CC BY-SA 3.0
2011-08-29T19:28:13.160Z
Thank you @Kaveh for reply, tips and recommended materials (I am watching it - it's great). In mean time I will read again faq, I am afraid I'm missed some differences to stackoverflow. I hope currently question is just not offending this place ;). I'll try to improve it later.
Grzegorz Wierzowiecki
<reference-request><pl.programming-languages><semantics><model-checking><compilers>
Equivalence of two basic blocks
Grzegorz Wierzowiecki
# Equivalence of two basic blocks

(Asked by: username_0 on 2011-08-28)

## My questions:

* What are other names for this and similar problems and their fields? ("equivalence of varieties in universal algebra", "equivalence of algebraic structures", "rewriting systems for searching equivalence"?)
* what algorithms do you know solving this kind of problems?
* What papers/books do you recommend?

## Problem

I'm interested in approaches of finding, whether two computations are equivalent?

I try to find my way between rewriting systems, automated theorem proving, logic programming, [varieties](http://en.wikipedia.org/wiki/Variety_(universal_algebra)), or just visiting graph of all possible basic block transformations (in order to find corresponding vertices (with some luck ;) ) ).

Of course. In finite domains, I could enumerate all possible inputs for all possible symbols permutations, check whether computations gives same results, and do this in finite time. I am looking for other approaches.

### Computations

Computations are given as [basic blocks](http://en.wikipedia.org/wiki/Control_flow_graph) represented in [SSA - static single assignment form](http://en.wikipedia.org/wiki/Static_single_assignment_form). We can assume finite number integer arithmetic (for example 64bit numbers). Computations run in RAM model.

For those not familiar with compilers theory and design, *Basic Block has no jumps, no loops, no function call, one exit, and one entry* etc. So we can say, that each execution of BB has O(1) complexity.

[SSA - static single assignment form](http://en.wikipedia.org/wiki/Static_single_assignment_form) of [basic block](http://en.wikipedia.org/wiki/Control_flow_graph) is [DAG (Direct Acyclic Graph)](http://en.wikipedia.org/wiki/Directed_acyclic_graph). In that sense, there is [similar question on TCS.SE about unification theory and DAG isomorphism](https://cstheory.stackexchange.com/questions/6842/questions-on-unification-theory-and-its-application-to-dag-isomorphism), while my context, focus, purpose and approach is different.

### Equivalence

Let me be more specific what I mean by *equivalence of computations*. Let's take following setup:

* two computations $f$ and $g$ and treat them as functions.
* $P$ is a vector of $f$'s parameters $p\_1, p\_2, \ldots, p\_n$
* $P' = \operatorname{perm}(P)$ is permutation of parameters.

By equivalence, I mean, there exist permutation $P'$ that for any inputs $P$ , we have $f(P) = g(P')$ same (vector of) results in both computations.

### Another equivalence definition

I've just found, definition of basic block equivalence, very similar to mine. I hope it might clarify, what I mean by that.

Let me cite from [C Decompilation: Is It Possible? by Katerina Troshina, Alexander Chernov and Yegor Derevenets](http://decompilation.info/wp-content/uploads/2011/03/iwpu09.pdf):

> Let $f$ be an object renaming transformation (...) $f(C\_1) = C\_2$ if there exists a renaming of named objects such as registers, labels, etc, preserving program semantics and making the programs $f(C\_1)$ and $C\_2$ syntactically indistinguishable. Existence of such an f transformation is a sufficient condition of program equivalence. (...) Equivalence of basic blocks may be checked by reducing them to a RISC-like representation. Let $h$ be a basic block reduction transformation. Let $B\_1$ and $B\_2$ be basic blocks, let $B'\_1 = h(B\_1)$ and $B'\_2 = h(B\_2)$ be the corresponding basic blocks in the RISC-like representation. Let $g$ be an instruction reordering transformation preserving the program semantics. If for the basic blocks $B\_1$ and $B\_2$ there exist transformations $f$ , $g$ and $h$ making $g(f(h(B\_1))$ and $h(B\_2)$ syntactically indistinguishable, basic blocks $B\_1$ and $B\_2$ are equivalent.

Although, their approach is more focused on assembly code, my approach is more in direction of path-algebra for algorithm pattern matching. What it implies, I'd like to take into account, not only instruction reordering, but equations they represent as well. (Simple example : $(a + b) / 2$ is different to $a / 2 + b / 2$ on $k$-bits integer computations - [modular arithmetic](http://en.wikipedia.org/wiki/Modular_arithmetic). When $a + b \ge 2^k$ results are different. While algorithms, authors/implementators intentions might be the same. That's why I'd like to mix approaches from different fields).

**Tags:** reference-request, pl.programming-languages, semantics, model-checking, compilers

> **Comments:**
> **username_1**: I fail to understand the question.  Do you say that a+b and 2*c are equivalent because you can map both a and b to c?  
> **username_1**: Do you mean a bijective mapping when you say “mapping between symbols in X and symbols in Y”?  
> **username_0**: Yes, bijective. Thanks for comment, I've added "bijective" to problem statement.  
> **username_2**: @Grzegorz: do you mean http://en.wikipedia.org/wiki/Rewriting ?  The general problem you seem to be describing would then be related to the word problem and would then be undecidable.  
> **username_0**: @andras-salamon Yes, it includes rewriting systems :). I re-edit problem statement, and update specification.  
> **username_3**: I do not understand the problem at all. What do you mean by 'structures'? What do you mean by 'answer'? What do you mean by 'transformation'? Can you use rigorous mathematical definitions please? Usually an algebraic structure is a carrier set with some operations on it obeying (algebra for a signature). Are you talking about one of these?  
> **username_0**: Thank you for comment's. I've completly re-edited question. I hope it will be clearer now :).  
> **username_1**: (1) You removed the definition of equivalence.  Please do not expect that the reader reads old revisions to understand the question.  
> **username_1**: (2) I do not like a complete rewriting of a question, although this might be a personal taste.  
> **username_0**: Thanks @tsuyoshi-ito for comments. I've added previous version. I hope, now it's ok :).  
> **username_1**: I do not think that just listing the old and the new questions is a solution.  If you want to state both versions, you have to relate the two questions.  But obviously I do not know what you really want to know, and it is you who decides the best way to present your question.  
> **username_0**: What do you think about making new question with this sorter -more concrete - one , and relating to this? Maybe closing this one?  
> **username_1**: In my opinion, you have to make up your mind about how to present your question.  I understand that it is sometimes difficult especially if you have many ways to choose from, but it is important.  Easily giving up one formulation and moving to another seems to me like you posted a problem without thinking about it carefully, and that is why I do not like a complete rewriting.  I do not have a strong opinion about edit vs repost, but keep in mind that usually posting the same question twice is frowned upon.  (more)  
> **username_1**: (cond’d)  I do not know the answer to your question, but I hope that my comments might help you find a better way to pose your question.  
> **username_0**: As far as I know, this is Q&A Wiki ! Wiki is about collaborating. Collaborating, also on forms of questions. If oyu have any suggestions about question, please let me know. As you see I try to satisfy people comments and improve question, also according to your needs. Thanks to your comments, I've found out, what was wrong, that's why I've made new version. I haven't found similar question here, so I couldn't follow any pattern, like question about proof,complexity,papers.  
> **username_0**: Yes, @tsuyoshi-ito , Your answers and other comment authors, helped me a lot in understanding, what to stress out in my question, what to take away. Please, don't mind, I will leave now, a new version, which I've created in collaboration with all of you - Thanks :). It's my second question here, I need practice to adjust customs and habits here in formulation of questions :).  
> **username_4**: 1. It is not a Q&A Wiki. 2. This is your question, other cannot guess what you intend to ask. 3. I think the question is not still in a form that it can be answered, please read the FAQ, in particular entries about how to ask a good question. 4. I suggest you check the [this](http://www.youtube.com/watch?v=7XfA5EhH7Bc), it might help you in formulating your question.  
> **username_0**: Thank you @username_4 for reply, tips and recommended materials (I am watching it - it's great). In mean time I will read again faq, I am afraid I'm missed some differences to stackoverflow. I hope currently question is just not offending this place ;). I'll try to improve it later.  

---

## 2 answers

### Answer by username_3 on 2011-08-29. Score: 10

The actual field you seem to be talking about is *formal methods*, and in particular, *formal semantics* of programming languages. The particular programming language you have (the machine language of the processor) seems to be without recursion and with some global state involved. This kind of *effectful* semantics has been well investigated in various forms and approaches.

The fields involved have developed so much that a full overview is out of the question. Also, these not only contain results, but tools employed to attack the difficulties inherent in establishing eqivalences. I will try to mentionsome keywords and topics.

One famous approach is that of *axiomatic semantics*. In this approach one interleaves the program with formulae from a prespecified logic, used to reason about the language. For example, in your case this logic might encode statements about the state of the processor's registers: $\exists n: r\_1 =n \wedge r\_2 >n^2+n-5$. These combine to form a logic (rigorous reasoning system), where statements have the form $\{\phi\}C\{\psi\}$. $\phi$ is a formula in this logic representing a *precondition* known about the state of the world prior to the execution of the program phrase $C$. $\psi$ is a formula representing the *postcondition*, guaranteed to be valid in state of the world (under the assumption that the precondition held).

The semantics is then given axiomatically as a collection of pre/post-conditions and inference rules. For instance, the semantics of register addition may look like this:
$\{r\_1 = n \wedge r\_2 = m\} {\rm addi\ r3,r1,r2}\{r\_3=m+n\}$. The inference rules may include rules for using intermediate formulae to compose smaller phrases into larger ones.

So in your case, you will need to show that for all preconditions and postconditions, the statement $\{\phi\}B\_1\{\psi\}$ is valid iff $\{\phi\}B\_2\{\psi\}$ is valid. There are several such systems, applied academically and industrially. The keywords are Hoare logic, separation logic, invariants.

Another approach is *operational semantics*. In this approach the meaning is given by an implementation of the language. It is desirable to give an abstract implementation, so that rigorous reasoning is possible. Nowadays it is also reasonable to expect this semantics to be *structural*: the operation of the machine is directed by the structure of the languages syntax, and the meaning of a composite program is given by the meaning of its components.

The implementation is commonly given as a transition system, where each state is a configuration containing the current program phrase that awaits execution. Some keywords and tools that are useful for your problem: structural operational semantics, structural induction, small-step and big-step semantics, observational equivalence, contextual equivalence.

A third approach is *denotational semantics*. In this, the meaning of a program phrase is given by a mathematical function of its components. This semantics tends to give a *global* understanding of the mathematical structure of the semantics. As a consequence, their presentation is a lot less elementary, and tend to lag behind the other approaches. On the other hand, this global understanding may give rise to deep insights about the behaviour and structure of the language. Some keywords: domain theory, category theory, monads, call-by-push-value.

The bottom line is that program equivalence has been investigated quite a lot. It is one of the most fundamental questions in semantics. In your case, determining algorithmically and tractably whether two such computations are equivalent will probably involve tools from *model checking*. Indeed, if you have $n$ registers of $k$ bits then the state-space has at least $n2^k$ points. An exhaustive search of this space is then $\Omega(n2^km)$ where $k$ is the length of the program. Of course, it might even be much worse than this. So I guess you'll need to employ some non-trivial reasoning to establish such equivalences. Some keywords: the state-space explosion, abstract and symbolic interpretation, normalization by evaluation.

Some places to start looking at things. The Handbook of Theoretical Computer Science (Volume B) has some chapters covering various topics in semantics (Chapters 7, 9, 11, 12, 15 and 19). By now these topics are taught to undergraduates in various universities, they usually concentrate on operational and axiomatic semantics (as they are more elementary). There is a [related question about that here at TCS@SE](https://cstheory.stackexchange.com/questions/3670/formal-semantics-of-programming-languages/3674#3674).

I'm sorry for speaking in such broad terms, but the body of knowledge and tools underlying this problem is quite extensive. I hope that I at least given you somewhere to start looking!

It is a pet peeve of mine that the formal semantics community, who explores these questions inherent to compiler theory, have drifted apart from the compiler community. This is not entirely the semantics' community fault: first, as usual in TCS, a big body of theory needs to be developed before a substantial application is possible. Also, Moore's law and other advances in computer science allowed compiler writers to concentrate on other problems, and dismiss formal semantics as abstract nonsense. Another observation I heard from Paul Levy is that people from outside the community take interest because of the usefulness of the problems, and then become so fascinated with the theory that they join the community.

Finally, i'll mention that the gap is closing. There are researchers around the world from both communities that take interest in each other and in closing the gap. A few local names in the semantics world: Nick Benton, Gordon Plotkin, Peter Sewell.

> **Comments:**
> **username_0**: if it's true what you've wrote, that semantics community is not joining their efforts with compiler community - is a big shame that this happened... If someone knows examples of such cooperation, please make new answer.  
> **username_0**: Good, you've mentioned *model checking*. So far I mostly tried to apply some methods used for propositional and predicate calculus, automated theorem proving (resolution, etc). But still curious about more. :)  
> **username_0**: You've said it can be done in $O(n2^k)$ time, and mentioned about need of "non-trivial reasoning". That's what I'm looking for. I'd love to see how already people tried to deal with problem (approaches, heuristics - maybe approximations), and investigate it.  
> **username_0**: You've mentioned "well investigated in various forms and approaches" - I would love to see references to read (or watched if video).  
> **username_0**: Thank you @Ohad-Kammar. You've gave a great answer. Such answers I'm looking for. I'd like to investigate topic, and learn more about it. Broad terms are completely ok, I feel only lack of references to papers,books,algorithms.  
> **username_3**: I think I address now these comments in the text. Feel free to replace them with new ones. I'll see whether I can think of good references, but they are more in the form of textbooks than single papers and results!  
> **username_0**: Books are very good to me :). In free moment, I'll read carefully what you've wrote, if something will come to my mind I'll write. Thanks for all details, so far :).  

---

### Answer by username_5 on 2011-08-29. Score: 6

The problem as you state it is extremely general and has been around in some form since the early days of computer science. For example, language equivalence of various kinds of machines is a kind of equivalence of computational devices.

That said, your question indicates you are interested in the equivalence of imperative programs. There are several ways and approaches to do this. One specific application of such work is to prove the correctness of compiler optimizations. Translation validation is another technical term you may want to look up.

The equivalence of two programs is a semantic property. It is difficult to check directly. A core idea behind many techniques is to find a structural property of programs (or the transition graphs they generate) that is easier to check and implies equivalence. For example, one may use bisimulation, simulation or related notions in a proof. The challenge is to lift these ideas from transition systems to the program text. Here are a few recent proposals in this area.

1. [Proving Optimizations Correct using Parameterized Program Equivalence](http://cseweb.ucsd.edu/~lerner/papers/pldi09-pec.html), Sudipta Kundu, Zachary Tatlock, and Sorin Lerner , PLDI 2009
2. [A Formally Verified Compiler Back-end](http://www.informatik.uni-trier.de/~ley/db/indices/a-tree/l/Leroy%3aXavier.html), Xavier Leroy, Journal of Automated Reasoning 2008.
3. [Translation validation for an optimizing compiler](http://dl.acm.org/citation.cfm?id=349314), George Necula, PLDI 2000
4. [Translation Validation](http://webcourse.cs.technion.ac.il/236803/Spring2006/ho/WCFiles/pnueli98translation-validation.pdf), A. Pnueli , M. Siegel , F. Singerman , TACAS 1998.

There is much more. I am not an expert. I believe the third paper was an important position statement. The work of Xavier Leroy and Sorin Lerner would give you pointers to two different but very current approaches.


---

