1
$\begingroup$

Consider the following two snipets of code:

If a >= 5:
   If b == 0:
     ....
   Else:
     ....
Else if a <= 5:
   ....

If a > 5:
   ....
Else If a >= 5 and b == 0:
   ....
Else If a >= 5:
   ....

Then these two constructs are logically equivalent. I am interested if there algorithms that detects if two or more constructs are the same. Papers in this field are also welcome.

$\endgroup$
  • $\begingroup$ Logically equivalent? They are not. Any algorithm detecting they are the same is absolutely broken. $\endgroup$ – gnasher729 Jan 20 '18 at 13:58
  • $\begingroup$ The first condition in the second snippet should be $a<5$. $\endgroup$ – Yuval Filmus Feb 19 '18 at 19:33
1
$\begingroup$

Practically speaking, you can use an SMT solver for LIA (linear integer arithmetic) or its modular version to check whether two codeblocks are reachable under exactly the same circumstances. LIA only allows linear inequalities. Indeed, if you allow polynomials then the general (non-moudlar) problem becomes undecidable, though real-life integer arithmetic is bounded and so decidable.

As a pointer to the (extensive) literature, you can check this recent paper.

$\endgroup$
1
$\begingroup$

(Here, I am assuming that the statements are taken from a Turing-equivalent programming language, since this is the common case in practice.)

In the general case, we know this is not feasible. That is, we know that there exists no algorithm (not even an inefficient one!) that, given two statements, can always output whether they are equivalent.

This is one of the standard results that can be proved using computability theory. A short proof is that, if $equiv(s_1,s_2)$ were decidable, then we can choose any statement $s_{\sf fixed}$ and obtain that the set $A = \{\langle s1 \rangle \ | \ equiv(s_1,s_{\sf fixed}\}$ is decidable. Indeed, to decide that, we can simply use a decider for $equiv(-,-)$ fixing its second argument to $s_{\sf fixed}$. However, Rice's theorem proves that $A$ is not decidable.

This can also proved without Rice, e.g. using the fact that the halting problem is not decidable, and constructing a suitable reduction.

$\endgroup$
0
$\begingroup$

In this case, it would be quite simple: There are three relevant cases for a: a > 5, a = 5, a < 5. And two relevant cases for b: b = 0, b ≠ 0. Let's call the first three cases A, B and C, and the other two cases 1 and 2.

In your first example, the three statements are executed in cases A1 and B1, A2 and B2, C1 and C2. In your second example, the tree statements are executed in cases A1 and A2, B1, and the third one in case B2. Nothing is executed in case C1 and C2.

So obviously they are not equivalent. You might find some other conditions that turn out to be equivalent.

$\endgroup$

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.