\renewcommand\cfile{trans.tex}

In translating a proof in \Mp\ into a proof in \dRA,
the first step is to translate an \Mp-sequent into a \dRA-sequent.
We start by giving an intuitive explanation of the meanings of sequents in both
systems, and of the correspondence between them.

Consider the \M-sequent 
$x[A]y, y[B]z, x[C]z \vdash $,
and take this to mean 
$$\lnot\exists x,y,z( (x,y) \in A \;\&\; (y,z) \in B \;\&\; (x,z) \in C)$$
that is, there are no points $x,y,z$ such that 
$(x,y) \in A$, $(y,z) \in B$ and $(x,z) \in C$.
Since 
$$A \circ B = \{ (x,z) \;|\; \exists y( (x,y) \in A 
\;\&\; (y,z) \in B) \}$$
this is equivalent to 
$$\lnot\exists x,z( (x,z) \in A  \circ B \;\&\; (x,z) \in C)$$
and so to 
$$\lnot\exists x,z( (x,z) \in (A  \circ B) \land C)$$
That is, there is no pair of points related by \mbox{$(A  \circ B) \land C$,}
which equates to \mbox{$(A  \circ B) \land C \vdash \bot$} in \dRA,
or, using the \dRA\ structural operators, 
$(A ; B) , C \vdash I$.

We now set this translation out systematically.
We translate an \M-sequent, other than the trivial sequent $\vdash$,
into a \dRA-sequent as follows
\begin{enumerate}
\renewcommand\labelenumi{(\M\arabic{enumi})}
\renewcommand\theenumi\labelenumi
\item \label{Mstmv} \label{Mst1}
Move all formulae on the right-hand side of the turnstile to the 
left-hand side, while changing $x[R]y$ to $x$$[*$$R]y$.
\item \label{Mstbl}
Whenever it would enable one of the following steps to proceed,
a formula $x[R]y$ may be changed to $y$$[\bullet $$R]x$.
\item \label{Mst,}
Replace any two formulae $x[R]y$ and $x[S]y$ by $x[R,S]y$.
\item \label{Mst;}
Whenever $x[R]y$ and $y[S]z$ are the only two formulae involving $y$
(and $x \not = y$ and $y \not = z$),
% and $x,y$ and $z$ are distinct,
replace $x[R]y$ and $y[S]z$ by $x[R;S]z$.
\item \label{Mst;'}
Replace $x[R]x$ and $x[S]z$ by $x[(R,\1);S]z$.
\item \label{Mst;`} \label{Mstlb1} 
Replace $x[R]z$ and $z[S]z$ by $x[R;(S,\1)]z$.
\item \label{Mstfin} \label{Mstlst} 
Finally, when only one formula $x[R]y$ remains,
then if $x$ and $y$ are distinct,
replace the sequent $x[R]y \vdash$ by $R \vdash I$.
Otherwise replace the sequent $x[R]x \vdash$ by $(R,\1) \vdash I$.
% For the special case of the trivial \M-sequent,
% replace $\vdash$ by $I \vdash I$.
\end{enumerate}

We will say that a translation \bfi{uses} $(x,y)$
when $(x,y)$ is the pair of point variables dropped in step \ref{Mstfin}.
(We will also say that the formula 
$x[A]y$ \bfi{uses} the ordered pair $(x,y)$,
and that it \bfi{uses}\label{usesuop} the unordered pair $\{x,y\}$).

Actually step \ref{Mstmv} is not entirely necessary as written;
it could be done only as needed to enable other steps to proceed.
But then other steps would need to be modified,
eg, step \ref{Mstfin} would also need to allow replacing
\mbox{$x[R]y \vdash x[S]y$} by $R \vdash S$.
However it is probably simpler to assume, as we will, that \emph{all} formulae 
have been moved to the left-hand side.
Alternatively, we could have moved all formulae to the right-hand side;
but then the relevant intuitions would include disjunction and relative sum of
relations, which are perhaps less easy than conjunction and relational
composition.

For example, the \M-sequent 
$x[A]y, y[B]z, x[C]z \vdash $ 
can be translated into $(A ; B) , C \vdash I$.
In terms of the intuitive explanation above, this corresponds to using
the sequence of steps shown on the left-hand side below.
The translation using the procedure given above is shown on the right.
\vpf
\begin{center}
\bpf
\A
"$\lnot\exists x,y,z( (x,y) \in A \;\&\; (y,z) \in B \;\&\; (x,z) \in C)$"
\U [:]
"$\lnot\exists x,z( (x,z) \in A  \circ B \;\&\; (x,z) \in C)$"
\U [:]
"$\lnot\exists x,z( (x,z) \in (A  \circ B) \land C)$"
\U ['] "\rule{0em}{1.9ex}"
\epf
\hfill
\bpf
\A
"$x[A]y, y[B]z, x[C]z \vdash $"
\U [:]
"$x[A; B]z, x[C]z \vdash $" "\ref{Mst;}"
\U [:]
"$x[(A; B), C]z \vdash $" "\ref{Mst,}"
\U [:]
"$(A; B), C \vdash I $" "\ref{Mstfin}"
\epf
\end{center}
However this procedure can produce several different \dRA-sequents from
the one \M-sequent.
We could equally well transform
$$\lnot\exists x,y,z( (x,y) \in A \;\&\; (y,z) \in B \;\&\; (x,z) \in C)$$
to either
$\lnot\exists y,z( (y,z) \in (\smile A  \circ C) \land B)$ or 
$\lnot\exists x,y( (x,y) \in (C  \circ \smile B) \land A)$. 
Correspondingly, the \M-sequent 
$x[A]y, y[B]z, x[C]z \vdash $
could equally well be translated to
$(\bullet A ; C) , B \vdash I$ or to 
$(C ; \bullet B) , A \vdash I$.

We will also look at such sequents in terms of a graphical representation.
The above sequents would correspond to the following graph
(which shows the points whose existence is denied).
\begin{center}
\begin{picture}(250,150)(-125,-75)
\thicklines
\put(0,50){\vector(-2,-1){100}} \put(-60,25){$A$}
\put(-100,0){\vector(2,-1){100}} \put(-60,-35){$B$}
% \put(0,50){\vector(2,-1){100}} \put(55,25){$G$}
% \put(100,0){\vector(-2,-1){100}} \put(55,-30){$H$}
\put(0,50){\vector(0,-1){100}} \put(5,0){$C$}
\put(-110,0){$y$}
% \put(105,0){$w$}
\put(0,55){$x$}
\put(0,-60){$z$}
\end{picture}
\end{center}

The inverse translation, to
translate a \dRA-sequent into an \M-sequent, 
would run along the following lines
(we start numbering the steps from \ref{dstpv} so that many of
the step numbers will
correspond to those of the forward translation)
\begin{enumerate}
\setcounter{enumi}{-1}
\renewcommand\labelenumi{({\boldmath $\delta$}\arabic{enumi})}
\renewcommand\theenumi\labelenumi
\item \label{dstpv} First, replace the sequent
$R \vdash I$ by $x[R]y \vdash $ , or
$R \vdash S$ by $x[R]y \vdash x[S]y$.
Then repeatedly apply which ever of the following steps is applicable.
\item For any formulae $x$$[*$$R]y$ on one side of the turnstile,
move it to the other side, deleting the `$*$';
eg, change
$\Gamma, x[*R]y \vdash \Delta $ to ${\Gamma \vdash \Delta, x[R]y} $.
\item \label{dstbl} Replace any formula $x$$[\bullet $$R]y$ by $y[R]x$.
\item \label{dst,} Replace any formula $x[R,S]y$ by $x[R]y, x[S]y$. 
\item \label{dst;} Replace any formula $x[R;S]z$ by $x[R]y, y[S]z$,
where $y$ is a new point variable.
\item \label{dstloop} Delete any formula $x[1]z$,
and change all other occurrences of $z$ to $x$.
\end{enumerate}

It may be noted that the translation process corresponds to transformations of
a graph like that in the diagram, for example:
\begin{itemize}
\label{grtr}
\item steps \ref{Mstbl} and \ref{dstbl} 
correspond to reversing the direction of an edge
\item step \ref{Mst,} 
corresponds to coalescing multiple edges (edges sharing the same endpoints),
and step \ref{dst,} 
corresponds to splitting an edge, to form multiple edges
\item steps \ref{Mst;} and \ref{dst;} 
correspond to deleting or creating a vertex of degree~2.
\end{itemize}

It will often be more convenient to discuss the translation 
process as though it were a process for transforming graphs,
rather than sequents.

We now give a more complicated example of the translation of an \M-sequent 
into \dRA, translating the \M-sequent 
$x[A]y, y[B]z, x[C]z, x[G]w, w[H]z \vdash \ $.
It can be translated into
(\emph{inter alia}) the following \dRA-sequents.
The pairs listed indicate the point variables dropped in the last
step \ref{Mstfin} of the translation process;
recall that we indicate this by
saying the translation uses $(x,y)$.
%(We will also say that the formula 
%$x[A]y$ \textbf{uses} the pair $(x,y)$).
\begin{center}
\begin{tabular}{c@{\qquad\qquad}c}
$A, ((C, (G;H)); \bullet B) \vdash I$ & $(x,y)$ \\
$B, (\bullet A; (C, (G;H))) \vdash I$ & $(y,z)$ \\
$((A;B), C), (G;H) \vdash I$ & $(x,z)$ \\
$(((A;B), C);\bullet H), G \vdash I$ & $(x,w)$ \\
$(\bullet G; ((A;B), C)), H \vdash I$ & $(w,z)$
\end{tabular}
\label{5alt}
\end{center}
As an example, we show the translation to the first \dRA-sequent above,
using steps \ref{Mst1} to \ref{Mstlst}.

\vpf
\begin{center}
\bpf
\A "$x[A]y, y[B]z, x[C]z, x[G]w, w[H]z \vdash$"
\U [:] "$x[A]y, y[B]z, x[C]z, x[G;H]z \vdash $" "\ref{Mst;}" 
\U [:] "$x[A]y, y[B]z, x[C,(G;H)]z \vdash $" "\ref{Mst,}"
\U [:] "$x[A]y, z[\bullet B]y, x[C,(G;H)]z \vdash $" "\ref{Mstbl}"
\U [:] "$x[A]y, x[(C,(G;H));\bullet B]y \vdash $" "\ref{Mst;}"
\U [:] "$x[A, ((C,(G;H));\bullet B)]y \vdash $" "\ref{Mst,}"
\U [:] "$A, ((C,(G;H));\bullet B) \vdash I$" "\ref{Mstfin}"
\epf
\end{center}

These may be visualized in terms of a graph;
in terms of concrete (representable) relations,
all the sequents express the non-existence of points $x,y,z,w$
related by relations $A,B,C,G,H$ as shown in \fig{5altgph}.

\begin{figure}[htbp]
\begin{center}
\begin{picture}(250,150)(-125,-75)
\thicklines
\put(0,50){\vector(-2,-1){100}} \put(-60,25){$A$}
\put(-100,0){\vector(2,-1){100}} \put(-60,-35){$B$}
\put(0,50){\vector(2,-1){100}} \put(55,25){$G$}
\put(100,0){\vector(-2,-1){100}} \put(55,-30){$H$}
\put(0,50){\vector(0,-1){100}} \put(5,0){$C$}
\put(-110,0){$y$}
\put(105,0){$w$}
\put(0,55){$x$}
\put(0,-60){$z$}
\end{picture}
\end{center}
\caption{Graph corresponding to \M-sequent 
  $x[A]y, y[B]z, x[C]z, x[G]w, w[H]z \vdash$}
\label{5altgph}
\label{fig:5altgph}
\end{figure}

Recall that a simple undirected graph 
is a graph with no loops or multiple edges,
where we do not distinguish edges 
which are between the same pair of points but in 
opposite directions.
A connected graph is a graph where any two vertices are joined by a sequence of
successive edges.
The only simple undirected graph 
on 4 vertices with more edges than the graph in
\fig{5altgph} is the complete graph,
since the only missing edge is the one between $y$ and $w$.
An \M-sequent whose graphical representation
is the complete graph on 4 vertices ($K_4$)
cannot be translated by steps \ref{Mst1} to \ref{Mstlst};
the following theorem explains why this is so.
We call an \M-sequent whose graphical representation is $K_4$ a 
\textbf{\boldmath $K_4$-sequent}\index{K4-sequent@$K_4$-sequent|textbf}.

\begin{thm} \label{thrm:nodeg2}
An \M-sequent, whose corresponding
graph has more than two vertices, has no loops or
multiple edges and has no vertices of degree~2,
cannot be translated using steps \ref{Mst1} to \ref{Mstlst}.
\end{thm}

\proof\
Step \ref{Mst;} is the only step (other than \ref{Mstfin})
which can reduce the number of point variables in a sequent.
Step \ref{Mst;} can only be applied to remove a point variable $y$
which appears in \emph{exactly two} formulae, such as
$x[R]y$ and $y[S]z$, where $x,y$ and $z$ are distinct;
that is, the vertex $y$ in the graph has to be of degree~2.
As the graph has no vertices of degree~2,
step \ref{Mst;} cannot be applied.
As it has no loops or multiple edges,
steps \ref{Mst,}, \ref{Mst;'} and \ref{Mst;`} cannot be applied. 
Steps \ref{Mstmv} and \ref{Mstbl} do not change the shape of the graph,
and step \ref{Mstfin} requires a graph of at most
two vertices and exactly one edge.

Therefore no translation step \ref{Mst1} to \ref{Mstlst} 
can be applied to change the shape of the graph,
so step \ref{Mstfin} can never be applied.
Thus the graph cannot be translated to \dRA. $\Box$

In particular, $K_4$ meets the criteria of \thrm{nodeg2}.
There are also some \M-sequents
whose corresponding graph 
has at most 4 point variables
and is simpler than $K_4$,
but still cannot be translated directly.
These are cases where the graph has more than two vertices of degree~1.

\begin{thm} \label{thrm:3deg1}
An \M-sequent which corresponds to
a graph with more than two vertices of degree~1
cannot be translated using steps \ref{Mst1} to \ref{Mstlst}.
\end{thm}

\proof\
None of the translation steps \ref{Mst1} to \ref{Mstlst} 
creates a new occurrence of a point variable;
that is, no step can
increase the degree of a vertex in the graph.
No step other than \ref{Mstfin} removes the sole occurrence of a point
variable;
that is, no step other than \ref{Mstfin}
can reduce the degree of a vertex to zero 
(or, equivalently, remove a vertex).
As step \ref{Mstfin} requires a graph with at most two vertices,
no translation step can reduce the number of vertices of degree~1,
and so the graph 
cannot be translated using steps \ref{Mst1} to \ref{Mstlst}. $\Box$
%(ie, a sequent with at most two point variables), 

One example is $y[B]z, x[C]z, w[H]z \vdash $,
whose corresponding graph is a 3-pointed star,
as shown in \fig{3star}.

\begin{figure}[htbp]
\begin{center}
\begin{picture}(250,150)(-125,-75)
\thicklines
%\put(0,50){\vector(-2,-1){100}} \put(-60,25){$A$}
\put(-100,0){\vector(2,-1){100}} \put(-60,-35){$B$}
%\put(0,50){\vector(2,-1){100}} \put(55,25){$G$}
\put(100,0){\vector(-2,-1){100}} \put(55,-30){$H$}
\put(0,50){\vector(0,-1){100}} \put(5,0){$C$}
%\put(-100,0){\vector(1,0){200}} \put(-20,5){$D$}
\put(-110,0){$y$}
\put(105,0){$w$}
\put(0,55){$x$}
\put(0,-60){$z$}
\end{picture}
\end{center}
\caption{Graph corresponding to the \M-sequent $y[B]z, x[C]z, w[H]z \vdash $}
\label{3star}
\label{fig:3star}
\end{figure}

Notice that it has no vertices of degree~2
and three vertices of degree~1, and so,
by either \thrm{nodeg2} or \thrm{3deg1},
the \M-sequent cannot be translated using 
steps \ref{Mst1} to \ref{Mstlst}.

These results are essentially negative.
As we shall see, there are some positive results, for
\thrm{trcond} characterizes when an \M-sequent can be translated into
\dRA.

In the case of graphs which cannot be translated because they have
too many vertices of degree~1, 
there is an
equivalent \M-sequent which \emph{can} be translated.
\lem{mtl} can be used to change the \M-sequent, and the graph,
into one which can be translated.

\begin{lemma} \label{lem:misc} \label{lem:mtl}
In \M\ (equivalently, in \Mp),
$\Gamma \vdash \Delta  \iff \Gamma, x [\top] y \vdash \Delta$ 
\end{lemma}

\proof\
The forward direction is an instance of the monotonicity ($M \vdash$) rule.
For the reverse direction cut with the axiom $\vdash x [\top] y$.
$\Box$
 
We now indicate how this lemma can be used to 
turn an \M-sequent into an equivalent one which can be translated using
steps \ref{Mst1} to \ref{Mstlst}.

An \M-sequent such as
$y[B]z, x[C]z, w[H]z \vdash $ has a corresponding graph
which is a 3-pointed star, as shown in \fig{3star}.
To handle this case, we can add a formula $x [\top] y$,
effectively adding a dummy edge from $x$ to $y$ labelled $\top$.
\lem{mtl} shows that the resulting sequent is equivalent in \M.
A similar case is the \M-sequent
$x[G]w, y[B]z \vdash$, whose corresponding graph
consists of two unconnected edges.

Recall from \S\ref{madint} 
that \M-proofs whose sequents contain at most four point
variables characterise the class of relation algebras,
so we are particularly interested in relating 4-sequents and 4-proofs in \M\
to sequents and proofs in \dRA.

In fact, we can use \lem{mtl} 
to translate all \M-sequents with four
point variables other than ones whose graph is either $K_4$,
the graph with four vertices all of degree 3,
or $K_4$ with loops and/or multiple edges.
We define a 
\textbf{\boldmath $K_4^*$-graph}\index{K4*-graph@$K_4^*$-graph|textbf}
to be a graph which is
$K_4$, but possibly with loops or multiple edges added, and a 
\textbf{\boldmath $K_4^*$-sequent}\index{K4*-sequent@$K_4^*$-sequent|textbf}
to be a sequent whose corresponding graph is a $K_4^*$-graph.

\begin{thm} \label{thrm:notK4}
Every \M-sequent containing at most four point variables
can be translated into a \dRA-sequent
using steps \ref{Mst1} to \ref{Mstlst} and \lem{mtl},
if and only if it is not a $K_4^*$-sequent.
%Using \lem{mtl} as well as
%steps \ref{Mst1} to \ref{Mstlst},
%we can translate all \M-sequents with at most four
%point variables, other than $K_4^*$-sequents, into \dRA.
\end{thm} 

\proof\
Suppose the \M-sequent is not a $K_4^*$-sequent,
so its corresponding graph is not a $K_4^*$-graph.
Firstly, use step \ref{Mst,} to collapse multiple edges.
Next, use steps \ref{Mst;'} and \ref{Mst;`} to remove loops.
(In the special case where the vertex which is the endpoints of a loop is not
adjacent to any other edge, first use \lem{mtl} to add such an edge).

Now, as the graph has at most four vertices and is not $K_4$,
it has a vertex of degree 1 or 2.
A vertex of degree~1 can be turned into 
a vertex of degree~2 by using \lem{mtl}.
A vertex of degree~2 can be removed by step \ref{Mst;}.
We now have a graph with at most three vertices. 
It is easy to check that all graphs with at most three vertices
can be translated by steps \ref{Mst1} to \ref{Mstlst}.

If, on the other hand, 
the \M-sequent is a $K_4^*$-sequent,
and its corresponding graph is a $K_4^*$-graph,
then the argument is similar to that of \thrm{nodeg2}.
The graph may have loops or multiple edges,
but applying steps \ref{Mst,}, \ref{Mst;'} and \ref{Mst;`} to these
produces another $K_4^*$-graph.
Steps \ref{Mstmv} and \ref{Mstbl} do not change the shape of the graph.
As a $K_4^*$-graph has no vertices of degree~2,
step \ref{Mst;} can never be applied.
As step \ref{Mstfin} requires a graph of at most two vertices,
the graph cannot be translated to \dRA. 
$\Box$

\renewcommand\cfile{}