\section{Peirce algebras -- modelling software} \label{Peirce-appl}

As discussed in \S4.1 of \cite{BBS}, Peirce algebras can be used 
where programs are modelled as binary relations,
and in \S\ref{Peirce}, we showed how relation algebras capture the
essence of Peirce algebras.

A program fragment (or command) $C$ can be modelled as a binary relation 
on machine states, where the pair 
(\textit{pre},\textit{post}) refers to
the command $C$ being executed when the machine is in the initial state 
\textit{pre} and terminating in state \textit{post}.
The relation $R$ which represents a command $C$ is such that
$(\textit{pre},\textit{post}) \in R$
if and only if, when $C$ is executed from initial state \textit{pre}, and
terminates, then \textit{post} is one of the states in which it can terminate.
(Thus a \emph{relation}, as opposed to a \emph{function},
can represent a non-deterministic program, or
an incomplete program specification).
Henceforth we will use the same symbol to denote the command and the relation.
When we model a program in this way, 
composition of commands $C;D$ (where `;' represents sequencing of commands)
is represented as relational composition $C \circ D$.
A conditional statement of the form
\texttt{if} $\phi$ \texttt{then} $C$
would be modelled as 
$(\Phi \land C) \lor (\lnot \Phi \land \1)$,
where $\Phi$ denotes the set of (\textit{pre},\textit{post})
pairs such that \textit{pre} satisfies $\phi$, ie
$\Phi = \{(s,t) \,|\, \phi(s)\}$.
(Recall that \1 is the identity relation, here 
$\{(s,s) \,|\, s \textrm{ is a state}\}$,
and represents the null command, which does not affect the 
machine state.)

We then ask how to model a loop of the form
\texttt{while} $\phi$ \texttt{do} $C$.
If we let $L$ represent this loop, we have that
$L$ is also \texttt{if} $\phi$ \texttt{then} $\{C;L\}$,
so we have
$L = (\Phi \land (C \circ L)) \lor (\lnot \Phi \land \1)$.

In another way of viewing the while loop,
the possibility that $C$ is not executed at all is represented by
$ (\lnot \Phi \land \1)$, as before.
But if $C$ is executed, then the first iteration can be represented by
$(\Phi \land C)$,
and this first iteration is then followed by executing $L$,
giving
$L = ((\Phi \land C) \circ L) \lor (\lnot \Phi \land \1)$.

Clearly we would like to show that the two views of the while
loop are the same.
Now, as $\Phi = \{(s,t) \,|\, \phi(s)\}$,
$\Phi = A \circ \top$, where $A = \{(s,s) \,|\, \phi(s)\}$.
Then theorem \ttdef{th56sr} (see \page{th56sr}),
with the structural operators 
`$I$'~`;'~`,' changed to the logical ones `$\top $'~`$ \circ $'~`$ \land$',
gives the equality of 
$\Phi \land (C \circ L)$ and
$(\Phi \land C) \circ L$, whence
the two representations of $L$ are equal.
(In fact, the above example was the reason for attempting the
theorem \texttt{th56sr} in the first place).

This illustrates how a proof system for relation algebras may potentially be
applicable in reasoning about software programs.

\section{Window inference}

In classical (2-valued) propositional logic, a term such as
$A \land B$ can be simplified by focussing on the sub-term $B$, and 
rewriting $B$ under the assumption that $A = \top$.
Thus $D \land (D \land C)$ would be rewritten to 
$D \land (\top \land C)$, and so to $D \land C$;
similarly $D \land (D \lor C)$ would be rewritten to 
$D \land (\top \lor C)$, and then to $D \land \top$ and to $D$.

The justification for this is that if $A$ is $\bot$, then so is
$A \land B$, regardless of what change is made to $B$;
if, on the other hand, $A$ is $\top$, then the rewriting is obviously sound.
Corresponding context-dependent rewrite rules are available for 
terms other than conjunctions, such as $A \lor B$, $A \supset B$, etc.

This principle is used in the ``window inference'' paradigm of
Robinson \& Staples \cite{wi}, and developed by Grundy \cite{jgwi},
where the user focusses on $B$ by putting it in
its own window in a prover based on a graphical user interface.

Focussing on a particular sub-term $B$ has an obvious resemblance to 
displaying a sub-structure in Display Logic; it would be interesting to see if
the principles of Display Logic can be used in window inference, or vice
versa.

\section{Soundness and completeness}

In \S\ref{provRA} we have used Isabelle
to show that \dRA\ is complete, in that
theorems of \RA\ are provable in \dRA.
In Chapters \ref{ch:gord} and \ref{ch:mad} 
we have shown that the systems \NRA\ and \M\ are sound
(with respect to \dRA\ and so to \RA), by showing
that proofs of relational equations or inequalities
in these systems can be mimicked in \dRA.

There are corresponding converse results which we have not shown.
The converse to \S\ref{provRA} would be to use Isabelle
to show that any \dRA-proof could be turned into
a proof in \RA;
this would demonstrate mechanically the soundness of
\dRA\ (with respect to \RA), which is
Theorem 4 of Gor\'e \cite{dRA}.

For \NRA\ and \M, the converse results would be to show that 
any theorem of \dRA,
when expressed in the appropriate form, could be proved in these systems.
This could be done by showing that any \dRA-proof could be turned into
a proof in \NRA\ or \M.
This would show that \NRA\ and \M\ are complete.

In the case of \M\ this would mean translating each \dRA-sequent into an
\M-sequent: an indication of the procedure is given in \S\ref{trans}.
However the difficult problem would be to produce a proof in \M\
using at most \emph{four} point variables.

\section{Embedding in an atomic relation algebra}
\label{atomic}

An \textbf{atom}\index{atom|textbf} in a Boolean algebra is 
an element that is not the join of smaller elements
(intuitively, like a singleton set);
a Boolean algebra is 
\textbf{atomic}\index{relation algebra!atomic|textbf}
if every element is a join of atoms.
Although Oheimb \& Gritzner \cite{RALL}
appear to say that every relation algebra is atomic,
this is clearly not the case.

\begin{lemma} \label{lem:non-atomic}
There is a non-atomic Boolean algebra $\mathcal L$.
\end{lemma} 
\proof\
We construct such an algebra on the set $\mathbb Z$.
Define a set $P \subseteq \mathbb Z$ to be \emph{periodic}
%if it is of the form 
%$\{q + kn \,|\, q \in Q, k \in \mathbb Z\}$, 
%for some $Q \subseteq \mathbb Z$ and $n \in \mathbb Z$.
if it satisfies $P = P + n$ for some non-zero integer $n$ 
(which is the \emph{period}),
where $P + n$ is defined as $\{p + n \,|\, p \in P\}$.
(Then $P$ is also periodic with period $kn$, for any non-zero integer $k$).
Then the complement, union and intersection of periodic sets are
periodic.
For suppose $P$ and $Q$ are periodic with periods $n$ and $m$.
Then they are both periodic with period $nm$, and we have
$$ (P \cup Q) + nm = (P + nm) \cup (Q + nm) = P \cup Q $$
and so $P \cup Q$ is periodic.
Similarly $P \cap Q$ is periodic, and it is easy to see that the
complement $\lnot P = \mathbb Z \setminus P$
(where $ \setminus $ denotes set difference) is periodic.
Thus the periodic subsets of $\mathbb Z$ form a Boolean algebra 
$\mathcal L$, with top $\mathbb Z$ and bottom $\emptyset$.
Clearly any non-empty periodic set contains a properly smaller periodic set,
so $\mathcal L$ has no atoms, and cannot be atomic. $\Box$

\begin{thm} \label{notatom}
There is a non-atomic relation algebra $\mathcal R$.
\end{thm}
\proof\
Let $\mathcal L$ be a non-atomic Boolean algebra on a set $U$,
such as that defined in \lem{non-atomic}.
Let $\mathcal R$ be the proper relation algebra on the 
set $U = \mathbb Z$, defined by 
$\mathcal R = \{ i(L) \,|\, L \in \mathcal L\}$
where $i(L) = \{(l,l) \,|\, l \in L\}$,
$\1 = \top = i(\mathbb Z)$, $\0 = \bot = \emptyset$,
and $\lnot A = i(\mathbb Z) \setminus A$.
%where $ \setminus $ denotes set difference.
Noting that $i(A) \circ i(B) = i(A) \cap i(B) = i(A \cap B)$,
we have that $\mathcal R$ is closed under the relational operations
and so is a relation algebra.
As a Boolean algebra, it is isomorphic to $\mathcal L$ and so is non-atomic.
$\Box$

Oheimb \& Gritzner's proof system, RALL \cite{RALL} (see \S\ref{RALL}),
makes heavy use of the atomicity of relation algebras.
The basis for using the atomic structure is the theorem (\cite{RALL}, Thm.~2)
that a relation algebra can be
represented as a ``relational atom structure",
which enables a relation algebra to be considered in terms of its atoms.
It seems possible, using this structure, to prove some theorems 
more simply than from the relation algebra axioms.
At the conference where \cite{RALL} was presented, Oheimb stated
that the paper and the proof system was meant to refer only to
atomic relation algebras.
Thus the proof system described by them applies (directly) only
to atomic relation algebras.
%As it is based on the atomic structure of relation algebras,
%it applies only to atomic relation algebras.

However every relation algebra can be \emph{embedded}
in an atomic relation algebra (see \cite{JTII}, Thm.~4.21 or
\cite{CylII}, Thm.~5.3.6).
It would seem therefore, that there is a possibility of using this
atomic structure to provide proof techniques which apply also to
non-atomic relation algebras.

\section{The place of (cut) in \M} \label{mad-cut}

As was observed in \S\ref{intro-mad}
proofs in \M\ may require the (cut) rule;
Maddux \cite{seqra} gives an example of a sequent which is 4-provable 
without using (cut), but 3-provable only using (cut).
However, the formula 
$x[\1 \circ R]y \vdash x[R]y$
cannot be proved without using (cut), regardless of how many variables are
allowed.
The following is a proof using (cut).

\comment{
\bpf
\A "$z[R]y \vdash z[R]y$"
\U "$z[R]y \vdash y[\smile R]z $" "($\vdash \smile $)"
\U "$y[\lnot \smile R]z, z[R]y \vdash $" "($\lnot \vdash $)"
\U "$z[R]y \vdash y[\lnot \lnot \smile R]z $" "($\vdash \lnot $)"
\U "to (1) below"
\epf 
\hfill
\bpf
\A "$ x[R]y \vdash x[R]y$" 
\U "$ y[\smile R]x \vdash x[R]y$" "($\smile \vdash $)"
\U "$ \vdash y[\lnot \smile R]x, x[R]y$" "($\vdash \lnot $)"
\U "$ y[\lnot \lnot \smile R]x \vdash x[R]y$" "($\lnot \vdash $)"
\U "to (2) below"
\epf 
\vpf
\begin{center}
\bpf
\A "(1)"
\A "$y[\lnot \smile R]z \vdash y[\lnot \smile R]z $" 
\U "$x[\1]z,  y[\lnot \smile R]x \vdash y[\lnot \smile R]z $" "(Id)"
\U "$x[\1]z, y[\lnot \lnot \smile R]z, y[\lnot \smile R]x \vdash $" 
"($\lnot \vdash $)"
\B [2em] "$x[\1]z, z[R]y, y[\lnot \smile R]x \vdash $" "(cut)"
\U "$x[\1]z, z[R]y \vdash y[\lnot \lnot \smile R]x$" "($\vdash \lnot $)"
\A "(2)"
\B [2em] "$x[\1]z, z[R]y \vdash x[R]y$" "(cut)"
\U "$x[\1 \circ R]y \vdash x[R]y$" "($\circ \vdash $)"
\epf
\end{center}

\bpf
\A "$ x[R]y \vdash x[R]y$" 
\U "$ y[\smile R]x \vdash x[R]y$" "($\smile \vdash $)"
\U "$ \vdash y[\lnot \smile R]x, x[R]y$" "($\vdash \lnot $)"
\U "to (2) below"
\epf 
\hfill
\bpf
\A "$z[R]y \vdash z[R]y$"
\U "$z[R]y \vdash y[\smile R]z $" "($\vdash \smile $)"
\U "$y[\lnot \smile R]z, z[R]y \vdash $" "($\lnot \vdash $)"
\U "to (1) below"
\epf 
\vpf
\begin{center}
\bpf
\A "(2)"
\A "$y[\lnot \smile R]z \vdash y[\lnot \smile R]z $" 
\U "$x[\1]z,  y[\lnot \smile R]x \vdash y[\lnot \smile R]z $" "(Id)"
\A "(1)"
\B [2em] "$x[\1]z, z[R]y, y[\lnot \smile R]x \vdash $" "(cut)"
\B [2em] "$x[\1]z, z[R]y \vdash x[R]y$" "(cut)"
\U "$x[\1 \circ R]y \vdash x[R]y$" "($\circ \vdash $)"
\epf
\end{center}
}

\vpf
\begin{center}
\bpf
\A "$ x[R]y \vdash x[R]y$" 
\U "$ y[\smile R]x \vdash x[R]y$" "($\smile \vdash $)"
\U "$ \vdash y[\lnot \smile R]x, x[R]y$" "($\vdash \lnot $)"
\U "$\downarrow$"
\U ['] "$\downarrow$"
\U ['] "$\downarrow$"
\U ['] "$\downarrow$"
\A "$y[\lnot \smile R]z \vdash y[\lnot \smile R]z $" 
\U "$x[\1]z,  y[\lnot \smile R]x \vdash y[\lnot \smile R]z $" "(Id)"

\A "$z[R]y \vdash z[R]y$"
\U "$z[R]y \vdash y[\smile R]z $" "($\vdash \smile $)"
\U "$y[\lnot \smile R]z, z[R]y \vdash $" "($\lnot \vdash $)"

\U "$\downarrow$"
\U ['] "$\downarrow$"
\U ['] "$\downarrow$"
\B [-2em] "$x[\1]z, z[R]y, y[\lnot \smile R]x \vdash $" "(cut)"
\B [-4em] "$x[\1]z, z[R]y \vdash x[R]y$" "(cut)"
\U "$x[\1 \circ R]y \vdash x[R]y$" "($\circ \vdash $)"
\epf
\end{center}



Now the ($\circ \vdash $) is clearly the only rule (other than
(cut) or the monotonicity rules) that could be applied at the bottom step;
(Id) is the only rule that can introduce $x[\1]z$,
so it is clear that the use of (cut) is unavoidable.
Note that \Mp\ uses (cut) heavily; it is used to derive all the \M\ rules.

Further work in this area might involve
\begin{itemize} \shrinklist{0.5}
\item[--] finding a version $\mathcal M''$ of the calculus \M\ that enjoys
cut-elimination
%set of axioms and rules whereby use of the (cut) rule can be eliminated
\item[--] investigating the relationships between $MA_n$ for various $n$,
and the classes of sequents that can be proved without using (cut),
using at most $n$ variables, for various $n$
\end{itemize}

\section{Further enhancements to the Isabelle code}

The following are also possible areas for further work.
\begin{itemize} \shrinklist{0.5}
\item[--] enhancing the flip tactics to make them more robust (see \S\ref{flip})
\item[--] allowing the user to specify the search strategy in the
search-and-replace tactics, as suggested on \page{fwconv}
\item[--] automatically converting a proof in one system (eg the Chin \& Tarski
axiomatization, or the Gordeev system) to \dRA, or vice-versa
\item[--] finding a procedure, for use in \texttt{C8} (\page{C8}),
which works where arbitrary derived
rules are used to introduce the cut-formula $A$
\item[--] automatically checking, for a given set of Display Logic rules,
whether they satisfy the conditions (C1) to (C8) of Belnap's
cut elimination theorem \cite{Bel}
\end{itemize}