
\section{\label{sec:patches}Patches}

We start by introducing \emph{patches}, and the concept of \emph{patch
commutation}.

\begin{Idefinition}[patches]
We have a (possibly infinite) set of patches $\patches$.
\end{Idefinition}

\start{definition}{patch-commute}
$\begin{array}[t]{@{}r@{~}l@{}}
 \multicolumn{2}{@{}l@{}}{\forall p \in \patches, q \in \patches .}\\
     &\left( \exists p' \in \patches, q' \in \patches .
      \pair{p}{q} <-> \pair{q'}{p'} \right )\\
 \vee&\pair{p}{q} <-> \fail
 \end{array}$
\begin{Iexplanation}
We write $\pair{p}{q} <-> \pair{q'}{p'}$ if $p$ and $q$ commute,
resulting in $q'$ and $p'$. In other words, doing $p$ and then $q$ is
equivalent to doing $q'$ and then $p'$, where $p$ and $p'$ are morally
equivalent, and likewise $q$ and $q'$ are morally equivalent.

For example, adding ``Hello'' to line 3 of a file and then adding
``World'' to line 5 of the file is equivalent to adding ``World'' to line
4 of the file and then adding ``Hello'' to line 3 of a file. We
therefore say that
$\pair{\textrm{add ``Hello'' 3}}{\textrm{add ``World'' 5}}
 <->
 \pair{\textrm{add ``World'' 4}}{\textrm{add ``Hello'' 3}}$.

We can represent this diagramatically thus:\\
\begin{mfpic}{0}{4}{-1}{1}
    \pointdef{O}(0,0)
    \pointdef{midP}(1,0.8)
    \pointdef{P}(2,1)
    \pointdef{midQ}(1,-0.8)
    \pointdef{Q}(2,-1)
    \pointdef{midPQ}(3,0.8)
    \pointdef{midQP}(3,-0.8)
    \pointdef{PQ}(4,0)
    \point{\O,\P,\Q,\PQ}
    \arrlab{\O}{\midP}{\P}{br}{$p$}
    \arrlab{\P}{\midPQ}{\PQ}{bl}{$q$}
    \arrlab{\O}{\midQ}{\Q}{tr}{$q'$}
    \arrlab{\Q}{\midQP}{\PQ}{tl}{$p'$}
\end{mfpic}\\
Here the dots are repository states, and the arrows are patches;
$pq$ and $q'p'$ get us from the same state, to the same state, but
via different intermediate states.

We write $\pair{p}{q} <-> \fail$ if $p$ and $q$ do not commute. In other
words, it is not possible to do the moral equivalent of $q$ before $p$.

For example,
$\pair{\textrm{replace line 3 with ``Hello''}}{\textrm{replace line 3 with ``World''}}
<-> \fail$
\end{Iexplanation}
\end{Idefinition}

\start{axiom}{patch-commute-unique}
$\begin{array}[t]{@{}l@{}}
 \forall p \in \patches, q \in \patches,
         r \in (\patches \times \patches) \cup \mkset{\fail},
         s \in (\patches \times \patches) \cup \mkset{\fail} .\\
 (\pair{p}{q} <-> r) \wedge (\pair{p}{q} <-> s) => r = s
 \end{array}$
\begin{Iexplanation}
Either $p$ and $q$ \emph{always} commute, or they \emph{never} commute.
If they do commute, then the result is always the same.
\end{Iexplanation}
\end{Iaxiom}

Now that we know that the result of a commute is unique, we can afford
to be a bit lax about quantifying over variables. For example, if we are
dealing with two patches $p$ and $q$ and we say that
$\pair{p}{q} <-> \pair{q'}{p'}$
then it is implied that we are considering the case where $p$ and $q$
commute, and that the result of the commutation is $q'$ and $p'$.

\start{axiom}{patch-commute-self-inverse}
$\begin{array}[t]{@{}l@{}}
 \forall p  \in \patches, q  \in \patches,
         p' \in \patches, q' \in \patches .\\
 (\pair{p}{q} <-> \pair{q'}{p'}) <=> (\pair{q'}{p'} <-> \pair{p}{q})
 \end{array}$
\begin{Iexplanation}
If you commute a pair of patches, and then commute them back again, then
you end up back where you started. Note also that we require that if
commuting one way succeeds then commuting the other way also succeeds.
\end{Iexplanation}
\end{Iaxiom}

