% Notes: 
% change definition of canonical path to start with (k-1 k) ... (i+1 i)?
% Go back to ``an associated permutation''
% Use <-p-> notation.
% Explain problems with random equality

\documentclass{article}

\usepackage{verbatim}
\usepackage{amsmath}
\usepackage{amsthm}

\usepackage{multiletter}

\newcommand{\commute}{\leftrightarrow}
\newcommand{\commutefails}{\leftrightarrow \textbf{fail}}
\newcommand{\commutelift}{\commute^{\uparrow}}
\newcommand{\commutestar}{\commute^{*}}
\newcommand{\notexists}{\not\!\exists}
\newcommand{\idpatch}{\textbf{id}}
\newcommand{\idperm}{\textit{id}}
\newcommand{\commutesto}{\sim}
\newcommand{\doubleimplies}{\Leftrightarrow}
\newcommand{\composeperm}{\odot}

\newtheorem{theorem}{Theorem}
\newtheorem{corollary}{Corollary}

\begin{document}

\title{Darcs patch theory}
\author{Ganesh Sittampalam \textit {et al.}}

\maketitle

\begin{abstract}
The purpose of this document is to formalise the properties of
darcs patch theory.
\end{abstract}

\section{Introduction}

Darcs (``David's advanced revision control system'') 
is a {\em change-based} revision control system. It differs from most
other revision control systems in that it treats changes as the most
fundamental quantity to be manipulated, rather than states of the
repository.

\section{Definitions and notation}

In the most general terms, a {\em change} is an abstract concept 
representing some logical or semantic effect
on a repository. For example, adding support for SSL to an HTTP server
could be thought of as a change.

A {\em patch} is a concrete representation of a change, which applies
to a repository in one particular state. For example, the specific set
of differences resulting from adding support for SSL to Apache 1.3.27 
would be a patch. The differences resulting from adding support for SSL
to Apache 1.3.28 would be a different patch representing the same change.

In an ideal world, we would be able to take a patch 
that represents a change for some repository and automatically
produce a patch that represents the same change for any other repository. 
For example, it would be nice if we could automatically derive the patch
that adds SSL to the thttpd server from the patch that adds it to 
Apache 1.3.27.

In practice, this is of course completely infeasible; the extent to which
we can take a patch against one repository and work out an equivalent patch
for another repository is limited by the intelligence built into our 
revision control system. Therefore, we limit our notion of change
to the range of patches that we can automatically produce.

The fundamental purpose of a revision control system is to 


$A$, $B$ etc are individual patches, that cannot be expressed as a sequence
of two smaller patches.

Sequential patch composition is written with juxtaposition. Not all patches
can be sequentially composed, but use of the notation $AB$ implicitly assumes 
that they can.
\footnote{It is likely that a mechanised proof about patch theory would 
have to make this precondition explicit.}

Commutation is written $AB \commute B'A'$. 
If $\notexists B'A' \mbox{ s.t. } AB \commute B'A'$, then we write
$AB \commutefails$.

We write $As$ to represent a (possibly empty) sequence of patches of 
arbitrary length
The empty sequence is written as $\idpatch$.

$\commutelift$ is a commutation between sequences of patches, defined 
as follows:

\[
\begin{array}{rcrcl}
AB \commute B'A' & \implies & AB & \commutelift & B'A' \\
As \commutelift Bs & \implies & AsC & \commutelift & BsC \\
As \commutelift Bs & \implies & CAs & \commutelift & CBs
\end{array}
\]

We distinguish different derivations of $As \commutelift Bs$ from each other,
so any particular statement of $As \commutelift Bs$ has precisely one set of
antecedents in the above definition.
\footnote{This is unpleasant, and it would be good to find some
better notation. In Section~\ref{nwaypermutivity} we show
that in fact all ``similar'' derivations must produce the same result, 
so after that point we can
start treating $\commutelift$ and $\commutestar$ (defined below)
as a simple relation.}

We define $\commutestar$, the reflexive transitive closure of $\commutelift$,
as follows:

\[
\begin{array}{rcrcl}
& & As & \commutestar & As \\
As \commutelift Bs & \implies & As & \commutestar & Bs \\
As \commutestar Bs \land Bs \commutestar Cs & \implies & As & \commutestar & Cs
\end{array}
\]

Again we distinguish different derivations.

The relation $\commutesto$ between individual patches is defined as follows.

\[
\begin{array}{rcrcl}
& & A & \commutesto & A\\
AB \commute B'A' & \implies & A & \commutesto & A'\\
AB \commute B'A' & \implies & B & \commutesto & B'\\
A \commutesto A' \land A' \commutesto A'' & \implies & A & \commutesto & A''
\end{array}
\]
We {\em do not} attempt to distinguish different derivations of 
$\commutesto$; it is a simple relation.

We adopt a notational convention that if we mention $A$ and $A'$ together,
then $A \commutesto A'$ (etc). 
\footnote{This is another thing that would 
need to be made explicit in a mechanised proof}

In some discussions of patch theory, $A \commutesto A'$ has been described
as $A$ and $A'$ having the same {\em identity} or {\em ancestor}. We will
not use those terms here.

\section{Assumed properties}

In this section we define certain properties that must be true
about primitive patches and commutation. It is the responsibility
of the implementer of any given kind of patch to verify that this is so.

Associativity of patch sequencing:
\[
(AB)C = A(BC)
\]

This property means that we can omit parentheses, and that the list notation
introduced above makes sense.

Uniqueness of commutation:
\[
AB \commute B'A \land AB \commute B''A'' \implies A'=A'' \land B'=B''
\]

Invertibility of commutation:
\[
AB \commute B'A' \implies B'A' \commute AB
\]

Note that this means that $\commutesto$ is an equivalence relation.

Consistency of failure:

If $A \commutesto A'$, $B \commutesto B'$, 
then $AB \commutefails implies A'B' \commutefails$.

3-way permutivitiy of commutation:

If
\[
ABC 
\commutelift B'A'C 
\commutelift B'C'A'' 
\commutelift C''B''A''
\commutelift C''A'''B''
\commutelift A''''C'''B''
\commutelift A''''B'''C''''
\]

Then
\begin{eqnarray*}
A & = & A''''\\
B & = & B'''\\
C & = & C''''
\end{eqnarray*}

\section{N-way permutivity}
\label{nwaypermutivity}

Informally, the 3-way permutivity property above guarantees that
if we commute a sequence of 3 patches arbitrarily, eventually returning
them to the original order, we will get exactly the same patches.

The purpose of this section is to show that this is also true for
arbitrarily long sequences.

We start by explicitly writing down some ``obvious'' properties and 
constructing some useful machinery.

\begin{theorem}
If $As \commutelift Bs$, then $|As| = |Bs|$.

If $As \commutestar Bs$, then $|As| = |Bs|$.
\end{theorem}

\begin{proof}
By induction on the structure of $\commutelift$ and $\commutestar$.
\end{proof}

We now define the concept of the {\em associated permutation} 
for $\commutelift$ and $\commutestar$, by induction on their structure.

Informally, if $p$ is the associated permutation for $As \commutestar Bs$,
and $A_i$ occurs at position $i$ in $As$, then $A_i$ ends up being commuted
into position $p(i)$ in $Bs$.

If $AB \commute B'A'$, then $AB \commutelift B'A'$ has the associated 
permutation $(1~2)$.

If $As \commutelift Bs$ has the associated permutation $(n~n+1)$, 
then $AsC \commutelift BsC$ has the associated permutation $(n~n+1)$.

If $As \commutelift Bs$ has the associated permutation $(n~n+1)$, 
then $CAs \commutelift CBs$ has the associated permutation $(n+1~n+2)$.

Note that by induction, the associated permutation for $\commutelift$ 
is always a single transposition, so this definition makes sense.

$As \commutestar As$ has the associated permutation $\idperm$.

If $As \commutelift Bs$ has the associated permutation $p$, 
then so does $As \commutestar Bs$.

If $As \commutestar Bs$ has the associated permutation $p$
and $Bs \commutestar Cs$ has the associated permutation $q$, 
then $As \commutestar Cs$ has the associated permutation $q \composeperm p$.

Note that the alphabet for the associated permutation of 
$As \commutelift Bs$ or $As \commutestar Bs$ is $1 \ldots |As|$.

Every such commutation has precisely one associated permutation (since it is
defined by induction on the structure of the commutation and we only allow one
derivation for each commutation).

\begin{theorem}
If $As = A_{p(1)} \ldots A_{p(n)} \commutestar B_1 \ldots B_n = Bs$
has the associated permutation $p$,
then $\forall i . 1 \leq i \leq n . A_i \commutesto B_i$.
\footnote{It would be nice if the converse were true, i.e. 
$A_{p(1)} \ldots A_{p(n)} \commutestar B_1 \ldots B_n$ has the associated 
permutation $p$
if $\forall i . 1 \leq i \leq n . A_i \commutesto B_i$. However I think 
it would
require some kind of stronger property, such as unique patch ids, to make 
it so.}
\end{theorem}
\begin{proof}
By induction on the structure of $\commutelift$ and $\commutestar$.
\end{proof}

Note that the indexing of the patches is somewhat counter-intuitive; 
nonetheless,
it is correct. We expect the $A_{p(i)}$, which is the $i$th element of $As$,
to commute into $B_{p(i)}$, the $p(i)$th element of $Bs$.


$(i~i+1)(j~j+1) = (j~j+1)(i~i+1)$ if $j > i+1$.

$(i~i+1)(i~i+1) = \idperm$.

$(i~i+1)(i+1~i+2)(i~i+1) = (i+1~i+2)(i~i+1)(i+1~i+2)$.

We now define the concept of a {\em canonical representation}
of a permutation $p$. Such a representation is a sequence of transpositions.

If $p = \idperm$, the canonical representation of $p$ is the empty
sequence.

Otherwise, pick the smallest $i$ such that $p(i) \not= i$
(if no such $i$ existed then $p = \idperm$).
Let $j$ = $p^{-1}(i)$.
The first element of the sequence is $(j-1~j)$, and the remainder of
the sequence is the canonical representation of $p' = p \composeperm (j-1~j)$.

Note that $j$ cannot be $1$, so this definition is well-formed.
[If $j=1$, then $i = p(1)$, so $i \not= 1$ (otherwise $i = p(i)$),
so $p(1) \not= 1$, so $i$ is not the smallest for which this property
holds.]

Also, this procedure must terminate, so the canonical representation
is finite.
Either:
\begin{itemize}
\item{$p' = idperm$ and we terminate}
\item{$p'^{-1}(i) = i$. Then the new $i$ we will pick for $p'$ is strictly
greater than the original $i$ for $p$.}
\item{Otherwise, the new $i$ we will pick for $p'$ is the same as that
for $p$,\footnote{Need to make this into a theorem and move 
it below the following theorem so we can use that}
and $p'^{-1}(i) = p^{-1}(i) - 1$.}
\end{itemize}
So either $i$ increases (and is bounded by $n$) or it stays the same
and $p^{-1}(i)$ decreases.

\begin{theorem}
If $(j-1~j)$ is the first element of the canonical representation of $p$,
then $p(j-1) > p(j)$, and $p(j) < j$.
\end{theorem}
\begin{proof}
Let $i = p(j)$. We know that $\forall k . k < i . p(k) = k$, and
so $\forall k . k < i . k = p^{-1}(k)$. Also, $i \not=p(i)$.

Clearly, $p(j-1) \not= p(j)$. 

Suppose $p(j-1) < p(j)$. Then $p(j-1) < i$, so $j-1 < i$, 
so $j < i+1$. If $j=i$, then $p(i) = j = i$, so $j < i$.
But then $p(j) = j < i$, which is impossible.

So $p(j-1) > p(j)$.

Now suppose $j < p(j)$. Then $p(j) = j$, which is impossible.
So $p(j) < j$.

\end{proof}


We now define the {\em canonical commutation path} for a permutation $p$.
Such a path starts from $A_{p(1)}' \ldots A_{p(n)}'$
and finishes at $A_1 \ldots A_n$, where the alphabet of $p$
is $1 \ldots n$.
The path is the same length as the canonical representation of $p$,
and each $\commutelift$ step in the path has the corresponding
transposition in the canonical representation of $p$ as its associated
permutation.

Informally, one is constructed by first commuting $A_1'$ to the left of 
the sequence, then commuting $A_2'$ to the one-but-leftmost position, 
and so on. 

It is not guaranteed that all of these commutes will succeed, so there
might not be any canonical commutation path for any given $p$ and sequence
of patches.

By construction, any suffix of a canonical commutation path is also a 
canonical commutation path (for a different permutation, but the same ending 
patch sequence).

\begin{theorem}
If $Bs \commutestar As$ is a canonical commutation path for $p$, then
$p$ is the associated permutation of $Bs \commutestar As$.
\end{theorem}

\begin{proof}
Obvious, from the definition of the canonical representation of $p$
and the construction of the canonical commutation path.
\end{proof}

\begin{theorem}
If $Bs \commutestar As$ is a canonical commutation path for $p$, and
$Cs \commutestar As$ is also a canonical commutation path for $p$,
then $Bs = Cs$.

If $As \commutestar Bs$ is a canonical commutation path for $p$, and
$As \commutestar Cs$ is also a canonical commutation path for $p$,
then $Bs = Cs$.
\end{theorem}

\begin{proof}
Since the commutation paths must have the same structure, this follows from
the ``Uniqueness of commutation'' and ``Invertibility of commutation'' axioms.
(More formally, by induction on the length of the canonical representation
of $p$.)
\end{proof}

We therefore talk about ``the'' canonical commutation path for $p$ 
starting with or ending with a particular patch sequence.

With all this machinery set up, we can move on to proving some useful 
properties.

\begin{theorem}
Suppose that $p$ is the associated permutation for
$As' \commutestar As$
Then there is a canonical commutation path for $p$ that
starts with $As'$.
\end{theorem}

\begin{proof}
We use induction on the length of the canonical representation of $p$.

If $p = \idperm$, then we are done.

Otherwise, 
Let $As' = A_{p(1)}' \ldots A_{p(n)}'$, and $As = A_1 \ldots A_n$.

Let (i-1~i) be the first element in the canonical representation of
$p$, and let $j = p(i-1)$ and $k = p(i)$, so that
$A_j'$ and $A_k'$ are the first patches in $As'$ 
we try to commute. Recall that $j > k$.

If $A_j' A_k' \commute A_k'' A_j''$, then let 
$As'' = A_{p(1)}' \ldots A_{p(i-2)}' A_k'' A_j'' A_{p(i+1)}' \ldots A_{p(n)}'$,
giving $As' \commutelift As''$ as the first step on the canonical commutation
path.

Then use the inverse of this commute
together with $As' \commutestar As$ to construct a new path 
$As'' \commutestar As$,
and apply the induction hypothesis
to construct the canonical commutation path from $As'' \commutestar As$.

Now suppose that $A_j' A_k' \commutefails$.
But we know that $j > k$, so $A_k$ occurs before $A_j$ in $As$.

So somewhere
in the path $As' \commutestar As$, some patches $A_j''$ and $A_k''$ must swap 
position\footnote{This claim really should be formalised}, 
{\em i.e.}$A_j''A_k'' \commutestar A_k'''A_j'''$. 
But this violates our ``Consistency of failure'' axiom.
\end{proof}

\begin{theorem}
Suppose:
\begin{itemize}
\item{$As \commutestar Bs$ is a canonical commutation path for $p$}
\item{$As' \commutelift As$ with associated permutation $(i-1~i)$}
\item{$As' \commutestar Bs'$ is a canonical commutation path for 
$p \composeperm (i-1~i)$}
\item{The canonical representation for $p \composeperm (i-1~i)$ is 
one transposition longer than that for $p$}
\end{itemize}
Then $Bs = Bs'$.
\end{theorem}

\begin{proof}
Write $As$ as $A_{p(1)} \ldots A_{p(n)}$ and
$As'$ as 
$A_{p(1)} \ldots A_{p(i-2)} A_{p(i-1)}' A_{p(i)}' A_{p(i+1)} \ldots A_{p(n)}$.

Write $Bs$ as $B_1 \ldots B_n$
and $Bs'$ as $B_1' \ldots B_n'$.

Let $p' = p \composeperm (i-1~i)$.
Let $q$ be the canonical representation of $p$
and $q'$ be the canonical representation of $p'$.

Intuitively, $q'$ carries out the same sequence of
commutations as $q$, except that at some point it also has to swap 
commuted versions of $A_i'$ and $A_{i-1}'$, which is why it is one 
element longer. Also, $A_{i-1}$ and $A_i$ are in the correct
order, so $p(i-1) < p(i)$.
\footnote{Ought to formalise this paragraph too...}

We use induction on the length of $q'$.

Consider the first transposition in $q'$, $(j-1~j)$.

Recall that $p'(j-1) > p'(j)$, and that 
$\forall k . k < p'(j) . k = p^{-1}(k) \land k = p(k)$.

We now proceed by case analysis on the value of $j$.

If $j = i$, then the ``swapping back''
happens immediately. The first commutation in
$As' \commutestar Bs'$ must be $As' \commutelift As$ 
(by ``Uniqueness of commutation''),
so $As \commutestar Bs'$ must be a canonical commutation path for $p$
(since suffixes of canonical commutation paths are also canonical).
So $Bs = Bs'$.

Suppose $j = i-1$.
Then $p'(j) = p'(i-1) = p(i)$, and $p'(j+1) = p'(i) = p(i-1)$.
Since $p(i-1) < p(i)$, $p'(j+1) < p'(j)$. So $p'(j+1) = j+1$, 
so $j < j+1 < p'(j)$, so $p'(j) = j$, which is impossible.

Now suppose $j = i+1$.
Then $p'(j) < p'(j-1)$ So $p(i+1) = p'(i+1) < p'(i) = p(i-1)$.
Recall also that $p(i-1) < p(i)$.
We also know that $p'(j) < j$. So $p(i+1) < i+1$.

Now, $forall k . k <  p'(j) . p'(k) = k$, so
$forall k . k < p(i+1) . p'(k) = k$, and 
since $p(i+1) < i+1$, $p'(k) = p(k)$.

Suppose $p(i+1) = i$. Then $i-1 < p(i+1)$ so $p(i-1) = i-1$.
So $p'(i) = i-1$, and $p'(i+1) = i$.
So $p''(i) = i$ and $p''(i+1) = i-1$, and $p''(i-1) = p'(i-1) = p(i)$.

Now, consider $p'' = p' \composeperm (j-1~j) = p' \composeperm (i~i+1)$.
If $k < p''(i) = p'(i+1) = p(i+1)$, then $p''(k) = p(k) = k$.
Also, $p''(i) = p'(i+1) = p(i+1) \not= i$. So the first
transposition in the canonical representation of $p''$ is $(i-1~i)$.

First transposition in $p$ is $(i~i+1)$ and second is $(i-1~i)$. 
\footnote{More rabbits out of hats.}

We have that
\[
As' = 
A_{p(1)} \ldots A_{p(i-2)} 
A_{p(i)}' A_{p(i-1)}' A_{p(i+1)} 
A_{p(i+2)} \ldots A_{p(n)}
\]
The first commutation gives us
\[
A_{p(1)} \ldots A_{p(i-2)} 
A_{p(i)}' A_{p(i+1)}'' A_{p(i-1)}'' 
A_{p(i+2)} \ldots A_{p(n)}.
\]
The next commutation gives us
\[
A_{p(1)} \ldots A_{p(i-2)} 
A_{p(i+1)}''' A_{p(i)}'' A_{p(i-1)}'' 
A_{p(i+2)} \ldots A_{p(n)}.
\]
Call this sequence $As'''$.

Now consider
\[
As = 
A_{p(1)} \ldots A_{p(i-2)} 
A_{p(i-1)} A_{p(i)} A_{p(i+1)} 
A_{p(i+2)} \ldots A_{p(n)}
\]
The first commutation gives us
\[
A_{p(1)} \ldots A_{p(i-2)} 
A_{p(i-1)} A_{p(i+1)}'''' A_{p(i)}'''
A_{p(i+2)} \ldots A_{p(n)}.
\]
The next commutation gives us
\[
A_{p(1)} \ldots A_{p(i-2)} 
A_{p(i+1)}''''' A_{p(i-1)}''' A_{p(i)}'''
A_{p(i+2)} \ldots A_{p(n)}.
\]
Call this sequence $As''$.

Now, by ``Consistency of failure'', 
we can commute $A_{p(i)}'' A_{p(i-1)}''$ 
in $As''$ to give $A_{p(i-1)}'''' A_{p(i)}''''$.

Taking apart the structure of $\commutelift$ and inverting some of the 
commutations,
we can construct the commutation path

\[
A_{p(i+1)}''''' A_{p(i-1)}''' A_{p(i)}'''
\commute 
A_{p(i-1)} A_{p(i+1)}'''' A_{p(i)}'''
\commute
A_{p(i-1)} A_{p(i)} A_{p(i+1)} 
\commute
A_{p(i)}' A_{p(i-1)}' A_{p(i+1)} 
\commute
A_{p(i)}' A_{p(i+1)}'' A_{p(i-1)}'' 
\commute
A_{p(i+1)}''' A_{p(i)}'' A_{p(i-1)}'' 
\commute
A_{p(i+1)}''' A_{p(i-1)}'''' A_{p(i)}''''
\]

By the ``Three-way permutivity of commute'' axiom, the initial and final 
sequences must actually be equal. 
In other words, $As''$ and $As'''$ are linked by a single commutation,
and we have the canonical paths $As'' \commutestar Bs$ 
and $As''' \commutestar Bs'$

We now apply induction on the length of these canonical paths, since they
are shorter than the original ones.

For $j > i+1$, the first commutation from $As'$ gives
$A_1 \ldots A_{i-1} A_{i+1}' A_i' A{i+2} 
\ldots A_{j-1} A_{j+1}' A_j' A_{j+2} \ldots A_n$,
and the first commutation from $As$ gives
$A_1 \ldots A_{i-1} A_i A_{i+1} A{i+2} 
\ldots A_{j-1} A_{j+1}' A_j' A_{j+2} \ldots A_n$,
and these two are also linked by a single commutation with shorter 
canonical paths, so we can apply induction.

A similar argument follows for $j < i-1$.
\end{proof}

These two results are key. From here, it is a series of short easy steps
to proving an ``N-way permutivity'' result.

\begin{corollary}
Suppose:
\begin{itemize}
\item{$As \commutestar Bs$ is a canonical commutation path for $p$}
\item{$As' \commutelift As$ with associated permutation $(i~i+1)$}
\item{$As' \commutestar Bs'$ is a canonical commutation path for 
$p \composeperm (i~i+1)$}
\end{itemize}
Then $Bs = Bs'$.
\end{corollary}

\begin{proof}
The canonical commutation path for $p \composeperm (i~i+1)$ must
be either one transposition shorter or one transposition longer than 
that for $p$.
If it is one transposition longer, apply the previous theorem. 
If it is one transposition
shorter, construct the inverse commutation $As \commutelift As'$ 
and apply the previous theorem with $As, Bs$ and $As', Bs'$ reversed.
\end{proof}

\begin{theorem}
Suppose:
\begin{itemize}
\item{$As \commutestar Bs$ is a canonical commutation path for $p$}
\item{$As' \commutelift As$ with associated permutation $(i~i+1)$}
\end{itemize}
Then there exists a canonical commutation path $As' \commutestar Bs$ for
$p \composeperm (i~i+1)$.
\end{theorem}

\begin{proof}
We can construct $As' \commutestar Bs$ with associated permutation 
$p \composeperm (i~i+1)$ from $As' \commutelift As$ and 
$As \commutestar Bs$. So by an earlier theorem a canonical path 
$As' \commutestar Bs'$
for this permutation must exist (for some $Bs'$). By the previous 
corollary, $Bs' = Bs$.
\end{proof}

\begin{theorem}
Suppose:
\begin{itemize}
\item{$As \commutestar Bs$ is a canonical commutation path for $p$}
\item{$As \commutestar As'$ with associated permutation $q$}
\end{itemize}
Then there exists a canonical commutation path $As' \commutestar Bs$ for
$p \composeperm q^{-1}$.
\end{theorem}
\begin{proof}
Invert $As \commutestar As'$ to give $As' \commutestar As$, 
and then apply induction
on the structure of $As' \commutestar As$, along with the previous theorem.
\end{proof}


\begin{corollary}
If $As \commutestar As'$ has associated permutation 
$\idperm$, then $As = As'$.
\end{corollary}

\begin{proof}
Let $p = \idperm$ and $q = \idperm$. 
Then we can trivially construct a canonical commutation path for $p$,
$As \commutestar As$.

Applying the previous theorem, there must be
a canonical commutation path $As' \commutestar As$
for $\idperm \composeperm \idperm^{-1} = \idperm$,
so by an earlier theorem showing uniqueness of canonical
commutation paths, $As' = As$.
\end{proof}


\end{document}