Added a simplify pattern for XOR that reduces A xor 0 to A.

[jclapis]

This is a small PR that adds a rule regarding XOR to the common simplifier patterns:

X ⊕ 0 = X

Our group encounters this kind of pattern occasionally, so we would like to see this added to the canonical Simplify() method. All of the unit tests pass with this new rule in place, and we have added some unit tests to cover this new behavior.

[WhiteBlackGoose]

In fact, xor is not exactly a numeric operation. It's an operation on booleans, so

a xor false

would get reduced to a, and

a xor true

gets reduced to not a

[jclapis]

That is true for the bitwise operation, certainly. Our group is using AngouriMath for some quantum computing research, so we are using XOR to compare two quantum registers which are usually represented as variables and numbers instead of the bitwise approach. In either case, I just tested it with the following:

        [Fact] public void Xor3() => AssertSimplify(new Entity.Xorf(false, x), x);
        [Fact] public void Xor4() => AssertSimplify(new Entity.Xorf(x, false), x);

The pattern above still passes these tests, but fails the a xor true tests. I will amend this PR with patterns for that in place shortly.

[codecov-commenter]

Codecov Report

Merging #498 (1b3909d) into master (e45a06c) will not change coverage.
The diff coverage is n/a.

❗ Current head 1b3909d differs from pull request most recent head 9e4b6b8. Consider uploading reports for the commit 9e4b6b8 to get more accurate results

@@      Coverage Diff      @@
##   master   #498   +/-   ##
=============================
=============================

---

Continue to review full report at Codecov.

Legend - Click here to learn more
Δ = absolute <relative> (impact), ø = not affected, ? = missing data
Powered by Codecov. Last update e45a06c...9e4b6b8. Read the comment docs.

[WhiteBlackGoose]

You can write it as Xorf(var any1, Boolean(true)) => any1.Not() thanks to pattern matching. But don't those rules in fact already exist? Let me check

[WhiteBlackGoose]

Our group is using AngouriMath for some quantum computing research

Sounds amazing.

[WhiteBlackGoose]

As far as I can see, those patterns are already there, aren't they?

(this is an F# wrapper of the library, but it's powered by the same kernel)

[WhiteBlackGoose]

So here's the thing. The most basic operations (like exclusive or against a constant, or multiplication by 0, or etc.) are covered by inner simplification than by patterns, and it seems to be covered already.

Although now I think that having it in patterns is not a bad idea too 🤔 .

[WhiteBlackGoose]

There's no logic backing xor on numbers, so this pattern is not particularly useful. Or you have some other, broader idea regarding xor? Please, share!

[jclapis]

I'm not sure what you mean about backing logic; are you referring to the solver system? If so, we're just using the symbolic algebra representation and simplification systems so this isn't something we had considered. In quantum notation, you see things like this quite frequently:

That is, some variable XOR'd against some other variable. In some cases one of those variables is simply the integer 0, and that can be simplified to just using the other value. That's the use case this was intended to support.

[WhiteBlackGoose]

Right. What I am saying is that we don't support boolean operators on integers. So if we want to add it, it should be added for all boolean operators and for all cases, not only for a few cases for xor. That's what I mean 😅 . But before doing so, we need to think how it will be designed.

[WhiteBlackGoose]

By the way, maybe you want to join our discord server (see the repo's readme's green badge)? It's a chat, so we can discuss it more conveniently there (and having others potentially involved)

[jclapis]

Sure, I'll hop in tomorrow if you believe there's more to this discussion that what you've mentioned here.

[jclapis]

As far as I can see, those patterns are already there, aren't they?

Probably, I hadn't tested them before because we don't use Boolean as one of the arguments for Xorf. We use Integer, as in this pattern:

X ⊕ 0 = X

This is our sample code:

Entity.Variable n = "n";
Entity.Xorf xor = new Entity.Xorf(n, 0);
xor.Simplify();
Console.WriteLine(xor);

It produces the following:

n xor 0

We would like it to produce n instead of n xor 0. Clearly it works out of the box with Boolean as you have demonstrated, but it doesn't work for Integer. That's what the original incarnation of this PR aimed to add.

[WhiteBlackGoose]

Let's keep this PR open for now, because I'm not sure whether we need it for integers (it doesn't work on integers currently ; to make it work, you would need to implement all logic for boolean operators).

In your case, you can do

Entity ReplaceIntsWithBooleans(Entity expr) => expr.Substitute(0, false).Substitute(1, true);
Entity ReplaceBooleansWithInts(Entity expr) => expr.Substitute(false, 0).Substitute(true, 1);

[Happypig375]

If this were to be added, the xor operator would probably be made to work like a bitwise operator, and other logical operators like and not or implies would also need to be updated.

[Rafael-SOWNet]

Validated against today's master, since this has been open a while. It applies cleanly and the suite is green with it (Failed: 0, Passed: 4467, Skipped: 14, Total: 4481), so nothing here is broken. But the measurement supports what @WhiteBlackGoose said in 2021.

Four of the six rules are already true without the patch. On current master:

	master	with this PR
x xor false	x	x
false xor x	x	x
x xor true	not x	not x
true xor x	not x	not x
x xor 0	0 xor x	x
0 xor x	0 xor x	x

The boolean cases come out of inner simplification, exactly as described above, so those four pattern lines never fire and the four tests asserting them pass on master unchanged. The whole effect of the patch is the last two rows.

And those two are the part worth thinking about. They make xor partly defined on integers: x xor 0 would simplify to x, while 2 xor 0 still does not evaluate and x xor 1 still does nothing. A rule that fires for one integer and not another is the kind of inconsistency #497 names as the thing to design out, and @Happypig375's point is the same one — if xor is to work on integers it should work as a bitwise operator, with and, or, not and implies following.

So the shape of a mergeable change here is bitwise integer logic as a whole, not this one identity. If that is wanted, I am happy to write it; it is a contained piece of work.

@jclapis — for the original use, if the two registers are compared as booleans rather than integers, the four boolean reductions you want are already there today with no patch at all. Worth checking whether that covers you five years on.

No action taken on this PR either way; this is validation, not a verdict.

[Happypig375]

needs an analysis on how mathematicians vs physicians approach this operator.

[Rafael-SOWNet]

@Happypig375 — the analysis you asked for.

The split is not mathematicians vs physicists

Both communities use ⊕ in both senses, and the real dividing line is what the operands are.

On truth values, ⊕ is exclusive disjunction. Propositional logic and Boolean algebra, in both fields.

On numbers, ⊕ is bitwise XOR — addition in GF(2)ⁿ — and mathematicians use it that way constantly:

• Nim and Sprague–Grundy theory. The Grundy value of a sum of games is the bitwise XOR of the parts. Nim with heaps 3, 5, 7 is a first-player win because 3 ⊕ 5 ⊕ 7 = 1 ≠ 0. Conway's nimber addition is this operator, and it is written ⊕.
• Coding theory. Linear codes over GF(2) are built on addition of binary vectors, which is bitwise XOR — syndromes, parity checks, Hamming codes.
• Cryptography. ⊕ on bit strings, everywhere.

And physicists — specifically the field this PR comes from — use exactly the same numeric reading. The CNOT and the standard oracle are written |x⟩|y⟩ ↦ |x⟩|y ⊕ x⟩, where x and y are bit strings. Simon's algorithm is stated as the promise f(x) = f(x ⊕ s); Bernstein–Vazirani and Deutsch–Jozsa are the same shape. @jclapis's registers are bit strings, so ⊕ on them is bitwise, unambiguously and by the textbook.

A third meaning, worth naming because it is arguably the most common in pure mathematics: ⊕ is the direct sum — V ⊕ W of vector spaces, modules, groups, and of Hilbert spaces in physics. Unrelated to either of the above, and a good reason to prefer an unambiguous name over the symbol.

So there is no community that reads ⊕ on two integers as a boolean operation. If anything, the boolean-only reading is the outlier.

What the library does today

Measured on current master — and it is consistent, which is worth saying:

input	result
true xor false	True
x xor false / x xor true	x / not x
2 xor 0, 2 xor 3, 6 xor 3	all unevaluated
6 and 3, 6 or 3, not 6, 6 implies 3	all unevaluated

Boolean operators are boolean; given integers they decline, uniformly. No bitwise route exists.

What the other systems do — two operators, not one

• SymPy (measured, 1.14): Xor is boolean and coerces by truthiness, so Xor(6, 3) is False and Xor(2, 0) is True. Bitwise lives elsewhere: Integer(6) ^ Integer(3) is 5.
• Mathematica: Xor[] boolean, BitXor[] integer — likewise BitAnd, BitOr, BitNot, BitShiftLeft.
• Maxima: xor boolean, bitwise through separate functions.

Nobody overloads one operator across both. And note that SymPy's Xor(6, 3) is False where bitwise 6 ⊕ 3 is 5 — same input, two defensible answers, which is exactly why they are kept apart.

Where that leaves this PR

The rule it adds, x ⊕ 0 → x, is true under the bitwise reading. It is not a wrong identity. The difficulty is that it would be the only bitwise behaviour in existence: 2 xor 3 would still not evaluate, x xor 1 would still not reduce, and and, or, not would stay boolean-only. One operator would be half-bitwise, which is the kind of inconsistency #497 is written against.

Recommendation

Add BitXor, BitAnd, BitOr, BitNot (and shifts, if wanted) as their own operations over integers, and leave the boolean operators boolean.

That answers your objection directly: with a split, and/or/not/implies need no change at all, because the bitwise ones are different functions. It gives @jclapis's quantum registers the operator they actually mean, defined on every input rather than on one. And it follows Mathematica, the closest precedent.

@jclapis — for the original problem: if the two registers are compared as booleans rather than integers, all four reductions you wanted already work on master today with no patch. The bitwise route is what is missing.

I am happy to implement the bitwise family. It is contained: a node kind, evaluation over integers, the parser names, both compilers, and the identities (a ⊕ a = 0, a ⊕ 0 = a, associativity, commutativity). Say the word and I will open it — then this PR can close as superseded with its request satisfied rather than declined.