views:

87

answers:

1

Hi, I'm writing a compiler for a dataflow programming language I have designed. One of the features that I really like about it is that you can express the following:

x <- a + 1 if b > 3;

x <- a - 1 if b <= 3;

Which implies something like:

x <- a - 1 + 2*(b>3);

In order to pull this off though the compiler needs to know that:

((b > 3) && (b <= 3)) = false

((b > 3) || (b <= 3)) = true

Are there any C/C++ libraries that anyone knows of that would be able to validate these 2 statements (as well as much more complicated ones)? Or are there any papers available via the web that anyone knows of that detail a similar system? Or could someone describe a possible approach?

Thanks,

Daniel

+3  A: 

I think you need a small set of simple rules that tell you whether two expressions are equal, or are totally different.

Let's start with the easiest ones: b>3 and b<=3

Checking whether they're equal is easy: b>3 and b>3 are equal, b>3 and b<=3 clearly aren't.

To see whether they are completely different, we would have to compare b>3 and NOT (b<=3). By simply adding the NOT in front of it, we changed the "distinct" to an "equal" comparison.

Your software should now have the logic to transform NOT (b<=3) to (b>3). And since these are completely equal, the original ones are completely distinct.

If the comparisons are more difficult, you should start to use Morgans Law. This law states that the following expressions are equal:

NOT (A AND B) is equal to NOT A OR NOT B
NOT (A OR B) is equal to NOT A AND NOT B

Now combine both rules:

  • Put NOT in front of one of the expressions
  • Distribute NOT to the most elemental parts of the expression using Morgans law.
  • Then compare all the elements

e.g. suppose we want to know if the following expressions are completely distinct:

(a<3) and not (b>=7)
(b>=7) or (a>=3)

First put a big NOT before the second one:

NOT ((b>=7) or (a>=3))

Then distribute the NOT:

(NOT (b>=7)) and (NOT (a>=3))

Now remove the NOTS from both expressions using the first rule:

(a<3) and (b<7)
(b<7) and (a<3)

Then find the same elements between the two expressions. In this case all the elements from the first expression can be found in the second one and vice versa. This means that the original expressions are completely distinct.

Patrick
I suppose an alternative to manipulating the graph of each expression is to enumerate the truth-table for each expression, and compare them.
Oli Charlesworth
@Oli, that would require you to have explicit values for a and b. What the OP was asking how you could compare this without having actual values.
Patrick
@Oli producing a truth table may work in some circumstances, but there are expressions that could produce an intractably large table.
dan_waterworth
@Patrick: You could do it in terms of the raw predicates (e.g. `(a < 3)`). It doesn't matter what `a` is, simply that `(a < 3)` can be `true` or `false`. @dan: yes, you're probably right.
Oli Charlesworth
@dan: However, the truth-table size is the same as the number of possible permutations of the logic graph that Patrick is suggesting...
Oli Charlesworth
@oli, Patrick's method produce nodes proportionally to the number of variables roughly. Your table would be exponentially bigger, also I plan to include other types of expression like modulo arithmetic and even string operations, so having an extensible framework is important. On balance, Patrick's suggestion is best.
dan_waterworth
@dan: Agreed, Patrick's graph is proportional to the # variables. However, I don't believe it's trivial to find a deterministic set of rules (in the general case) that allows two Boolean expressions to be compared for identity (as Patrick's method requires), based on hazy recollection of digital logic lectures. If I'm right about that, then you may end up having to enumerate all potential applications of de Morgan's rule, etc. to the graph. Obviously, if I'm wrong, then Patrick's method is certainly better.
Oli Charlesworth
@dan: Actually, I take that back. So long as you can reduce each expression to a consistent form, like sum-of-products in a consistent set of basic predicates, then Patrick's method should work. Presumably it gets more complicated if your expression contains non-complementary predicates (e.g. `(b < 3)`, `(b >= 3)` *and* `(b > 3)`).
Oli Charlesworth
You have to make sure you cover every edge case. If for example you have (b > 3) and (b >= 3), a rule that says that all constraints that are sub-constraints of another are removed would deal with that. There are certainly lots of cases to cover, but it's not impossible.
dan_waterworth