\documentclass[11pt,a4paper]{article}
\usepackage[T1]{fontenc}
\usepackage{isabelle,isabellesym}
\usepackage{amssymb,ragged2e}
\usepackage{pdfsetup}

\isabellestyle{it}
\renewenvironment{isamarkuptext}{\par\isastyletext\begin{isapar}\justifying\color{blue}}{\end{isapar}}
\renewcommand\labelitemi{$*$}

\begin{document}

\title{Stone Relation Algebras}
\author{Walter Guttmann}
\maketitle

\begin{abstract}
  We develop Stone relation algebras, which generalise relation algebras by replacing the underlying Boolean algebra structure with a Stone algebra.
  We show that finite matrices over bounded linear orders form an instance.
  As a consequence, relation-algebraic concepts and methods can be used for reasoning about weighted graphs.
  We also develop a fixpoint calculus and apply it to compare different definitions of reflexive-transitive closures in semirings.
\end{abstract}

\tableofcontents

\section{Synopsis and Motivation}

This document describes the following six theory files:
\begin{itemize}
\item Fixpoints develops a fixpoint calculus based on partial orders.
      We also consider least (pre)fixpoints and greatest (post)fixpoints.
      The derived rules include unfold, square, rolling, fusion, exchange and diagonal rules studied in \cite{AartsBackhouseBoitenDoornbosGasterenGeldropHoogendijkVoermansWoude1995}.
      Our results are based on the existence of fixpoints instead of completeness of the underlying structure.
\item Semirings contains a hierarchy of structures generalising idempotent semirings.
      In particular, several of these algebras do not assume that multiplication is associative in order to capture models such as multirelations.
      Even in such a weak setting we can derive several results comparing different definitions of reflexive-transitive closures based on fixpoints.
\item Relation Algebras introduces Stone relation algebras, which weaken the Boolean algebra structure of relation algebras to Stone algebras.
      This is motivated by the wish to represent weighted graphs (matrices over numbers) in addition to unweighted graphs (Boolean matrices) that form relations.
      Many results of relation algebras can be derived from the weaker axioms and therefore also apply to weighted graphs.
      Some results hold in Stone relation algebras after small modifications.
      This allows us to apply relational concepts and methods also to weighted graphs.
      In particular, we prove a number of properties that have been used to verify graph algorithms.
      Tarski's relation algebras \cite{Tarski1941} arise as a special case by imposing further axioms.
\item Subalgebras of Relation Algebras studies the structures of subsets of elements characterised by a given property.
      In particular we look at regular elements (which correspond to unweighted graphs), coreflexives (tests), vectors and covectors (which can be used to represent sets).
      The subsets are turned into Isabelle/HOL types, which are shown to form instances of various algebras.
\item Matrix Relation Algebras lifts the Stone algebra hierarchy, the semiring structure and, finally, Stone relation algebras to finite square matrices.
      These are mostly standard constructions similar to those in \cite{ArmstrongFosterStruthWeber2016,ArmstrongGomesStruthWeber2016} implemented so that they work for many algebraic structures.
      In particular, they can be instantiated to weighted graphs (see below) and extended to Kleene algebras (not part of this development).
\item Matrices over Bounded Linear Orders studies relational properties.
      In particular, we characterise univalent, injective, total, surjective, mapping, bijective, vector, covector, point, atom, reflexive, coreflexive, irreflexive, symmetric, antisymmetric and asymmetric matrices.
      Definitions of these properties are taken from relation algebras and their meaning for matrices over bounded linear orders (weighted graphs) is explained by logical formulas in terms of matrix entries.
\end{itemize}
Following a refactoring, the selection of components of a graph in Stone relation algebras, which was originally part of Nicolas Robinson-O'Brien's theory \texttt{Relational\_Minimum\_Spanning\_Trees/Boruvka.thy}, has been moved into a new theory in this entry.

The development is based on a theory of Stone algebras \cite{Guttmann2016b} and forms the basis for an extension to Kleene algebras to capture further properties of graphs.
We apply Stone relation algebras to verify Prim's minimum spanning tree algorithm in Isabelle/HOL in \cite{Guttmann2016c}.

Related libraries for semirings and relation algebras in the Archive of Formal Proofs are \cite{ArmstrongFosterStruthWeber2016,ArmstrongGomesStruthWeber2016}.
The theory \texttt{Kleene\_Algebra/Dioid.thy} introduces a number of structures that generalise idempotent semirings, but does not cover most of the semiring structures in the present development.
The theory \texttt{Relation\_Algebra/Relation\_Algebra.thy} covers Tarski's relation algebras and hence cannot be reused for the present development as most properties need to be derived from the weaker axioms of Stone relation algebras.
The matrix constructions in theories \texttt{Kleene\_Algebra/Inf\_Matrix.thy} and \texttt{Relation\_Algebra/Relation\_Algebra\_Models.thy} are similar, but have strong restrictions on the matrix entry types not appropriate for many algebraic structures in the present development.
We also deviate from these hierarchies by basing idempotent semirings directly on the Isabelle/HOL semilattice structures instead of a separate structure; this results in a somewhat smoother integration with the lattice structure of relation algebras.

\begin{flushleft}
\input{session}
\end{flushleft}

\bibliographystyle{abbrv}
\bibliography{root}

\end{document}

