Editing XOR swap algorithm (section)

==Proof of correctness==
The [[binary operation]] XOR over bit strings of length <math>N</math> exhibits the following properties (where <math>\oplus</math> denotes XOR):{{Efn|The first three properties, along with the existence of an inverse for each element, are the definition of an [[abelian group]]. The last property is the statement that every element is an [[Involution (mathematics)|involution]], that is, having [[Order (group theory)|order]] 2, which is not true of all abelian groups.}}

* '''L1.''' [[Commutative operation|Commutativity]]: <math>A \oplus B = B \oplus A</math>
* '''L2.''' [[Associativity]]: <math>(A \oplus B) \oplus C = A \oplus (B \oplus C)</math>
* '''L3.''' [[Identity element|Identity exists]]: there is a bit string, 0, (of length ''N'') such that <math>A \oplus 0 = A</math> for any <math>A</math>
* '''L4.''' Each element is its own [[inverse element|inverse]]: for each <math>A</math>, <math>A \oplus A = 0</math>.

Suppose that we have two distinct registers <code>R1</code> and <code>R2</code> as in the table below, with initial values ''A'' and ''B'' respectively. We perform the operations below in sequence, and reduce our results using the properties listed above.

{| class="wikitable"
|- 
! Step
! Operation
! Register 1
! Register 2
! Reduction
|-
| 0 || Initial value || <math>A</math> || <math>B</math> || — 
|-
| 1 || <code>R1 := R1 XOR R2</code>  || <math>A \oplus B</math> ||<math>B</math>|| —
|- 
| 2 || <code>R2 := R1 XOR R2</code>  || <math>A \oplus B</math> || <math>(A \oplus B) \oplus B = A \oplus (B \oplus B)</math><br><math>= A \oplus 0</math><br><math>=A</math> || '''L2<br> L4<br> L3'''
|-
| 3 || <code>R1 := R1 XOR R2</code>  || <math>(A \oplus B) \oplus A = (B \oplus A) \oplus A</math><br><math> = B \oplus (A \oplus A)</math><br><math> = B \oplus 0 </math><br><math> = B </math> || <math>\ A</math> || '''L1<br>L2<br>L4<br>L3'''
|}

=== Linear algebra interpretation ===
As XOR can be interpreted as binary addition and a pair of bits can be interpreted as a vector in a two-dimensional [[vector space]] over the [[field with two elements]], the steps in the algorithm can be interpreted as multiplication by 2&times;2 matrices over the field with two elements. For simplicity, assume initially that ''x'' and ''y'' are each single bits, not bit vectors.

For example, the step:
<syntaxhighlight lang="pascal">
X := X XOR Y
</syntaxhighlight>
which also has the implicit:
<syntaxhighlight lang="pascal">
Y := Y
</syntaxhighlight>
corresponds to the matrix <math>\left(\begin{smallmatrix}1 & 1\\0 & 1\end{smallmatrix}\right)</math> as
:<math>\begin{pmatrix}1 & 1\\0 & 1\end{pmatrix} \begin{pmatrix}x\\y\end{pmatrix}
= \begin{pmatrix}x+y\\y\end{pmatrix}.
</math>
The sequence of operations is then expressed as:
:<math>
\begin{pmatrix}1 & 1\\0 & 1\end{pmatrix}
\begin{pmatrix}1 & 0\\1 & 1\end{pmatrix}
\begin{pmatrix}1 & 1\\0 & 1\end{pmatrix}
=
\begin{pmatrix}0 & 1\\1 & 0\end{pmatrix}
</math>
(working with binary values, so <math>1 + 1 = 0</math>), which expresses the [[elementary matrix]] of switching two rows (or columns) in terms of the [[Shear mapping|transvections]] (shears) of adding one element to the other.

To generalize to where X and Y are not single bits, but instead bit vectors of length ''n'', these 2&times;2 matrices are replaced by 2''n''&times;2''n'' [[block matrices]] such as <math>\left(\begin{smallmatrix}I_n & I_n\\0 & I_n\end{smallmatrix}\right).</math>

These matrices are operating on ''values,'' not on ''variables'' (with storage locations), hence this interpretation abstracts away from issues of storage location and the problem of both variables sharing the same storage location.