Re: Synopsis 3: quick junction question

[Damian Conway]

Sean O'Rourke wrote:

S3 says:

    1|2 + 3&4;                              # (4|5) & (5|6) 

but shouldn't that equal

      (1 + (3&4)) | (2 + (3&4))
    = (4&5) | (5&6)
    = (4|6) & 5                             # ???
No, it shouldn't.

You should read:

        1|2 + 3&4

as:

        "Is there a number that you can get by adding either 1 or 2
         to *both* 3 and 4?"
And there is: if you add 2 to 3 *and* 1 to 4, both ways you get 5.
And there's no other combination of 1 or 2 that you can add to both
3 and 4 and get the same number both ways.
So 1|2 + 3&4 has to equal 5. And only CNF semantics achieve that.
Which is why CNF is what junctions use.
Let's take another example (mainly because it's sometimes easier to see the 
necessity of CNF when talking about comparisons). Suppose we had written:

        1|4 == 1&4

So we're asking if the lhs expression is simultaneously equal to 1 and 4.
Which it is. The lhs can be 1, so its equal to 1. But at the same time it can 
also be 4, so it's equal to 4. So it's simultaneously equal to 1 and 4. So the 
comparison is true.

And, under CNF semantics, that's what we get:

       1|4 == 1&4
     = ((1|4) == 1) & ((1|4) == 4))
     = (1|0) & (0|1)
     = 1
But, under DNF semantics that would be:

       1|4 == 1&4
     = (1 == (1&4)) | (4 == (1&4))
     = (1&0) | (0&1)
     = 0
Which is wrong.

Which, again, is why we use CNF.

Damian