From 0757c0221a6dbaf18bdb7cdfedcf7c1fb94211b2 Mon Sep 17 00:00:00 2001
From: Tim Daly
Date: Mon, 9 Oct 2017 19:30:26 0400
Subject: [PATCH] books/bookvol10.1 add Doye's Coercion Algorithm chapter
Goal: Axiom Literate Programming

books/Makefile.pamphlet  112 +
books/bookheader.tex  168 +
books/bookvol10.1.pamphlet  5593 +++++++++++++++++++++++++++++++++++++++
changelog  4 +
patch  133 +
src/axiomwebsite/patches.html  2 +
6 files changed, 5723 insertions(+), 289 deletions()
diff git a/books/Makefile.pamphlet b/books/Makefile.pamphlet
index 75b7549..f2f3fae 100644
 a/books/Makefile.pamphlet
+++ b/books/Makefile.pamphlet
@@ 58,55 +58,6 @@ COOKPAGES = ${COOKBOOK}/eucdomgcd.pdf
\end{chunk}
\section{Signature file}
Axiom's bookheader.tex file specifies a file of signatures created
from calls to the latex sig macro (mostly used in the compiler and
interpreter files).

These signature files need to be sorted by function name.

A typical signature entry reads:
\begin{verbatim}
\hyperpage {301}\hskip 1em\relax mkprompt : Void $\rightarrow $ String
\end{verbatim}

We read the generated signatures.tex file, sort it on function name,
and write signatures.sort which gets read as input to the latex step.

We do this by invoking gcl with the following progn before the last
latex is complete.
\begin{chunk}{sortsig.lisp}
; sort the signatures file based on function name, if it exists
(progn

(defun sortsig ()
 (labels (
 (selectFunctionName (sig)
 (readfromstring (subseq sig (+ 6 (search "relax" sig :test #'string=)))))
 (readSignatures ()
 (withopenfile (sigfile "signatures.tex")
 (loop for line = (readline sigfile nil)
 while line
 unless (string= line "") collect line)))
 (writeSignatures (siglist)
 (withopenfile (sigfile "signatures.sort" :direction :output)
 (loop for sig in siglist
 do (writeline sig sigfile)
 (terpri sigfile))))
 )
 (when (probefile "signatures.tex")
 (writeSignatures (sort (readSignatures) #'string< :key #'selectFunctionName)))))

(sortsig)
(quit)
)

\end{chunk}

\begin{chunk}{gclbin}
GCLBIN=${MNT}/${SYS}/bin/${GCLVERSION}
\end{chunk}

\section{The Makefile}
\begin{chunk}{*}
SHELL=bash
@@ 125,23 +76,16 @@ COOKIN=${BOOKS}/cookbook
COOKBOOK=${PDF}/cookbook
\getchunk{cookbook}
\getchunk{gclbin}
\getchunk{sourcecode}
PROVE=${PROOFS}/acl2.lisp ${PROOFS}/coq.lisp
OTHER= ${PDF}/refcard.pdf ${PDF}/endpaper.pdf ${PDF}/rosetta.pdf
all: announce tanglecopy sortsig ${PDF}/axiom.bib ${PROVE} ${OTHER} \
 ${COOKPAGES} ${BOOKPDF} ${PDF}/toc.pdf spadedit axbook
+all: announce tanglecopy ${PDF}/axiom.bib ${PROVE} ${OTHER} ${COOKPAGES} \
+ ${BOOKPDF} ${PDF}/toc.pdf spadedit axbook
@(cd ${PDF} ; ${RM} *.out *.toc *.sty *.def *.png *.bbl *.blg)
sortsig:
 @ echo ==================================
 @ echo EXTRACTING SORTSIG
 @ echo ==================================
 @ ${BOOKS}/tanglec Makefile.pamphlet sortsig.lisp >${PDF}/sortsig.lisp

tanglecopy:
@ echo ==================================
@ echo COPY TANGLEC TO BIN
@@ 242,6 +186,54 @@ ${COOKBOOK}/%.pdf: ${COOKIN}/%.pamphlet
${RM} $*.ilg $*.ind *.bbl *.blg *.sty)
+${PDF}/bookvol10.1.pdf: ${IN}/bookvol10.1.pamphlet \
+ ${PDF}/axiom.bib ${PDF}/axiom.bst
+ @ echo ===========================================
+ @ echo making ${PDF}/bookvol10.1.pdf from ${IN}/bookvol10.1.pamphlet
+ @ echo ===========================================
+ @(cd ${PDF} ; \
+ cp ${BOOKS}/*.sty ${PDF} ; \
+ cp ${IN}/bookvol10.1.pamphlet ${PDF} ; \
+ cp ${IN}/bookheader.tex ${PDF} ; \
+ cp pr ${IN}/ps ${PDF} ; \
+ ${RM} bookvol10.1.toc ; \
+ touch signatures.tex ; \
+ touch bookvol10.1.sigs ; \
+ if [ z "${NOISE}" ] ; then \
+ ${LATEX} bookvol10.1.pamphlet ; \
+ cp signatures.tex bookvol10.1.sigs ; \
+ ${MAKEINDEX} bookvol10.1.idx 1>/dev/null 2>/dev/null ; \
+ ${BIBTEX} bookvol10.1.aux ; \
+ ${LATEX} bookvol10.1.pamphlet >/dev/null ; \
+ ${LATEX} bookvol10.1.pamphlet >/dev/null ; \
+ ${DVIPS} bookvol10.1.dvi 2>/dev/null ; \
+ ${PS2PDF} bookvol10.1.ps 2>/dev/null ; \
+ ${RM} bookvol10.1.aux bookvol10.1.dvi bookvol10.1.log \
+ ${RM} bookvol10.1.ps bookvol10.1.idx bookvol10.1.tex \
+ ${RM} bookvol10.1.pamphlet ; \
+ ${RM} bookvol10.1.ilg bookvol10.1.ind *.sigs signatures.tex ; \
+ ${RM} bookheader.tex ; \
+ else \
+ ${LATEX} bookvol10.1.pamphlet >${TMP}/trace ; \
+ cp signatures.tex bookvol10.1.sigs ; \
+ ${MAKEINDEX} bookvol10.1.idx 1>/dev/null 2>/dev/null ; \
+ ${BIBTEX} bookvol10.1.aux 1>/dev/null 2>/dev/null ; \
+ ${LATEX} bookvol10.1.pamphlet >${TMP}/trace ; \
+ ${LATEX} bookvol10.1.pamphlet >${TMP}/trace ; \
+ ${DVIPDFM} bookvol10.1.dvi 2>${TMP}/trace ; \
+ ${RM} bookvol10.1.aux bookvol10.1.dvi bookvol10.1.log \
+ ${RM} bookvol10.1.ps bookvol10.1.idx bookvol10.1.tex \
+ ${RM} bookvol10.1.pamphlet ; \
+ ${RM} bookvol10.1.ilg bookvol10.1.ind ; \
+ ${RM} bookvol10.1.ilg bookvol10.1.ind *.sigs signatures.tex ; \
+ ${RM} bookheader.tex ; \
+ fi ; \
+ ${RM} bookvol10.1.aux bookvol10.1.dvi bookvol10.1.log \
+ ${RM} bookvol10.1.ps bookvol10.1.idx bookvol10.1.tex \
+ ${RM} bookvol10.1.pamphlet ; \
+ ${RM} bookvol10.1.ilg bookvol10.1.ind ; \
+ ${RM} bookheader.tex )
+
${PDF}/%.pdf: ${IN}/%.pamphlet ${PDF}/axiom.bib ${PDF}/axiom.bst
@ echo ===========================================
@ echo making ${PDF}/$*.pdf from ${IN}/$*.pamphlet
@@ 260,7 +252,6 @@ ${PDF}/%.pdf: ${IN}/%.pamphlet ${PDF}/axiom.bib ${PDF}/axiom.bst
${MAKEINDEX} $*.idx 1>/dev/null 2>/dev/null ; \
${BIBTEX} $*.aux ; \
${LATEX} $*.pamphlet >/dev/null ; \
 cat sortsig.lisp  ${GCLBIN} >/dev/null ; \
${LATEX} $*.pamphlet >/dev/null ; \
${DVIPDFM} $*.dvi 2>/dev/null ; \
${RM} $*.aux $*.dvi $*.log $*.ps $*.idx $*.tex $*.pamphlet ; \
@@ 272,12 +263,11 @@ ${PDF}/%.pdf: ${IN}/%.pamphlet ${PDF}/axiom.bib ${PDF}/axiom.bst
${MAKEINDEX} $*.idx 1>/dev/null 2>/dev/null ; \
${BIBTEX} $*.aux 1>/dev/null 2>/dev/null ; \
${LATEX} $*.pamphlet >${TMP}/trace ; \
 cat sortsig.lisp  ${GCLBIN} >/dev/null ; \
${LATEX} $*.pamphlet >${TMP}/trace ; \
${DVIPDFM} $*.dvi 2>${TMP}/trace ; \
${RM} $*.aux $*.dvi $*.log $*.ps $*.idx $*.tex $*.pamphlet ; \
${RM} $*.ilg $*.ind ; \
# ${RM} $*.ilg $*.ind *.sigs signatures.tex ; \
+ ${RM} $*.ilg $*.ind *.sigs signatures.tex ; \
${RM} bookheader.tex ; \
fi ; \
${RM} $*.aux $*.dvi $*.log $*.ps $*.idx $*.tex $*.pamphlet ; \
diff git a/books/bookheader.tex b/books/bookheader.tex
index a773b84..8368ded 100644
 a/books/bookheader.tex
+++ b/books/bookheader.tex
@@ 12,16 +12,31 @@ citecolor=red}
\usepackage{catmac} % for Weber chapter in vol 10.1
\usepackage{dissdef} % for Weber chapter in vol 10.1
+\newtheorem{DoyeTheorem}[subsection]{Theorem}
+\newtheorem{DoyeDefinition}[subsection]{Definition}
+\newtheorem{DoyeExample}[subsection]{Example}
+\newtheorem{DoyeNotation}[subsection]{Notation}
+\newtheorem{DoyeConjecture}[subsection]{Conjecture}
+\newtheorem{DoyeCorollary}[subsection]{Corollary}
+\newtheorem{DoyeLemma}[subsection]{Lemma}
+\newtheorem{DoyeAssumption}[subsection]{Assumption}
+\newtheorem{DoyeAlgorithm}[subsection]{Algorithm}
+\newcommand*{\QED}{\hfill\ensuremath{\blacksquare}} % for qed
+
\setlength{\textwidth}{400pt}
\makeindex
\usepackage{graphicx}
\usepackage{changepage} % for adjustwidth environment
+\usepackage{pstnode} % for commutative diagrams
\newwrite\sigfile
+%\usepackage{breakurl}
+%\def\UrlBreaks{\do\/\do\} % linebreaking urls
+
\begin{document}
\immediate\openout\sigfile=signatures.tex
\frontmatter
\setcounter{secnumdepth}{1}
+\setcounter{secnumdepth}{2}
\begin{titlepage}
\center{\includegraphics{ps/axiomfront.ps}}
\vskip 0.1in
@@ 105,86 +120,85 @@ influence on Axiom development.
\begin{tabular}{lll}
Michael Albaugh & Cyril Alberga & Roy Adler\\
Christian Aistleitner & Richard Anderson & George Andrews\\
Jerry Archibald & S.J. Atkins & Jeremy Avigad\\
Henry Baker & Martin Baker & Stephen Balzac\\
Yurij Baransky & David R. Barton & Thomas Baruchel\\
Gerald Baumgartner & Gilbert Baumslag & Michael Becker\\
Nelson H. F. Beebe & Jay Belanger & David Bindel\\
Fred Blair & Vladimir Bondarenko & Mark Botch\\
Raoul Bourquin & Alexandre Bouyer & Karen Braman\\
Wolfgang Brehm & Peter A. Broadbery & Martin Brock\\
Manuel Bronstein & Christopher Brown & Stephen Buchwald\\
Florian Bundschuh & Luanne Burns & William Burge\\
Ralph Byers & Quentin Carpent & Pierre Casteran\\
Robert Cavines & Bruce Char & Ondrej Certik\\
TzuYi Chen & Bobby Cheng & Cheekai Chin\\
David V. Chudnovsky & Gregory V. Chudnovsky & Mark Clements\\
James Cloos & Jia Zhao Cong & Josh Cohen\\
Christophe Conil & Don Coppersmith & George Corliss\\
Robert Corless & Gary Cornell & Meino Cramer\\
Jeremy Du Croz & David Cyganski & Nathaniel Daly\\
Timothy Daly Sr. & Timothy Daly Jr. & James H. Davenport\\
David Day & James Demmel & Didier Deshommes\\
Michael Dewar & Inderjit Dhillon & Jack Dongarra\\
Jean Della Dora & Gabriel Dos Reis & Claire DiCrescendo\\
Sam Dooley & Zlatko Drmac & Lionel Ducos\\
Iain Duff & Lee Duhem & Martin Dunstan\\
Brian Dupee & Dominique Duval & Robert Edwards\\
HansDieter Ehrich & Heow EideGoodman & Lars Erickson\\
Mark Fahey & Richard Fateman & Bertfried Fauser\\
Stuart Feldman & John Fletcher & Brian Ford\\
Albrecht Fortenbacher & George Frances & Constantine Frangos\\
Timothy Freeman & Korrinn Fu & Marc Gaetano\\
Rudiger Gebauer & Van de Geijn & Kathy Gerber\\
Patricia Gianni & Gustavo Goertkin & Samantha Goldrich\\
Holger Gollan & Teresa GomezDiaz & Laureano GonzalezVega\\
Stephen Gortler & Johannes Grabmeier & Matt Grayson\\
Klaus Ebbe Grue & James Griesmer & Vladimir Grinberg\\
Oswald Gschnitzer & Ming Gu & Jocelyn Guidry\\
Gaetan Hache & Steve Hague & Satoshi Hamaguchi\\
Sven Hammarling & Mike Hansen & Richard Hanson\\
Richard Harke & Bill Hart & Vilya Harvey\\
Martin Hassner & Arthur S. Hathaway & Dan Hatton\\
Waldek Hebisch & Karl Hegbloom & Ralf Hemmecke\\
Henderson & Antoine Hersen & Nicholas J. Higham\\
Hoon Hong & Roger House & Gernot Hueber\\
Pietro Iglio & Alejandro Jakubi & Richard Jenks\\
Bo Kagstrom & William Kahan & Kyriakos Kalorkoti\\
Kai Kaminski & Grant Keady & Wilfrid Kendall\\
Tony Kennedy & David Kincaid & Keshav Kini\\
+S.J. Atkins & Jeremy Avigad & Henry Baker\\
+Martin Baker & Stephen Balzac & Yurij Baransky\\
+David R. Barton & Thomas Baruchel & Gerald Baumgartner\\
+Gilbert Baumslag & Michael Becker & Nelson H. F. Beebe\\
+Jay Belanger & David Bindel & Fred Blair\\
+Vladimir Bondarenko & Mark Botch & Raoul Bourquin\\
+Alexandre Bouyer & Karen Braman & Wolfgang Brehm\\
+Peter A. Broadbery & Martin Brock & Manuel Bronstein\\
+Christopher Brown & Stephen Buchwald & Florian Bundschuh\\
+Luanne Burns & William Burge & Ralph Byers\\
+Quentin Carpent & Pierre Casteran & Robert Cavines\\
+Bruce Char & Ondrej Certik & TzuYi Chen\\
+Bobby Cheng & Cheekai Chin & David V. Chudnovsky\\
+Gregory V. Chudnovsky & Mark Clements & James Cloos\\
+Jia Zhao Cong & Josh Cohen & Christophe Conil\\
+Don Coppersmith & George Corliss & Robert Corless\\
+Gary Cornell & Meino Cramer & Jeremy Du Croz\\
+David Cyganski & Nathaniel Daly & Timothy Daly Sr.\\
+Timothy Daly Jr. & James H. Davenport & David Day\\
+James Demmel & Didier Deshommes & Michael Dewar\\
+Inderjit Dhillon & Jack Dongarra & Jean Della Dora\\
+Gabriel Dos Reis & Claire DiCrescendo & Sam Dooley\\
+Zlatko Drmac & Lionel Ducos & Iain Duff\\
+Lee Duhem & Martin Dunstan & Brian Dupee\\
+Dominique Duval & Robert Edwards & Heow EideGoodman\\
+Lars Erickson & Mark Fahey & Richard Fateman\\
+Bertfried Fauser & Stuart Feldman & John Fletcher\\
+Brian Ford & Albrecht Fortenbacher & George Frances\\
+Constantine Frangos & Timothy Freeman & Korrinn Fu\\
+Marc Gaetano & Rudiger Gebauer & Van de Geijn\\
+Kathy Gerber & Patricia Gianni & Gustavo Goertkin\\
+Samantha Goldrich & Holger Gollan & Teresa GomezDiaz\\
+Laureano GonzalezVega & Stephen Gortler & Johannes Grabmeier\\
+Matt Grayson & Klaus Ebbe Grue & James Griesmer\\
+Vladimir Grinberg & Oswald Gschnitzer & Ming Gu\\
+Jocelyn Guidry & Gaetan Hache & Steve Hague\\
+Satoshi Hamaguchi & Sven Hammarling & Mike Hansen\\
+Richard Hanson & Richard Harke & Bill Hart\\
+Vilya Harvey & Martin Hassner & Arthur S. Hathaway\\
+Dan Hatton & Waldek Hebisch & Karl Hegbloom\\
+Ralf Hemmecke & Henderson & Antoine Hersen\\
+Nicholas J. Higham & Hoon Hong & Roger House\\
+Gernot Hueber & Pietro Iglio & Alejandro Jakubi\\
+Richard Jenks & Bo Kagstrom & William Kahan\\
+Kyriakos Kalorkoti & Kai Kaminski & Grant Keady\\
+Wilfrid Kendall & Tony Kennedy & David Kincaid\\
+Keshav Kini & Ted Kosan & Paul Kosinski\\
+Igor Kozachenko & Fred Krogh & Klaus Kusche\\
\end{tabular}
\vfill
\newpage
\begin{tabular}{lll}
Ted Kosan & Paul Kosinski & Igor Kozachenko\\
Fred Krogh & Klaus Kusche & Bernhard Kutzler\\
Tim Lahey & Larry Lambe & Kaj Laurson\\
Charles Lawson & George L. Legendre & Franz Lehner\\
Frederic Lehobey & Michel Levaud & Howard Levy\\
J. Lewis & RenCang Li & Rudiger Loos\\
Craig Lucas & Michael Lucks & Richard Luczak\\
Camm Maguire & Francois Maltey & Osni Marques\\
Alasdair McAndrew & Bob McElrath & Michael McGettrick\\
Edi Meier & Ian Meikle & David Mentre\\
Victor S. Miller & Gerard Milmeister & Mohammed Mobarak\\
H. Michael Moeller & Michael Monagan & Marc MorenoMaza\\
Scott Morrison & Joel Moses & Mark Murray\\
William Naylor & Patrice Naudin & C. Andrew Neff\\
John Nelder & Godfrey Nolan & Arthur Norman\\
Jinzhong Niu & Michael O'Connor & Summat Oemrawsingh\\
Kostas Oikonomou & Humberto OrtizZuazaga & Julian A. Padget\\
Bill Page & David Parnas & Susan Pelzel\\
Michel Petitot & Didier Pinchon & Ayal Pinkus\\
Frederick H. Pitts & Frank Pfenning & Jose Alfredo Portes\\
E. QuintanaOrti & Gregorio QuintanaOrti & Beresford Parlett\\
A. Petitet & Andre Platzer & Peter Poromaas\\
Claude Quitte & Arthur C. Ralfs & Norman Ramsey\\
Anatoly Raportirenko & Guilherme Reis & Huan Ren\\
Albert D. Rich & Michael Richardson & Jason Riedy\\
Renaud Rioboo & Jean Rivlin & Nicolas Robidoux\\
Simon Robinson & Raymond Rogers & Michael Rothstein\\
Martin Rubey & Jeff Rutter & Philip Santas\\
David Saunders & Alfred Scheerhorn & William Schelter\\
+Bernhard Kutzler & Tim Lahey & Larry Lambe\\
+Kaj Laurson & Charles Lawson & George L. Legendre\\
+Franz Lehner & Frederic Lehobey & Michel Levaud\\
+Howard Levy & J. Lewis & RenCang Li\\
+Rudiger Loos & Craig Lucas & Michael Lucks\\
+Richard Luczak & Camm Maguire & Francois Maltey\\
+Osni Marques & Alasdair McAndrew & Bob McElrath\\
+Michael McGettrick & Edi Meier & Ian Meikle\\
+David Mentre & Victor S. Miller & Gerard Milmeister\\
+Mohammed Mobarak & H. Michael Moeller & Michael Monagan\\
+Marc MorenoMaza & Scott Morrison & Joel Moses\\
+Mark Murray & William Naylor & Patrice Naudin\\
+C. Andrew Neff & John Nelder & Godfrey Nolan\\
+Arthur Norman & Jinzhong Niu & Michael O'Connor\\
+Summat Oemrawsingh & Kostas Oikonomou & Humberto OrtizZuazaga\\
+Julian A. Padget & Bill Page & David Parnas\\
+Susan Pelzel & Michel Petitot & Didier Pinchon\\
+Ayal Pinkus & Frederick H. Pitts & Frank Pfenning\\
+Jose Alfredo Portes & E. QuintanaOrti & Gregorio QuintanaOrti\\
+Beresford Parlett & A. Petitet & Andre Platzer\\
+Peter Poromaas & Claude Quitte & Arthur C. Ralfs\\
+Norman Ramsey & Anatoly Raportirenko & Guilherme Reis\\
+Huan Ren & Albert D. Rich & Michael Richardson\\
+Jason Riedy & Renaud Rioboo & Jean Rivlin\\
+Nicolas Robidoux & Simon Robinson & Raymond Rogers\\
+Michael Rothstein & Martin Rubey & Jeff Rutter\\
+Philip Santas & Alfred Scheerhorn & William Schelter\\
Gerhard Schneider & Martin Schoenert & Marshall Schor\\
Frithjof Schulze & Fritz Schwarz & Steven Segletes\\
V. Sima & Nick Simicich & William Sit\\
diff git a/books/bookvol10.1.pamphlet b/books/bookvol10.1.pamphlet
index cd05954..d76b876 100644
 a/books/bookvol10.1.pamphlet
+++ b/books/bookvol10.1.pamphlet
@@ 1,4 +1,4 @@
\documentclass[dvipdfm]{book}
+\documentclass{book}
\newcommand{\VolumeName}{Volume 10.1: Axiom Algebra: Theory}
\input{bookheader.tex}
\mainmatter
@@ 2853,7 +2853,7 @@ directions in space equally imaginary, or rather equally real, thereby
ensuring to his Calculus the power of dealing with space
indifferently in all directions.
In fact, as we shall see, the Quaternion method is independent
+In fact, as we will see, the Quaternion method is independent
of axes or any supposed directions in space, and takes its reference
lines solely from the problem it is applied to.
@@ 3711,7 +3711,7 @@ $$\overline{OQ}_1=\phi(t+dt)$$
will be the vector of the point after the additional interval $dt$.
But this, in general, gives us little or no information as to the
velocity of the point at $P$. We shall get a better approximation
+velocity of the point at $P$. We will get a better approximation
by halving the interval $dt$, and finding $Q_2$ ,
where $\overline{OQ}_2 = \phi(t + \frac{1}{2}dt)$,
as the position of the moving point at that time. Here the vector
@@ 3775,7 +3775,7 @@ $$d\rho = \phi^{\prime}(x)ds$$
From the very nature of the question it is obvious that the length
of $dp$ must in this case be $ds$, so that $\phi^{\prime}(s)$
is necessarily a unitvector.
This remark is of importance, as we shall see later; and
+This remark is of importance, as we will see later; and
it may therefore be useful to obtain afresh the above result without
any reference to time or velocity.
@@ 4039,7 +4039,7 @@ is a conjugate ray of the cone. ({\sl Ibid}. p. 96.)
{\bf 45}. We now come to the consideration of questions in which
the Calculus of Quaternions differs entirely from any previous
mathematical method; and here we shall get an idea of what a
+mathematical method; and here we will get an idea of what a
Quaternion is, and whence it derives its name. These questions
are fundamentally involved in the novel use of the symbols of
multiplication and division. And the simplest introduction to
@@ 4122,7 +4122,7 @@ signify that $\alpha$ is multiplied by (or operated on by) $q$, not $q$
multiplied by $\alpha$.
This remark is of extreme importance in quaternions, for, as we
shall soon see, the Commutative Law does not generally apply to
+will soon see, the Commutative Law does not generally apply to
the factors of a product.
We have also, by \S\S 47, 48,
@@ 4457,7 +4457,7 @@ known as {\sl Spherical Conics}. As they are not usually familiar to
students, we make a slight digression for the purpose of proving
these fundamental properties ; after Chasles, by whom and Magnus
they were discovered. An independent proof of the associative
principle will presently be indicated, and in Chapter VIII. we shall
+principle will presently be indicated, and in Chapter VIII. we will
employ quaternions to give an independent proof of the theorems
now to be established.
@@ 4659,10 +4659,10 @@ fractional power of a quaternion.
from whose properties it is easy to deduce all the foregoing
results of this chapter. It was, in fact, these properties whose
invention by Hamilton in 1843 led almost intuitively to the
establishment of the Quaternion Calculus. We shall content
+establishment of the Quaternion Calculus. We will content
ourselves at present with an assumption, which will be shown
to lead to consistent results ; but at the end of the chapter we
shall show that no other assumption is possible, following for this
+will show that no other assumption is possible, following for this
purpose a very curious quasimetaphysical speculation of Hamilton.
{\bf 65}. Suppose we have a system of three mutually perpendicular
@@ 4762,7 +4762,7 @@ $$q^2=\frac{\overline{OA^{\prime}}}{\overline{OB}}.
{\bf 69}.
Having thus found that the squares of {\sl i}, {\sl j}, {\sl k} are each
equal to negative unity ; it only remains that we find the values of
their products two and two. For, as we shall see, the result is such
+their products two and two. For, as we will see, the result is such
as to show that the value of any other combination whatever of
{\sl i},{\sl j}, {\sl k}
(as factors of a product) may be deduced from the values of
@@ 5097,7 +5097,7 @@ Hence the {\sl distributive principle is true in the multiplication of
vectors}.
It only remains to show that it is true as to the scalar and
vector parts of a quaternion, and then we shall easily attain the
+vector parts of a quaternion, and then we will easily attain the
general proof.
Now, if $a$ be any scalar, $\alpha$ any vector, and $q$ any quaternion,
@@ 5158,7 +5158,7 @@ so that\hbox{\hskip 4cm}$q.q^{\prime}=\rho\alpha.\alpha\sigma=\rho.\sigma$
The student may easily extend this process.
For variety, we shall now for a time forsake the geometrical
+For variety, we will now for a time forsake the geometrical
mode of proof we have hitherto adopted, and deduce some of our
next steps from the analytical expression for a quaternion given in
\S 80, and the properties of a rectangular system of unitvectors as
@@ 5225,7 +5225,7 @@ $$\frac{1}{x^2+y^2+z^2}$$
It is easy enough to interpret these expressions by means of
ordinary coordinate geometry : but a much simpler process will
be furnished by quaternions themselves in the next chapter, and, in
giving it, we shall refer back to this section.
+giving it, we will refer back to this section.
{\bf 85}. The associative law of multiplication is now to be proved
by means of the distributive (\S 81). We leave the proof to the
@@ 8695,7 +8695,7 @@ meaning of an expression is independent of the particular coercions
that are used in order to type it.
We shall also impose some conditions on the interaction between
+We will also impose some conditions on the interaction between
polymorphic operations defined in type classes and coercions that will
yield a unique meaning of an expression independent of the type which
is assigned to it  if coercions are present there will very
@@ 8826,7 +8826,7 @@ type inference improves considerably the usefulness of a system for a
user. Thus we will investigate the problems connected with type
inference extensively and will also give some results on the
computational complexity of various type inference problems. Another
important problem we shall investigate in various, precisely defined
+important problem we will investigate in various, precisely defined
ways is a possible ambiguity of a type system.
Some of the results we give are contained in some form in the
@@ 8926,7 +8926,7 @@ imply that the meaning of an expression is independent of the
particular coercions that are used in order to type it. These results
will also appear in \cite{Webe95}.
We shall also impose some conditions on the interaction between
+We will also impose some conditions on the interaction between
polymorphic operations defined in type classes and coercions that will
yield a unique meaning of an expression independent of the type which
is assigned to it  if coercions are present there will very
@@ 9430,7 +9430,7 @@ declaration}. \index{declarationii} The signature $(S, \leq, \Sigma)$
is often identified with $\Sigma$. If $\omega=n$ then $f$ is called
a $n$ary operator symbol. \index{operator symbolii} $0$ary
operator symbols are {\em constant symbols}. \index{constant
symbolsii} As in \cite{Smo89} we will assume in the following
+symbolsii} As in \cite{SmolkaNutt89} we will assume in the following
that for any $f$ there is only a single $n \in \NN$ such that $f$ is a
$n$ary operator symbol.}
@@ 13981,6 +13981,5559 @@ existing. Nevertheless, it seems to be very likely that some of the
obtained results are applicable to the type inference problem for a
user interface of a computer algebra system.
+
+\chapter[Doye's Coercion Algorithm]{Doye's Coercion Algorithm by Nicolas Doye}
+
+This chapter is based on a PhD thesis by Nicolas James Doye
+\cite{Doye97}. Changes have been made to integrate it.
+
+\section{Introduction}
+\label{DoyeChap1}
+\subsection{Abstract Datatypes in General}
+\label{DoyeSec1.4}
+
+Abstract datatypes provide a way of specifying a type. As a (useful)
+side effect an abstract datatype can express how a whole collection
+of types may act.
+
+An incredibly specific specification will only specify types which are
+all ``the same'' (isomorphic). A less exacting specification may
+result in types which are similar, but not the same.
+
+This ``sideeffect'' of using a less exacting specification to collect
+similar types together forms the basis of strict categorical type
+systems.
+
+For example, we may say which operations are available on a certain
+family of types. We may also state certain facts about the structure
+of all types in a certain family. Most importantly of all, we can
+enforce relationships between various types (of different families),
+how they interact, and how they may depend upon each other (or not).
+
+See section \ref{DoyeSec4.2} for how we may specify types and what
+operations are available to them. Look at section \ref{DoyeSec4.7} for
+the relationships between different types. Section \ref{DoyeSec4.6}
+details how we may restrict the structure of certain types using sets
+of equations.
+
+As a simple example, a polynomial ring depends for its specification
+on the underlying ring (from which the coefficients are taken).
+
+As a more complicated example, a polynomial ring could also depend
+upon: the type from which it takes its variables; the type of the
+exponents; a boolean algebra; an ordered free monoid with one
+generator (the natural numbers adjoin \{0\} is often a good choice);
+and maybe a few others.
+
+Another factor is the actual relationship between the various
+types. In our above example, of the polynomial ring, we know that:
+\begin{enumerate}
+\item there is a ring monomorphism from the underlying ring to the
+polynomial ring
+\item there is an injection from the variable type\footnote{The
+type from which all the variables are taken. In Axiom, the
+variables are usually elements such as X, Y, and Z which are
+from the type Symbol} to the polynomial ring. (In fact, an
+orderedset monomorphism\footnote{This is an injective function,
+$\phi$, which is both a sethomomorphism (which is just a total
+function) and preserves order. So if $a
+ PolynomialCategory(R,NonNegativeInteger,Symbol)
+\end{verbatim}
+{\bf UnivariatePolynomial} exports a function
+\[{\rm coerce : R} \rightarrow \%\]
+which is the natural monomorphism including the ring {\tt R} in the
+polynomial ring as the constant polynomials.
+
+\begin{DoyeExample}
+\label{Doye1.6.3}
+$\mathbb{Z}[X]\rightarrow\mathbb{Z}[X,Y]$
+({\rm where} $\mathbb{Z}[X,Y]=\mathbb{Z}[X][Y]$)
+\end{DoyeExample}
+
+This is the same as the previous example, $[Y]$ is acting as a
+morphism\\
+$\mathbb{Z}[X]\rightarrow\mathbb{Z}[X][Y]$.
+
+\begin{DoyeExample}
+\label{Doye1.6.4}
+$\mathbb{Z}[X]\rightarrow\mathbb{Z}[X,Y]$
+({\rm where} $\mathbb{Z}[Y,Z]=\mathbb{Z}[Y][X]$)
+\end{DoyeExample}
+
+Axiom knows that $\mathbb{Z}\rightarrow\mathbb{Z}[Y]$ is a coercion,
+and that the map\\
+$[X]:\mathbb{Z}[Y]\rightarrow\mathbb{Z}[Y][X]$
+(i.e. {\tt UnivariatePolynomial}) lifts this coercion.
+
+\begin{DoyeExample}
+\label{Doye1.6.5}
+$\mathbb{Z}\rightarrow\mathbb{Q}[X,Y]$
+\end{DoyeExample}
+
+This is built by the chain of coercions
+\[\mathbb{Z}\rightarrow\mathbb{Q}\rightarrow\mathbb{Q}[X]\rightarrow
+\mathbb{Q}[X,Y]\]
+
+\begin{DoyeExample}
+\label{Doye1.6.7}
+$\mathbb{Z}[X]\rightarrow\mathbb{Z}(X)$
+\end{DoyeExample}
+
+This uses the coercion from {\tt Fraction} discussed above, since
+$\mathbb[Z](X)$ is represented by
+{\tt Fraction(UnivariatePolynomial(X,Integer))}
+
+\begin{DoyeExample}
+\label{Doye1.6.8}
+$\mathbb{Z}\rightarrow\mathbb{Z}_5$
+\end{DoyeExample}
+
+This uses the function
+\[{\rm coerce : \mathbb{Z}\rightarrow\%}\]
+defined in {\tt IntegerMod(n:PositiveInteger)}
+
+\begin{DoyeExample}
+\label{Doye1.6.9}
+$\mathbb{Z}_{25}\rightarrow\mathbb{Z}_5$
+\end{DoyeExample}
+
+Axiom cannot coerce from {\tt IntegerMod(25)} to {\tt IntegerMod(5)}.
+
+\subsubsection{Structural coercions}
+\label{DoyeSubSec1.6.9}
+
+The structural coercions are ``lifts'' of other coercions. In the case
+of {\tt Lists}, one may perform a structural coercion as follows:
+\begin{verbatim}
+ coerce(x:List(A)):List(B) == map(coerce,x)@List(B)
+\end{verbatim}
+\begin{verbatim}
+ map(f:List(A) > List(B),x:List(A)):List(B) ==
+ nullp(x) => nil()$List(B)
+ cons(f(car(x)),map(f,cdr(x)))
+\end{verbatim}
+
+In the case of {\tt Polynomials}, a similar {\tt map} function exists
+which uses $+$ instead of {\tt cons}
+
+In the case of {\tt Matrix} a similar map function can be used (though
+since matrices are of fixed sizes  unlike sets, lists, and
+polynomials  a default valued matrix $(0)$ has to be created, then
+all the values substituted into (added to) it).
+
+\subsection{Mathematical solution overview}
+\label{DoyeSec1.7}
+
+The solution to the questions raised in section \ref{DoyeSec1.5} rely
+on abstract datatypes. These ``collect'' large numbers of types into
+collections of similar types. We will be considering abstract
+datatypes in the language of universal algebra; specifically,
+ordersorted algebra (section \ref{DoyeSec4.4}).
+
+Universal algebra has close links with the ideas of category
+theory. Indeed, (see chapter \ref{DoyeChap3} for category theory
+and section \ref{DoyeSec5.4} for the links between the two theories).
+Axiom uses the language of category theory to describe
+its algebraic design. Thus we will also discuss the fundamentals of
+category theory in relation to this work.
+
+Using the ordersorted algebra framework we will show that there is
+indeed a strict mathematical definition
+(definition \ref{Doye5.5.2})
+which we may use to tell us
+which type changes are natural, and therefore, in our definition,
+coercions.
+
+Moreover we will show that this approach allows us to create such
+coercions algorithmically. (algorithm \ref{Doye7.4.1})
+
+In section \ref{DoyeSec1.8} we will show an analogy with moving
+buildings to the solution of changing the type of (i.e. coercing)
+something.
+
+\subsection{Constructing coercions algorithmically}
+\label{DoyeSec1.8}
+
+Consider the following analogy.
+
+Suppose you have been given the job of moving London Bridge from one
+location to another. The bridge is too large to move in one piece.
+
+You will merely be supervising the work and will not have to carry any
+of the bricks yourself, hence efficiency is not your concern.
+
+You are also planning to move other different bridges in the future,
+and once you have a method for moving one bridge, you would like to be
+able to apply that method to the next. This means that next time a
+bridge needs moving, you won't have to do much work at all.
+
+Lucky for you someone has already worked out a way of moving any of
+the bricks at the very bottom of the bridge to their new location,
+regardless of any obstruction, which would normally leave civil
+engineers crying. This person was clearly a magician.
+
+So here is your algorithm for moving London bridge, and hence any
+future bridge.
+\begin{verbatim}
+ If the original bridge has no bricks left then finished.
+ Else,
+ take a brick from the top of the original bridge.
+ If this brick is a bottom brick then,
+ use the magical bottom brick mover, to place
+ the brick in the corresponding location of
+ the new bridge.
+ Else
+ hold the brick in place, in the corresponding
+ location in the new bridge.
+ Endif.
+ Endif.
+ Repeat.
+\end{verbatim}
+
+Indeed, you realize that this method will work for other brickbased
+constructions, or indeed anything that is ``built''. (Obviously, there
+are other considerations, is the new location for the bridge a
+``natural'' one? For example, is it long or tall enough?)
+
+The analogue of the bridge is a ``thing'' or ``item'' in our computer
+algebra system. The original location of the bridge is the original
+type of the ``item'' and the new location for the bridge is the
+analogue of the type to which we are coercing the ``item''.
+
+Thus what we need to know are:
+\begin{enumerate}
+\item what are the foundations of the bridge?\\
+({\bf Analogue}: what are the constants of our type?)
+\item what is the length, width, strength of the bridge?\\
+({\bf Analogue}: what are the parameters of the type?)
+\item how do you alter the bricks to be of a new shape/material?\\
+({\bf Analogue}: we need to be able to recursively call the coercion
+algorithm on types which are ``recursively required for
+coercion''. That is types which form the bits of the ``item'' once we
+have chopped it up.)
+\end{enumerate}
+
+This is our analogy and we may consider many data types to be
+constructed (or built) similarly. For example, lists (in the
+Lispsense) are always constructed either by being the empty list, (),
+or by being the {\tt cons} of something to the front of another list.
+
+As a more complicated example, polynomials are constructed via one of
+the following mechanisms:
+\begin{enumerate}
+\item by being a member of (the included monomorphic copy of) the
+underlying ring (a constant polynomial)
+\item by being a symbol exponentiated to some positive power (a
+univariate monic monomial)
+\item by being the product of a monic monomial and a univariate monic
+monomial (a monic monomial)
+\item by being the product of a monic monomial and a member of the
+underlying ring (a monomial)
+\item by adding a monomial to a polynomial
+\end{enumerate}
+
+So we see that at least two of the most basic types in computer
+algebra are constructed in this way.
+
+\section{Types in Computer Algebra}
+\label{DoyeChap2}
+
+\subsection{Introduction}
+\label{DoyeSec2.1}
+
+Axiom's main view of things is that every object has a type, and that
+there are ostensibly four layers.
+\[{\rm items} \in {\rm Domains} \in {\rm Categories} \in {\rm
+Category}\]
+For example,
+\[3 \in Integer \in Ring \in Category\]
+and the top layer is the unique distinguished symbol, ``Category''. In
+general, this top layer is never referred to, and the three lower
+layers are all that are ever considered.
+
+Strictly speaking, if one considers Axiom's {\tt Categories} to be
+categories, and Axiom's {\tt Category} symbol, to signify the category
+of all the {\tt Categories}\footnote{{\tt Category} is not one of the
+{\tt Categories} in Axiom}, then one should write,
+\[3 \in {\rm Integer},\quad {\rm Integer} \in {\rm Obj(Ring)},\quad
+{\rm Ring} \in {\rm Obj(Category)}\]
+where $3 \in {\rm Integer}$ means 3 is an element of the carrier of
+the principal sort of the signature to which {\rm Integer} belongs.
+
+Users may extend the Axiom system by writing new {\tt Domains} and
+{\tt Categories} in the Axiom language called Spad.
+
+A category is a collection of domains all of which are ``similar''. In
+\cite{Dave90} the authors state that they designed the Scratchpad system
+of categories or ``abstract algebras''\footnote{Axiom's
+{\tt Categories} can also be thought of as ordersorted algebras, but
+the order on sorts is never explicitly defined and there are some
+difficulties in the definition of the operator symbols.} for the
+following reasons:
+\begin{enumerate}
+\item economy of effort (section \ref{DoyeSubSec2.5.1})
+\item interest (section \ref{DoyeSubSec2.5.2})
+\item functoriality (section \ref{DoyeSubSec2.5.3})
+\end{enumerate}
+
+\subsubsection{Economy of effort}
+\label{DoyeSubSec2.5.1}
+
+The most obvious reason for this is the view of inheritance. A
+category (in Axiom) is said to extend another if it inherits all the
+other's functions, attributes, and equations. This allows for a
+significant amount of reuse.
+
+A more important issue in an algebra system is that if one can prove a
+theorem in some generality, i.e. for all the objects in a category,
+then one does not have to go around proving the theorem for each
+object of the category.
+
+\subsubsection{Interest}
+\label{DoyeSubSec2.5.2}
+
+Some categories are interesting and some are not. For example,
+{\tt Ring} and {\tt Field} are particularly interesting. Many theorems
+can be proved {\sl for all} {\tt Fields}.
+
+However (to borrow an example from \cite{Dave90}), the category of all
+rings which when viewed as Abelian groups, have an involution with
+precisely one fixed point, is not particularly interesting.
+
+One may think of the designer's concept of ``interest'' as congruent
+to ``useful'' (usually to the user, but occasionally to the
+designers).
+
+\subsubsection{Functoriality}
+\label{DoyeSubSec2.5.3}
+
+This is called ``higher order Polymorphism'' in \cite{Crol93}. There
+are operators which given objects of a category can create new objects
+of a given (potentially different) category. For example, {\tt List}
+is a functor from {\tt SetCategory} to {\tt ListAggregate}
+\[\begin{array}{rcl}
+{\rm List:SetCategory} & \rightarrow & {\rm ListAggregate}\\
+{\rm S} & \mapsto & {\rm List(S)}
+\end{array}\]
+
+Indeed, this target category may even be the distinguished symbol
+{\tt Category}.
+
+In Axiom, the {\tt Category} constructors (often called functors) are
+functors from
+\[\prod_{n\in {\rm N}\cup 0}{{\rm Category} \rightarrow {\rm Category}}\]
+
+For example, the {\tt Ring} functor takes no arguments and returns the
+{\tt Category} of {\tt Ring}.
+\[\begin{array}{rcl}
+{\tt Ring} : () & \rightarrow & {\rm Category}\\
+() & \mapsto & {\tt Ring}
+\end{array}\]
+
+The special {\tt Category} creation operation, {\tt Join} is also a
+functor. {\tt Join} is used to declare a new {\tt Category} to be a
+subcategory of the intersection of two or more {\tt Categories}. Here
+we illustrate the case of {\tt Join} acting on two {\tt Categories}.
+\[\begin{array}{rcl}
+{\rm Join : (Category,Category)} & \rightarrow & {\rm Category}\\
+{\rm (A,B)} & \mapsto & {\rm A}\cap{\rm B}
+\end{array}\]
+
+More commonly in Axiom, and Axiom's own use of the word
+``{\sl functor}'' covers cases as follows. This is similar to the case
+of {\tt Ring}, only less trivial. {\tt ListAggregate} in the
+{\tt Category} of all types of finite lists.
+\[\begin{array}{rcl}
+{\rm ListAggregate:(SetCategory)} & \rightarrow & {\rm Category}\\
+{\rm S} & \mapsto & {\rm ListAggregate(S)}
+\end{array}\]
+
+Here we see the subcategory {\rm ListAggregate(S)} of the
+{\tt Category} {\tt ListAggregate}. When using Axiom, one usually
+thinks of one's type as belonging to the smaller, concrete
+(sub){\rm Category}, {\rm ListAggregate(S)}. Mathematically, one
+usually thinks of one's type as being in the larger, more abstract
+{\tt ListAggregate}.
+
+\section{Category Theory}
+\label{DoyeChap3}
+
+As we have already hinted at, category theory is one of the main
+foundations of Axiom. In this chapter, we will give the necessary
+definitions to investigate this claim. We will also investigate the
+claim in itself.
+
+The definitive text on Category Theory is Mac Lane \cite{Macl91}. The
+amount of theory we require is relative small. We define categories
+without worrying about Russell's Paradox \cite{Mend87}.
+
+\subsection{About Category Theory}
+\label{DoyeSec3.2}
+
+\noindent
+\begin{DoyeDefinition}
+\label{Doye3.2.1}
+A category, C, consists of two collections. The
+first collection is called the {\tt objects} of the category, or
+{\rm Obj}(C). The second collection is called the arrows of category,
+or {\rm Arr}(c).
+
+Also, for each arrow, f, there exists two special objects with
+which it is associated. The first is the source of f, called
+{\tt source}(f). The second is called the target of f, called
+{\tt target}(f).
+
+There also exists a ``{\rm law of composition}'' for arrows:
+\[\begin{array}{l}
+(\forall g,f {\rm arrows})(({\rm source}(g) = {\rm target}(f))
+\Rightarrow\\
+(\exists g \circ f {\rm arrow})(({\rm source}(g \circ f) = {\rm
+source}(f)) \land ({\rm target}(g \circ f) = {\rm target}(g))))
+\end{array}\]
+
+Next, for each object, c, there exists a unique arrow, called the
+{\rm identity arrow} on c, or ${\rm id}_c$.
+
+Finally the following two axioms must hold:
+\[\begin{array}{l}
+(\forall k,g,f~{\rm arrows})
+((g\circ f,k\circ g~{\rm arrows})\Rightarrow\\
+\quad((k\circ(g\circ f),(k\circ g)\circ f~{\rm arrows})\land\\
+\quad\quad(k\circ(g\circ f) = (k\circ g)\circ f)))\\
+\end{array}\]
+\[\begin{array}{l}
+(\forall f~{\rm arrows})(({\rm id}_{{\rm target}(f)}\circ f = f)\land
+(f\circ {\rm id}_{{\rm source}(f)} = f))
+\end{array}\]
+\end{DoyeDefinition}
+
+To introduce the concept, here are some simple finite categories.
+
+\begin{DoyeExample}
+\label{Doye3.2.2}
+{\bf 0} is the empty category, it has no objects and no
+arrows
+\end{DoyeExample}
+
+\begin{DoyeExample}
+\label{Doye3.2.3}
+{\bf 1} is the category with one object and one arrow.
+\end{DoyeExample}
+
+\begin{DoyeExample}
+\label{Doye3.2.4}
+{\bf 2} is the category with two objects, $a,b$ and one
+nonidentity arrow, $f:a\rightarrow b$
+\end{DoyeExample}
+
+\begin{DoyeExample}
+\label{Doye3.2.5}
+$\downarrow\downarrow$ is the category with two objects,
+$a,b$ and two nonidentity arrows, $f,g:a\rightarrow b$
+\end{DoyeExample}
+
+Now let us consider some more useful categories. The collection of
+objects in the following examples do not always form a set
+\cite{Macl91}\cite{Bern91}\cite{Devl79}\cite{Fran73}
+
+\begin{DoyeExample}
+\label{Doye3.2.6}
+{\bf Set} is the category which has as objects, all
+sets, and has as arrows, all total functions between sets.
+\end{DoyeExample}
+
+\begin{DoyeExample}
+\label{Doye3.2.7}
+{\bf Grp} is the category which has as objects, all
+groups, and has as arrows, all group homomorphisms between them.
+\end{DoyeExample}
+
+\begin{DoyeExample}
+\label{Doye3.2.8}
+{\bf Ring} is the category which has as objects, all
+rings, and has as arrows, all ring homomorphisms between them.
+\end{DoyeExample}
+
+\begin{DoyeExample}
+\label{Doye3.2.9}
+{\bf Poly} is the following category. An object of
+{\bf Poly} is a set of all polynomials with: variables from a fixed
+ordered set $V$; coefficients from a fixed ring $R$; and the exponents
+of the variables from an ordered free monoid with one generator $E$.
+\end{DoyeExample}
+
+An arrow of {\bf Poly} is a Polynomial homomorphism. That is, a Ring
+homomorphism which also acts homomorphically on a certain set of
+functions which act on polynomials.
+
+Some texts call the arrows of a category the {\sl morphisms} of a
+category. Examples Set, Grp, Ring, and Poly show us that for some
+naturally occuring categories, the arrows (or morphisms) are just the
+homomorphisms of the category. Indeed, an arrow of {\bf Set} (a total
+function) is really just a homomorphism between sets.
+
+So we see that the arrows preserve a certain set of properties for
+each element of the object.
+
+We also see that every object of {\bf Grp} is an object of {\bf Set};
+every object of {\bf Ring} is an object of {\bf Grp}; and every object
+of {\bf Poly} is an object of {\bf Ring}.
+
+Now similarly, replace the word ``object'' with the word ``arrow'' in
+the previous paragraph and it still holds true.
+
+Hence we see that in an algebra system, there is a certain amount of
+``inheritance'' amongst the categories. The categories are the
+socalled {\sl abstract datatypes} since they type the usual
+datatypes.
+
+We can also see how the categories can collect together all similar
+types. This functionality can be used for the three design goals of
+Axiom: economy of effort  the code for many similar types need only
+be written once; interest  collecting similar types together gives
+the user an identiical interface to similar types; and functoriality
+which is best left to be discussed after the following definition.
+
+\begin{DoyeDefinition}
+\label{Doye3.2.10}
+ Let B, C be categories, then a functor,
+$T : C \rightarrow B$ consists of two functions
+\begin{enumerate}
+\item $T:{\rm Obj}(C) \rightarrow {\rm Obj}(B)$
+(the {\rm object} function)
+\item $T:{\rm Arr}{C} \rightarrow {\rm Arr}{B}$
+(the {\rm arrow} function)
+\end{enumerate}
+
+These must obey the following:
+
+\[\begin{array}{rcl}
+(\forall f~{\rm arrow})(T({\rm source}(f)) & = & {\rm source}(T(f)));\\
+(\forall f~{\rm arrow})(T({\rm target}(f)) & = & {\rm target}(T(f)));\\
+(\forall c~{\rm object})&=&({\rm id}_{T(c)})\\
+(\forall g,f~{\rm arrows})(({\rm source}(g) = {\rm target}(f)) &\Rightarrow&
+(T(g\circ f) = T(g)\circ T(f)))
+\end{array}\]
+\end{DoyeDefinition}
+
+This is a very useful definition. It shows us that when we have two
+objects and an arrow between them in one category, then a ``sensible''
+map of these objects to another category will induce the obvious map
+between these image objects.
+
+In fact, one can see that if one were to define a category which has
+as objects ``all categories'', and as arrows ``all functors'' then we
+would (set theoretical concerns aside) have a welldefined category.
+
+Categories, just like many other mathematical constructs, may form
+products.
+
+\begin{DoyeDefinition}
+\label{Doye3.2.11}
+For two categories $B$ and $C$ we may construct a
+new category denoted $B\times C$ called the product of $B$ and $C$.
+
+An object of $B\times C$ is a pair $\langle b,c\rangle$ where $b$
+is an object of $B$ and $c$ an object of $C$
+
+An arrow of $B\times C$ is a pair $\langle f,g\rangle$ where
+$f:b\rightarrow b^\prime$ is an arrow of $B$,
+$g:c\rightarrow c^\prime$ is an arrow of $C$,
+the source of $\langle f,g\rangle$ is $\langle b,c\rangle$
+and the target of $\langle f,g\rangle$ is
+$\langle b^\prime,c^\prime\rangle$.
+
+Composition of arrows is
+$\langle f^\prime,g^\prime\rangle : \langle b^\prime,c^\prime\rangle
+\rightarrow\langle b^{\prime\prime}, c^{\prime\prime}\rangle$ and
+$\langle f,g\rangle : \langle b,c\rangle\rightarrow
+\langle b^\prime, c^\prime\rangle$ is defined via
+\[\langle f^\prime,g^\prime\rangle \circ \langle f\circ g\rangle =
+\langle f^\prime\circ f, g^\prime\circ g\rangle\]
+\end{DoyeDefinition}
+
+Axiom makes use of such products implicitly in its functor
+definitions. For example, see the discussion of
+{\tt PolynomialCategory} below.
+
+``Natural transformations'' are another important part of category
+theory. They are to functors as functors are to categories. Here is a
+more formal definition.
+
+\begin{DoyeDefinition}
+\label{Doye3.2.12}
+For two functors $S,T: C \rightarrow B$ a
+natural transformation $\tau : S\dot\rightarrow T$ is a function which
+assigns to every $c \in {\rm Obj}(C)$ an arrow
+$\tau_c = \tau c : S c\rightarrow Tc$ of $B$ such that
+\[(\forall c~\in {\rm Obj}(C))
+(\forall f :c\rightarrow c^\prime \in {\rm Arr}(C))
+(T f\circ \tau c = \tau c^\prime \circ S f)\]
+\end{DoyeDefinition}
+
+Now we may define the following interesting category.
+
+\begin{DoyeDefinition}
+\label{Doye3.2.13}
+For two categories, $B,C$, the {\rm functor
+category} $B^C$ is the category with objects the functors
+$T:C\rightarrow B$ and arrows, the natural transformations between two
+such functors.
+\end{DoyeDefinition}
+
+As another fairly abstract definition, consider the following.
+
+\begin{DoyeDefinition}
+\label{Doye3.2.14}
+Let $S:D\rightarrow C$ be a functor and
+$c \in {\rm Obj}(C)$. A universal arrow $c\rightarrow S$ is a pair
+$\langle r,u\rangle \in {\rm Obj}(D)\times{\rm Arr}(C)$ where
+$u:c \rightarrow Sr$ such that
+\[(\forall(d,f)\in{\rm Obj}(D) \times {\rm Arr}(C) {\rm where}
+f : c \rightarrow Sd)
+(\exists! f^\prime:r\rightarrow d\in{\rm Arr}(D))(Sf^\prime\circ
+~u=f)\]
+\end{DoyeDefinition}
+
+Functoriality in a computer algebra system allows us to view objects
+of one category as objects of another.
+
+As we have already seen, an object of {\tt Poly} is an object of
+{\tt Ring} and hence an object of {\tt Grp} and thus an object of
+{\tt Set}. We have also seen this is true for their arrows. This
+relationship is called the subcategory relationship, defined formally
+as follows.
+
+\begin{DoyeDefinition}
+\label{Doye3.1.15}
+A category $C$ is a subcategory of a category
+$B$ iff every object of $C$ is an object of $B$ and every arrow of $C$
+is an arrow of $B$.
+\end{DoyeDefinition}
+
+Functors from subcategories to the categories of which they are
+subcategories are often called ``forgetful functors''. This is more
+often true when the target of the functor is {\sl Set}.
+
+Axiom's designers also use functors to create instances of abstract
+datatypes. {\tt PolynomialCategory(.,.,.)} (Axiom's equivalent of
+{\tt Poly}) is in Axiom's view a functor.
+
+\[\begin{array}{c}
+{\rm Ring}\times {\rm OrderedAbelianMonoid}\times {\rm OrderedSet}\rightarrow
+{\rm PolynomialCategory(.,.,.)}\\
+{\rm (R,E,V)}\mapsto {\rm PolynomialCategory(R,E,V)}
+\end{array}\]
+
+This functoriality provides the ``glue'' for Axiom's type mechanism.
+
+Now, trivially for categories $A,B$ if $\exists F:A\rightarrow B$ a
+forgetful functor, the $B$ is a subcategory of $A$. Equally trivially,
+a concrete instance of {\rm PolynomialCategory(R,E,)} is a subcategory
+of {\tt PolynomialCategory(R,.,.)} which is a subcategory of
+{\rm Poly}.
+
+It is this first form of subcategory relation that provides Axiom's
+inheritance mechanism.
+
+\subsection{Categories and Axiom}
+\label{DoyeSec3.3}
+
+\begin{DoyeNotation}
+\label{Doye3.3.1}
+To distinguish between Axiom's internal structures
+and those commonly used in mathematics, things which belong to Axiom
+will be writtin in {\bf this font}. Specifically,
+\begin{itemize}
+\item {\bf Category} will always refer to Axiom's distinguished
+symbol, to which all Axiom's {\bf Categories} belong.
+\item Hence, a {\bf Category} is an Axiom object declared to be
+such an object, e.g. {\bf Ring}, {\bf PolynomialCategory(R,E,V)}
+\item A {\bf Domain} is an Axiom object declared to be a member
+of a particular {\bf Category}, e.g. {\bf Integer},
+{\bf Polynomial(Integer)}
+\item An {\bf item} is an element of a {\bf Domain}, e.g. 1, 5*x**2+1
+\end{itemize}
+\end{DoyeNotation}
+
+Axiom's main view of things is that every object
+has a type, and that there are four layers.
+\[{\bf items}\in{\bf Domains}\in{\bf Categories}\in{\bf Category}\]
+
+{\bf Categories} also may inherit from or extend other {\bf
+Categories}, forming an inheritance lattice. Thanks to the higher
+order polymorphism available in Axiom, {\bf Categories} may also be
+parameterized by {\bf items}\footnote{One may view a domain as a
+category, whose objects are the items, and whose arrows are either
+trivial (i.e. solely the identity arrows) or some other natural
+occurring meaning, e.g. in {\bf PositiveInteger} one may think that
+there is a natural map $35\rightarrow 5$, since $5\vert 35$. This
+would then mean that this map could be ``lifted'' to
+{\bf IntegerMod 35 $\rightarrow$ IntegerMod 5}} or {\bf Domains}.
+
+This parameterisation may cause some confusion. For example,
+\[{\bf List(S) : ListAggregate(S)}\]
+declares for each and every {\bf S}, {\bf List(S)} is in the category
+{\bf ListAggregate(S)}. For example, {\bf List(Integer)} is an object
+of {\bf ListAggregate(Integer)}. However, {\bf ListAggregate(Integer)}
+is a mere subcategory of ``the category of all objects which are
+domains of linked lists''. This is {\bf ListAggregate(S)}.
+
+So {\bf ListAggregate(S)} contains, for example, both
+{\bf List(Integer)} and\\
+{\bf List(Fraction(Integer))} as objects, but
+what are the arrows of this category? This is something which is not
+made explicit in the Axiom literature, and is indeed the core of this
+work.
+
+We will discuss what it means to be a ``natural map'' and how this
+related to categorical arrows.
+
+\subsection{Functors and Axiom}
+\label{DoyeSec3.4}
+
+Axiom describes its domain constructors as functors, and this is
+true. After all, (neglecting difficulties with constructors which take
+domain elements for arguments) these constructors are maps from a
+cross product of categories to another category.
+
+The difficulties with constructors which take domain elements for
+arguments disappear when considering the argument use in the
+footnote in section \ref{DoyeSec3.3}.
+
+\subsection{Coercion and category theory}
+\label{DoyeSec3.5}
+
+If {\bf coerce : A $\rightarrow$ B}, then we are going to have that
+{\bf A} and {\bf B} are objects of the same category {\bf ACAT}, and
+that {\bf coerce} is an arrow of that category. (See definition
+\ref{Doye5.5.2})
+
+Also, if {\bf T} is a functor from {\bf ACat} to {\bf TCat}, which in
+Axiom would look like
+\[{\bf T(A:ACat) : TCat}\]
+then {\bf T} lifts the arrows of {\bf ACat} to {\bf TCat}, and in
+particular
+\[{\bf T : coerce : A \rightarrow B \mapsto
+coerce:TCat(A)\rightarrow TCat(B)}\]
+
+In many types (and some other languages) {\bf T} is acting like the
+familiar ``map'' operator on the {\bf coerce} function.
+
+\subsection{Conclusion}
+\label{DoyeSec3.6}
+
+We have seen in this section how category theory and abstract
+datatyping especially with respect to Axiom's {\bf Category} mechanism
+are ideologically similar.
+
+We have also shown how Axiom's functors interact with coercions from a
+category theoretical perspective.
+
+\section{Order sorted algebra}
+\label{DoyeChap4}
+
+In this section we will introduce the concepts of universal
+algebra. We will look at the unsorted case to start with and then move
+on to the sorted case.
+
+We then follow up with the equational calculus which allows us to
+consider sets of equations which must hold in a concrete instance of
+an algebra.
+
+All the work in this section is taken from \cite{Dave93a} except for a
+couple examples.
+
+\subsection{Universal Algebra}
+\label{DoyeSec4.2}
+
+Universal algebra will provide us with a natural way of representing
+categories of types which possess certain functions. In the following
+lengthy section of definitions, keep in mind that what we will define
+as a ``signature'' will be equivalent (in some sense) to our notion of
+a category (or abstract datatype). An algebra will be the ideological
+equivalent of an object (or type).
+
+\begin{DoyeDefinition}
+\label{Doye4.2.1}
+A sortlist $S$, is a (finite) sequence of
+symbols (called sorts) normally denoted ($s_1,\ldots,s_m$).
+\end{DoyeDefinition}
+
+\begin{DoyeDefinition}
+\label{Doye4.2.2}
+Given a sortlist of size $m$, a set $A$ of
+$S$carriers is an ordered $m$tuple of sets $A_{s_i}$, indexed by
+$S$.
+\end{DoyeDefinition}
+
+\begin{DoyeExample}
+\label{Doye4.2.3}
+One may consider the sortlist of a vector space to
+be ($K$,$V$) where $K$ is to be identified with the underlying field
+and $V$ is to be identified with the set of all points in the vector
+space. Then considering {\bf C} to be a vector space of {\bf R}, the
+($K$,$V$)carriers of {\bf C} are ({\bf R}, {\bf C}).
+\end{DoyeExample}
+
+So we see that the carriers of a particular type are a list of types
+which ``have something to do with'' the type in question. The sort
+list is a list of the same length where the $i$th element is the
+symbol corresponding to a particular abstract datatype to which the
+$i$th carrier belongs\footnote{Notice that the sort list is defined
+first and that the carriers depend on the sort list. One does not
+define a list of carriers and then fix a list of abstract datatypes
+{\sl post facto}.}.
+
+\begin{DoyeDefinition}
+\label{Doye4.2.4}
+Given a sortlist $S$ and
+$n\in \mathbb{N} \cup \{0\}$, an $S$arity of rank $n$ is an ordered
+$n$tuple of elements of $S$.
+\end{DoyeDefinition}
+
+An arity is merely a list of elements of the sort list. This will be
+useful when we wish to type polymorphic (or abstract) functions.
+
+\begin{DoyeDefinition}
+\label{Doye4.2.5}
+Given a sortlist $S$,
+$n\in \mathbb{N} \cup \{0\}$, $q=(q_1,\ldots,q_n)$ an $S$arity of
+rank $n$, and a set $A$ of $S$carriers, we define
+\[A^q := \prod_{i\in\{1,\ldots,n\}} A_{q_i}\]
+\end{DoyeDefinition}
+
+This is the map of an arity to the list of carriers.
+
+\begin{DoyeDefinition}
+\label{Doye4.2.6}
+An $S$operator of arity $q$ is a function from
+$A^q$ to one of the elements of $A$.
+\end{DoyeDefinition}
+
+\begin{DoyeDefinition}
+\label{Doye4.2.7}
+An $S$operator set or $S$sorted signature is a
+set $\Sigma$ of sets $\Sigma_{n,q,s}$ indexed by
+$n\in\mathbb{N}\cup\{0\}$, $q$ an $S$arity of rank $n$, and $s\in S$,
+such that $\cup_{n,q,s}\Sigma_{n,q,s}$ is a subset of some
+alphabet. An element of some $\Sigma_{n,q,s}$ is called an operator
+symbol.
+
+The usual notation for such a signature is ($\Sigma$,$S$).
+\end{DoyeDefinition}
+
+So this defines a set of sets of polymorphic
+functions\footnote{Functions without methods.} for a particular
+sortlist. A signature is like a category in that it is an abstract
+datatype.
+
+A signature collects together all types which share a similar family
+of operators.
+
+\begin{DoyeExample}
+\label{Doye4.2.8}
+Monoids: $\mathbb{N}\cup\{0\}$ is an additive
+monoid, whereas $\mathbb{N}$ is a multiplicative monoid.
+
+The signature for monoids could be viewed as being
+\[\langle\Upsilon,U\rangle =
+\langle(M,B),((c),(),(id),(ep),(),(),(b),()\ldots)\rangle\]
+where $M$ is the monoid sort, $B$ is the sort of boolean logic
+types. The operator symbol $e$ is a member of $\Upsilon_{(0,(),M)}$
+and corresponds to the function which always returns the identity
+constant\footnote{Constants are often represented by (if not compiled
+in the same way as) functions in programming languages, such as
+Axiom's Spad language. This gives a homogeneous interface for
+providing constants.} of the monoid.
+
+$id$ is the operator symbol in $\Upsilon_{(1,(M),M)}$ which
+corresponds to the identity function.
+
+$ep$ is the operator symbol in $\Upsilon_{(1,(M),B)}$ which
+corresponds to the ``is this the identity element?'' function.
+
+Last (in our example) but by no means least, $b$ is the monoid's
+binary operator from $\Upsilon_{(1,(M,M),M)}$.
+
+So in $\mathbb{N}\cup\{0\}$, $e$, $id$, $ep$, $b$ correspond to
+0, $id$, 0?, $+$, respectively. Whereas in $\mathbb{N}$, $e$, $id$,
+$ep$, $b$, correspond to 1, $id$, 1?, $\times$ respectively.
+\end{DoyeExample}
+
+\begin{DoyeDefinition}
+\label{Doye4.2.9}
+A (multisorted, total) $\Sigma$algebra is an
+ordered pair $\langle A,\alpha\rangle$ where $A$ is an $S$carrier set
+and
+\[\alpha=\{\alpha_{n,q,s}\vert n\in\mathbb{N}\cup\{0\},
+q {\rm\ an\ arity\ of\ rank\ }n,s\in S\}\]
+\[\alpha_{n,q,s}=\{\alpha_{n,q,s,\sigma}:A^q\rightarrow
+A_s\}_{\sigma \in \Sigma_{n,q,s}}\]
+
+So if $\langle\Upsilon,U\rangle$ is the monoidal signature, the
+\[\langle({\bf N},{\bf
+Boolean}),((1),(),(id),(1?),(),(),(\times),\ldots)\rangle\]
+is an $\Upsilon$algebra.
+\end{DoyeDefinition}
+
+\begin{DoyeNotation}
+\label{Doye4.2.10}
+Let $\langle A,\alpha\rangle$ be a
+$\Sigma$algebra. For an operator symbol $\sigma_{n,q,s}$ of the
+signature $\langle\Sigma,S\rangle$ the function associated with this
+symbol in $\langle A,\alpha\rangle$ is represented by either
+$\alpha_{n,q,s,\sigma}$ or $\alpha_{\sigma_{n,q,s}}$.
+\end{DoyeNotation}
+
+This second form of notation is useful for when we refer to operator
+symbols by names other than those in the form $\sigma_{n,q,s}$. For
+example, if $\tau = \sigma_{n,q,s}$ then
+\[\alpha_{n,q,s,\sigma} = \alpha_{\sigma_{n,q,s}} = \alpha_\tau\]
+
+\begin{DoyeDefinition}
+\label{Doye4.2.11}
+Given $\langle A,\alpha\rangle$,
+$\langle B,\beta\rangle$ both $\Sigma$algebras, then a
+$\Sigma$homomorphism\\
+$\phi:\langle A,\alpha\rangle\rightarrow\langle B,\beta\rangle$
+is an $S$indexed family of functions
+$\phi_s:A_s\rightarrow B_s$ (for each $s$ in $S$) such that
+\[(\forall n\in\mathbb{N}\cup\{0\})
+(\forall q{\rm\ arities\ of\ rank\ }n)
+(\forall (a_1,\ldots,a_n)\in A^q)
+(\forall s\in S)
+(\forall \sigma \in \Sigma_{n,q,s})\]
+we have
+\[\phi_s(\alpha_{n,q,s,\sigma}(a_1,\ldots,a_n))=
+\beta_{n,q,s,\sigma}(\phi_{q_1}(a_1),\ldots,\phi_{q_n}(a_n))\]
+\end{DoyeDefinition}
+
+As an example of a homomorphism, let us consider our monoidal case
+once more. The map $\psi$ from $\mathbb{N}\cup\{0\}$ which
+maps\footnote{We haven't provided an exponentiation function in our
+monoidal algebra, but adding an extra sort and a function it is
+possible. Otherwise think of the map as taking 0 to 1; 1 to 2; 2 to
+2$\times$2; 3 to 2$\times$2$\times$2; and so on.} $n\mapsto 2^n$ is
+a homomorphism.
+
+\subsection{Term Algebras}
+\label{DoyeSec4.3}
+
+Term algebras provide us with at least one example of an algebra for
+each signature. In some sense, it is the ``freeest'' algebra of the
+signature and all other algebras are isomorphic to quotients of the
+term algebra.
+
+Notice that given $\langle\Upsilon,U\rangle$ the definition of the
+monoidal signature from Example \ref{Doye4.2.8}, the term algebra
+is not the free monoid, since we have not added in any ``laws'' or
+``equations'' to the algebra. Thus we do not have associativity in the
+term algebra, whereas we do in the free monoid.
+
+Thus we see that, as yet, universal algebra does not model real
+mathematics perfectly. However this situation will be remedied
+somewhat in section \ref{DoyeSec4.6}.
+
+\begin{DoyeNotation}
+\label{Doye4.3.1}
+We will define the set $\Delta$ to be the set
+containing three special symbols
+\[\Delta := \{(\}\cup\{)\}\cup\{,\}\]
+\end{DoyeNotation}
+
+$\Delta$ is just a piece of notation that will make the following
+definition less verbose.
+
+\begin{DoyeDefinition}
+\label{Doye4.3.2}
+Let $X$ be an $S$indexed family of sets
+disjoint from each other, from the set $\Delta$ and from
+$\bigcup_{n,q,s}\Sigma_{n,q,s}$. We define $T_\Sigma(X)$ to be the
+$S$indexed family of sets of strings of symbols from
+$\bigcup_{s\in S}X_x\cup\Delta\cup\bigcup_{n,q,s}\Sigma_{n,q,s}$
+each set as small as possible satisfying these conditions:
+\begin{enumerate}
+\item $(\forall s \in S)(\Sigma_{0,(),s} \subseteq T_\Sigma(X)_s)$
+\item $(\forall s \in S)(X_s \subseteq T_\Sigma(X)_s)$
+\item $(\forall \sigma \in \Sigma_{n,q,s})
+(\forall i \in \{1,\ldots,n\})
+(\forall t_i \in T_\Sigma(X)_{q_i})
+(\sigma(t_1,\ldots,t_n)\in T_\Sigma(X)_s)$
+\end{enumerate}
+
+We make $T_\Sigma(X)$ into a $\Sigma$algebra by defining
+operators $\sigma_T$ on $T_\Sigma(X)$, for each
+$\sigma \in \Sigma_{n,q,s}$ via:
+\begin{itemize}
+\item If $n=0$ then $\sigma_T:=\sigma$ (Guaranteed to be in
+$T_\Sigma(X)$ by (1)).
+\item Else, define $\sigma_T(t_1,\ldots,t_n)$ to be the string
+$\sigma(t_1,\ldots,t_n)$
+\end{itemize}
+
+$T_\Sigma(X)$ is called the {\rm term algebra}, and an element
+of $T_\Sigma(X)$ is called a {\rm term}.
+\end{DoyeDefinition}
+
+\subsection{Ordersorted algebras}
+\label{DoyeSec4.4}
+
+Order sorted algebras extend the concept of universal algebras by
+imposing an order on the elements of the sortlist. This can be useful
+if we know that all algebras of our signature
+$\langle\Sigma, S\rangle$ have the carrier of $S_2$ as a subset of
+$S_1$, say.
+
+The ordering of sorts imposes a subtype lattice on the sorts (and
+hence their carriers). This can then be used in any algebra of the
+signature to either restrict a function already defined on one type
+to a subtype of that type, or extend a function on a type to a partial
+functon of the supertype. Partial functions and order sorted algebra
+are discussed in section \ref{DoyeSec5.2}.
+
+Firstly, we had better define what we mean by an ``order''.
+
+\begin{DoyeDefinition}
+\label{Doye4.4.1}
+A strict partial order on a set $S$ is a
+relation $\prec$ on $S$ which is transitive, antisymmetric, and
+irreflexive.
+\end{DoyeDefinition}
+
+A weak partial order on a set $S$ is a relation $\preceq$ such
+that,
+$a\preceq b \Leftrightarrow (a \prec b) \lor (a = b)$.
+Such a relation is transitive.
+
+\begin{DoyeNotation}
+\label{Doye4.4.2}
+Let $S$ be a set of sort symbols, such that there
+is a partial order $\prec$ defined on $S$, and a ``top'' element $u$
+of $S$ such that $s \prec u$ for all $s$ in $S$.
+\end{DoyeNotation}
+
+$u$ provides us with a universe in which to work. Equivalently, we
+could set $u$ to be any class$_w$ which is ``big enough'' (The term
+class$_w$ is defined later.)
+
+\begin{DoyeDefinition}
+\label{Doye4.4.3}
+Extend $\preceq$ from $S$ to the $S$arities of
+rank $n$ by defining\\
+$(s_1,\ldots,s_n)\preceq(t_1,\ldots,t_n)$ iff
+$(\forall i \in \{1,\ldots,n\})(s_i\preceq t_i)$.
+\end{DoyeDefinition}
+
+\begin{DoyeDefinition}
+\label{Doye4.4.4}
+An ordersorted, total $\Sigma$algebra is an
+ordered triple\\
+$\langle A,\{A_s : s \in S\},\alpha\rangle$, where $A$
+is a class known as the {\rm universe}, $\{A_s,s \in S\}$ is an
+$S$indexed family of subsets of $A$, known as the carriers of the
+algebra, and $\alpha$ is a set of sets of functions
+$\alpha_{n,q,s}=\bigcup_{\sigma\in\Sigma_{n,q,s}}
+\{\alpha_{n,q,s,\sigma} : A^q\rightarrow A_s\}$, such that:
+\begin{enumerate}
+\item $A_u=A$
+\item If $s\preceq s^\prime$ in $S$, then $A_s \subseteq A_{s^\prime}$
+\item If $\sigma\in\Sigma_{n,q,s}\cap\Sigma_{n,q^\prime,s^\prime}$,
+with $s\preceq s^\prime$ and $q^\prime \preceq q$, then
+$\alpha_{n,q,s,\sigma}\vert_{A^{q^\prime}}=
+\alpha_{n,q^\prime,s^\prime,\sigma}$
+\end{enumerate}
+
+\end{DoyeDefinition}
+
+Strictly speaking, that last condition should be
+\[\iota_{A_s\rightarrow A_{s^\prime}}\circ
+\alpha_{n,q,s,\sigma}\vert_{A^{q^\prime}} =
+\alpha_{n,q^\prime,s^\prime,\sigma}\]
+
+(where $\iota_{A_s\rightarrow A_{s^\prime}}$ is the inclusion
+operator $A_s\rightarrow A^\prime_s$) since otherwise the target
+of the left hand side would be $A^s$ and of the right hand side would
+be $A^{s^\prime}$.
+
+This is typical of the sort of ``abuse of notation'' that computer
+systems often have to implement.
+
+The definition of order sortedness ensures some confluence amongst
+operators on subtypes. However, it does not provide enough for most
+sensible applications. The following definition ensures a more
+confluent system.
+
+\begin{DoyeDefinition}
+\label{Doye4.4.5}
+The ordersorted signature $\Sigma$ is regular
+if whenever $\tilde{q}$ is an arity and $\sigma\in\Sigma_{n,q,s}$ with
+$\tilde{q}\preceq q$, there is a least pair $q^\prime$,$s^\prime$ such
+that $\sigma\in\Sigma_{n,q^\prime,s^\prime}$ and
+$\tilde{q}\preceq q^\prime$ and $s^\prime\preceq s$.
+\end{DoyeDefinition}
+
+Now, we will extend the definition of term algebras to the order
+sorted case.
+
+\begin{DoyeDefinition}
+\label{Doye4.4.6}
+Let $X$ be an $S$indexed family of sets
+disjoint from each other, from the set $\Delta$ and from
+$\bigcup_{n,q,s}\Sigma_{n,q,s}$. We define $T_\Sigma(X)$ to be the
+$S$indexed family of sets of strings of symbols from
+$\bigcup_{n,q,s}X_s\cup\Delta\cup
+\bigcup_{n,q,s}\Sigma_{n,q,s}$, each set of small as possible
+satisfying these conditions:
+
+\begin{enumerate}
+\item $(\forall s\in S)(\Sigma_{0,(),s}\subseteq T_\Sigma(X)_s)$
+\item $(\forall s\in S)(X_s \subseteq T_\Sigma(X)_s)$
+\item $(\forall s,s^\prime\in S)
+((s\preceq s^\prime) \Rightarrow (T_\Sigma(x)_s\subseteq
+T_\Sigma(X)_{s^\prime}))$
+\item $(\forall \sigma \in \Sigma_{n,q,s})
+(\forall i \in \{1,\ldots,n\})
+(\forall t_i\in T_\Sigma(X)_{q_i})
+(\sigma(t_1,\ldots,t_n)\in T_\Sigma(X)_s)$
+\end{enumerate}
+
+We make $T_\Sigma(X)$ into a $\Sigma$algebra by letting the
+first component be $T_\Sigma(X)_u$ and defining operators $\sigma_T$
+on $T_\Sigma(X)$, for each $\sigma\in\Sigma_{n,q,s}$ via:
+\begin{itemize}
+\item If $n=0$ then $\sigma_T:=\sigma$. (Guaranteed to be in
+$T_\Sigma(X)_s$ by (1))
+\item Else, define $\sigma_T(t_1,\ldots,t_n)$ to be the string
+$\sigma(t_1,\ldots,t_n)$
+\end{itemize}
+
+$T_\Sigma(X)$ is called the {\rm algebra}, and an element of
+$T_Sigma(X)$ is called a {\rm term}.
+\end{DoyeDefinition}
+
+The following theorem proves the ``freeness'' of term algebras. That
+is to say all algebras are isomorphic to a quotient of the term
+algebra. In this way we see that all algebras, once represented as a
+term algebra and a set of rewrite rules are easily implementable in a
+rewrite system.
+
+It also says something about the constructibility of types. That is,
+if $\bigcup_{n,q,s}\Sigma_{n,q,s}$ is finite then clearly only a
+finite number of functions in each and every $\Sigma$algebra
+construct the whole algebra.
+
+Moreover, suppose in every real algebra which we wish to study, a
+certain set of equations hold (see section \ref{DoyeSec4.6}).
+Then all our algebras are isomorphic to
+factors of the term algebra factored out by that set of equations.
+
+Then if every element of this freeest factor algebra is equal to one
+constructed by a (potentially very small, finite) subset of a
+(potentially infinite) $\bigcup_{n,q,s}\Sigma_{n,q,s}$, we may utilise
+this to construct elements of our algebra.
+
+In the automated coercion algorithm (section \ref{DoyeSec7.3})
+we utilise a small (but not
+necessarily minimal) set to construct all (or some) of the elements of
+one of the sorts of an algebra.
+
+\begin{DoyeTheorem}
+\label{Doye4.4.7}
+{\bf (First universality theorem)} Let
+$\langle A,\alpha\rangle$ be any $\Sigma$algebra, $\theta$ any map
+($S$indexed family of maps) from $X$ into $A$. Then there exists a
+unique $\Sigma$homomorphism $\theta^*$ from $T_\Sigma(S)$ to $A$ such
+that $(\forall s \in S)(\forall x \in X_s)$
+\[\theta_s^*(\iota(x))=\theta_s(x)\]
+\end{DoyeTheorem}
+
+The proof may be found in \cite{Dave93a}
+
+\subsection{Extension of signatures}
+\label{DoyeSec4.5}
+
+In this section we will formalise what we mean for one algebra to be
+an extension of another, or more importantly, from our point of view,
+for one algebra to be a portion of another.
+
+More formally we are saying how the abstract datatypes (or categories
+or signatures) may inherit from each other. This sometimes corresponds
+to algebras depending on each other.
+
+First, a piece of notation.
+
+\begin{DoyeNotation}
+\label{Doye4.5.1}
+If $S$ and $T$ are two sets of sets both indexed
+by the same set, $I$, we say that
+$S \overset{\rightarrow}{\subseteq} T$ iff
+$(\forall i \in I)(S_i \subseteq T_i)$
+\end{DoyeNotation}
+
+This extends the definition of subsets to $n$tuples of sets.
+
+\begin{DoyeDefinition}
+\label{Doye4.5.2}
+Let $S$, $S^\prime$ be two sortlists, such
+that, as sets of symbols $S\subseteq S^\prime$, and that
+$(\forall s,t\in S)((s\preceq_S t) \Leftrightarrow
+(s \preceq_{S^\prime} t))$. Let $\Sigma$ be an $S$sorted signature
+and $T$ be a $S^\prime$sorted signature. If
+$\Sigma\overset{\rightarrow}{\subseteq} T$, we say that $\Sigma$ is a
+{\rm subsignature} of $T$ and that $T$ is a supersignature of
+$\Sigma$.
+\end{DoyeDefinition}
+
+Thus we have the obvious definition of subsignature. As an example,
+the monoidal signature is a subsignature of the signature for
+groups. The notion of subsignature corresponds directly with that of
+subcategory.
+
+\begin{DoyeDefinition}
+\label{Doye4.5.3}
+With $S$, $S^\prime$, $\Sigma$, $T$ as in the
+previous definition, let $\langle A,\alpha\rangle$
+be an $S^\prime$sorted $T$ algebra. Define
+$\langle A,\alpha\rangle\vert_\Sigma$,
+called $\langle A,\alpha\rangle$ restricted to $\Sigma$, to be the
+$S$sorted $\Sigma$algebra with carriers, those carriers of
+$\langle A,\alpha\rangle$ which are indexed by sort symbols from $S$,
+and operators, $n$ary operators $\alpha_\tau$ of arity $q$, and
+result sort $s$, for every $\tau\in\Sigma_{n,q,s}$.
+\end{DoyeDefinition}
+
+This is applying the forgetful functor (from the category
+(corresponding to) $T$ to that (corresponding to) $\Sigma$) to
+$\langle A,\alpha\rangle$.
+
+\subsection{The equational calculus}
+\label{DoyeSec4.6}
+
+Again, we borrow heavily from Davenport's lecture
+notes\cite{Dave93a}. Throughout this section, we assume that
+$S=\{s_1,\ldots,s_n\}$ is our indexing family of sort symbols, and
+$\Sigma = \{\Sigma_{n,q,s}\}$ is an $S$sorted signature.
+
+The equational calculus presented here applies to multisorted
+algebra. The reader will see that it clearly may be extended to the
+ordersorted case.
+
+The equational calculus allows us to add ``equations'' to our
+signatures (and hence, algebras). This will allow us to assert facts
+about all the algebra in a signature. For example, we may wish to note
+that one of the binary operators is always associative. Other more
+complicated expressions are available also.
+
+The equational calculus does not allow us to define everything that we
+need: only those things that are easily definable as equations.
+
+\begin{DoyeDefinition}
+\label{Doye4.6.1}
+An $S$indexed family of relations
+$R = \{R_{s_1},\ldots,R_{s_n}\}$ on a $\Sigma$algebra,
+$\langle A,\alpha\rangle$ is called a $\Sigma$congruence if it
+satisfies the following four families of conditions:
+\[\begin{array}{rclr}
+a\in A_{s_i} & \Rightarrow & aR_{s_i}a & (R)\\
+aR_{s_i}b & \Rightarrow & bR_{s_i}a & (S)\\
+aR_{s_i}b {\rm\ and\ }bR_{s_i}c & \Rightarrow & aR_{s_i}c & (T)\\
+(\forall \sigma\in\Sigma_{n,q,s})
+(a_1 R_{q_1}b_1,\ldots,a_n R_{q_n}b_n) & \Rightarrow &
+\sigma(a_1,\ldots,a_n)R_s\sigma(b_1,\ldots,b_n) & (C_\sigma)
+\end{array}\]
+\end{DoyeDefinition}
+
+The first three conditions imply that $R_{s_i}$ is an
+{\sl equivalence relation} on the set $A_{s_i}$, while the conditions
+($C$) explain how $R$ relates to the various operators of
+$\Sigma$. The operators of $\Sigma_{n,q,s}$ are welldefined on the
+equivalence classes.
+
+\begin{DoyeDefinition}
+\label{Doye4.6.2}
+Let $\langle A,\alpha\rangle$ be an
+$\Sigma$algebra, and $\equiv$ be a $\Sigma$congruence on
+$\langle A,\alpha\rangle$. Define $\langle A,\alpha\rangle/\equiv$ to
+be the $\Sigma$algebra $\langle B,\beta\rangle$, where the carrier
+set $B_{s_i}$ of $B$ is the set of equivalence classes of $A_{s_i}$
+under the equivalence relation $\equiv_{s_i}$, and $\beta_\sigma$ is
+the operator defined by
+\[\beta_\sigma([a_1],[a_2],\ldots,[a_n])=
+[\alpha_\sigma(a_1,a_2,\ldots,a_n)]\]
+for every operator symbol $\sigma$ in every $\Sigma_{n,q,s}$.
+\end{DoyeDefinition}
+
+This is merely the quotient algebra, and to be sure, the following is
+a theorem.
+
+\begin{DoyeTheorem}
+\label{Doye4.6.3}
+The operators $\beta_\sigma$ in the above definition are welldefined.
+\end{DoyeTheorem}
+
+The following definition actually turns out to be very important.
+
+\begin{DoyeDefinition}
+\label{Doye4.6.4}
+We say that a sort $s$ is {\rm void} in the
+signature $\Sigma$ if $T_\Sigma(\emptyset)_s = \emptyset$.
+\end{DoyeDefinition}
+
+Basically, having a void sort $\tilde{s}$ in the signature means that
+there are no constants of that type
+$(\Sigma_{0,(),\tilde{s}}=\emptyset$) and that one of the following is
+true.
+\begin{itemize}
+\item no operators have $\tilde{s}$ as a return type:
+$((\forall q,n)(\Sigma_{n,q,s}=\emptyset)$ where $q$ is an arity of
+rank $n$)
+\item every operator with $\tilde{s}$ as a return type has an argument
+whose sort is either void or $\tilde{s}$:
+$((\forall q,n)(\Sigma_{n,q,s}\ne\emptyset)\Rightarrow
+(\exists i \in \{1,\ldots,n\})
+(q_i {\rm\ is\ a\ void\ sort\ or\ }\tilde{s}))$ where $q$ is an arity
+of rank $n$)
+\end{itemize}
+
+\begin{DoyeLemma}
+\label{Doye4.6.5}
+If $s$ is not void in the signature $\Sigma$, then in
+every $\Sigma$algebra $\langle A,\alpha\rangle$, $A_s\ne\emptyset$.
+\end{DoyeLemma}
+
+Goguen and Meseguer suggest the following rules of deduction for a
+sound multisorted equational calculus.
+
+\begin{DoyeNotation}
+\label{Doye4.6.6}
+Let $X$ be an $S$indexed family of sets of
+variable symbols, such that each $X_{s_i}$ is disjoint from all the
+others, from the operator symbols of $\Sigma$, and from any symbols in
+any particular algebras we may be reasoning over.
+
+We will be reasoning frequently with $S$indexed families of
+sets, and wishing to perform operations on them. Let
+$X=\langle X_1,\ldots,X_n\rangle$ and
+$Y=\langle Y_1,\ldots,Y_n\rangle$ be two $S$indexed families of sets,
+and define $X\overset{\rightarrow}{\cup}Y$ to be the $S$indexed family
+$\langle X_1\cup Y_1,\ldots,X_n\cup Y_n\rangle$. Similarly, we will
+write $X\overset{\rightarrow}{\subseteq}Y$ to indicate that each
+component of $X$ is a subset of the corresponding element of $Y$.
+
+A final piece of notation is that the indexed family of empty
+sets will be donoted by $\overset{\rightarrow}{\emptyset}$.
+\end{DoyeNotation}
+
+\begin{DoyeDefinition}
+\label{Doye4.6.7}
+A {\rm multisorted equation} for the signature
+$\Sigma$ consists of a triple $\langle Y,T_1,t_2\rangle$ where
+$Y\overset{\rightarrow}{\subseteq}X$, $t_1$ and $t_2$ are terms from
+the same carrier set of $T_\Sigma(X)$ (or
+$T_\Sigma(X\overset{\rightarrow}{\cup}A)$ if we are dealing with
+equations in the particular algebra $\langle A,\alpha\rangle$), and
+every variable occurring in $t_1$ and $t_2$ occurs in the appropriate
+memeber of $Y : t_1,t_2\in T_\Sigma(Y)$. Such equations are written
+$\forall Y t_1=t_2$.
+
+If $t_1$ and $t_2$ come from the same carrier set of
+$T_\Sigma(X)$ we say that the equation is $\Sigma$generic.
+\end{DoyeDefinition}
+
+One should read the symbol $\forall Y$ as meaning ``for all values of
+all the variables of $Y$ in the appropriate sorts (and there had
+better be some values in those sorts)''. It is this interpretation
+that will solve the paradox mentioned earlier.
+
+\begin{DoyeDefinition}
+\label{Doye4.6.8}
+An {\rm equational system} for the signature
+$\Sigma$ is a set of equations for $T_\Sigma(X)$ (or
+$T_\Sigma(X\overset{\rightarrow}{\cup}A$) if we are dealing with
+equations in a particular algebra $\langle A,\alpha\rangle$).
+\end{DoyeDefinition}
+
+We will tend to write $e = f$ for an equation from an equational
+system, meaning $\forall Y e=f$ where $Y$ is the $S$indexed family of
+sets of variables consisting {\sl precisely} of those variables
+occurring in $e$ and $f$.
+
+\begin{DoyeNotation}
+\label{Doye4.6.9}
+$x_i/t_i$ means substitute the variable $x_i$ with the
+term $t_i$. We call this a {\rm substitution instance.}
+\end{DoyeNotation}
+
+\begin{DoyeDefinition}
+\label{Doye4.6.10}
+A {\rm proof in the multisorted equational calculus}
+of the equation $\forall Y e = f$ from the equational system
+$\mathcal{E}$ is a finite set of equations $\forall Y_i e_i=f_i$ such
+that each equation is justified by one of the seven following rules of
+inference.
+\[\begin{array}{cr}
+\overline\forall Y\quad e[x_1/t_1,\ldots,x_n/t_n] =
+f[x_1/t_1,\ldots,x_n/t_n] & (E)
+\end{array}\]
+where $\forall X e=f$ is an equation of $\mathcal{E}$, the $t_i$
+are terms of the appropriate sort of $T_\Sigma(X)$ and $Y$ is the
+$S$indexed family of sets whose $s$th component is the set of all
+variables of sort $s$ in all the $t_i$ and those variables of $X_s$
+which have not been substituted for, i.e. which are not one of the
+$x_i$.
+\[\begin{array}{cr}
+\overline\forall Y\quad e = e & (R)\\
+\end{array}\]
+where $Y$ is the $S$indexed family of sets whose $s$th
+component is the set of all variables of sort $s$ in $e$
+\[\begin{array}{cr}
+\forall Ye = f \quad \overline\forall Y f = e & (S)\\
+\forall Y e = f \quad \forall Y^\prime f = g \quad
+\overline\forall Y \overset{\rightarrow}{\cup}Y^\prime~ e = g &
+(T)\\
+\left.
+\begin{array}{lr}
+\forall Y_1~ e_1=f_1 \ldots \forall Y_n~ e_n=f_n\\
+\overline{\forall} Y_1\overset{\rightarrow}{\cup}\ldots
+\overset{\rightarrow}{\cup}Y_n~
+\sigma(e_1,\ldots,e_n)=\sigma(f_1,\ldots,f_n)\\
+\end{array}
+\right\} & (C_\sigma)
+\end{array}\]
+where $\sigma$ is any symbol of $\Sigma_{n,q,s}$, and each $e_i$
+is a term of sort $q_i$
+\[\begin{array}{lr}
+\forall Y~e = f\quad\overline{\forall}Y^\prime~e=f & (A)
+\end{array}\]
+where $Y\overset{\rightarrow}{\subseteq}Y^\prime$
+\[\begin{array}{cr}
+\forall Y~e=f\quad\overline{\forall}\langle Y_1,\ldots,Y_{i1}
+\backslash \{y\},Y_{i+1},\ldots,Y_n\rangle\quad e=f & (Q)
+\end{array}\]
+where $y$ does not occur in $e$ or $f$, and the sort $i$ is nonvoid
+for $\Sigma$.
+\end{DoyeDefinition}
+
+We use the notation $\vdash\forall Y~e=f$ (or
+$\vdash_\mathcal{E}\forall Y~e=f$ if we wish to make clear which
+equational system is being considered) to mean that $e=f$ is provable
+in the equational system using the above rules of inference.
+
+\begin{DoyeDefinition}
+\label{Doye4.6.11}
+If $\forall Y~e=f$ is an $S$sorted
+$\Sigma$equation (call it E), and $\langle A,\alpha\rangle$ is a
+$\Sigma$algebra, then we say that $\langle A,\alpha\rangle$ satisfies
+E, or that $\langle A,\alpha\rangle$ is a model for E, if for all
+$S$sorted maps $\theta$ from $Y$ to $A$, $\theta^*(e)=_A\theta^*(f)$,
+where $\theta^*$ is the map from
+$T_\Sigma(X\overset{\rightarrow}{\cup}A)$ to
+$\langle A,\alpha\rangle$, whose existence is guaranteed by the
+theorem \ref{Doye4.4.7}. We extend the notation to sets of equations
+$\mathcal{E}$ by insisting that $\langle A,\alpha\rangle$ be a model
+for each equation in $\mathcal{E}$.
+\end{DoyeDefinition}
+
+\begin{DoyeTheorem}
+\label{Doye4.6.12}
+{\bf (The Soundness Theorem)} If
+$\langle A,\alpha\rangle$ is a model for $\mathcal{E}$, and
+$\vdash_\mathcal{E} \forall Y~e=f$, then $\langle A,\alpha\rangle$
+is a model for $\mathcal{E}\cup\{\forall Y~e=f\}$.
+\end{DoyeTheorem}
+
+The proof of the soundness theorem may be found in \cite{Gogu82}.
+
+\begin{DoyeDefinition}
+\label{Doye4.6.13}
+Let $\langle A,\alpha\rangle$ be a
+$\Sigma$algebra, and let $\mathcal{E}$ be an equational system for
+$\langle A,\alpha\rangle$. The congruence induced by $\mathcal{E}$,
+denoted by $\equiv_\mathcal{E}$ on $\langle A,\alpha\rangle$ is
+defined by $A\equiv_\mathcal{E} B$ if, and only if,
+$\vdash_\mathcal{E} \forall Y~a=b$, where $Y$ is the $S$sorted family
+of empty sets.
+\end{DoyeDefinition}
+
+The following two definitions are very important. A theory specifies a
+type, and we define a variety to be the collection of all types which
+model that theory.
+
+\begin{DoyeDefinition}
+\label{Doye4.6.14}
+We define a theory to be the ordered pair
+$\langle\langle\Sigma, S\rangle,S\rangle$ where $\Sigma$ is an $S$sorted
+signature and $S$ is a set of $S$sorted $\Sigma$equations. We say
+that a $\Sigma$algebra {\rm models} or {\rm satisfies} the theory iff
+it is a model for $S$.
+\end{DoyeDefinition}
+
+\begin{DoyeDefinition}
+\label{Doye4.6.15}
+The collection of all models of a particular theory
+is called a variety
+\end{DoyeDefinition}
+
+Clearly, since a signature $\langle\Sigma,S\rangle$ may be viewed as a
+theory $(\langle\Sigma,S\rangle,\emptyset)$, the collection of all
+$\Sigma$algebras forms a variety.
+
+When referring to the variety of all models of a particular
+signature, (for example, $\langle\langle\Sigma,S\rangle,S\rangle$) we
+usually say the ``variety defined by (or specified by) the signature
+$\langle\langle\Sigma,S\rangle,S\rangle$.''
+
+\begin{DoyeTheorem}
+\label{Doye4.6.16}
+{\bf (Second universality theorem)} Let $X$ be an
+$S$sorted set of variables, $\Sigma$ an $S$sorted operator set,
+$\mathcal{E}$ a set of equations for $\Sigma$,
+$\langle A,\alpha\rangle$ a $\Sigma$algebra which is a model for
+$\mathcal{E}$, and $\theta$ an $S$sorted mapping from $X$ to $A$. Then
+there is a unique $\Sigma$homomorphism $\theta^{**}$ from
+$T_\Sigma(X)/\equiv_\mathcal{E}$ to $A$ such that
+\[\begin{array}{cr}
+\theta^{**}(\iota^*(x))=\theta(x) & (**)
+\end{array}\]
+for all $x\in X$, where $\iota^*$ is the map from $X$ into
+$T_\Sigma(X)/\equiv_\mathcal{E}$ defined by $x\mapsto[x]$.
+\end{DoyeTheorem}
+
+\begin{DoyeTheorem}
+\label{Doye4.6.17}
+{\bf (The Completeness Theorem}) If every
+$\Sigma$algebra which satisfies the equation $\mathcal{E}$ also
+satisfies the equation $\forall Y~e=f$, then
+$\vdash_\mathcal{E}\forall Y~e=f$.
+\end{DoyeTheorem}
+
+Again, the proof of this may be found in \cite{Gogu82}
+
+Finally, we state the definition of an extension and a protecting
+extension. Extensions are selfexplanatory.
+
+\begin{DoyeDefinition}
+\label{Doye4.6.18}
+Suppose that $\Sigma$ and
+$\Sigma\overset{\rightarrow}{\cup}T$ are signatures where $\Sigma$ is
+$S$sorted and $\Sigma\overset{\rightarrow}{\cup}T$ is
+$S^\prime$sorted where $S\subseteq S^\prime$. Then
+$\Sigma\overset{\rightarrow}{\cup}T$ is said to be an extension of
+$\Sigma$.
+\end{DoyeDefinition}
+
+A protecting extension is an extension which preserves the equational
+system for the theory. Combining the second universality theorem
+in section \ref{Doye4.6.16} with
+the definition of protecting extension allows us to view a model of a
+theory as a model of a protecting extension of that theory.
+
+More importantly, if we have an algebra which is a model for a
+protecting extension of a theory, then we may view the algebra as a
+model of that theory (unextended).
+
+For example, if the Ring theory is defined to be a protecting
+extension of the Group theory, then we may view any ring
+(Ringalgebra) as a group (Groupalgebra).
+
+\begin{DoyeDefinition}
+\label{Doye4.6.19}
+With $\Sigma$, $T$, $S$, and $S^\prime$ as in
+\ref{Doye4.6.18}, Let $\mathcal{E}$ be an equational system on
+$\Sigma$. Also let $\mathcal{E}\cup\mathcal{F}$ be an equational
+system on $\Sigma\overset{\rightarrow}{\cup}T$. Such an extension is
+called a protecting extension if
+\[T_{\Sigma\overset{\rightarrow}{\cup}T}(X)/
+\equiv_{\mathcal{E}\cup\mathcal{F}}\vert_\Sigma\]
+is isomorphic to $T_\Sigma(X)/\equiv_\mathcal{E}$ (isomorphism meaning
+``isomorphism as $\Sigma$algebras'').
+\end{DoyeDefinition}
+
+Notice that the definition of protecting extension is equivalent to
+the notion of {\sl enrichment} given in \cite{Pada80} (although, this
+does not allow for the existence of $S^\prime$). Thus a theory
+$\Omega_1$ is a protecting extension of another $\Omega_0$ iff
+$\Omega_1$ is complete and consistent with respect to $\Omega_0$.
+
+\subsection{Signatures, theories, varieties, and Axiom}
+\label{DoyeSec4.7}
+
+Axiom's type system uses the terminology from category theory, yet its
+design is based on order sorted signatures.
+
+A {\bf Category} definition in Axiom (i.e. the source code that
+defines the {\bf Category}) is equivalent to a signature or theory,
+being a specification of a type or types.
+
+The {\bf Category} viewed as a collection of objects ({\bf Domains})
+is the variety specified by the theory which defined the
+{\bf Category} in the {\bf Category} definition.
+
+The sorts are {\bf \%} for the (principal) sort (see definition
+\ref{Doye7.2.1}), and the argument and return types of all the operator
+symbols of the {\bf Category}\footnote{Unless they are concrete types
+ {\bf Domains}. See section \ref{DoyeSec9.6}}.
+
+For example, {\bf PolynomialCategory(R,E,V)} is a {\bf Category}.
+{\bf \%} is the (principal) sort. Other sorts include {\bf R},
+{\bf E}, {\bf V} a sort each for the {\bf Boolean} and
+{\bf PositiveInteger} types.
+
+The equations of a theory in an Axiom {\bf Category} definition are
+either defined in the comments or a certain ``attributes'' of
+operators. For example {\bf commutative(*)} means that {\bf *} is
+commutative and the traditional commutativity equation (for the
+operator {\bf *}) is an equation of the theory. (There is currently no
+method for enforcing the equations to hold in any model.)
+
+An algebra (or model for a theory) in Axiom is a
+{\bf Domain}. Declaring a {\bf Domain} to be in a {\bf Category} is
+equivalent to saying that it is an algebra of that signature (or model
+of that theory). Or in other words, a member of the variety defined
+by the theory which specifies the {\bf Category}.
+
+For example, {\bf Polynomial(Integer)} is a model for
+{\bf PolynomialCategory(R,E,V)}.
+
+An operator symbol in Axiom is a function declaration in a
+{\bf Category}. An operator name in Axiom always corresponds to the
+operator symbol.
+
+For example, $+$ is an operator symbol in {\bf Ring}. In
+{\bf Integer}, a model for {\bf Ring}, the operator name of
+$+$ is (and has to be) $+$.
+
+A carrier is the concrete type substituted for a parameter in any
+instantiation of a {\bf Domain}.
+
+In {\bf Polynomial(Integer)}, {\bf Polynomial(Integer)} is the carrier
+{\bf \%}. Whereas {\bf Integer}, {\bf NonNegativeInteger} and
+{\bf Symbol} are the carriers of {\bf R}, {\bf E}, and {\bf V},
+respectively. (No sort is given for the {\bf Boolean} and
+{\bf PositiveInteger} types.)
+
+All of Axiom's extensions are protecting extensions. That is, if a
+{\bf Category} is declared to extend another then it is always a
+protecting extension of that {\bf Category}.
+
+In section \ref{DoyeChap9} we will discuss how Axiom differs from order
+sorted algebra and how we may remedy this situation.
+
+\subsection{Conclusion}
+\label{DoyeSec4.8}
+
+In this section we have introduced all the basics of order sorted
+algebra and the equational calculus. We have also shown how these
+notions are represented in Axiom.
+
+We have demonstrated that order sorted algebra combined with the
+equational calculus provides a sound basis for a computer algebraic
+type system.
+
+A multisorted signature is a specification for a type and hence is an
+abstract datatype.
+
+Adding an order on the sorts to obtain an order sorted signature
+enforces relations between the sorts. It also guarantees sensible
+interaction between these carriers of these sorts and operators thereon
+in any algebra of the signature.
+
+Combining signatures with the equational calculus yields
+theories. Theories further enhance the usefulness of signatures by
+ensuring certain equations will hold in any model (algebra) of the
+theory (signature).
+
+\section{Extending order sorted algebra}
+\label{DoyeChap5}
+
+We will discuss how partial functions and conditional signatures may
+``tiein'' with traditional order sorted algebra. This will mean that
+any facts that we may prove for or use from traditional order sorted
+algebra will also apply when partial functions and/or conditional
+signatures are considered, provided certain extra facts hold.
+
+Next, we will look at the similarities between order sorted algebra
+and category theory. This will demonstrate why computer algebra
+systems such as Axiom use category theory terminology, whereas most of
+this work uses order sorted algebra as its framework.
+
+Last, we define what we mean by a coercion. This definition is
+fundamental to the rest of this work.
+
+\subsection{Partial Functions}
+\label{DoyeSec5.2}
+
+This subsection is based on \cite{Broy88} after a suggestion by
+Richardson and Martin.
+
+We ask the question, ``How do partial functions interact with
+classical universal algebra?''. We need this in case some of the
+functions used to create our coercions later are only partial. This
+can happen (see definition \ref{Doye7.3.3}). For example, the division
+operator in any quotient field is partial, but could be viewed as a
+constructor function.
+
+In our previous section on universal algebra, we defined an
+$S$operator of arity $q$, to be a (total) function from some $A^q$ to
+some element of $A$. (Where $A$ is a set of $S$carriers.) Is it
+possible to redefine this so that the $S$operators are partial?
+Indeed, is this necessary? One of the original reasons for the
+``invention'' of ordersorted algebra (definition \ref{Doye4.4.4}) (rather
+than multisorted algebra (see definition \ref{Doye4.2.9})) was so that all
+functions could be considered total. See, for example, \cite{Gogu92}.
+
+For example, if $\alpha_{\sigma_{1,(P),T}} : A_P\rightarrow A_T$ were
+a partial function in a $\Sigma$algebra, $\langle A,\alpha\rangle$,
+then we could insert a new sort $N\prec P$, such that
+$\alpha_{\sigma_{1,(N),T}} : A_N\rightarrow A_T$ were a total
+function.
+
+In the example of a quotient field, one would introduce a subsort of
+the integral domain which would represent all the nonzero elements of
+the domain.
+
+We may proceed by either attempting to redefine all of universal
+algebra using partial functions, or through some different
+mechanism. The following mechanism which uses ``virtual sorts'' turns
+out to be flawed. Virtual sorts are an onthefly way of generating
+sorts to represent things like the nonzero elements of an integral
+domain or nonempty stacks.
+
+\begin{DoyeDefinition}
+\label{Doye5.2.1}
+Let $\langle\Sigma, S\rangle$ define an
+ordersorted signature. If we define $\langle\Lambda,L\rangle$ to be
+the signature where
+\begin{enumerate}
+\item $L=S\cup\{u_1,\ldots,u_m\}$ (a set of symbols distinct from all
+those in $S$)
+\item $(\forall i \in \{1,\ldots,m\})(\exists s_{u_i}\in S)
+(u_i\prec_L s_{u_i})$
+\item $(\forall n\in \mathbb{N}\cup\{0\})(\forall s \in S)
+(\forall q\in S^n)(\Lambda_{n,q,s}=\Sigma_{n,q,s})$
+\item $(\exists n\in\mathbb{N})(\exists q\in L^n \backslash S^n)
+(\exists s\in S)(\Lambda_{n,q,s}\ne\emptyset)$ (Note that there may be
+more than one such triple $\langle n,q,s\rangle$)
+\end{enumerate}
+then we say that the $u_i$ are {\rm virtual sorts} of
+$\langle\Sigma, S\rangle$ and\\
+$\lambda_{n,q,s}\in\Lambda_{n,q,s}(n\in\mathbb{N})
+(q\in L^n \backslash S^n)(s\in S)$ a virtual operator symbol of
+$\langle\Sigma,S\rangle$.
+\end{DoyeDefinition}
+
+Unfortunately, virtual sorts, virtual operators, and homomorphism do
+not interact in a satisfactory manner. The introductions of a virtual
+sort in the source of a homomorphism may be meaningless in the target
+or vice versa.
+
+For traditional examples, like the nonempty stack, they are fine since
+this has some meaning in all stackalgebras. But for types like ``all
+the elements which do not map to 5 under a particular coercion,'' then
+it may be meaningless to create a virtual sort which attempts to
+represent this.
+
+Broy\cite{Broy88} defined $\Sigma$algebras as having either partial or
+total operators. A (partial) $\Sigma$homomorphism is then defined as
+follows:
+
+\begin{DoyeDefinition}
+\label{Doye5.2.2}
+{\bf ((Partial) homomorphism)} If
+$\langle A,\alpha\rangle$ and $\langle B,\beta\rangle$ are
+$\langle \Sigma,S\rangle$ algebras\footnote{with partial operators, in
+our terminology} and $\psi$ is a family of partial maps
+$\psi_s : A_s\rightarrow B_s$, the $\psi$ is a (partial)
+$\Sigma$homomorpsism
+$\langle A,\alpha\rangle\rightarrow\langle B,\beta\rangle$ iff the
+following two conditions are fulfilled:
+
+Firstly,
+\[(\forall n\in\mathbb{N}\cup\{0\})(\forall q{\rm\ arities\ of\ rank\ }n)
+(\forall s\in S)(\forall\sigma\in\Sigma_{n,q,s})\]
+\[(\forall(a_1,\ldots,a_n)\in A^q)\]
+{\rm if both}
+$\psi_s(\alpha_{\sigma_{n,q,s}}(a_1,\ldots,a_n))$ and
+$\beta_{\sigma_{n,q,s}}(\psi_{q_1}(a_1),\ldots,\psi_{q_n}(a_n))$
+{\rm are defined, then}
+\[\psi_s(\alpha_{\sigma_{n,q,s}}(a_1,\ldots,a_n)) =
+\beta_{\sigma_{n,q,s}}(\psi_{q_1}(a_1),\ldots,\psi_{q_n}(a_n))\]
+
+Secondly.
+\[(\forall n\in\mathbb{N}\cup\{0\})(\forall q{\rm\ arities\ of\ rank\
+}n)(\forall s\in S)(\forall\sigma\in\Sigma_{n,q,s})\]
+\[((\forall a_1,a^\prime_1\in A_{q_1}),\ldots,
+(\forall a_n,a^\prime_n\in A_{q_n})\]
+\[(\bigwedge_{i\in\{1,\ldots,n\}}(\phi_q(a_i)=_{\rm strong}
+\phi_{q_i}(a^\prime_i))))\]
+\[\Rightarrow\phi_s(\alpha_{\sigma_{n,q,s}}(a_1,\ldots,a_n))
+=_{\rm strong}\phi_s(\alpha_{\sigma_{n,q,s}}
+(a^\prime_1,\ldots,a^\prime_n))\]
+
+Where ``$=_{\rm strong}$'' is the strong equality defined via
+\[(a=_{\rm strong})\Leftrightarrow((a{\rm\ defined}\Leftrightarrow
+b{\rm\ defined})\land(a{\rm\ defined}\Rightarrow a=b))\]
+\end{DoyeDefinition}
+
+Broy's definition of homomorphism (definition \ref{Doye5.2.2}) is (as he
+states) rather liberal. A special factor which he notes is that the
+composition of partial homomorphisms need not be a homomorphism again.
+
+The following two definitions turn out to be useful in distinguishing
+between types of partial homomorphism.
+
+\begin{DoyeDefinition}
+\label{Doye5.2.3}
+Let $\langle \Sigma^\prime,S^\prime\rangle$ be a subsignature of
+$\langle \Sigma,S\rangle$. A $\Sigma^\prime$algebra
+$\langle A,\alpha\rangle$ is said to be a $\Sigma^\prime$subalgebra
+of the $\Sigma$algebra $\langle B,\beta\rangle$ iff
+\begin{enumerate}
+\item $(\forall s\in S^\prime)(A_s=B_s)$
+\item $(\forall n\in\mathbb{N}\cup\{0\})
+(\forall q{\rm\ arities\ of\ rank\ }n)(\forall s\in S)
+(\forall\sigma\in\Sigma_{n,q,s})
+(\alpha_\sigma=\beta_\sigma\vert_{A^q})$
+\end{enumerate}
+\end{DoyeDefinition}
+
+\begin{DoyeDefinition}
+\label{Doye5.2.4}
+Let $\langle \Sigma^\prime,S^\prime\rangle$ be a subsignature of
+$\langle \Sigma,S\rangle$. A $\Sigma^\prime$algebra
+$\langle A,\alpha\rangle$ is said to be a weak
+$\Sigma^\prime$subalgebra of the $\Sigma$algebra
+$\langle B,\beta\rangle$ iff
+\begin{enumerate}
+\item $(\forall s\in S^\prime)(A_s=B_s)$
+\item $(\forall n\in\mathbb{N}\cup\{0\})
+(\forall q{\rm\ arities\ of\ rank\ }n)(\forall s\in S)
+(\forall\sigma\in\Sigma_{n,q,s})(\alpha_\sigma
+\le_\bot \beta_\sigma\vert_{A^q})$
+\end{enumerate}
+where ``$\le_\bot$'' is defined via
+\[f\le_\bot g\Leftrightarrow(\forall x)((f(x){\rm\ is\ not\ defined\ }
+\lor (f(x)=g(x)))\]
+\end{DoyeDefinition}
+
+Broy notes that any partial homomorphism may be decomposed using the
+following methodology. A partial homomorphism $\phi : A\rightarrow B$
+defines a weak subalgebra $A^\prime$ of $A$ defined via
+\[(\forall s\in S)(A^\prime_s=\{a\in A_s : \psi(a){\rm\ defined}\})\]
+with the functions taking the meanings
+\[\alpha^\prime_{\sigma_{n,q,s}}(a_1,\ldots,a_n)=
+\alpha_{\sigma_{n,q,s}}(a_1,\ldots,a_n)\]
+if $(\forall i\in\{1,\ldots,n\})$($\phi(a_i)$ are defined) and
+$\phi(\alpha^\prime_{\sigma_{n,q,s}}(a_1,\ldots,a_n))$ is defined.
+Otherwise $\alpha^\prime_{\sigma_{n,q,s}}(a_1,\ldots,a_n)$ is not
+defined.
+
+By $\phi^\prime$ we denote the weak partial identity function
+$A\rightarrow A^\prime$. Then we define
+$\tilde{\phi} : A^\prime\rightarrow B$ to be the total homomorphism
+which is the restriction of $\phi$ to $A^\prime$.
+
+Being total, $\tilde{\phi}$ induces a weak subalgebra $B^\prime$ of
+$B$ defined via:
+\[(\forall s \in S)(B^\prime_s =
+\{b\in B_s : (\exists a \in A_s)(\tilde{\psi}(a)=b)\})\]
+with the functions defined via
+\[\beta^\prime_{\sigma_{n,q,s}}(a_1,\ldots,a_n)=
+\tilde{\phi}(\alpha_{\sigma_{n,q,s}}(a_1,\ldots,a_n))\]
+where $b_i=\tilde{\phi}(a_i)$ and
+$\beta_{\sigma_{n,q,s}}(a_1,\ldots,a_n)$ is defined.
+
+This then induces a total surjective homomorphism
+$\phi^n : A^\prime\rightarrow B^\prime$. Also, by construction
+$B^\prime$ is a weak subalgebra of $B$. Therefore there also exists a
+total injective homomorphism $\phi^m : B^\prime\rightarrow B$ which is
+the natural inclusion operator.
+
+As examples consider the following coercions. (We are only looking at
+the carrier of the principal sort (definition \ref{Doye7.2.1}) in
+these examples.
+
+\begin{DoyeExample}
+\label{Doye5.2.5}
+$\mathbb{Q}\rightarrow\mathbb{Z}_5$
+
+{\bf Fraction Integer $\rightarrow$ PrimeField 5}
+\[A^\prime = \mathbb{Q} \backslash \{q\frac{1}{5}~\vert~
+q\in\mathbb{Q} \backslash \{0\}\}\]
+\[B^\prime = B\]
+\end{DoyeExample}
+
+Notice that in this example, we are considering a
+field homomorphism, and that $A^\prime$ is a weak subfield of $A$.
+(For example $/$ is undefined on the pair (1,5) in $A^\prime$.)
+Clearly, $B^\prime$ is a subfield of $B$.
+
+\begin{DoyeExample}
+\label{Doye5.2.6}
+$\mathbb{Q}[x]\rightarrow\mathbb{Z}(x)=\mathbb{Q}(x)$
+
+{\bf Polynomial Fraction Integer $\rightarrow$
+Fraction Polynomial Integer}
+\[A^\prime = A\]
+\[B^\prime=mathbb{Q}[x]=\{p~\vert~p\in\mathbb{Q}(x)\land
+(\exists q\in\mathbb{Q}(x))(p=q\land{\rm\ denom}(q)\in\mathbb{Q})\}\]
+\end{DoyeExample}
+
+In this example, it is an integral domain homomorphism that concerns
+us. So although $B^\prime$ is only a weak subfield of $B$ this does
+not matter, as it is a subintegral domain of $B$.
+
+\begin{DoyeExample}
+\label{Doye5.2.7}
+
+{\bf Polynomial Fraction Integer $\rightarrow$
+Fraction Polynomial PrimeField 5}
+
+\[A^\prime = \mathbb{Q}[x] \backslash
+\{\Sigma_{i\in\mathbb{N}\cup\{0\}}(q_ix^i)\in\mathbb{Q}[x]~\vert~
+(\exists i\in\mathbb{N}\cup\{0\})
+(s\in\mathbb{Q} \backslash \{0\})
+(q_i=s\frac{1}{5})\}\]
+\[B^\prime=\mathbb{Z}_5[x]=
+\{p~\vert~p\in\mathbb{Z}_5(x)\land(\exists q\in\mathbb{Z}_5(x))
+(p=q \land{\rm\ denom}(q)\in\mathbb{Z}_5)\}\]
+\end{DoyeExample}
+
+In this example we are again considering an integral domain
+homomorphism, and both $A^\prime$ and $B^\prime$ are subintegral
+domains of $A$ and $B$, respectively.
+
+These show that real examples of coercions may indeed cause $A$ and
+$A^\prime$ to differ as well as $B$ and $B^\prime$.
+
+As Broy notes, this definition of partial homomorphism allows the
+everywhere undefined function to be a partial homomorphism. Thus this
+definition is too weak for our purposes.
+
+\begin{DoyeDefinition}
+\label{Doye5.2.8}
+A partial homomorphism, $\phi$ is called strict iff
+\[(\forall n\in\mathbb{N}\cup\{0\})
+(\forall q{\rm\ arities\ of\ rank\ }n)(\forall s \in S)
+(\forall \sigma\in\Sigma_{n,q,s})
+(\forall(a_1,\ldots,a_n)\in A^q)\]
+\[\phi(\alpha_\sigma(a_1,\ldots,a_n))=_{\rm strong}
+\beta_\sigma(\phi(a_1),\ldots,\phi(a_n))\]
+\end{DoyeDefinition}
+
+Broy notes that a strict homomorphism ensures that $B^\prime$ is a
+$\Sigma$subalgebra of $B$ (and not just a weak $\Sigma$subalgebra).
+$\phi^n$ is always strict, and if $\phi$ is strict, then $B^\prime$ is
+indeed a $\Sigma$subalgebra of $B$.
+
+Our requirements for homomorphism are that it act strictly on a
+certain set of partial functions (the constructors, definition
+\ref{Doye7.3.3}). In other words, we will require that our coercion be
+a strict partial $\Sigma^C$homomorphism (again, see definition
+\ref{Doye7.3.3})
+
+For the rest, we will not in general concern ourselves with the
+partiality of homomorphisms, operators, or strictness. Since, provided
+our homomorphisms act strictly on the constructors of the type (and
+any type recursively required for construction (definition
+\ref{Doye7.6.5})) then the strong equality in the definition of
+strictness puts us in good shape.
+
+\subsection{Conditional varieties}
+\label{DoyeSec5.3}
+
+Axiom contains the notion of ``conditional {\bf Categories}'' or in
+the language of universal algebra, ``conditional varieties''. In this
+section we define and reconcile the notions of conditional and
+nonconditional\footnote{Unconditional may have been a better choice
+of word from an English language point of view. However, we are not
+saying that an algebra is unconditionally an algebra of a variety; we
+are saying that it is an algebra of a variety which has no conditions}
+varieties. This means that in future sections we will be able to
+ignore the existence of conditional varieties in Axiom.
+
+Notice that our choice of the word conditional here is similar to
+that used in the phrase ``conditional algebraic specifications''. The
+difference being that our conditions are predicates evaluated over
+arities not terms. Ours is a higher order notion and should not be
+confused with the ordinary lower order work.
+
+We extend the definition of conditional signature, via the following
+definition:
+
+\begin{DoyeDefinition}
+\label{Doye5.3.1}
+A $S$sorted {\rm conditional signature} is a set $C\Sigma$ of
+sets $C\Sigma_{n,q,s}$ indexed by $n\in\mathbb{N}\cup\{0\}$, $q$ an
+$S$arity of rank $n$, and $s\in S$. Each element of $C\Sigma$ is of
+the form
+\[{\rm if\ }P(w){\rm\ then\ }\sigma_{n,q,s}\]
+{where $P$ is a wellformed proposition in some language, and $w$ is an
+arity of finite rank (if it is a tautology, it is always represented
+by $T$). The $\sigma_{n,q,s}$ are the} conditional operator symbols.
+\end{DoyeDefinition}
+
+Firstly, we need to define a conditional term algebra.
+
+\begin{DoyeDefinition}
+\label{Doye5.3.2}
+Let $S$ be an $S$indexed family of sets disjoint from each
+other, from the set $\Delta$, the set \{if,P,then\} and from\\
+\[\{\sigma~\vert~(\exists {\rm\ arity\ }w)
+(``if\ P(w)\ then\ \sigma''\in\bigcup_{n,q,s}\Sigma_{n,q,s})\}\]
+We define $T_{C\Sigma}(X)$ to be the $S$indexed family of sets of
+strings of symbols from
+$\{if,P,then\}\cup\bigcup_{s\in S}X_s\cup\Delta\cup\bigcup_{n,q,s}
+\Sigma_{n,q,s}$ each set as small as possible satisfying these
+conditions:
+\begin{enumerate}
+\item $(\forall s\in S)(\Sigma_{0,(),s}\subseteq T_{C\Sigma}(X)_s)$
+\item $(\forall s\in S)(X_s\subseteq T_{C\Sigma}(X)_s)$
+\item $(\forall ``if\ P(w)\ then\ \sigma''\in C\Sigma_{n,q,s})
+(\forall i\in\{1,\ldots,n\})
+(\forall t_i\in T_{C\Sigma}(X)_{q_i})\\
+(``if\ P(w)\ then\ \sigma'' (t_1,\ldots,t_n)\in T_{C\Sigma}(X)_s)$
+\end{enumerate}
+
+We make $T_{C\Sigma}(X)$ into a conditional $C\Sigma$algebra by
+defining conditional operators ``$if\ P(w)\ then\ \sigma_T$'' on
+$T_{C\Sigma}(X)$, for each ``$if\ P(w)\ then\ \sigma''\in
+C\Sigma_{n,q,s}$ via:
+\begin{itemize}
+\item if $n=0$ then ``$~if\ P(w)\ then\ \sigma_T$'':=``$~if\ P(w)\ then\
+\sigma$''. (Guaranteed to be in $T_{C\Sigma}(X)_s$ by (1)).
+\item Else, define ``$~if\ P(w)\ then\ \sigma_T(t_1,\ldots,t_n)$''
+to be the string\\
+``$~if\ P(w)\ then\ \sigma(t_1,\ldots,t_n)$''
+\end{itemize}
+$T_{C\Sigma}(X)$ is called the {\rm conditional term algebra}, and an
+element of $T_{C\Sigma}(X)$ is called a {\rm conditional term}.
+\end{DoyeDefinition}
+
+Associated with the notion of conditional signature are the notions of
+conditional theory and conditional variety. However, we require a new
+definition for equations and equational systems.
+
+\begin{DoyeDefinition}
+\label{Doye5.3.3}
+A {\rm conditional (multisorted) equation} for the conditional
+signature $C\Sigma$ consists of a quadruple $(P(w),Y,t_1,t_2)$, where
+$P$ is a wellformed proposition in some language, and $w$ is an arity
+of finite rank, (if it is a tautology, it is always represented by
+$T$) where $Y\overset{\rightarrow}{\subseteq}X$, $t_1$ and $t_2$ are
+terms from the same carrier set of $T_{C\Sigma}(X)$ (or
+$T_{C\Sigma}(X\overset{\rightarrow}{\cup}A)$ if we are dealing with
+equations in a particular algebra $\langle A,\alpha\rangle$), and
+every variable occurring in $t_1$ and $t_2$ occurs in the appropriate
+member of $~Y:t_1,t_2\in T_{C\Sigma}(Y)$. Such equations are more
+usually written $({\rm if\ }P(w))(\forall Y~t_1=t_2)$. If $t_1$ and
+$t_2$ come from the same carrier set of $T_{C\Sigma}(X)$ we say that
+the equation is $C\Sigma$generic.
+\end{DoyeDefinition}
+
+Note that this definition of conditional equation should not be
+confused with that found in work such as \cite{Koun90}. In that context,
+a conditional equation is a clause such as
+$({\rm if\ }P(t))(\forall Y~t1=t2)$ where $t$ is a subterm of $t_1$,
+for example.
+
+\begin{DoyeDefinition}
+\label{Doye5.3.4}
+A {\rm conditional equation system} for the signature $\Sigma$ is
+a set of conditional equations for $T_{C\Sigma}(X)$
+(or $T_{C\Sigma}(X)\overset{\rightarrow}{\cup}A$ if we are dealing with
+equations in a particular algebra $\langle A,\alpha\rangle$).
+\end{DoyeDefinition}
+
+Associated with definition \ref{Doye5.3.1} are two special signatures
+$\Sigma$ and $\tilde{\Sigma}$. The former is the extension of all the
+$C\Sigma$s; the latter is extended by all $C\Sigma$s. More formally,
+
+\begin{DoyeDefinition}
+\label{Doye5.3.5}
+Using the definitions of definition \ref{5.3.1}, we define
+$\Sigma$ to be the $S$sorted signature where $\forall n,q,s
+(n\in\mathbb{N}\cup\{0\}$, $q$ an $S$arity of rank $n$, and $s\in S$)
+\[\Sigma_{n,q,s}=\{\sigma_{n,q,s}~\vert~``~if\ P(w)\ then\
+\sigma_{n,q,s}\ '' \in C\Sigma_{n,q,s}\}\]
+Now similarly, we define $\tilde{\Sigma}$ to be the
+$\tilde{S}$sorted signature where\\
+$\forall n,q,s (n\in\mathbb{N}\cup\{0\}$,
+$q$ an $\tilde{S}$arity rank $n$,
+and $s\in\tilde{S}$)
+\[\tilde{\Sigma}_{n,q,s}=\{\sigma_{n,q,s}~\vert~
+``~if\ T\ then\ \sigma_{n,q,s}\ ''\in C\Sigma_{n,q,s}\}\]
+where $\tilde{S}$ is the largest subset of $S$ such that
+$\tilde{\Sigma}$ has no void sorts
+\end{DoyeDefinition}
+
+The algebras of conditional signatures are the same as ordinary
+algebras, except that the proposition $P$ is evaluated over $A^w$, and
+iff this is true, there is an operator $\alpha_{n,q,s,\sigma}$ in that
+algebra. More formally,
+
+\begin{DoyeDefinition}
+\label{Doye5.3.6}
+An {\rm ordersorted, total, conditional $C\Sigma$algebra} is an
+ordered triple $\langle A,\{A_s:s\in S\},\alpha\rangle$, where $A$ is
+a class known as the universe, $\{A_s:s\in S\}$ is an $S$indexed
+family of subsets of $A$, known as the {\rm carriers} of the algebra,
+and $\alpha$ is a set of sets of functions
+$\alpha_{n,q,s}=\bigcup_{\sigma\in\Sigma_{n,q,s}}
+\{\alpha_{n,q,s,\sigma}:A^q\rightarrow A_s~\vert~P(A^w)\}$, such that
+\begin{enumerate}
+\item $A_u=A$
+\item If $s\preceq s^\prime\in S$, then $A_s\subseteq A_{s^\prime}$
+\item If ``$~if\ P(w)\ then\ \sigma''\in C\Sigma_{n,q,s}$\\
+and ``$~if\ P^\prime(w^\prime)\ then\ \sigma'' \in
+C\Sigma{n,q^\prime,s^\prime}$, with $s\preceq s^\prime$\\
+and
+$q^\prime\preceq q$, and also $P(A^w)$ and $P^\prime(A^{w^\prime})$\\
+then
+$\alpha_{n,q,s,\sigma}~\vert_{A^{q^\prime}}=
+\alpha_{n,q^\prime,s^\prime,\sigma}$
+\end{enumerate}
+\end{DoyeDefinition}
+
+Clearly, if all the $P$ are tautologies then a conditional signature
+$C\Sigma$ is identical to its nonconditional partner,
+$\Sigma$. Therefore all conditional $C\Sigma$algebras are
+(nonconditional) $\Sigma$ algebras in this case.
+
+In any case a $C\Sigma$algebra is a $\tilde{\Sigma}$algebra. Thus we
+can see that $\tilde{\Sigma}$ is a minimal\footnote{Minimal in the
+sense that it has fewest operator symbols and sorts. The variety it
+specifies is maximal, if you consider the number of algebras that
+model it.} signature for $C\Sigma$.
+
+\begin{DoyeDefinition}
+\label{Doye5.3.7}
+We define a {\rm conditional theory} to be the ordered pair\\
+$\langle\langle C\Sigma,S\rangle,S\rangle$ where $C\Sigma$ is an
+$S$sorted conditional signature and $S$ is a set of $S$sorted
+conditional $\Sigma$equations. We say that a $C\Sigma$algebra
+$\langle A,\alpha\rangle$ {\rm models} or {\rm satisfies} the
+conditional theory iff it is a model for
+$S~\vert_{\langle A,\alpha\rangle}$, where
+$S~\vert_{\langle A,\alpha\rangle}$ is defined as follows,
+\[S~\vert_{\langle A,\alpha\rangle}:=
+\{(Y,t_1,t_2)~\vert~((P(w),Y,t_1,t_2)\in S)\land P(A^w)\}\]
+\end{DoyeDefinition}
+
+A {\rm theoretical interpretation} of a conditional theory
+$\langle\langle C\Sigma,S\rangle,S\rangle$ is a theory
+$\langle\langle\Sigma_\tau,S\rangle,S_\tau\rangle$ equivalent to
+$\langle\langle C\Sigma,S\rangle,S\rangle$ with all the propositions
+$P(w)$ evaluated in some consistent manner.
+
+Finally we demand that for all possible pairs of theoretical
+interpretations
+$\langle\langle\Sigma_0,S\rangle,S_0\rangle$,
+$\langle\langle\Sigma_1,S\rangle,S_1\rangle$ where
+$\Sigma_0\overset{\rightarrow}{\subseteq}\Sigma_1$ and
+$S_0\subseteq S_1$ that $\langle\langle\Sigma_1,S\rangle,S_1\rangle$
+is a protecting extension of
+$\langle\langle\Sigma_0,S\rangle,S_0\rangle$.
+
+\begin{DoyeDefinition}
+\label{Doye5.3.8}
+The collection of all models of a particular conditional theory
+is called a {\rm conditional variety}.
+\end{DoyeDefinition}
+
+In fact the conditional variety defined by
+$\langle\langle C\Sigma,S\rangle,S\rangle$ is equivalent to the
+variety defined by
+$\langle\langle \tilde{\Sigma},\tilde{S}\rangle,S\rangle$.
+
+Also, the variety specified by any theoretical interpretation of the
+conditional theory $\langle\langle C\Sigma,S\rangle,S\rangle$ forms a
+subclass of the conditional variety. Moreover, for a pair of
+theoretical interpretations
+$\langle\langle\Sigma_0,S\rangle,S_0\rangle$,
+$\langle\langle\Sigma_1,S\rangle,S_1\rangle$ where
+$\Sigma_0\overset{\rightarrow}{\subseteq}\Sigma_1$ and
+$S_0\subseteq S_1$, the variety specified by
+$\langle\langle\Sigma_1,S\rangle,S_1\rangle$ forms a subclass of the
+variety specified by
+$\langle\langle\Sigma_0,S\rangle,S_0\rangle$.
+
+If we consider two conditional algebras from the same conditional
+variety, then we wish to know whether there is a homomorphism from one
+to the other. For this we need to define ``conditional
+homomorphism''.
+
+A technical definition which will allow us to define homomorphisms
+more easily.
+
+\begin{DoyeDefinition}
+\label{Doye5.3.9}
+Let $\langle A,\alpha\rangle$, and $\langle B,\beta\rangle$ be
+$C\Sigma$algebras. For all $n,q,s$, we define
+\[\mu_{\alpha,n,q,s}:\alpha_{n,q,s}\rightarrow\Sigma_{n,q,s}\]
+to be the map,
+\[\alpha_{n,q,s,\sigma}\mapsto\sigma_{n,q,s}\]
+Similarly, define $\mu_{\beta,n,q,s}$ for
+$\langle B,\beta\rangle$.
+\end{DoyeDefinition}
+
+The family of maps, $\mu_\alpha$ (as we show in notation
+\ref{Doye5.3.11} map an algebra, $\langle A,\alpha\rangle$ to a
+nonconditional signature which it models.
+
+\begin{DoyeDefinition}
+\label{Doye5.3.10}
+$\phi:\langle A,\alpha\rangle\rightarrow\langle B,\beta\rangle$
+is a {\rm conditional $C\Sigma$homomorphism} iff it is a
+nonconditional $\Sigma^{AB}$homomorphism, where
+\[\left(\begin{array}{rcl}
+\Sigma^{AB} & = &\{
+\ \{\mu_{\alpha,n,q,s}(\alpha_{n,q,s,\sigma})~\vert~
+\alpha_{n,q,s,\sigma}\in\alpha_{n,q,s}\}\cap\\
+&&\quad\{\mu_{\beta,n,q,s}(\beta_{n,q,s,\sigma})~\vert~
+\beta_{n,q,s,\sigma}\in\beta_{n,q,s}\}~\vert~\\
+&&n\in\mathbb{N}\cup\{0\},q{\rm\ \tilde{S}arity\ of\ rank\ }n,
+s\in\tilde{S}\}\end{array}\right)\]
+$\Sigma^{AB}$ is a $\tilde{S}$sorted
+signature where $\tilde{S}$ is
+the largest subset of $S$ such that $\Sigma^{AB}$ has no void sorts.
+\end{DoyeDefinition}
+
+In fact, if we use the following piece of notation.
+
+\begin{DoyeNotation}
+\label{Doye5.3.11}
+If $\langle A,\alpha\rangle$ is a conditional $C\Sigma$algebra,
+we define $\Sigma^{NC(A)}$ to be the nonconditional signature
+\[\begin{array}{l}
+\{\{\mu_{\alpha,n,q,s}(\alpha_{n,q,s,\sigma})~\vert~
+\sigma_{n,q,s,\sigma}\in\alpha_{n,q,s}\}~\vert~\\
+\quad n\in\mathbb{N}\cup\{0\},q{\rm\ an\ \hat{S}arity\ of\ rank\ }n,
+s\in\hat{S}\}\end{array}\]
+
+$\Sigma^{NC(A)}$ is a $\hat{S}$sorted signature where $\hat{S}$
+is the largest subset of $S$ such that $\Sigma^{NC(A)}$ has no void
+sorts.
+\end{DoyeNotation}
+
+As an aside, notice that for each $C\Sigma$algebra
+$\langle A,\alpha\rangle$, there is an associated nonconditional term
+algebra $T_{\Sigma^{NC(A)}}(X)$. This term algebra is the equivalent of
+evaluating each $P(w)$ over $A$ in $T_{C\Sigma}(X)$.
+
+Then $\langle A,\alpha\rangle$ is a nonconditional
+$\Sigma^{NC(A)}$algebra, and
+\[\Sigma^{AB}=\{\Sigma^{NC(A)}_{n,q,s}\cap\Sigma^{NC(B)}_{n,q,s}
+~\vert~n\in\mathbb{N}\cup\{0\},q{\rm\ an\ \breve{S}arity\ of\ rank\ }n,
+s\in\breve{S}\}\]
+
+So, for any two conditional algebras of the same conditional
+signature, there exists a fixed (maximal) nonconditional signature of
+which they are both nonconditional algebras. (We may have to forget
+some operators and even some sorts, which may only exist in
+conditions).
+
+Our definition of conditional homomorphism is that of the
+nonconditional homomorphism from this fixed nonconditional
+signature.
+
+Hence, the concept of conditional signatures can always be reduced to
+one for nonconditional signatures and therefore any results we prove
+or use need only be for nonconditional signatures.
+
+As we have seen in definition \ref{Doye5.3.7} this concept may also be
+extended to theories. In addition to adding new operators when certain
+propositions hold, we also allow for new equations to be added
+(conditionally). However, we demand that any such extension is a
+protecting extension of the minimal nonconditional theory (the theory
+over the signature $\langle \overline{\Sigma},\overline{S}\rangle$).
+
+More explicitly, let us define $\hat{S}$ to be all those equations
+from $S$ which only involve arity from $\Sigma^{NC(A)}$ (as well as
+all equations not involving arities)\footnote{Alternatively, define
+$\hat{S}$ to be those equations from $S$ for which
+$\langle A,\alpha\rangle$ is a model, since it may not model all the
+equations in the definition of $\hat{S}$ in the main text.} Similarly,
+define $\overline{S}$ to be all those equations from $S$ which only
+involve arities from $\overline{\Sigma}$ (as well as all equations not
+involving arities).
+
+If $\langle A,\alpha\rangle$ is a conditional $C\Sigma$model then
+$\langle\langle\Sigma^{NC(A)},\hat{S}\rangle\hat{S}\rangle$ must be a
+protecting extension of
+$\langle\langle\overline{\Sigma},\overline{S}\rangle,\overline{S}\rangle$.
+
+\subsection{A Category theory approach}
+\label{DoyeSec5.4}
+
+This section is an aside from the rest of the section. We are not
+extending the theory of order sorted algebra nor category theory,
+merely explaining why we cover both.
+
+There is a great deal of correspondence between category theory
+(specifically, categorical type theory) and universal algebra. There
+is not enough room here to cover this huge topic, but the reader is
+pointed to \cite{Crol93}, which covers categoriecal type theory in
+great depth.
+
+As usual, Mac Lane \cite{Macl91} also contains a great deal of
+information on the correspondence between universal algebra and
+adjoint functors in the section on ``Monads and Algebras''.
+
+All the ideas from multisorted algebra theory may be represented in
+the categorical type theory framework, although an equivalent for
+ordersorted algebra appears not to be covered. However, the author
+believes that the notion could be introduced.
+
+One area which we will discuss here is the concept of algebraic
+homomorphism and the arrows (morphisms) of a given category.
+
+The correspondence between a categorical type theory $C$ and its
+associated algebraic type theory
+$\langle\langle\Sigma,S\rangle,S\rangle$ is the following
+\[{\rm Obj}(C) = {\rm\ all\ the\ } \Sigma{\rm algebras\ for\ a
+\ given\ \Sigma\ which\ model\ } S.\]
+\[{\rm Arr}(C)={\rm\ all\ (or\ a\ fixed\ subcollection\ of)\ the
+\ \Sigmahomomorphisms}.\]
+
+The category of all algebras which model a given theory
+$\langle\langle\Sigma,S\rangle,S\rangle$ has as an initial object the
+free algebra $T_\Sigma(X)/\equiv_\mathcal{E}$. (This is why the second
+universality theorem \ref{Doye4.6.16} holds).
+
+So we see that both categories and theories collect together similar
+types. This abstraction of information forms the basis of abstract
+datatyping.
+
+\subsection{Coercion}
+\label{DoyeSec5.5}
+
+In this work we are interested in coercions which so far have been
+explained as being natural, typechanging maps. We may define them in
+a far more strict fashion.
+
+The following would seem to be a good definition for
+coercion. However, in practice this definition is not welldefined
+enough since it does not state which theory a coercion should come
+from.
+
+\begin{DoyeDefinition}\label{Doye5.5.1}
+Let $\langle A,\alpha\rangle$ and $\langle B,\beta\rangle$ be
+algebras from the variety specified by some theory
+$\langle\langle \Sigma,S\rangle,S\rangle$. The map
+$\phi:\langle A,\alpha\rangle\rightarrow\langle B,\beta\rangle$ is a
+coercion if it is a homomorphism of that theory.
+\end{DoyeDefinition}
+
+Using the category theory correspondence above, we see that a function
+between two types of the category of all algebras which model a
+particular theory is a coercion iff it is an arrow of that category.
+
+The only problem with this definition of coercion is that it does not
+specify from which theory (or equivalently, category) we
+should demand the homomorphism be taken. In general, we would like
+this to be the most specific, or smallest category to which both
+algebras belong.
+
+If we just used the definition of coercion above (definition
+\ref{Doye5.5.1}) then any total map between types would be a coercion!
+Any small category may be forgotten back to {\bf Set} via the
+forgetful functor and any total function is an arrow of
+{\bf Set}. Most types in a computer algebra system are objects of
+{\bf Set} (which is equivalent to {\bf SetCategory} in Axiom  the
+second most basic {\bf Category} in Axiom).
+
+Richardson notes that we also require a fixed framework in
+which we define our coercions. If we were to attempt to define a
+coercion $\langle A,\alpha\rangle$ to $\langle B,\beta\rangle$ to be
+``any map which is a homomorphism for all theories which both algebras
+model'' then the definition would not be welldefined. We need to
+state a context.
+
+We are attempting to reflect the situation that appears in a system
+like Axiom. Thus we must state that we have been given
+{\sl a priori} a fixed collection of theories, and that given any
+type, we know precisely which theories it models.
+
+This precludes a user from adding another theory which the algebras
+model which could redefine what ``coercion'' means for those algebras.
+
+In the category theory correspondence, we say that Axiom's
+{\bf Category} is a fixed collection of categories, and given any type
+we know of which categories it is an object.
+
+\begin{DoyeDefinition}{\bf (Coercion)}
+\label{Doye5.5.2}
+Let $\Upsilon$ be a fixed collection of theories.
+
+Let $\langle A,\alpha \rangle$ be a model for theories $\Theta_i$ (for
+$i$ in some indexing set $I$) where $(\forall i\in I)$($\Theta_i$ is a
+theory from $\Upsilon$).
+
+Similarly, let $\langle B,\beta\rangle$ be a model for theories
+$\Omega_j$ (for $j$ in some indexing set $J$) where
+$(\forall j \in J)$($\Omega_j$ is a theory from $\Upsilon$).
+
+Then we call a map $\langle A,\alpha\rangle$ to
+$\langle B,\beta\rangle$ a {\rm coercion} iff it is a homomorphism for
+all the theories in
+\[\{\Theta_i~\vert~i\in I\}\cap\{\Omega_j~\vert~j\in J\}\]
+\end{DoyeDefinition}
+
+In Axiom, {\bf Domains} are only members of a fixed set of
+{\bf Categories}.\footnote{A user could reimplement one of these
+{\bf Categories} and ruin everything.}
+
+In fact, in Axiom we are in a slightly better position. If a
+{\bf Domain} is an object of two {\bf Categories} then there must
+exist a {\bf Category} which extends (potentially trivially) both of
+these {\bf Categories} of which the {\bf Domain} is an object.
+
+Thus, in Axiom, definition \ref{Doye5.5.2} reduces to,
+\begin{quote}
+``A coercion in Axiom from a type {\bf A} to a
+ type {\bf B} is a homomorphism of the most restrictive
+ {\bf Category} to which both {\bf A} and {\bf B} belong''
+\end{quote}
+
+It would be useful to have a name for maps which are ``coercions'' in
+the sense of definition \ref{Doye5.5.1}. These maps are in a sense
+natural, and may be the nextmost natural map between two
+types. However, as we have shown in the example using {\bf Set} the
+map need not be particularly ``natural'' from a realistic point of view.
+
+As it stands, with our current terminology maps which satisfy
+definition \ref{Doye5.5.1} which are not coercions are merely
+``homomorphisms which are not coercions''.
+
+If no coercion existed between two types, but a ``homomorphism which
+is not a coercion'' existed and a user required that homomorphism then
+either the user only required a conversion or the theory lattice for
+the algebra system has not been designed correctly.
+
+\subsection{Conclusion}
+\label{DoySec5.6}
+
+In this section we have shown how classical order sorted algebra may
+be extended to encompass the notion of partial functions and
+conditional signatures. We have also stated how these notions interact
+with the equational calculus. These are important extensions due to
+the fact that these notions are used extensively in Axiom.
+
+We have also mentioned some of the correlation between category theory
+and universal algebra. Finally we have made the important definition
+of a coercion and demonstrated why the definition is necessarily strict.
+
+\section{Coherence}
+\label{DoyeChap6}
+
+We will look at a conjecture by Weber which is important to our
+work. We will state his assumptions and proof (which is incorrect).
+
+We will then add in some extra assumptions and truly prove the
+theorem. Finally we will relax one of Weber's assumptions and prove
+that the theorem still holds.
+
+The assumptions made by Weber provide a strict formal setting for
+types in an algebra system. The theorem in itself proves confluence
+for coercions in this setting.
+
+All the work in this section (except the explanation of ``$n$ary type
+constructor'') and the next are from Weber
+\cite{Webe93b} and \cite{Webe95}. All the rest is original work.
+
+\subsection{Weber's work I: definitions}
+\label{DoyeSec6.2}
+
+This section contains the definitions from Weber's thesis
+\cite{Webe93b} and \cite{Webe95} required for the statement and
+Weber's ``proof' of Weber's coercion conjecture \ref{Doye6.3.7}.
+His assumptions are in the next section.
+
+These statements will also be used when we correctly prove the
+coherence theorem \ref{Doye6.4.7} in section \ref{DoyeSec6.4}
+
+It should be noted that Weber's coercion conjecture only makes up part
+of one section of his thesis \cite{Webe93b} which also covers various
+areas of type classes, type inference, and coercion in great depth and
+detail.
+
+Weber uses the phrase ``type class'' where we would use the terms
+``category'' or ``variety''.
+
+\begin{DoyeDefinition}
+\label{Doye621}
+A {\rm base type} is any type which is not a parametrically
+defined type. (i.e. a 0ary operator in the term algebra of type
+classes)
+\end{DoyeDefinition}
+
+So for example, the {\bf Integer} and {\bf Boolean} types are base
+types.
+
+\begin{DoyeDefinition}
+\label{Doye6.2.2}
+A {\rm ground type} is any type within the system which is either
+a base type or a parametrically defined type with all the paramters
+present. Any nonground type is called a {\rm polymorphic type}.
+\end{DoyeDefinition}
+
+As examples, we have {\bf Integer} and
+{\bf Polynomial(Fraction(Integer))}. As a nonexample, we have
+{\bf Polynomial(R:Ring)}.
+
+\begin{DoyeDefinition}
+\label{Doye6.2.3}
+If there exists a coercion from $t$ to $t^\prime$ we say that
+$t\trianglelefteq t^\prime$.
+\end{DoyeDefinition}
+
+This definition places an order on the ground types.
+
+Weber uses the phrase ``nary type constructor'' to mean a functor
+from the product of $n$ categories to a specific category.
+
+Equivalently, it is a function from the product of $n$ varieties
+(specified respectively by the theories $\Omega_1,\ldots,\Omega_n$) to
+a variety (specified by the theory
+$\langle\langle\Sigma,S \rangle,S \rangle$. This is a function which,
+for all $i$ maps the carrier of the principle sort (and potentially
+the carriers of some of the nonprincipal sorts) of a model of
+$\Omega_i$ to one (for each sort mapped) of the nonprincipal sorts of
+a model of $\langle\langle\Sigma,S \rangle,S\rangle$.
+
+If the model returned as $\langle A,\alpha\rangle$, this function must
+map one and only one sortcarrier to each and every member of
+$A \backslash \{A_{S_1}\}$ where $S_1$ is the principal sort.
+
+\begin{DoyeDefinition}
+\label{Doye6.2.4}
+For a ground type $t$ we define {\rm com}($t$) to be 1, if $t$ is a
+base type or if $t=f(t_1,\ldots,t_n)$ (an $n$ary type constructor)
+then {\rm com}($t$) is defined to be
+$1+{\rm max}(\{{\rm com}(t_i)~\vert~\{1,\ldots,n\}\})$.
+\end{DoyeDefinition}
+
+This defined the ``complexity'' of a ground type to be how far up the
+type lattice it is.
+
+\begin{DoyeDefinition} {\bf (Coherence)}
+\label{Doye6.2.5}
+A type system is {\rm coherent} if the following condition is
+satisfied.
+\[(\forall ground~types~t_1,t_2)
+((\phi,\psi:t_1\rightarrow t_2~coercions)\Rightarrow(\phi=\psi))\]
+\end{DoyeDefinition}
+
+This guarantees that there only exist one coercion from one ground
+type to another. This is a highly desirable feature of any type
+system. The main results of this section (the coherence theorem
+\ref{Doye6.4.7} and the extended coherence theorem \ref{Doye6.5.4})
+are that we may be able to guarantee that our type system is coherent
+providing some sensible assumptions hold true.
+
+In the following definitions, all the $\sigma$ and $\sigma^\prime$
+are type classes.
+
+\begin{DoyeNotation}
+\label{Doye6.2.6}
+$t:\sigma$ means that the type $t$ is an object of the type class
+$\sigma$.
+\end{DoyeNotation}
+
+\begin{DoyeDefinition}
+\label{Doye6.2.7}
+The $n$ary type constructor $f$ $(n\in\mathbb{N})$ induces a
+{\rm structural coercion} if there are sets
+$\mathcal{A}_f\subseteq\{1,\ldots,n\}$ and
+$\mathcal{M}_f\subseteq\{1,\ldots,n\}$ such that the following
+condition is satisfied:
+\begin{quote}
+If $f:(\sigma_1,\ldots,\sigma_n)\rightarrow\sigma$ and
+$f:(\sigma^\prime_1,\ldots,\sigma^\prime_n)\rightarrow\sigma^\prime$,
+and $(\forall i\in\{1,\ldots,n\})(\forall~ground~types~
+t_i:\sigma_i$ and $t^\prime_i:\sigma^\prime_i)
+(i\notin\mathcal{A}_f\cup\mathcal{M}_f\Rightarrow t_i=t^\prime_i)$ and
+there exist coercions:
+\[\begin{array}{rcl}
+\phi_i:t_i\rightarrow t^\prime_i & {\rm if} & i\in\mathcal{M}_f\\
+\phi_i:t^\prime_i\rightarrow t_i & {\rm if} & i\in\mathcal{A}_f\\
+\phi_i={\rm id}_{t_i}={\rm id}_{t^\prime_i} & {\rm if} &
+i \neq \mathcal{A}_f\cup\mathcal{M}_f
+\end{array}\]
+then there exists a {\bf uniquely defined} coercion
+\[\mathcal{F}_f(t_1,\ldots,t_n,t^\prime_1,\ldots,t^\prime_n,
+\phi_1,\ldots,\phi_n):f(t_1,\ldots,t_n)\rightarrow
+f(t^\prime_1,\ldots,t^\prime_n)\]
+\end{quote}
+
+The type constructor $f$ is {\rm covariant} (or {\rm monotonic})
+in its $i$th argument if\\
+$i\in\mathcal{M}_f$. $f$ is
+{\rm contravariant} or ({\rm antimonotonic}) in its $i$th argument
+if $i\in\mathcal{A}_f$
+\end{DoyeDefinition}
+
+Note that if $i\in\mathcal{A}_f\cap\mathcal{M}_f$ then
+$t_i\cong t^\prime_i$.
+
+As an example of covariance, the list constructor in Axiom,
+{\bf List} (a functor ${\bf Set}\rightarrow{\bf ListAggregate()})$
+takes one argument in which it is covarient. Given types {\bf A} and
+{\bf B}, such that there exists a coercion
+$\phi_1:{\bf A}\rightarrow{\bf B}$ then
+\[\mathcal{F}_{\rm List}({\bf A},{\bf B},\phi_1):
+{\bf List(A)}\rightarrow{\bf List(B)}\]
+
+Since Axiom's type constructors are functors, then category theory
+states this more simply as
+\[\mathcal{F}_{\rm List}({\bf A},{\bf B},\phi_1)={\bf List}(\phi_1)\]
+
+Contravariance is a rarer case. However, Axiom's {\bf Mapping} functor
+is contravariant in its first argument and covariant in its second.
+{\bf Mapping} takes two types {\bf A} and {\bf B} and returns the type
+of all mappings from {\bf A} to {\bf B}.
+
+As a concrete example for {\bf Mapping}, suppose we wish to find the
+uniquely defined coercion.
+\[\begin{array}{c}
+{\bf Mapping(Fraction(Integer),Fraction(Integer))}\rightarrow\\
+{\bf Mapping(Integer,Fraction(Integer))}
+\end{array}\]
+
+There exists a coercion
+\[\iota:{\bf Integer}\rightarrow{\bf Fraction(Integer)}\]
+
+the inclusion operator. There also exists a coercion
+\[{\rm id}:{\bf Fraction(Integer)}\rightarrow{\bf Fraction(Integer)}\]
+which is the identity operation. The uniquely defined coercion is as
+follows:
+
+\[\begin{array}{c}
+\mathcal{F}_{\rm Mapping}({\bf Fraction(Integer)}),
+{\bf Fraction(Integer)},{\bf Integer},{\bf Fraction(Integer)},
+\iota,{\rm id}):\\
+{\bf Mapping(Fraction(Integer),Fraction(Integer))}\rightarrow\\
+{\bf Mapping(Integer,Fraction(Integer))}
+\end{array}\]
+which sends $f\mapsto{\rm id}\circ f\circ\iota$.
+
+The following definitions shows that there is a homomorphism image of
+a parameter in the created type. For example there is a homomorphic
+image of the underlying ring in any polynomial ring.
+
+\begin{DoyeDefinition}
+\label{Doye6.2.8}
+Let $f:(\sigma_1,\ldots,\sigma_n)\rightarrow\sigma$ be an $n$ary
+type constructor.\\
+If $(\forall i \in\{1,\ldots,n\})(for~some~ground
+~types~t_i:\sigma)$ such that there exists a coercion
+\[\Phi^i_{f,t_1,\ldots,t_n}:t_i\rightarrow f(t_1,\ldots,t_n)\]
+then we say that $f$ has a {\rm direct embedding} at its $i$th
+position.
+
+Moreover, let
+\[\mathcal{D}_f=\{i~\vert~f~has~a~direct~embedding~at~its~ith~
+position\}\]
+be the {\rm set of direct embedding positions} of $f$
+\end{DoyeDefinition}
+
+The definition of $\mathcal{D}_f$ is a technical definition of
+Weber's, needed for one of his assumptions (\ref{Doye6.3.5}).
+
+\subsection{Weber's work II: Assumptions and a conjecture}
+\label{DoyeSec6.3}
+
+This section provides all the assumptions and results which Weber used
+in his ``proof'' of Weber's coherence conjecture \ref{Doye6.3.7} which
+will will state and at the end of this section. The assumptions and
+results are also require in our proof of the coherence theorem
+\ref{Doye6.4.7}.
+
+\begin{DoyeAssumption}
+\label{Doye6.3.1}
+For any ground type $t$, the identity on $t$ will be a
+coercion. The (welldefined) composition of two coercions is also a
+coercion
+\end{DoyeAssumption}
+
+This is clearly a sensible (if notoften implemented) statement. Since
+our coercions are always arrows of a category the above
+assumption must hold.
+
+\begin{DoyeLemma}
+\label{Doye6.3.2}
+If assumption \ref{Doye6.3.1} holds, then the set of ground types as
+objects together with their coercions as arrows form a category.
+\end{DoyeLemma}
+
+{\bf Proof}. Immediate.
+
+The following assumption will provide us with the basis for a coherent
+type system. Our coherence is built by ensuring confluence amongst
+different paths leading to the same coercion. If we do not have
+coherence at the base types then we will not have coherence amonst the
+general types.
+
+\begin{DoyeAssumption}
+\label{Doye6.3.3}
+The subcategory of base types and coercions between base types
+forms a preorder, i.e. if $t_1$, $t_2$ are base types and
+$\phi,\psi:t_1\rightarrow t_2$ are coercions, then $\phi=\psi$.
+\end{DoyeAssumption}
+
+The following condition states that $\mathcal{F}_f$ is a functor over
+the category of all $f(\cdot,\ldots,\cdot)$s.
+
+\begin{DoyeAssumption}
+\label{Doye6.3.4}
+Let $f$ be an $n$ary type constructor which induces a structural
+coercion and let $f(t_1,\ldots,t_n)$,
+$f(t^\prime_1,\ldots,t^\prime_n)$,
+$f(t^{\prime\prime}_1,\ldots,t^{\prime\prime}_n)$ be ground types.
+Assume that the following are coercions.
+
+\[\begin{array}{c}
+\iota\in\mathcal{M}_f\Rightarrow\phi_i:t_i\rightarrow t^\prime_i,
+\phi^\prime_i: t^\prime_i\rightarrow t^{\prime\prime}_i\\
+\iota\in\mathcal{A}_f\Rightarrow\phi^\prime_i:t^{\prime\prime}_i
+\rightarrow t^\prime_i,\phi_i: t^\prime_i\rightarrow t_i\\
+\iota\notin \mathcal{A}_f\cup\mathcal{M}_f\Rightarrow
+t_i=t^\prime_i=t^{\prime\prime}_i ~and~
+\phi_i=\phi^\prime_i={\rm id}_{t_i}
+\end{array}\]
+
+Then the following conditions are satisfied:
+\begin{enumerate}
+\item $\mathcal{F}_f(t_1,\ldots,t_n,t_1,\ldots,t_n,
+{\rm id}_{t_1},\dots,{\rm id}_{t_n})={\rm id}_{f(t_1,\ldots,t_n)}$
+\item $\mathcal{F}_f(t_1,\ldots,t_n,
+t^{\prime\prime}_1,\ldots,t^{\prime\prime}_n,
+\phi_1\circ \phi^\prime_1,\ldots,\phi_n\circ \phi^\prime_n)=$\\
+$\mathcal{F}_f(t_1,\ldots,t_n,t^\prime_1,\ldots,t^\prime_n,
+\phi_1,\ldots,\phi_n)\circ
+\mathcal{F}_f(t^\prime_1,\ldots,t^\prime_n,
+t^{\prime\prime}_1,\ldots,t^{\prime\prime}_n,
+\phi^\prime_1,\ldots,\phi^\prime_n)$
+\end{enumerate}
+\end{DoyeAssumption}
+
+This is a condition which stops direct embeddings ``becoming
+confused''. Firstly, Weber declares that any type constructor can only
+have one direct embedding. (We will show how to relax this condition
+in a later section (\ref{DoyeSec6.5}).) Secondly, he states that
+direct embeddings, where they exist, are unique.
+
+\begin{DoyeAssumption}
+\label{Doye6.3.5}
+Let $f$ be an $n$ary type constructor. Then the following
+conditions hold:
+\begin{enumerate}
+\item $\vert\mathcal{D}_f\vert$ = 1
+\item Direct embedding coercions are unique, i.e. if~
+$\Phi^i_{f,t_1,\ldots,t_n}:t_i\rightarrow f(t_1,\ldots,t_n)$ and
+$\Psi^i_{f,t_1,\ldots,t_n} : t_i\rightarrow f(t_1,\ldots,t_n)$
+then
+\[\Phi^i_{f,t_1,\ldots,t_n}=\Psi^i_{f,t_1,\ldots,t_n}\]
+\end{enumerate}
+\end{DoyeAssumption}
+
+The following assumption is highly technical and shows how direct
+embeddings interact with structural coercions. Basically, they
+commute.
+
+\begin{DoyeAssumption}
+\label{Doye6.3.6}
+Let $f$ be an $n$ary type constructor which induces a structural
+coercion and has a direct embedding at its $r$th position. Assume that\\
+$f:(\sigma_1,\ldots,\sigma_n)\rightarrow\sigma$ and
+$f:(\sigma^\prime_1,\ldots,\sigma^\prime_n)\rightarrow\sigma$, and\\
+$(\forall i\in\{1,\ldots,n\})
+(\exists t_i:\sigma_i~and~t^\prime_i:\sigma^\prime_i)$.
+If there are coercions $\psi_r:t_r\rightarrow t^\prime_r$, if the
+coercions $\Phi^r_{f,t_1,\ldots,t_n}$ and
+$\Phi^r_{f,t^\prime_1,\ldots,t^\prime_n}$ are defined, and if $f$ is
+covariant in its $r$th argument, then the following holds:
+\[\Phi^r_{f,t^\prime_1,\ldots,t^\prime_n}\circ\psi_r=
+\mathcal{F}_f(t_1,\ldots,t_n,t^\prime_1,\ldots,t^\prime_n,
+\psi_1,\ldots,\psi_n)\circ\Phi^r_{f,t_1,\ldots,t_n}\]
+
+\[\begin{array}{c@{\hspace{7cm}}c}
+\Rnode{N1}{t_r} & \Rnode{N2}{t^\prime_r}\\
+&\\
+&\\
+&\\
+&\\
+&\\
+\Rnode{N3}{f(t_1,\ldots,t_n)} &
+\Rnode{N4}{f(t^\prime_1,\ldots,t^\prime_n)}
+\end{array}
+\psset{nodesep=0.3cm}
+\everypsbox{\scriptstyle}
+\ncLine{>}{N1}{N2}
+\Aput{\displaystyle\psi_r}
+\ncLine{>}{N1}{N3}
+\Aput{\displaystyle\Phi^r_{f,t_1,\ldots,t_n}}
+\ncLine{>}{N2}{N4}
+\Bput{\displaystyle\Phi^r_{f,t^\prime_1,\ldots,t^\prime_n}}
+\ncLine{>}{N3}{N4}
+\Aput{\displaystyle\mathcal{F}_f(t_1,\dots,t_n,t^\prime_1,\ldots,t^\prime_n,
+\psi_1,\ldots,\psi_n)}
+\]
+
+However, if $f$ is contravariant in the $r$th argument then:
+\[\mathcal{F}_f(t_1,\ldots,t_n,t^\prime_t,\ldots,t^\prime_n,
+\psi_1,\ldots,\psi_n)\circ
+\Phi^r_{f,t^\prime_1,\ldots,t^\prime_n}\circ\psi_r=
+\Phi^r_{f,t)_1,\ldots,t*n}\]
+
+or equivalently, the following diagram commutes:
+
+\[\begin{array}{c@{\hspace{7cm}}c}
+\Rnode{N1}{t_r} & \Rnode{N2}{t^\prime_r}\\
+&\\
+&\\
+&\\
+&\\
+&\\
+\Rnode{N3}{f(t_1,\ldots,t_n)} &
+\Rnode{N4}{f(t^\prime_1,\ldots,t^\prime_n)}
+\end{array}
+\psset{nodesep=0.3cm}
+\everypsbox{\scriptstyle}
+\ncLine{>}{N1}{N2}
+\Aput{\displaystyle\psi_r}
+\ncLine{>}{N1}{N3}
+\Aput{\displaystyle\Phi^r_{f,t_1,\ldots,t_n}}
+\ncLine{>}{N2}{N4}
+\Bput{\displaystyle\Phi^r_{f,t^\prime_1,\ldots,t^\prime_n}}
+\ncLine{>}{N4}{N3}
+\Bput{\displaystyle\mathcal{F}_f(t_1,\dots,t_n,t^\prime_1,\ldots,t^\prime_n,
+\psi_1,\ldots,\psi_n)}
+\]
+\end{DoyeAssumption}
+
+We are now in a position to state Weber's coherence conjecture and
+his ``proof''. This attempts to show that when the aforementioned
+assumptions hold true, then we have a coherent type system. We will
+give more assumptions and a proper proof in section
+\ref{DoyeSec6.4}.
+
+\begin{DoyeConjecture} {\bf (Weber's coherence conjecture)}
+\label{Doye6.3.7}
+Assume that all coercions between ground types are only built by
+one of the following mechanisms:
+\begin{enumerate}
+\item coercions between base types
+\item coercions induced by structural coercions
+\item direct embeddings in a type constructor
+\item composition of coercions
+\item identity funciton on ground types as coercions
+\end{enumerate}
+
+If assumptions 6.3.1, 6.3.3, 6.3.4, 6.3.5, and 6.3.6 are
+satisfied, then the set of ground types as objects, and the coercions
+between them as arrows form a category which is a preorder.
+\end{DoyeConjecture}
+
+This is the ``proof'' of this conjecture given in
+\cite{Webe93b} and \cite{Webe95}.
+
+Weber's ``Proof''. By assumption 6.3.1 and lemma 6.3.2, the set of
+ground types as objects and the coercions between them form a
+category.
+
+For any two ground types $t$ and $t^\prime$ we will prove by induction
+on max(com($t$),com($t^\prime$)) that if
+$\phi,\psi:t\rightarrow t^\prime$ are coercions then
+$\phi=\psi$.
+
+If max(com($t$),com($t^\prime$))~$= 1$ then the claim follows by
+assumption 6.3.3. Now assume that the inductive hypothesis holds for
+$k$, and let max(com($t$),com($t^\prime$))$=k+1$. Assume
+w.l.o.g. that $t\trianglelefteq t^\prime$ and that
+$\phi,\psi:t\rightarrow t^\prime$ are coercions.
+
+Now $t\trianglelefteq t^\prime\Rightarrow{\rm com}(t)\le
+{\rm com}(t^\prime)$. So we may assume that
+$t^\prime=f(u_1,\ldots,u_n)$ for some $n$ary type constructor $f$.
+
+By assumption 6.3.4 and the induction hypothesis, we can assume that
+there are ground types $s_1,s_2$ and unique coercions
+$\psi_1:t\rightarrow s_1$ and $\psi_2:t\rightarrow s_2$ such that
+either
+\[\phi=\mathcal{F}_f(\ldots,t,\ldots,s_1,\ldots,\psi_1,\ldots)\]
+or
+\[\phi=\psi_1\circ\Psi^i_{f,\ldots,s_1,\ldots}\]
+Similarly either,
+\[\psi=\mathcal{F}_f(\ldots,t,\ldots,s_2,\ldots,\psi_2,\ldots)\]
+or
+\[\psi=\psi_2\circ\Psi^j_{f,\ldots,s_2,\ldots}\]
+
+If $\phi$ is of form 6.1 and $\psi$ is of the form 6.3 then
+$\phi=\psi$ by assumption 6.3.4 and the uniqueness of $\mathcal{F}_f$.
+
+If $\phi$ is of form 6.2 and $\psi$ is of form 6.3 then
+$\phi=\psi$ by assumption 6.3.6.
+
+Analogously if $\phi$ is of form 6.1 and $\psi$ is of form 6.4.
+
+If $\phi$ is of form 6.2 and $\psi$ is of form 6.4 then assumption
+6.3.5 implies that $i=j$ and $s_1=s_2$. Because of the induction
+hypothesis we have $\psi_1=\psi_2$ and hence $\phi=\psi$ again by
+assumption 6.3.5.\QED
+
+\subsection{The coherence theorem}
+\label{DoyeSec6.4}
+
+In the above proof, there seem to be some irregularities.
+
+\subsubsection{On coercibility and complexity}
+
+Weber states in the proof that
+\[t\trianglelefteq t^\prime\Rightarrow{\rm com}(t)\le
+{\rm com}(t^\prime)\]
+
+Weber does not prove this, and indeed it is not true.
+
+Suppose that $f$ is an $n$ary type constructor and that it is
+contravarient in its $i$th position. If
+\[\mathcal{F}_f(s_1,\ldots,s_n,t_1,\ldots,t_n,
+\phi_1,\ldots,\phi_n):f(s_1,\ldots,s_n)\rightarrow
+f(t_1,\ldots,t_n)\]
+
+and $\phi_i:t_i\rightarrow s_i$ with
+\[{\rm com}(s_i)>{\rm max}({\rm com}(s_1),\ldots,
+{\rm com}(s_{i1}),{\rm com}(s_{i+1}),\ldots,{\rm com}(s_n))\]
+
+In other words, com($s_i$) is the {\sl unique}, maximum member of the
+set
+\[\{{\rm com}(s_j)~\vert~j\in\{1,\ldots,n\}\}\]
+
+Then if com($t_i$)$<$com($s_i$) and for all $j$ in
+$\{1,\ldots,n\}\backslash\{i\}$ we have that $s_j=t_j$, we have a
+counterexample to Weber's claim, that
+\[{\rm com}(f(s_1,\ldots,s_n))>{\rm com}(f(t_1,\ldots,t_n))\]
+
+Thus Weber's assertion in invalid.
+
+\subsubsection{Structural coercions (in the ``proof'')}
+
+In equation 6.2 (and similarly equation 6.4) $\phi$ is given as a
+function
+\[f(\ldots,t,\ldots)\rightarrow f(\ldots,s_1,\ldots)\]
+however, $\phi$ is supposed to be a function of $t$.
+
+\subsubsection{Structural coercions (syntax)}
+
+Weber calls the structural coercion function from
+$f(s_1,\ldots,s_n)$ to $f(t_1,\ldots,t_n)$
+\[\mathcal{F}_f(s_1,\ldots,s_n,t_1,\ldots,t_n,
+\phi_1,\ldots,\phi_n)\]
+
+where $\phi_i$ is from $s_i$ to $t_i$ or $t_i$ to $s_i$ depending on
+whether $f$ is covariant or contravariant in the $i$th argument,
+respectively.
+
+However, this is merely the functorial action of $f$ on the maps
+$\phi_1,\ldots,\phi_n$ and could be represented more compactly as
+\[f(\phi_1,\ldots,\phi_n)\]
+
+The source and target of each $\phi_i$ and knowledge of the sets
+$\mathcal{A}_f$ and $\mathcal{M}_f$ uniquely determine the source and
+target of $f(\phi_1,\ldots,\phi_n)$. This also demonstrates the
+uniqueness of $f(\phi_1,\ldots,\phi_n)$ and guarantees that assumption
+6.3.4 holds.
+
+\subsubsection{Identity coercions}
+
+Weber states in assumption 6.3.1 that the identity function is a
+coercion. However, he never proves this to be unique. Indeed,
+automorphisms are perfectly natural maps $t\rightarrow t$.
+
+In a computer algebra system like Axiom, many automorphisms are not
+automorphisms of the smallest category to which a type belongs.
+
+For example, the ringautomorphism
+$\mathbb{Z}[X,Y]\rightarrow\mathbb{Z}[Y,X]$ is not a
+{\bf PolynomialCategory} homomorphism since, for instance, the
+{\bf leadingMonomial} function is not preserved under the map.
+
+For some categories, like the category of groups, this may not be so
+easy to implement.
+
+We add the following sensible assumption.
+
+\begin{DoyeAssumption}
+\label{Doye6.4.1}
+The only coercion from a type to itself is the identity function.
+\end{DoyeAssumption}
+
+We will of course allow any number of functions from a type to itself,
+including conversions. It is merely the number of coercions which we
+are restricting.
+
+\subsubsection{Composition of coercions}
+
+It is possibly symptomatic of the previous errors that Weber has
+neglected to cover all the possible case of $\phi$ and $\psi$.
+
+All our coercions are compositions of coercions (or just a single
+coercion) from the list
+\begin{enumerate}
+\item coercions between base types
+\item coercions induced by structural coercions
+\item direct embeddings in a type constructor
+\item identiy function on ground types as coercions
+\end{enumerate}
+
+Suppose that $\phi=\tau_1\circ\phi^\prime$ and that
+$\psi=\tau_2\circ\psi^\prime$ where $\tau_1$ and $\tau_2$ are single
+coercions, and $\phi^\prime$ and $\psi^\prime$ are also (compositions
+of) coercions. $\phi^\prime$ may be the identity coercion, as may be
+$\psi^\prime$.
+
+For a proof by induction on com, we need to cover all the cases of
+($\tau_1,\tau_2$) pairs. Thus the list we need to consider is
+\begin{enumerate}
+\item $\tau_1$ is a coercion between base types.
+$\tau_2$ is a coercion between base types.
+\item $\tau_1$ is a coercion between base types.
+$\tau_2$ is a structual coercion
+\item $\tau_1$ is a coercion between base types.
+$\tau_2$ is a direct embedding.
+\item $\tau_1$ is a coercion between base types.
+$\tau_2$ is an identity function.
+\item $\tau_1$ is a structural coercion.
+$\tau_2$ is a coercion between base types.
+\item $\tau_1$ is a structural coercion.
+$\tau_2$ is a structural coercion.
+\item $\tau_1$ is a structural coercion.
+$\tau_2$ is a direct embedding.
+\item $\tau_1$ is a structural coercion.
+$\tau_2$ is the identity function.
+\item $\tau_1$ is a direct embedding.
+$\tau_2$ is a coercion between base types.
+\item $\tau_1$ is a direct embedding.
+$\tau_2$ is a structural coercion.
+\item $\tau_1$ is a direct embedding.
+$\tau_2$ is a direct embedding.
+\item $\tau_1$ is a direct embedding.
+$\tau_2$ is an identity function.
+\item $\tau_1$ is an identity function.
+$\tau_2$ is a coercion between base types.
+\item $\tau_1$ is an identity function.
+$\tau_2$ is a structural coercion.
+\item $\tau_1$ is an identity function.
+$\tau_2$ is a direct embedding.
+\item $\tau_1$ is an identity function.
+$\tau_2$ is a identity function.
+\end{enumerate}
+
+Firstly notice we are only interested in the pairs as unordered
+entities. Thus some of these cases are duplicates.
+
+Indeed: case 5 is case 2; case 9 is case 3; case 10 is case 7; case 13
+is case 4; case 14 is case 8; case 15 is case 12. So we may discard
+cases 5, 9, 10, 13, 14, and 15.
+
+Now notice that a base type can not have a direct embedding, neither
+can it induce a structural coercion. If either $\tau_1$ or $\tau_2$ is
+coercion between base types then the target of $\phi$ and $\psi$ is a
+base type. Hence the other $\tau_i$ can not be a direct embedding nor
+can it be a structural coercion.
+
+All the cases of this form are 2 (equivalently 5) and 3 (equivalently
+9). Thus we may ignore these too.
+
+Our remaining cases are 1, 4, 6, 7, 8, 11, 12, and 16.
+
+To really prove the coherence theorem we are going to require some
+more assumptions. Only one of them (6.4.5) is difficult to justify.
+
+We will replace this first assumption which uses Weber's definition
+6.2.8 of a direct embedding presently with our own definition
+6.4.3. In our definition assumption 6.4.2 will always hold
+(trivially).
+
+\begin{DoyeAssumption}
+\label{Doye6.4.2}
+If a type constructor $f$ has a direct embedding at its $i$th
+position and $f(t_1,\ldots,t_n)$ exists then
+$\Phi^i_{f,t_1,\ldots,t_n}:t_i\rightarrow f(t_1,\ldots,t_n)$
+\end{DoyeAssumption}
+
+Weber defines an $f$ to have a direct embedding (definition 6.2.8) at a
+particular position if there exists some $n$tuple of types
+$(t_1,\ldots,t_n)$ for which $t_i$ directly embeds in
+$f(t_1,\ldots,t_n)$.
+
+This seems sensible if we consider a type constructor to be a function
+which returns the carrier of the principal sort of the algebra. We are
+saying that direct embedding of a type in a constructor is equivalent
+to saying that a sort $\preceq$ is the principal sort.
+
+It is true that an Axiom type constructor returns the carrier of the
+principal sort of the algebra but Axiom is more specific than
+that. The type constructor furnished with full complement of arguments
+{\sl is} the principal sort of the algebra.
+
+In fact it would be better to replace definition \ref{Doye6.2.8} and
+assumption \ref{Doye6.4.2} with the following definition.
+
+\begin{DoyeDefinition}
+\label{Doye6.4.3}
+Let $f:(\sigma_1,\ldots,\sigma_n)\rightarrow\sigma$ be an $n$ary
+type constructor. If\\
+$(\forall i \in \{1,\ldots,n\})
+(\forall~ground~types~t_i:\sigma_i)$ there exists a coercion
+\[\Phi^i_{f,t_1,\ldots,t_n}:t_i\rightarrow f(t_1,\ldots,t_n)\]
+then we say that $f$ has a {\rm a direct embedding at its $i$th position}.
+
+Moreover, let
+\[\mathcal{D}_f=\{i~\vert~f~has~a~direct~embedding~at~its~ith~
+position\}\]
+be the {\rm set of direct embedding positions of $f$}.
+\end{DoyeDefinition}
+
+The next assumption is undesirable due to its difficulty to guarantee
+in any implementation. However, it is provable in the more common
+covariant case (and we will prove it in the proof of the coherence
+theorem \ref{Doye6.4.7}).
+
+We are assuming that structural coercions behave confluently. The
+assumption below (\ref{Doye6.4.4}) is stated ``too strongly''. We will
+state the assumption we really need (\ref{Doye6.4.5}  which is more
+complicated) immediately after. Assumption \ref{Doye6.4.4} gives the
+idea of what we require, whereas assumption \ref{Doye6.4.5} gives us
+what is necessary. It is an assumption about type constructors.
+
+\begin{DoyeAssumption}
+\label{Doye6.4.4}
+Let the type constructor $f$ induce a structural coercion. If\\
+$\phi:t\rightarrow f(s_1,\ldots,s_n),\psi:t\rightarrow
+f(u_1,\ldots,u_n)$ are coercions and
+$t^\prime=f(t^\prime_1,\ldots,t^\prime_n)$ then if there exists
+\[\mathcal{F}_f(s_1,\ldots,s_n,t^\prime_1,\ldots,t^\prime_n,
+\nu_1,\ldots,\nu_n):f(s_1,\ldots,s_n)\rightarrow t^\prime\]
+\[\mathcal{F}_f(u_1,\ldots,u_n,t^\prime_1,\ldots,t^\prime_n,
+\eta_1,\ldots,\eta_n):f(u_1,\ldots,u_n)\rightarrow t^\prime\]
+the following holds
+\[\mathcal{F}_f(s_1,\ldots,s_n,t^\prime_1,\ldots,t^\prime_n,
+\eta_1,\ldots,\eta_n)\circ\phi=
+\mathcal{F}_f(u_1,\ldots,u_n,t^\prime_1,\ldots,t^\prime_n,
+\zeta_1,\ldots,\zeta_n)\circ\psi\]
+
+\[\begin{array}{c@{\hspace{7cm}}c}
+\Rnode{N1}{t} & \Rnode{N2}{f(s_1,\ldots,s_n)}\\
+&\\
+&\\
+&\\
+&\\
+&\\
+\Rnode{N3}{f(u_1,\ldots,u_n)} &
+\Rnode{N4}{f(t^\prime_1,\ldots,t^\prime_n)}
+\end{array}
+\psset{nodesep=0.3cm}
+\everypsbox{\scriptstyle}
+\ncLine{>}{N1}{N2}
+\Aput{\displaystyle\phi}
+\ncLine{>}{N1}{N3}
+\Bput{\displaystyle\psi}
+\ncLine{>}{N2}{N4}
+\Bput{\displaystyle\mathcal{F}_f(s_1,\dots,s_n,t^\prime_1,\ldots,t^\prime_n,
+\eta_1,\ldots,\eta_n)}
+\ncLine{>}{N3}{N4}
+\Aput{\displaystyle\mathcal{F}_f(u_1,\dots,u_n,t^\prime_1,\ldots,t^\prime_n,
+\zeta_1,\ldots,\zeta_n)}
+\]
+\end{DoyeAssumption}
+
+Now, what we actually require. Suppose that a type $t$ is not
+constructed by the $n$ary type constructor $f$ which is contravariant
+in its $i$th position at which it also has a direct embedding.
+
+Suppose also that $t$ is coercible to two types which may be directly
+embedding in $f$ (at the $i$th position). Let us directly embed them
+to gain two new types (constructed by $f$). If these new types
+(constructed by $f$) can both be structurally coerced to the same type
+$t^\prime$ (also constructed by $f$) then the two compositions of
+coercions $t\rightarrow t^\prime$ are the same.
+
+Succinctly, A structural coercion of a direct embedding of any other
+coercion is unique.
+
+\begin{DoyeAssumption}
+\label{Doye6.4.5}
+Let $f$ be a type constructor contravariant at its $i$th
+position at which it also has a direct embedding, and let $t$ be a
+type not contructed by $f$.
+
+If $\phi^\prime_a:t\rightarrow a_i$ and
+$\psi^\prime_b:t\rightarrow b_i$ are coercions as
+$\phi_a:f(a_1,\ldots,a_n)\rightarrow f(t^\prime_1,\ldots,t^\prime_n)$
+and
+$\psi_a:f(b_1,\ldots,b_n)\rightarrow f(t^\prime_1,\ldots,t^\prime_n)$
+are structural coercions then
+\[\phi_a\circ\Phi^i_{f,a_1,\ldots,a_n}\circ\phi^\prime_a=
+\psi_b\circ\psi^i_{f,b_1,\ldots,b_n}\circ\psi^\prime_b\]
+or equivalently, the following diagram commutes
+
+\[\begin{array}{c@{\hspace{1.5cm}}c@{\hspace{1.5cm}}c}
+&\Rnode{N1}{t} & \\
+&&\\
+&&\\
+&&\\
+&&\\
+\Rnode{N2}{a_i}&&\Rnode{N3}{b_i}\\
+&&\\
+&&\\
+&&\\
+&&\\
+&&\\
+\Rnode{N4}{f(a_1,\ldots,a_n)}&&\Rnode{N5}{f(b_1,\ldots,b_n)}\\
+&&\\
+&&\\
+&&\\
+&&\\
+&\Rnode{N6}{f(t^\prime_1,\ldots,t^\prime_n)} & \\
+\end{array}
+\psset{nodesep=0.3cm}
+\everypsbox{\scriptstyle}
+\ncLine{>}{N1}{N2}
+\Bput{\displaystyle\phi^\prime_a}
+\ncLine{>}{N1}{N3}
+\Aput{\displaystyle\psi^\prime_b}
+\ncLine{>}{N2}{N4}
+\Bput{\displaystyle\Phi^i_{f,a_1,\ldots,a_n}}
+\ncLine{>}{N3}{N5}
+\Aput{\displaystyle\Phi^i_{f,b_1,\ldots,b_n}}
+\ncLine{>}{N4}{N6}
+\Bput{\displaystyle\phi_a}
+\ncLine{>}{N5}{N6}
+\Aput{\displaystyle\psi_b}
+\]
+\end{DoyeAssumption}
+
+Notice that assumption \ref{Doye6.4.5} is provable in the case that
+$f$ is covariant at $i$ (and we will prove this in the proof of the
+coherence theorem \ref{Doye6.4.7}). In the contravariant case, there is
+no link between $t$ and $t^\prime_i$ and it is this which make it an
+assumption.
+
+The following assumption is more easily ensurable. We merely require
+that for two types constructed by the same type constructor, if there
+exists a coercion between them then it equals the structural coercions
+between them which we now assume to exist. This is also an assumption
+on type constructors.
+
+\begin{DoyeAssumption}
+\label{Doye6.4.6}
+If $f(s_1,\ldots,s_n)\trianglelefteq f(t_1,\ldots,t_n)$ then there exists
+a structured coercion $f(s_1,\ldots,s_n)$ to $f(t_1,\ldots,t_n)$ and
+it is the unique coercion $f(s_1,\ldots,s_n)$ to $f(t_1,\ldots,t_n)$
+\end{DoyeAssumption}
+
+We are now finally in a position to state and prove the coercion
+theorem.
+
+\begin{DoyeTheorem} {\bf (Coherence theorem)}
+\label{Doye6.4.7}
+Assume that all coercions between ground types are only built by
+one of the following mechanisms:
+\begin{enumerate}
+\item coercions between base types
+\item coercions induced by structural coercions
+\item direct embeddings (definition \ref{Doye6.4.3}) in a type
+constructor
+\item composition of coercions
+\item identity function on ground types as coercions
+\end{enumerate}
+If assumptions \ref{Doye6.3.1}, \ref{Doye6.3.3}, \ref{Doye6.3,4},
+\ref{Doye6.3.5}, \ref{Doye6.3.6}, \ref{Doye6.4.1}, \ref{Doye6.4.5},
+\ref{Doye6.4.6} are satisfied, then the set of ground types as
+objects, and the coercions between them as arrows form a category
+which is a preorder.
+\end{DoyeTheorem}
+
+PROOF: By assumption \ref{Doye6.3.1} and lemma \ref{Doye6.3.2}, the
+set of ground types as objects and coercions between them form a
+category.
+
+All our coercions are either an individual coercion or a composition
+of finitely many coercions from the list: coercions between base
+types; structural coercions; direct embeddings (\ref{Doye6.4.2}) in a
+type constructor; and identity functions.
+
+Thus we may decompose any coercion into such a finite composition. We
+define len($\phi$) (the {\sl length} of $\phi$) to be the minimum
+number of coercions in any decomposition of $\phi$, Clearly, there are
+infinitely many values of len($\phi$) but there is a minimum value.
+
+For any two ground types $t$ and $t^\prime$ we will prove by induction
+on the length of the coercions between them that any coercions between
+them are unique.
+
+Let $\phi,\psi:t\rightarrow t^\prime$ be coercions.
+
+If the length of $\phi$ and $\psi$ is 1 then (replacing the unordered
+pair ($\phi,\psi$) with ($\tau_1,\tau_2$)) we need to look at our eight
+cases 1, 4, 6, 7, 8, 11, 12 and 16 defined above.
+
+{\bf Cases 1 and 4:} If $\phi$ is a base type coercion, then $t$ and
+$t^\prime$ are base types and coercions between base types are unique
+by assumption \ref{Doye6.3.3}.
+
+{\bf Case 8, 12, and 16:} If $\phi$ is an identity function on a
+ground type then $t=t^\prime$ then by assumption \ref{Doye6.4.1}
+$\phi=\psi$.
+
+{\bf Case 6:} If $\phi$ and $\psi$ are structural coercions then
+$\phi$ and $\psi$ are equal by assumption \ref{Doye6.3.4}.
+
+{\bf Case 7:} If $\phi$ is a direct embedding and $\psi$ is a
+structural coercion then there are two cases.
+
+{\bf Case 7a:} If $\psi$ is covariant. Then by assumption
+\ref{Doye6.4.6} $\psi=\phi$.
+
+{\bf Case 7b:} $\psi$ is contravariant. Thus $t=f(t_1,\ldots,t_n)$ and
+there exists $i$ and a coercion $t\rightarrow t_i$. This can not
+happen since no composition of our four basic coercions can create
+such a coercion.
+
+{\bf Case11:} If $\phi$ and $\psi$ are direct embedings then by
+assumption \ref{Doye6.3.5} $\psi=\phi$.
+
+We now may assume that any coercions of length less than or equal to
+$k$ are unique.
+
+Suppose that $\phi,\psi:t\rightarrow t^\prime$ are coercions and
+max(len($\phi$),len($\psi$))$=k+1$. Also suppose that
+$\phi=\tau_1\circ\phi^\prime$ and $\psi=\tau_2\circ\psi^\prime$ where
+for $i$ in \{1,2\} we have $\tau_i:s_i\rightarrow t^\prime$ are single
+atomic coercions. Also $\phi^\prime:t\rightarrow s_1$ and
+$\psi^\prime:t\rightarrow s_2$ are unique coercions since their
+lengths are less than or equal to $k$.
+
+If the length of $\phi$ or $\psi$ is 1 then we define $\phi^\prime$ or
+$\psi^\prime$ respectively to be the identity function on $t$.
+
+As stated before, there are eight cases 1, 4, 6, 7, 8, 11, 12, and
+16. (We may transpose $\tau_1$ and $\tau_2$ if we wish since their
+order is unimportant.)
+
+{\bf Case 1:} $\tau_1$ is a coercion between base types. $\tau_2$ is a
+coercion between base types. Then $t^\prime$, $s_1$, and $s_2$ are all
+base types. Base types may only be the targets of base type coercions
+hence $t$ is a base type. Thus $\phi$ and $\psi$ are coercions between
+base types and are thus equal by assumption \ref{Doye6.3.3}.
+
+{\bf Case 4:} $\tau_1$ is a coercion between base types. $\tau_2$ is
+an identity function. Again $t$ and $t^\prime$ must be base types and
+$\phi$ and $\psi$ are equal by assumption \ref{Doye6.3.3}.
+
+{\bf Case 6:} $\tau_1$ is a structural coercion. $\tau_2$ is a
+structural coercion. Let\\
+$t^\prime=f(t^\prime_1,\ldots,t^\prime_n)$
+
+If $t$ is equal to some $f(t_1,\ldots,t_n)$ then $\phi$ and $\psi$ are
+structural coercions $f(t_1,\ldots,t_n)$ to
+$t^\prime=f(t^\prime_1,\ldots,t^\prime_n)$ and hence are equal by
+assumption \ref{Doye6.3.4}.
+
+Else, we may assume that $t\ne f(t_1,\ldots,t_n)$. Since all our
+coercions are built from compositions of the four base types of
+coercion we may consider $\phi$ and $\psi$ to be chains of
+compositions. Without loss of generality, assume that the length of
+$\phi$ is $k+1$ and the length of $\psi$ is $l$ where $l\le k+1$.
+\[t=h_0\overset{\phi_0}{\rightarrow}h_1\cdots
+h_k\overset{\phi_k}{\rightarrow} h_{k+1}=t^\prime\]
+and
+\[t=s_0\overset{\psi_0}{\rightarrow}s_1\cdots
+s_{l1}\overset{\psi_{l1}}{\rightarrow} s_l=t^\prime\]
+
+In both the composition chains of coercions from $t$ to $t^\prime$
+there must exist a minimal element of the chain which is constructed
+by $f$ and this (by assumption) can not be $s_0$ or $h_0$. Also
+because $\tau_1$ and $\tau_2$ are structural coercions, these minimal
+elements are not $h_{k+1}$ or $s_l$.
+
+In the $\phi$chain we will assume that this element is $h_a$. In the
+$\psi$chain we will assume that this element is $s_b$.
+
+Since $h_a$ is constructed by $f$ and $h_{a1}$ is not and
+$\phi_{a1}$ is one of the four basic coercions, it must be a direct
+embedding. (It can not be a structural coercion since $h_{a1}$ is not
+constructed by $f$. It is not a coercion between base types because
+$h_a$ is constructed by $f$. It is not an identity coercion since
+$h_{a1}$ is not constructed by $f$ whereas $h_a$ is.)
+
+Similarly $\psi_{b1}$ is also a direct embedding.
+
+Now by assumption \ref{Doye6.3.5} the direct embedding must be at the
+same position. We will assume that this position is the $i$th.
+
+Let $h_a=f(a_1,\ldots,a_n)$ and $s_b=f(b_1,\ldots,b_n)$. Call the
+unique structural coercions \\
+$\phi_a:h_a\rightarrow t^\prime$ and
+$\psi_b:s_b\rightarrow t^\prime$. (Notice that $h_{a1}=a_i$ and
+$s_{b1}=b_i$.)
+
+Call the maps $\phi^\prime_a:t\rightarrow h_{a1}$ and
+$\psi^\prime_b:t\rightarrow s_{b1}$ where
+\[\phi^\prime_a=\phi_0\circ\cdots\circ\phi_{a2}\]
+and
+\[\psi^\prime_a=\psi_0\circ\cdots\circ\psi_{b2}\]
+(If $a$ or $b$ equal 1 then we may insert an initial identity coercion
+and lengthen the chain by one. This does not affect our induction on
+length since we are always in good shape with identity
+coercions. Neither $a$ nor $b$ may be 0 by our assumption on $t$.)
+
+Thus we have the following diagram, and we wish to prove that it
+commutes.
+
+\[\begin{array}{c@{\hspace{1.5cm}}c@{\hspace{1.5cm}}c}
+&\Rnode{N1}{t} & \\
+&&\\
+&&\\
+&&\\
+&&\\
+\Rnode{N2}{a_i}&&\Rnode{N3}{b_i}\\
+&&\\
+&&\\
+&&\\
+&&\\
+&&\\
+\Rnode{N4}{h_a=f(a_1,\ldots,a_n)}&&\Rnode{N5}{s_b=f(b_1,\ldots,b_n)}\\
+&&\\
+&&\\
+&&\\
+&&\\
+&\Rnode{N6}{f(t^\prime_1,\ldots,t^\prime_n)} & \\
+\end{array}
+\psset{nodesep=0.3cm}
+\everypsbox{\scriptstyle}
+\ncLine{>}{N1}{N2}
+\Bput{\displaystyle\phi^\prime_a}
+\ncLine{>}{N1}{N3}
+\Aput{\displaystyle\psi^\prime_b}
+\ncLine{>}{N2}{N4}
+\Bput{\displaystyle\Phi^i_{f,a_1,\ldots,a_n}}
+\ncLine{>}{N3}{N5}
+\Aput{\displaystyle\Phi^i_{f,b_1,\ldots,b_n}}
+\ncLine{>}{N4}{N6}
+\Bput{\displaystyle\phi_a}
+\ncLine{>}{N5}{N6}
+\Aput{\displaystyle\psi_b}
+\]
+
+{\bf Case 6a:} $f$ is covariant in the $i$th position.
+
+Consider the coercions $\alpha:a_i\rightarrow t^\prime_i$ and
+$\beta:b_i\rightarrow t^\prime_i$. (Recall that
+$t^\prime=f(t^\prime_1,\ldots,t^\prime_n))$. These must exist because
+$\phi_a$ and $\psi_b$ lift them covariently respectively.
+
+The definition of direct embeddings \ref{Doye6.4.3} guarantees the
+existence of $\Phi^i_{f,t^\prime_1,\ldots,t^\prime_n}$.
+
+Now by the definitions above
+\[\phi=\phi_a\circ\Phi^i_{f,a_1,\ldots,a_n}\circ\phi^\prime_a\]
+By assumption \ref{Doye6.3.6}
+\[\phi_a\circ\Phi^i_{f,a_1,\ldots,a_n}=
+\Phi^i_{f,t^\prime_1,\ldots,t^\prime_n}\circ\alpha\]
+Thus
+\[\phi=\Phi^i_{f,t^\prime_1,\ldots,t^\prime_n}\circ\alpha\circ
+\phi^\prime_a\]
+By induction on length we know that the coercion $t$ to $t^\prime_i$
+is unique. Hence
+\[\alpha\circ\phi^\prime_a=\beta\circ\psi^\prime_b\]
+So
+\[\phi=\Phi^i_{f,t^\prime_1,\ldots,t^\prime_n}\circ\beta\circ
+\psi^\prime_b\]
+Assumption \ref{Doye6.3.6} gives us
+\[\Phi^i_{f,t^\prime_1,\ldots,t^\prime_n}\circ\beta=
+\psi_b\circ\Phi^i_{f,b_1,\ldots,b_n}\]
+Thus
+\[\phi=\psi_b\circ\Phi^i_{f,b_1,\ldots,b_n}\circ\psi^\prime_b\]
+which by definition means $\phi=\psi$.
+
+Graphically, the following is a commutative diagram.
+
+\[\begin{array}{c@{\hspace{2cm}}c@{\hspace{2cm}}c}
+&\Rnode{N1}{t} & \\
+&&\\
+&&\\
+&&\\
+&&\\
+\Rnode{N2}{h_{a1}=a_i}&&\Rnode{N3}{s_{b1}=b_i}\\
+&&\\
+&&\\
+&&\\
+&&\\
+&\Rnode{N4}{t^\prime_i}&\\
+&&\\
+&&\\
+&&\\
+\Rnode{N5}{h_a=f(a_1,\ldots,a_n)}&&\Rnode{N6}{s_b=f(b_1,\ldots,b_n)}\\
+&&\\
+&&\\
+&&\\
+&&\\
+&\Rnode{N7}{t^\prime=f(t^\prime_1,\ldots,t^\prime_n)} & \\
+\end{array}
+\psset{nodesep=0.3cm}
+\everypsbox{\scriptstyle}
+\ncLine{>}{N1}{N2}
+\Bput{\displaystyle\phi^\prime_a}
+\ncLine{>}{N1}{N3}
+\Aput{\displaystyle\psi^\prime_b}
+\ncLine{>}{N2}{N4}
+\Aput{\displaystyle \alpha}
+\ncLine{>}{N3}{N4}
+\Bput{\displaystyle \beta}
+\ncLine{>}{N2}{N5}
+\Bput{\displaystyle\Phi^i_{f,a_1,\ldots,a_n}}
+\ncLine{>}{N3}{N6}
+\Aput{\displaystyle\Phi^i_{f,b_1,\ldots,b_n}}
+\ncLine{>}{N5}{N7}
+\Bput{\displaystyle\phi_a}
+\ncLine{>}{N4}{N7}
+\Aput{\displaystyle \Phi^i_{f,t^\prime_1,\ldots,t^\prime_n}}
+\ncLine{>}{N6}{N7}
+\Aput{\displaystyle\psi_b}
+\]
+
+{\bf Case 6b:} $f$ is contravariant in its $i$th position.
+
+There is nothing to link $t$ and $^\prime_i$ in this case and we must
+resort to assumption \ref{Doye6.4.5}.
+
+\[\begin{array}{c@{\hspace{0.5cm}}c@{\hspace{0.5cm}}c}
+&\Rnode{N1}{t} & \\
+&&\\
+&&\\
+&&\\
+&&\\
+&\Rnode{N4}{t^\prime_i}&\\
+&&\\
+&&\\
+&&\\
+\Rnode{N2}{h_{a1}=a_i}&&\Rnode{N3}{s_{b1}=b_i}\\
+&&\\
+&&\\
+&&\\
+&&\\
+&&\\
+\Rnode{N5}{h_a=f(a_1,\ldots,a_n)}&&\Rnode{N6}{s_b=f(b_1,\ldots,b_n)}\\
+&&\\
+&&\\
+&&\\
+&&\\
+&\Rnode{N7}{t^\prime=f(t^\prime_1,\ldots,t^\prime_n)} & \\
+\end{array}
+\psset{nodesep=0.3cm}
+\everypsbox{\scriptstyle}
+\ncLine{>}{N1}{N2}
+\Bput{\displaystyle\phi^\prime_a}
+\ncLine{>}{N1}{N3}
+\Aput{\displaystyle\psi^\prime_b}
+\ncLine{>}{N4}{N2}
+\ncLine{>}{N4}{N3}
+\ncLine{>}{N2}{N5}
+\Bput{\displaystyle\Phi^i_{f,a_1,\ldots,a_n}}
+\ncLine{>}{N3}{N6}
+\Aput{\displaystyle\Phi^i_{f,b_1,\ldots,b_n}}
+\ncLine{>}{N5}{N7}
+\Bput{\displaystyle\phi_a}
+\ncLine{>}{N6}{N7}
+\Aput{\displaystyle\psi_b}
+\]
+
+{\bf Case 7:} $\tau_1$ is a direct embedding. $\tau_2$ is a structural
+coercion.
+
+{\bf Case 7a:} $\tau_2$ is covariant. Then $\phi=\psi$ by case 6a
+above.
+
+{\bf Case 7b:} $\tau_2$ is contravarient. Let
+$s_2=f(s_{2_1},\ldots,s_{2_n})$ and
+$t^\prime=f(t^\prime_1,\ldots,t^\prime_n)$. If
+$\kappa:t^\prime_i\rightarrow s_{2_i}$, is the coercion lifted
+(contravariantly) by $\tau_2$ where
+\[\tau_2=\mathcal{F}_f(\ldots,s_2,\ldots,t^\prime_i,\ldots,\kappa,\ldots)\]
+Also
+\[\tau_1=\Phi^i_{f,t^\prime_1,\ldots,\tau^\prime_n}\]
+The uniqueness of $\tau^\prime$ implies that
+\[\phi^\prime=\Phi^i_{f,s_{2_1},\ldots,s_{2_n}}\circ\kappa\circ\phi^\prime\]
+By assumption \ref{Doye6.3.6} we have
+\[\mathcal{F}_f(\ldots,s_2,\ldots,t^\prime_i,\ldots,\kappa,\ldots)\circ
+\Phi^i_{f,s_{2_1},\ldots,s_{2_n}}\circ\kappa=
+\Phi^i_{f,t^\prime_1,\ldots,s^\prime_n}\]
+Thus
+\[\mathcal{F}_f(\ldots,s_2,\ldots,t^\prime_i,\ldots,\kappa,\ldots)\circ
+\Phi^i_{f,s_{2_1},\ldots,s_{2_n}}\circ\kappa=
+\Phi^i_{f,t^\prime_1,\ldots,s^\prime_n}\circ\psi^\prime\]
+and therefore
+\[\mathcal{F}_f(\ldots,s_2,\ldots,t^\prime_i,\ldots,\kappa,\ldots)\circ
+\phi^\prime =
+\Phi^i_{f,t^\prime_1,\ldots,s^\prime_n}\circ\psi^\prime\]
+Hence, $\phi=\psi$.
+
+{\bf Case 8:} $\tau_1$ is a structural coercion. $\tau_2$ is an
+identity function. Let
+$t^\prime=f(t^\prime_1,\ldots,t^\prime_n)$.
+By viewing $\tau_2$ as the identity function
+\[\mathcal{F}_f(t^\prime_1,\ldots,t^\prime_n,
+t^\prime_1,\ldots,t^\prime_n,{\rm id}_{t^\prime_1},\ldots,
+{\rm id}_{t^\prime_n})\]
+Thus $\phi=\psi$ by case 6.
+
+{\bf Case 11:} $\tau_1$ is a direct embedding. $\tau_2$ is a direct
+embedding. Assumption \ref{Doye6.3.5} implies that the direct
+embeddings must be at the same position, $i$. Therefore $s_1=s_2$. So
+by the inductive hypothesis $\phi^\prime=\psi^\prime$. By assumption
+\ref{Doye6.3.5} $\tau_1=\tau_2$. Hence $\phi=\psi$.
+
+{\bf Case 12:} $\tau_1$ is a direct embedding. $\tau_2$ is an identity
+function. Let\\
+$t^\prime=f(t^\prime_1,\ldots,t^\prime_n)$. By viewing $\tau_2$ as the
+identity structural coercion
+\[\mathcal{F}_f(t^\prime_1,\ldots,t^\prime_n,
+t^\prime_1,\ldots,t^\prime_n,
+{\rm id}_{t^\prime_1},\ldots,{\rm id}_{t^\prime_n})\]
+Thus $\phi=\psi$ by case 6, above.
+
+{\bf Case 16:} $\tau_1$ is an identity function. $\tau_2$ is an
+identity function. Thus $\phi=\phi^\prime$ and
+$\psi=\psi^\prime$. However, since $s_1=s_2$,
+$\phi^\prime=\psi^\prime$ by the induction hypothesis. Hence
+$\phi=\psi$.
+
+Thus we have proved $\phi=\psi$ for all coercions of length less than
+or equal to $k+1$. Hence the result holds for all coercions, by
+induction. \QED
+
+In case 10b of the case when the length is 1 we claimed that there can
+not be built a coercion from a type constructor to one of its
+arguments.
+
+From our description so far of Axiom, one might think that Axiom would
+permit the construction of the following type
+\[{\bf Fraction(Fraction(Integer))}\]
+which is the quotient field of the quotient field of
+integers\footnote{The quotient field of the integers ($\mathbb{Z}$) is
+more commonly known as the rationals ($\mathbb{Q}$).} However, the
+quotient field of a quotient field is itself and hence,
+\[{\bf Fraction(Fraction(Integer))\cong Fraction(Integer)}\]
+
+For this reason, Axiom contains special code in the interpreter to
+stop such pathological types being instantiated. A function
+({\bf isValidType}) checks to see if one is trying to create a type
+like the one above, or
+\[{\bf Polynomial(Polynomial(Integer))}\]
+
+But this is handcrafted, special code covering a few cases and
+mentions the types by name. It is conceivable that a user could create
+a new type called {\bf MyFraction} which is identical to
+{\bf Fraction}. This would not be picked up by {\bf isValidType} and thus
+\[{\bf MyFraction(MyFraction(Integer))}\]
+could be instantiated. Since the type is then isomorphic to one of its
+arguments, it is feasible that a coercion between the two could be
+defined, contradicting our claim in case 10b of the case when the
+length is 1.
+
+This coercion can still not be built from our four basic types, thus
+defining such a coercion contradicts our assumptions for the coherence
+theorem.
+
+\subsection{Extending the coherence theorem}
+\label{DoyeSec6.5}
+
+First, Weber's ``proof'' of his conjecture \ref{Doye6.3.7} relies on
+induction on com($t$). This assumes that there are no types of
+infinite complexity in our system. This is not the case in Axiom,
+since one could define the following types (in one file):
+
+{\bf R(r : Ring) : Ring == r}\\
+{\bf D1 : Ring == R(D2)}\\
+{\bf D2 : Ring == R(D1)}
+
+(though calling {\bf 1()\$D1} would be disastrous\footnote{This would
+try to create the constant 1 from the ring {\bf D1} which can not be
+evaluated.})! So we add the following extra assumption.
+
+\begin{DoyeAssumption}
+\label{Doye6.5.1}
+There do not exist any types of nonfinite complexity
+\end{DoyeAssumption}
+
+The proof of the coherence theorem \ref{Doye6.4.7} does not rely on
+type having finite complexity. However it is still a sensible
+assumption to make and can be easily guaranteed in a real
+implementation. It is also imperative that this assumption holds if
+the automated coercion algorithm \ref{Doye7.4.1} is to terminate.
+
+Assumption \ref{Doye6.3.5} states that we may have only one direct
+embedding into an algebra. However, in {\bf Polynomial(Integer)} one
+would wish to perform the direct embeddings of both of {\bf Integer}
+and {\bf Symbol}, yet this violates assumption \ref{Doye6.3.5} and
+thus we would not be able to prove that our algebra system is
+coherent.
+
+The reason for Weber's assumption is to stop coercions like the
+following occurring. If $A$ is a group, then being able to coerce
+$A\rightarrow A\times A$ whilst potentially useful, is ambiguous. As
+he points out in \cite{Webe93b} and \cite{Webe95}. $A$ can be
+coerced into $A\times A$ via the isomorphisms
+$A\cong A\times I$ or $A\cong I\times A$ (where $I$ is the trivial
+subgroup of $A$).
+
+In this example the inclusions are ambiguous, since using either
+coercion, the target of the inclusion is a group. However, in many
+cases the types are ``incomparable'', (e.g. {\bf Integer} and
+{\bf Symbol}) and thus the assumption seems to be too strong. The
+question is what do we mean by ``incomparable''?
+
+Certainly, there is no coercion function
+${\bf Integer}\rightarrow{\bf Symbol}$ or
+${\bf Symbol}\rightarrow{\bf Integer}$. But, for two distinct
+nontrivial, proper normal subgroups $G$, $H$ of $A$ such that
+$G\cap H=I$, then there is no coercion function
+$A/G\rightarrow A/H$, and coherency is lost. ($A/G$ is the quotient
+group ``$A$ factored out by $G$'' and is the set
+$\{aG~\vert~a\in A\}$ where $aG=a^\prime G$ iff
+$a^{1}a^\prime\in G$). Thus, the condition of there not existing a
+coercion function between our two types is not sufficient for our
+definition of ``incomparability''.
+
+However, we notice that there exists no type which can be coerced to
+both {\bf Symbol} and {\bf Integer}, but there does exist
+homomorphisms $A\rightarrow A/G$ and $A\rightarrow A/H$. So if we
+choose the statement ``Types $A$ and $B$ are incomparable if there
+does not exist a type $S$ which can be coerced to both $A$ and $B$''
+as a definition of incomparability then we are in good shape.
+
+We state this in the language of Weber as follows. To replace the
+assumption we first need to alter definition \ref{Doye6.4.3} (our
+previous replacement of definition \ref{Doye6.2.8} to the following.
+
+\begin{DoyeDefinition}
+\label{Doye6.5.2}
+Let $f:(\sigma_1,\ldots,\sigma_n)\rightarrow\sigma$ be an $n$ary
+type constructor. If\\
+$(\forall i\in\{1,\ldots,n\})(\forall~ground~types~t_i:\sigma_i)$
+there exists a coercion
+\[\Phi^i_{f,t_1,\ldots,t_n}:t_i\rightarrow f(t_1,\ldots,t_n)\]
+then we say that $f$ has a {\rm direct embedding at its $i$th
+position}.
+
+Moreover, let $s$ be a ground type and $i\in\{1,\ldots,n\}$ and
+define,
+\[\mathcal{P}(i,s):=((\exists \psi:s\rightarrow t_i)\land
+(\exists \Phi^i_{f,t_1,\ldots,t_n}:t_i\rightarrow
+f(t_1,\ldots,t_n)))\]
+where $\psi$ is a coercion, and also define,
+\[\overline{\mathcal{D}}_f:=\{(i,s)~\vert~\mathcal{P}(i,s)\}\]
+\end{DoyeDefinition}
+
+Note then that
+$\mathcal{D}_f=\{i~\vert~(\exists s)(\mathcal{P}(i,s))\}$.
+
+We now alter assumption \ref{Doye6.3.5} to the following
+
+\begin{DoyeAssumption}
+\label{Doye6.5.3}
+Let $f$ be an $n$ary type constructor. Then the following
+conditions hold:
+\begin{enumerate}
+\item $(i,s),(j,s)\in\overline{\mathcal{D}}_f\rightarrow i=j$
+\item Direct embedding coercions are unique. i.e. if
+$\Phi^i_{f,t_1,\ldots,t_n}:t_i\rightarrow f(t_1,\ldots,t_n)$ and
+$\Psi^i_{f,t_1,\ldots,t_n}:t_i\rightarrow f(t_1,\ldots,t_n)$ then
+\[\Phi^i_{f,t_1,\ldots,t_n}=\Psi^i_{f,t_1,\ldots,t_n}\]
+\end{enumerate}
+\end{DoyeAssumption}
+
+So we may now extend the coherence theorem (theorem \ref{Doye6.4.7})
+by altering the assumption list to our new relaxed set of
+assumptions. It is not necessary to reprove the entire theorem, but
+merely the cases which involved assumption \ref{Doye6.3.5}.
+
+\begin{DoyeTheorem} {\bf (Extended coherence theorem)}
+\label{Doye6.5.4}
+Assume that all coercions between ground types are only built by
+one of the following mechanisms:
+\begin{enumerate}
+\item coercions between base types
+\item coercions induced by structural coercions
+\item direct embeddings (definition \ref{Doye6.5.2}) in a type
+constructor
+\item composition of coercions
+\item identity function on ground types as coercions
+\end{enumerate}
+
+If assumptions \ref{Doye6.3.1}, \ref{Doye6.3.3}, \ref{Doye6.3.4},
+\ref{Doye6.3.6}, \ref{Doye6.5.1}, \ref{Doye6.4.6}, \ref{Doye6.4.1},
+\ref{Doye6.4.5}, and \ref{Doye6.5.3} are satisfied, then the set of
+ground types as objects, and the coercions between them as arrows form
+a category which is a preorder.
+\end{DoyeTheorem}
+
+PROOF: The entire proof of theorem \ref{Doye6.4.7} is valid except where
+assumption \ref{Doye6.3.5} was used.
+
+First we deal with the length of $\phi$ and $\psi$ being 1. The only
+case which relied on assumption \ref{Doye6.3.5} was case 11.
+
+{\bf Case 11:} If $\phi$ and $\psi$ are direct embeddings then by
+assumption \ref{Doye6.5.3} $\psi=\phi$.
+
+Now, the induction case. The only cases which relied on assumption
+\ref{Doye6.3.5} were cases 6 and 11.
+
+{\bf Case 6:} In the proof of theorem \ref{Doye6.4.7} in the case we
+relied on assumption \ref{Doye6.3.5} to show that the two direct
+embeddings $h_{a1}\rightarrow h_a$ and $s_{b1}\rightarrow s_b$ were
+at the same position.
+
+Now since $t\trianglelefteq h_{a1}$ and $t\trianglelefteq s_{b1}$ by
+assumption \ref{Doye6.5.3} the direct embeddings must be at the same
+position.
+
+Thus the rest of the proof of this case holds.
+
+{\bf Case 11:} $\tau_1$ is a direct embedding. $\tau_2$ is a direct
+embedding. Since $t\trianglelefteq s_1$ and
+$t\trianglelefteq s_2$ assumption \ref{Doye6.5.3} implies that the
+direct embeddings must be at the same position, $i$. Therefore,
+$s_1=s_2$. So by the inductive hypothesis
+$\phi^\prime=\psi^\prime$. By assumption \ref{Doye6.5.3}
+$\tau_1=\tau_2$. Hence, $\phi=\psi$.
+
+Inserting the rest of the proof of theorem \ref{Doye6.4.7} completes
+the proof.\QED
+
+Thus we have relaxed an important one of the conditions of the
+coherence theorem \ref{Doye6.4.7} and proved that the theorem still holds.
+
+\subsection{Conclusion}
+\label{DoyeSec6.6}
+
+In this section we stated all the mathematics needed to state Weber's
+coherence conjecture and give his proof.
+
+We have also stated extra mathematics to correct the statement of the
+conjecture and then prove it; hence promoting it to a theorem. We have
+then relaxed one of the conditions and shown that the theorem still
+holds.
+
+This theorem is the cornerstone for ensuring correct coercions.
+
+By having a coherent type system, then provided we are careful in how
+we implement our type constructors (they must satisfy the assumptions)
+and how we create our coercions (compositions of the four basic types)
+all our coercions are then unique.
+
+\section{The automated coercion algorithm}
+\label{DoyeChap7}
+
+We will introduce some extra mathematics which will allow us to state
+the automated coercion algorithm. Furthermore, this sound foundation
+will allow us to demonstrate that all coercions generated by the
+algorithm are, in fact, homomorphisms. Indeed, we may even guarantee
+that these are coercions in the sense of definition
+\ref{Doye5.5.2}.
+
+\subsection{Finitely generated algebras}
+\label{DoyeSec7.2}
+
+In this section we will define what it means to say that an algebra is
+finitely generated, and also what it means to say that a finitely
+generated algebra is decomposable.
+
+\begin{DoyeDefinition}
+\label{Doye7.2.1}
+Let $\Sigma$ be an ordersorted $S$signature. We say that $S$
+has a {\rm principal sort} if $\langle\Sigma,S\rangle$ defines an
+algebra which has one sort (which without loss of generality, we will
+always assume that to be $S_1$) which is the ``most interesting'' of
+the algebra.
+\end{DoyeDefinition}
+
+By ``most interesting'', we mean that a more na\"ive algebraist would
+consider this sort to define the entire algebra.
+
+For example, if we define $\Gamma$ to be the Group algebra with sort,
+\[(``the~group'',``a~boolean~sort'',``an~integer~number~system'')\]
+
+then the ``most interesting'' sort is the one for ``{\sl the group}''
+which would be carried by a set of all the group elements.
+
+All Axiom algebras must have a principal sort, referred to as \%, in
+the source code. One can think of $S_1=\%$ as the sort that the Axiom
+code ``constructs''. In the terminology of section \ref{DoyeChap6} it
+is the type constructed by the type constructor. (Axiom views base
+types as type constructors with no arguments.)
+
+\begin{DoyeDefinition}
+\label{Doye7.2.2}
+We say that a theory $\langle\langle\Sigma,S\rangle,S\rangle$, is
+finitely generated iff $S$ has a principal sort, $S_1$, and the
+following set is finite,
+\[\overset{..}{\sum}:=\bigcup_{n,q}{\Sigma_{n,q,S_1}}\]
+\end{DoyeDefinition}
+
+This states that given a finitely generated $\Sigma$algebra,
+$\langle A,\alpha\rangle$ (which is a model for $S$) then there are a
+finite number of operators which can return an element of the carrier
+of the principal sort.
+
+This means that only finitely many functions (directly) construct (the
+carrier of) the principal sort.
+
+The next definition allows us to decompose any element of such a
+$\Sigma$algebra into at least two pieces. Moreover, there exists such
+a decomposition for each one of the (finitely many) constructors.
+Furthermore, decomposing such an element and recombining using the
+corresponding constructor is equivalent to the identity function.
+
+\begin{DoyeDefinition}
+A finitely generated theory
+$\langle\langle\Sigma,S\rangle,S\rangle$ is decomposable iff
+\[\begin{array}{l}
+(\forall \sigma\in\overset{..}{\Sigma})
+((\sigma\in\Sigma_{n,q,S_1})\Rightarrow\\
+\quad(\forall i\in\{1,\ldots,n\})
+(\exists \pi_{\sigma,i})
+(\pi_{\sigma,i}\in\Sigma_{1,S_1,q_i})\land\\
+\quad\quad((\sigma(\pi_{\sigma,1}(\cdot),\ldots,\pi_{\sigma,n}(\cdot))
+={\rm id}_{S_1})\in S))
+\end{array}\]
+\end{DoyeDefinition}
+
+For example, in an algebra of lists, {\bf cons} is a constructor.
+The corresponding functions which decompose an element are {\bf car}
+and {\bf cdr}. The following equation holds.
+\[{\bf cons(car(x),cdr(x))=x}\]
+
+Notice that this equation is only well formed when {\bf x} is not the
+empty list. For the empty list, which is constructed by the 0ary
+function {\bf nil()}, there are no decomposers, and the equation is as
+follows.
+\[{\bf nil() = x}\]
+
+It is important to note that the part functions $\pi_{\sigma,i}$ are
+usually partial functions. For example, {\bf car} is not defined on
+the empty list.
+
+Notice that we have not yet defined a way of differentiating between
+which constructors construct which element. We will do this now.
+
+\subsection{Constructibility}
+\label{DoyeSec7.3}
+
+We now come to the most important concept of this thesis. The aim of
+this thesis is to provde a method for creating coercions
+constructively. We now supply the means to do so.
+
+As usual, we need to make some definitions first. We will state what
+we mean by a(n) (algorithmically) (re)constructible algebra. What we
+really mean is that an algebra is (algorithmically) (re)constructible
+if some subset of the elements of the most interesting sortcarrier of
+that algebra can be ``built up'' from a finite family of operators.
+
+This finite family consists of ``constructors'' used to create
+increasingly ``large'' elements of the principal sort.
+
+We will also have equations in the theory linking the constructors to
+``part functions'' which we will use to split large elements into an
+$n$tuple of smaller elements. The constructor applied to its
+associated part functions acting on an element will be equivalent to
+the identity function.
+
+We will be able to tell how an element is constructed by using a
+``query function''. That is to say we must be able to know which
+constructor(s) may construct any particular element of the principal
+sort.
+
+We require these definitions so that if an algebra is a model of some
+algorithmically reconstructible theory, and another algebra contains
+some of the constructors of the first algebra, then some subset of the
+elements of the most interesting sortcarrier can be ``coerced'' from
+the first type to the second. We will show this to be a
+$\Xi$homomorphism, where $\Xi$ is a particular signature to which
+both algebras belong.
+
+We demand our extensions to be protecting extensions so that
+performing operations on an algebra (or looking at equations of
+elements of that algebra) when viewed as a model of the original
+theory or the extension of the theory yield ``the same result''.
+
+\begin{DoyeDefinition}
+\label{Doye7.3.1}
+We call a theory $\langle\langle\Sigma,S\rangle,S\rangle$
+constructible iff $\Sigma$ is a protecting extension of a finitely
+generated theory. We then call $\Sigma$ a {\rm constructing}
+signature, and any model for the theory, a {\rm constructible algebra}.
+\end{DoyeDefinition}
+
+Similarly,
+
+\begin{DoyeDefinition}
+\label{Doye7.3.3}
+If $\langle\langle\Xi,X\rangle,\mathcal{X}\rangle$ is a decomposable
+theory extended by the reconstructible
+$\langle\langle\Sigma,S\rangle,S\rangle$, we define the
+{\rm constructors} of
+$\langle\langle\Sigma,S\rangle,S\rangle$ to be
+\[\Sigma^C:=\overset{..}{\Xi}\]
+We define the {\rm constant constructors} to be the constructors of
+arity 0, denoted by $\Sigma^0$ and the {\rm nonconstant constructors}
+to be the constructors of all other arities. We denote this set by
+$\Sigma^{C0}:=\Sigma^C\backslash\Sigma^0$.
+
+We also define the {\rm part functions} of
+$\langle\langle\Sigma,S\rangle,S\rangle$ associated with
+$\sigma\in\Sigma^{C0}$ to be the $\pi_{\sigma,i}$. (Constant
+constructors have no associated part functions.)
+
+Finally we define the {\rm constructor equations} to be the following
+set and demand it to be a subset of $S$ (and hence $\mathcal{X}$) given by
+\[\{(\sigma(\pi_{\sigma,1}(\cdot),\ldots,\pi_{\sigma,n}(\cdot)=
+{\rm id}_{S_1})~\vert~\sigma\in\Sigma^{C0}\}\]
+\end{DoyeDefinition}
+
+We also need to ensure that certain other relationships between
+constructors which hold in our source algebra hold in our target
+algebra.
+
+If an element of the source algebra may be constructed in more than
+one way, we require that reconstructing that element in the target
+algebra using any of those methods yields the same result.
+
+Notice that since our theories are protecting extensions we are in
+good shape, since any equation that holds in the protecting extension
+which concerns only the sorts from the original (unextended) signature
+must hold in the original signature. Thus these equations will hold in
+the target algebra.
+
+We call these equations that link different constructors together the
+secondary constructor equations.
+
+\begin{DoyeDefinition}
+\label{Doye7.3.4}
+We call a reconstructible theory
+$\langle\langle\Sigma,S\rangle,S\rangle$ algorithmically
+reconstructible iff : $S$ contains a boolean sort, $B$;
+$\Sigma$ contains a set of symbols, called the query functions,
+denoted and defined by
+\[\Sigma^Q:=\{\mathcal{X}_\sigma\in\Sigma_{1,S_1,B}~\vert~
+\sigma\in\Sigma^C\}\]
+and $S$ contains the following equations, called the {\rm query equations}
+\[(\forall \sigma_{n,q,S_1}\in\Sigma^C)(\mathcal{X}_{\sigma_{n,q,S_1}}
+(\sigma_{n,q,S_1}(a_1,\ldots,a_n))=T)\]
+We also demand that for each $\sigma_{n,q,S_1}$ in $\Sigma^C$
+\[((\nexists~a_1,\ldots,a_n)(\omega=\sigma_{n,q,S_1}(a_1,\ldots,a_n)))
+\Rightarrow(\mathcal{X}_{\sigma_{n,q,S_1}}(\omega)=F)\]
+Finally we demand that all secondary constructor equations are defined
+in the theory.
+
+A {\rm secondary constructor equation} is any equation which has
+a constructor as the final symbol on both right and left sides.
+\end{DoyeDefinition}
+
+We say ``final symbol'' to mean this is the operator applied last. In
+our notation (functions written on the left) a final symbol is written
+to the left of all the other elements of a formula.
+
+For example, $\sigma()$ and $\sigma(e_1,\sigma^\prime(e_2,e_3))$ both
+have $\sigma$ as a final symbol.
+
+In the algorithm we will demand that the decomposable theory which
+both types model is the smallest theory which they both model. This is
+to ensure that the algorithm not only creates a homomorphism, but that
+it is a coercion (definition \ref{Doye5.5.2}). The proof of this is
+given in corollary \ref{Doye7.6.8}.
+
+\begin{DoyeExample}
+\label{Doye7.3.5}
+We will take the variety of {\sl Lists} as our example, and we will
+assume that {\bf List} is a member of this variety. Then the
+constructors for the model are {\bf nil} and {\bf cons}, where
+{\bf nil} is a constant constructor whereas {\bf cons} is a
+nonconstant constructor. {\bf cons}' associated partfunctions are
+{\bf car} and {\bf cdr}. Thus we have the constructor equation
+\[{\bf cons(car(x),cdr(x))=id(x)}\]
+
+The query functions are {\bf null} and {\bf consp}, and our query
+equations are
+\[{\bf null(nil)=}{\sl T}\]
+and for any list $l$ and any element of the underlying type, $i$,
+\[{\bf consp(cons(}i,l{\bf))=}{\sl T}\]
+
+Notice also that ${\bf consp(nil)=}{\sl F}$ and also, for the same $l$ and
+$i$, ${\bf null(cons(}i,l{\bf))=}{\sl F}$
+\end{DoyeExample}
+
+It is now worth discussing some of the finer points of homomorphism.
+
+For $\phi$ to be a homomorphism we require that the constructor
+functions are preserved by homomorphism. We do not require that the
+part or query functions are homomorphically preserved; indeed we do
+not even require that they are in the signature of the algebra of the
+target of $\phi$.
+
+Thus we do not require that both the source and target of $\phi$ are
+models of the same algorithmically reconstructible theory, but that
+the source is a model of an algorithmically reconstructible theory
+$\mathcal{T}$, and that all the constructors of $\mathcal{T}$ are
+functions of the target of $\phi$, inherited from the {\sl same}
+signature (theory).
+
+This is an important point. As an example, we will consider polynomial
+rings. A polynomial is a function such as
+\[5x^2y^3+9xy^{45}34x+7y^212\]
+
+That is a sum of products of an element of the underlying ring (which
+in the above example might be the integers) and variables raised to
+nonnegative powers. A monomial is a polynomial which is a product of
+a nonzero element of the underlying ring and variables raised to
+nonnegative powers.
+
+A polynomial ring is ordered by an extension of the order on the
+variables. In particular, in $\mathbb{Z}[x,y]$ if $x>y$ then a
+monomial $m_1$ is greater than another $m_2$ if the exponent of $x$ is
+greater in $m_1$ than in $m_2$. Should the exponent of $x$ be equal in
+both, then the exponent of $y$ is compared in the same manner.
+
+The leading monomial of a polynomial is the largest monomial of a
+polynomial. If $x>y$ in the above polynomial then $5x^2y^3$ is the
+leading monomial. Should $y>x$ then the leading monomial would be
+$9xy^{45}$.
+
+The reductum of a polynomial is the polynomial less its leading
+monomial.
+
+Coercions between two polynomial rings need only use
+{\bf leadingMonomial} as a part function (which is not preserved via
+homomorphism, since it depends on the ordering given to the variables)
+instead of some (unnatural) fixed (for all polynomial rings with
+variables from a fixed domain) ``mostimportant monomial'' function
+which would choose the same monomial, regardless of variable ordering.
+
+Also, this allows us to form the natural homomorphism from
+$\mathbb{Q}[x]$ to $\mathbb{Z}(x)$, which in Axiom is
+\[{\bf Polynomial\ Fraction\ Integer}\ to\
+{\bf Fraction\ Polynomial\ Integer}\]
+which are, in Axiom's view (without clever hackery in the interpreter)
+two unrelated {\bf Rings}. This may be constructed {\sl without}
+having to force $+$ to be a constructor of
+{\bf Fraction Polynomial Integer}, or indeed {\bf leadingMonomial},
+etc. to be available in {\bf Fraction Polynomial Integer}.
+
+\subsection{The algorithm}
+\label{DoyeSec7.4}
+
+We are now in a position to state the automated coercion algorithm.
+
+The algorithm to create the coercion will be stated in English. It is
+too implementation dependent to state any finer.
+
+The actual algorithm to coerce will be stated as Lisp pseudocode. In
+Lisp,
+{\bf (a b c)} means apply the function {\bf a} to the arguments
+{\bf (b,c)}. {\bf cond} is like the switch statement in C or Java.
+
+{\bf cond} is equivalent to ``ifthenelse'' statements  if a
+condition is true, then we evaluate and return the following statement
+(and leave the {\bf cond} block), else go to the next condition and
+repeat.
+
+For example, the line
+\[((\alpha_{\chi_{\sigma_{0,\emptyset,S_1}}} x)~
+(\beta_{\sigma_{0,\emptyset,S_1}}))\]
+means
+\[{\bf if\ }\alpha_{\chi_{\sigma_{0,\emptyset,S_1}}}(x)
+{\bf \ then\ }\beta_{\sigma_{0,\emptyset,S_1}}()\]
+
+The final statement {\bf t}, is the default statement since {\bf t} is
+always true. This line will only be reached when all the other
+conditions have not been satisfied, and shows that we have failed to
+build a total automated coercion function.
+
+This could happen if one fails to list all the constructors (and their
+queries) for a type.
+
+The lines of the form
+\[((\alpha_{\chi_{\sigma_{0,\emptyset,S_1}}} x)~
+(\beta_{\sigma_{0,\emptyset,S_1}}))\]
+check for the constants of the type. For example, the constant
+polynomial 0 can not be constructed using a nonzero number of parts
+(using any normal construction methodology) thus coercing 0 from
+$\mathbb{Q}[x]$ to $\mathbb{Z}(x)$ we might say
+\[\begin{array}{c}
+{\bf if~zero?(x)\$Polynomial~Fraction~Integer}\\
+\quad{\bf then~zero()\$Fraction~Polynomial~Integer}
+\end{array}\]
+returning the appropriate 0 in $\mathbb{Z}(x)$.
+
+The lines of the form
+\[((\alpha_{\chi_{\sigma_{n,q,S_1}}} x)
+(\beta_{\sigma_{n,q,S_1}}
+(\psi_{q_1} (\alpha_{\pi_{\sigma_{n,q,S_1},1}} x)\ldots
+(\psi_{q_n} (\alpha_{\pi_{\sigma_{n,q,S_1},n}} x))))\]
+are the constructing lines. For example, in a polynomial ring we might
+write
+\[\begin{array}{c}
+{\bf if~x~}{\rm\ is~the~sum~of~a~monomial~and~a~polynomial}\\
+{\bf then~coerce(leadingMonomial(x))+coerce(reductum(x))}
+\end{array}\]
+where the addition function is that taken from the target domain.
+
+In this case {\bf leadingMonomial(x)} and {\bf reductum(x)} are both
+polynomials. In general, the parts of the element need not be of the
+same type as the original element.
+
+For example, in List algebras, coercing from {\bf List(A)} to
+{\bf List(B)} where there exists (or we can build) a coercion from
+{\bf A} to {\bf B} then we have (back in Lisp terminology)
+\[{\bf ((consp~x)~(cons~(coerce~(car~x))~(coerce~(cdr~x))))}\]
+{\bf (car x)} is the first element of the list and is of type
+{\bf A} rather than {\bf List(A)}  the type of {\bf x}. So
+{\bf (coerce (car x))} is of type {\bf B} and thus may be
+{\bf consed} on to the front of {\bf (coerce (cdr x))} which is
+of type {\bf List(B)}.
+
+\begin{DoyeAlgorithm}{\bf (The Automated Coercion Algorithm)}
+\label{Doye7.4.1}
+Let $\langle A,\alpha\rangle$ be a model for the algorithmically
+reconstructible theory
+$\langle\langle\Sigma,S\rangle,S\rangle$
+
+Let $\langle B,\beta\rangle$ be a model of
+$\langle\langle\Delta,\mathcal{D}\rangle,\mathcal{D}\rangle$ where
+$\langle\langle\Sigma,S\rangle,S\rangle$ is a protecting extension of
+$\langle\langle\Delta,\mathcal{D}\rangle,\mathcal{D}\rangle$ and some
+(or all) of the constructors of
+$\langle\langle\Sigma,S\rangle,S\rangle$ are in fact
+$\langle\langle\Delta,\mathcal{D}\rangle,\mathcal{D}\rangle$.
+
+Also we demand that there does not exist an extension
+$\langle\langle\Delta,\mathcal{D}\rangle,\mathcal{D}\rangle$ which both
+$\langle A,\alpha\rangle$ and $\langle B,\beta\rangle$ model.
+
+Then the following is an algorithm to coerce from the
+$\langle A,\alpha\rangle$ to the $\langle B,\beta\rangle$ model.
+
+The $\psi_i$ for $i\ne 1$ are the (potentially automated) coercions
+from $A_i$ to $B_i$ from the abstract type of $S_i$.
+
+The entire morphism created thus is called $\psi$ and not only is it a
+homomorphism, it is a coercion (definition \ref{Doye5.5.2}).
+\end{DoyeAlgorithm}
+
+$\psi_1(x) := (cond$\\
+\vbox{\vskip 0.4cm}
+\hbox{\hskip 1cm}$((\alpha_{\chi_{\sigma_{0,\emptyset,S_1}}} x)~
+(\beta_{\sigma_{0,\emptyset,S_1}}))$\\
+\vbox{\vskip 0.4cm}
+\hbox{\hskip 1cm}$\vdots~Repeat~for~each~\sigma_{0,\emptyset,S_1}~in~
+\Sigma^0$\\
+\vbox{\vskip 0.4cm}
+\hbox{\hskip 1cm}$((\alpha_{\chi_{\sigma_{n,q,S_1}}} x)~
+(\beta_{\sigma_{n,q,S_1}}
+(\psi_{q_1} (\alpha_{\pi_{\sigma_{n,q,S_1},1}} x))\ldots
+(\psi_{q_n} (\alpha_{\pi_{\sigma_{n,q,S_1},n}} x))))$\\
+\vbox{\vskip 0.4cm}
+\hbox{\hskip 1cm}$\vdots~Repeat~for~each~\sigma_{n,q,S_1}~in~
+\Sigma^{C0}$\\
+\vbox{\vskip 0.4cm}
+\hbox{\hskip 1cm}$(t~(error)))$
+
+{\sl The algorithm to create the coercion $\psi$ is}
+
+$createCoerce(\langle A,\alpha\rangle,\langle B,\beta\rangle):=$\\
+\vbox{\vskip 0.5cm}
+\hbox{\hskip 1cm}$determine~
+\langle\langle\Delta,\mathcal{D}\rangle,\mathcal{D}\rangle
+~(error~if~doesn't~exist)$\\
+\vbox{\vskip 0.5cm}
+\hbox{\hskip 1cm}$determine~
+\langle\langle\Sigma,\mathcal{S}\rangle,\mathcal{S}\rangle
+~(error~if~doesn't~exist)$\\
+\vbox{\vskip 0.5cm}
+\hbox{\hskip 1cm}$determine~\Sigma^0$\\
+\vbox{\vskip 0.5cm}
+\hbox{\hskip 1cm}$for~\sigma\in\Sigma^0$\\
+\vbox{\vskip 0.5cm}
+\hbox{\hskip 1.5cm}$determine~\alpha_{\chi_\sigma}$\\
+\vbox{\vskip 0.5cm}
+\hbox{\hskip 1.5cm}$determine~\beta_\sigma$\\
+\vbox{\vskip 0.5cm}
+\hbox{\hskip 1cm}$determine~\Sigma^{C0}$\\
+\vbox{\vskip 0.5cm}
+\hbox{\hskip 1cm}$for~\sigma\in\Sigma^{C0}$\\
+\vbox{\vskip 0.5cm}
+\hbox{\hskip 1.5cm}$determine~\alpha_{\chi_\sigma}$\\
+\vbox{\vskip 0.5cm}
+\hbox{\hskip 1.5cm}$determine~\beta_\sigma$\\
+\vbox{\vskip 0.5cm}
+\hbox{\hskip 1.5cm}$determine~\alpha_{\pi_{\sigma,i}}~
+(for~all~relevant~i)$\\
+\vbox{\vskip 0.5cm}
+\hbox{\hskip 1cm}$construct~and~return~\psi_1~as~defined~above$
+
+so the algorithm presented above allows us to algorithmically
+reconstruct elements of one type as elements of another.
+
+\subsection{Existence of the coercion}
+\label{DoyeSec7.5}
+
+Before we prove that the automated coercion algorithm constructs a
+coercion when one exists we must prove that it does not create some
+unnatural function when no coercion exists.
+
+We will use the terminology of algorithm \ref{Doye7.4.1} in this
+section.
+
+In the simplest case, some of the functions will not exist in the
+target type and the algorithm will error at an early stage. This will
+be because there is no
+$\langle\langle\Delta,\mathcal{D}\rangle,\mathcal{D}\rangle$ which
+both $\langle A,\alpha\rangle$ and $\langle B,\beta\rangle$ model.
+
+If a homomorphism exists but not a coercion then this means that there
+exists an extension of
+$\langle\langle\Delta,\mathcal{D}\rangle,\mathcal{D}\rangle$ which
+both $\langle A,\alpha\rangle$ and $\langle B,\beta\rangle$ model. In
+this case the algorithm will error at an early stage.
+
+If all the constructors of $\langle A,\alpha\rangle$ are available in
+$\langle B,\beta\rangle$ but no homomorphism (coercion) exists then
+this could be because of (at least one of) the following causes.
+
+\subsubsection{One of the coercions to be used does not exist}
+
+At least one of the types which is required for construction or
+recursively required for construction (and which is not the carrier of
+the principal sort) may not be coercible to its counterpart in the
+target. Provided the algorithm checks at construction time that every
+coercion used directly or indirectly by $\psi_i$ exists (or is
+constructible) then we may report an error at an early stage.
+
+\subsubsection{Nonhomomorphic constructors}
+
+The fact that $\langle\langle\Sigma,S\rangle,S\rangle$ is a protecting
+extension of
+$\langle\langle\Delta,\mathcal{D}\rangle,\mathcal{D}\rangle$ and that
+all secondary constructor equations hold in
+$\langle\langle\Sigma,\mathcal{S}\rangle,\mathcal{S}\rangle$
+guarantees that these equations hold in
+$\langle\langle\Delta,\mathcal{D}\rangle,\mathcal{D}\rangle$
+and hence in $\langle B,\beta\rangle$.
+
+This not only ensures that the order of the lines in $\phi_1$ is
+unimportant but also that if a certain relationship holds in
+$\langle A,\alpha\rangle$ it {\sl must} hold in
+$\langle B,\beta\rangle$.
+
+For example, if someone defines that all finite field algebras are
+constructed by {\bf 0} and {\bf succ} (the successor function) the
+automated coercion algorithm will not attempt to create the
+``coercion'' $\mathbb{Z}_5\rightarrow\mathbb{Z}_3$. This is because
+there exists a secondary constructor equation in the theory of finite
+fields of size $n$.
+
+\[{\bf succ^n(0)=0}\]
+
+So in this example
+$\langle A,\alpha\rangle=\mathbb{Z}_5$ and
+$\langle B,\beta\rangle=\mathbb{Z}_3$. The equation
+${\rm succ}^5(0)=0$ holds in the theory of finite fields of size 5.
+$\mathbb{Z}_5$ is obviously a model for this theory.
+
+This equation is not true in any theory which the above theory extends
+and of which $\mathbb{Z}_3$ is a model. Otherwise the equation would
+hold in $\mathbb{Z}_3$ and that patently is not true.
+
+Thus the automated coercion algorithm will error at any early stage
+from not being able to find
+$\langle\langle\Delta,\mathcal{D}\rangle,\mathcal{D}\rangle$.
+
+\subsection{Proving homomorphicity and coerciveness}
+\label{DoyeSec7.6}
+We now make some notational definitions so that we may prove the final
+result of the section. That is, we will show that algorithm
+\ref{Doye7.4.1} constructs a homomorphism (theorem \ref{Doye7.6.7})
+which is a coercion (corollary \ref{Doye7.6.8}).
+
+Recall notation \ref{Doye4.2.10}. Thus for any constructor symbol
+$\sigma_{n,q,S_1}$ the associated constructor function in
+$\langle A,\alpha\rangle$ is $\alpha_{\sigma_{n,q,S_1}}$ the query
+function is $\alpha_{\chi_{\sigma_{n,q,S_1}}}$ and for
+$i\in\{1,\ldots,n\}$ the part function
+$\alpha_{\pi_{\sigma_{n,q,S_1},i}}$
+
+\begin{DoyeDefinition}
+\label{Doye7.6.1}
+For a term $t$ in a term algebra $T_\Sigma(X)$ if
+\begin{enumerate}
+\item $t\in X_s~then~{\rm length}(t)=1$\\
+\item $t\in\Sigma_{0,(),s}~then~{\rm length}(t)=1$\\
+\item $t=\sigma(t_1,\ldots,t_n)~then~
+{\rm length}(t)=1+{\rm length}(t_1)+\cdots+{\rm length}(t_n)$
+\end{enumerate}
+\end{DoyeDefinition}
+
+The definition of length of an element will form the basis of our
+inductive proof of the automated coercion algorithm. However, in
+general, we will not be dealing with term algebras but their
+homomorphic images.
+
+\begin{DoyeDefinition}
+\label{Doye7.6.2}
+Let $x$ an element of a $\Sigma$algebra, we define
+\[{\rm length}(x):={\rm min}\{t\in T_\Sigma(X)~\vert~
+\theta^*(t)=x\}\]
+where $\theta^*$ is the unique homomorphism given in the first
+universality theorem \ref{Doye4.4.7}.
+\end{DoyeDefinition}
+
+\begin{DoyeAssumption}
+\label{Doye7.6.3}
+If one of the part functions
+$\alpha_{\pi_{\sigma_{n,q,S_1},i}}$ corresponds to
+$\alpha_{\sigma_1,(S_1),S_1}$ (thus $q_i=S_1$) then we demand that
+\[(\forall t\in T_\Xi(X)_1)({\rm length}(
+\alpha_{\pi_{\sigma_{n,q,S_1},i}}(\theta^*(t)))<
+{\rm length}(\theta^*(t)))\]
+where $\theta^*$ is the unique homomorphism given in the first
+universality theorem \ref{Doye4.4.7}
+\end{DoyeAssumption}
+
+A couple to technical definitions make the next assumption easier
+to understand.
+
+\begin{DoyeDefinition}
+\label{Doye7.6.4}
+Suppose $\langle A,\alpha\rangle$ is a constructed algebra,
+constructed by the $S$sorted signature $\Sigma$. If for any
+$\i\in\{2,\ldots,\vert S\vert\}$ we have that $S_i$ appears in the
+arity of any of the constructors of $\Sigma$, we say that $A_i$ is
+required for construction by $A_1$.
+\end{DoyeDefinition}
+
+So far example, in {\bf List(Integer)} we have that {\bf Integer} is
+required for construction since it is an argument of {\bf
+cons}. Notice that {\bf List(Integer)} is not required for consruction
+itself since it is the carrier of $S_1$.
+
+\begin{DoyeDefinition}
+\label{Doye7.6.5}
+Suppose $\langle A,\alpha\rangle$ is a constructed algebra,
+constructed by the $S$sorted signautre $\Sigma$. Let $A_i$ be
+required for construction by $A_1$. Now consider $A_i$ as the carrier
+of the principal sort of $\langle B,\beta\rangle$, a constructed
+algebra.
+
+If $B_j$ is required for construction by $B_1=A_i$ (hence $j\ne 1$)
+then we say that $B_j$ is {\rm recursively required for construction} by
+$A_1$.
+
+Now suppose that the carrier $D_1$ of the principal sort of a
+constructed algebra $\langle D,\delta\rangle$ is recursively required
+for construction by $A_1$. If $D_k$ is required for construction by
+$D_1$, then we also say that $D_k$ is {\rm recursively required for
+construction} by $A_1$.
+\end{DoyeDefinition}
+
+So for example in {\bf List(List(Integer))}, the only type which is
+required for construction is {\bf List(Integer)} since this is the
+only argument of {\bf cons} which is not the carrier of the principal
+sort, {\bf List(List(Integer))}.
+
+Thus the only types which are recursively required for construction
+are {\bf List(Integer)} and the types which are recursively required
+for construction by {\bf List(Integer)}.
+
+Since {\bf Integer} is the only type required for construction by
+{\bf List(Integer)} it is the only type recurively required for
+construction by {\bf List(Integer)}.
+
+Thus the types which are recurively required for construction by
+{\bf List(List(Integer))} are {\bf List(Integer)} and {\bf Integer}.
+
+The following assumption is required so that we may prove that the
+automated coercion algorithm terminates.
+
+\begin{DoyeAssumption}
+\label{Doye7.6.6}
+We demand that $A_1$ is not recursively required for construction.
+\end{DoyeAssumption}
+
+\begin{DoyeTheorem}
+\label{Doye7.6.7}
+Let $\langle\langle\Sigma,S\rangle,S\rangle$ be an algorithmically
+reconstructible theory which is a protecting extension of the theory
+$\langle\langle\Xi,X\rangle,X\rangle$ such that
+$\Sigma^C\subseteq\overset{..}{\Xi}$.
+
+Let $\langle B,\beta\rangle$ be a model for
+$\langle\langle\Xi,X\rangle,X\rangle$ and $\langle A,\alpha\rangle$ be
+a model for $\langle\langle\Sigma,S\rangle,S\rangle$.
+
+Then the function $\psi$ given in algorithm \ref{Doye7.4.1} is a
+$\Xi$homomorphism
+$\langle A,\alpha\rangle\rightarrow\langle B,\beta\rangle$
+\end{DoyeTheorem}
+
+PROOF:
+
+Let $\phi$ be the correct homomorphism which $\psi$ is attempting to
+emulate.
+
+Since $\psi_1$ contains finitely many cases, and covers all cases of
+construcctors for $\Sigma$, we need only consider one line from
+$\psi_1$. Also by induction on ${\rm com}(t)$ we can assume that\\
+$(\forall i \in \{2,\ldots,\vert S\vert\})(\psi_i=\phi_i)$
+
+Since $\psi_1$ covers all cases of constructor for $\Sigma$ we do not
+need to consider the error line since it will never be reached.
+
+For $\psi_1$ we may induct on length, and we are in good shape by
+assumption \ref{Doye7.6.3} (on length) and \ref{Doye7.6.6} (on the
+interaction between length and com).
+
+Here is one line from $\psi_1$
+\[(if~(\alpha_{\sigma_q} ~a)~(\beta_{\sigma_c}
+~(\psi_{c_1} ~(\alpha_{p_1} ~a)) \ldots
+(\psi_{c_n} ~(\alpha_{p_n} ~a))))\]
+Now, assuming $(\alpha_{\sigma_q} ~a)$, we know that,
+\[(\phi_1 ~a)=(\phi_1 ~(\alpha_{\sigma_c}
+~(\alpha_{p_1} ~a)\ldots(\alpha_{p_n} ~a)))\]
+then since $\phi$ is a $\Sigma$homomorphism
+\[(\phi_1 ~(\alpha_{\sigma_c} ~(\alpha_{p_1} ~a)\ldots
+(\alpha_{p_n} ~a)))=
+(\beta_{\sigma_c} ~(\phi_{c_1} ~(\alpha_{p_1} ~a)\ldots
+(\phi_{c_n} ~(\alpha_{p_n} ~a)))\]
+Now we know that, by our induction argument
+\[(\beta_{\sigma_c} ~(\phi_{c_1} ~(\alpha_{p_1} ~a)) \ldots
+(\phi_{c_n} ~(\alpha_{p_n} ~a))) =
+(\beta_{\sigma_c} ~(\psi_{c_1} ~(\alpha_{p_1} ~a))\ldots
+(\psi_{c_n} ~(\alpha_{p_n} ~a)))\]
+whence for this line, and therefore every line and the entire function\\
+$(\psi_1 ~a)=(\phi ~a)$. So by induction, $\psi=\phi$ and thus $\psi$ is
+a homomorphism.\QED
+
+Now by adding one extra condition, we may prove that the automated
+coercion algorithm generates coercions in the sense of definition
+\ref{Doye5.5.2}.
+
+\begin{DoyeCorollary}
+\label{Doye7.6.8}
+Let $\langle\langle\Sigma,S\rangle,S\rangle$ be an algorithmically
+reconstructible theory which is a protecting extension of the theory
+$\langle\langle\Xi,X\rangle,X\rangle$ such that
+$\Sigma^C\subseteq\overset{..}{\Xi}$
+
+Let $\langle B,\beta\rangle$ be a model for
+$\langle\langle\Xi,X\rangle,X\rangle$ and $\langle A,\alpha\rangle$
+be a model for $\langle\langle\Sigma,S\rangle,S\rangle$ such that there
+does not exist any extension of
+$\langle\langle\Xi,X\rangle,X\rangle$ which both
+$\langle A,\alpha\rangle$ and $\langle B,\beta\rangle$ model.
+
+Then the function $\psi$ given in algorithm \ref{Doye7.4.1} is a
+coercion $\langle A,\alpha\rangle\rightarrow
+\langle B,\beta\rangle$
+\end{DoyeCorollary}
+
+PROOF: No other theories extend
+$\langle\langle\Xi,X\rangle,X\rangle$ which both
+$\langle A,\alpha\rangle$ and $\langle B,\beta\rangle$ model so the
+only thing which could stop $\psi$ being a coercion would be for there
+to exist a theory which both $\langle A,\alpha\rangle$ and
+$\langle B,\beta\rangle$ were to model which was not extended by
+$\langle\langle\Xi,X\rangle,X\rangle$.
+
+So, suppose (for a contradiction) $\langle A,\alpha\rangle$ and
+$\langle B,\beta\rangle$ were to model a theory $\Omega$ which
+$\langle\langle\Xi,X\rangle,X\rangle$ does not extend, then we may
+manufacture a new theory containing all the sorts, operator symbols,
+and equations of both theories.
+
+We may have some duplication of sorts and operators, so this
+manufacturing process would need to be performed
+intelligently. Explicitly, $\Omega$ and
+$\langle\langle\Xi,X\rangle,X\rangle$ may both be extensions of some
+theory $\Theta$. We might (but not always\footnote{The theory of rings
+inherits from the theory of monoids twice}) only wish our manufactured
+theory to contain the sorts, operator symbols, and equations
+$\Theta$ once, not twice.
+
+This new theory would clearly extend
+$\langle\langle\Xi,X\rangle,X\rangle$ and $\langle A,\alpha\rangle$
+and $\langle B,\beta\rangle$ would both model this new theory. Hence
+we have a contradiction and such an $\Omega$ can not exist.
+
+So $\langle\langle\Xi,X\rangle,X\rangle$ must specify the unique
+``smallest'' variety to which both $\langle A,\alpha\rangle$ and
+$\langle B,\beta\rangle$ belong. We already know by theorem
+\ref{Doye7.6.7} that $\psi$ is a $\Xi$homomorphism; by definition
+\ref{Doye5.5.2} it must be a coercion.
+
+This is why algorithm \ref{Doye7.4.1} looks for
+$\langle\langle\Delta,\mathcal{D}\rangle,\mathcal{D}\rangle$, since it
+must specify the smallest variety to which both
+$\langle A,\alpha\rangle$ and $\langle B,\beta\rangle$ belong.
+
+\subsection{Conclusion}
+\label{DoyeSec7.7}
+
+In conclusion, we have shown that it is possible to create a
+homomorphism between two types from an important subset of types.
+
+Moreover, this homomorphism may be constructed algorithmically and
+hence the general construction of homomorphisms is implementable on a
+computer.
+
+Furthermore, if the type system adheres to all the assumptions made,
+and the homomorphism is from the theory which specifies the smallest
+variety to which both types belong, then it is the unique
+{\sl coercion} between the two types.
+
+\section{Implementation Details}
+\label{DoyeChap8}
+
+The basic design was as follows. To perform a coercion from a
+{\bf Domain A} to a {\bf Domain B}, one needs to be able to ascertain
+which constants, queries, constructors, and part functions are
+available to both {\bf A} and {\bf B}. These functions should all come
+from the same algorithmically reconstructible theory
+({\bf Category}).
+
+The automated coercion function should be created and then compiled
+and stored away ready for fast access in case of future use. Such
+items are called ``cached lambdas'' or ``clams'', for short, and are
+already part of the Axiom system. Thus this was implemented.
+
+The automated coercion function should be integrated with the current
+coercion mechanism in Axiom. This was done by inserting the relevant
+line at the correct point of the function {\bf coerceInteractive}.
+
+\subsection{Labelling operstors}
+\label{DoyeSec8.4}
+
+We had to decide on a mechanism to mark which operators were
+constructors, part functions, etc.
+
+One method would have been to create subtypes of the Axiom
+{\bf Domain}, {\bf Mapping}, which would have been infeasible,
+requiring much rewriting of Spad compilers. This is also true of the
+method given in a later section.
+
+A Spad {\bf Domain} contains the following parts:
+\begin{enumerate}
+\item the name of the type constructor
+\item a (variable name, {\bf Category}) pair\footnote{Occasionally a
+(variable name, {\bf Domain}) pair. For example,
+{\bf IntegerMod(p:PositiveInteger)}} for each\footnote{This is not the
+same as all the sorts of the signature. One may declare extra unused
+sorts. Also we may declare a function where the source of the target
+may contain a ground type. For example, functions which return a
+booleanlike type are usually declared to return {\bf Boolean} rather
+than a pair where the {\bf Category} is the {\bf Category} of
+booleanlike types.} of the parameters of the type constructor
+\item a {\bf Category} or {\bf Join} (intersection) of
+{\bf Categories} to which the {\bf Domain} belongs
+\item a list of additional operator symbols (functions) for the type
+\item a list of methods for (some of or all) the operator symbols of
+the type
+\end{enumerate}
+
+Every operator symbol definition in a {\bf Domain} or {\bf Category}
+(and hence available in a {\bf Domain} of that {\bf Category}) has a
+certain number of special comments called $++$ comments.
+
+These $++$ comments (as opposed to ordinary comments in most languages
+and Axiom's other style of comments, $$ comments) are parsed by the
+compiler to produce the documentation for Axiom's sophisticated
+online help system, {\bf HyperDoc}. ({\bf HyperDoc} was one of the
+first hypertext systems.)
+
+This parsing of the $++$ comments allowed us to enter special keywords
+for each special function which were read and stored at compile time
+for each {\bf Domain}. We could then read them at runtime using the
+Axiom interpreter's built in $++$ comments reader.
+
+\subsection{Getting information from domains}
+\label{DoyeSec8.5}
+The $++$ comments were gathered for a {\bf Domain} by recursion up the
+{\bf Category} inheritance lattice, using the {\bf GETDATABASE}
+function. We asked the database for all the documentation for each
+{\bf Category}, and then asking which {\bf Categories} it
+extended. The documentation includes all the functions and their
+respective $++$ comments. This allowed the automated searching for
+keywords, and hence, the special functions of a {\bf Domain}.
+
+Note that we only needed the comments for functions (operator symbols)
+declared in a {\bf Category}. Functions declared in {\bf Domains} are
+of no interest to the automated coercion algorithm. This is because
+these do not correspond to any of the special functions (constructors,
+part functions, or queries) of a signature or theory.
+
+The keywords were checked quite simply, being members of the
+following list:
+\[{\bf list('"constant",'"constructor",'"part",'"query")}\]
+Part number checking was only slightly more difficult with each number
+having to be converted from a (Lisp) string to a (Lisp) integer. A
+restriction was placed on queries that they must be called the same as
+their associated constant (or constructor), but with a "?"
+appended. This restriction was not necessary and could have been
+worked around easily.
+
+The special function lists from both {\bf Domain}s were compared and
+the required functions were extracted from both.
+
+\subsection{Checking information from domains}
+\label{DoyeSec8.6}
+
+For each special function, a check was performed to see whether that
+function was really available in the {\bf Domain}.
+
+The envisaged problem was that Axiom's {\bf Categories} can be
+conditional: that is to say, some function definitions only exist if
+certain relationships hold for {\bf Category}'s parameters.
+
+{\bf GETDATABASE} ignores the parameters to a {\bf Category} and
+returns all the functions which may be exported by a {\bf Domain} of
+that {\bf Category}. Hence, the extra check was necessary to ensure
+that the automated coercion function did not try to include these
+unavailable functions.
+
+Thus the homomorphism created by the automated coercion algorithm was
+always equivalent to definition of a conditional homomorphism given in
+section \ref{DoyeSec5.3}.
+
+\subsection{Flaws in the implementation}
+\label{DoyeSec8.7}
+
+The implementation was originally envisaged as a fully working piece
+of code of production standard and hence shippable with a commercial
+release of Axiom. For various reasons outlined below, only a working
+prototype was implemented.
+
+Deliberate restrictions placed by the author on the deisgn were:
+\begin{enumerate}
+\item Query function names were restricted to be the name of their
+associated constant function with a "?" appended.
+\item The number of (non 0ary) constructors was limited to one
+\item Recursion through {\bf coerceInteractive} was achieved using a
+na\"ive means
+\item Neither the existence of
+$\langle\langle\Sigma,S\rangle,S\rangle$ nor
+$\langle\langle\Delta,\mathcal{D}\rangle,\mathcal{D}\rangle$ were
+checked. (See algorithm \ref{Doye7.4.1} for the meaning of these).
+\end{enumerate}
+
+Both the first two items could have easily been worked around but
+would have required a more complex $++$ comment reader. This was
+considered to be a minor detail, which would have required too much
+implementation time.
+
+The third item was more problematic. Attempts were made to remedy this
+situation. However, the depth of knowledge needed to implement this
+correctly would have required too much time to learn. This was the
+main factor in the downgrading of the implementation to mere prototype
+status.
+
+The method to work around the complexities of Axiom's evaluation loop
+was to add a (Spad) {\bf Package} which exported a function which then
+called the Lisp function. The code for this
+{\bf Package} (called {\bf NCoerce}) follows.
+
+$$\%~{\bf Coercion~Package}\\
+{\bf )abbrev package NCOERCE NCoerce}
+
+{\bf NCoerce(Source:Type,Target:Type):Exports $==$
+Implementation where}
+
+{\bf\quad Exports $==>$ with}
+
+{\bf\quad\quad nCoerce: Source $>$ Target}
+
+{\bf\quad Implementation $==>$ add}
+
+{\bf\quad\quad nCoerce(x:Source):Target $==$}\\
+\vskip 0.6cm
+{\bf\quad\quad\quad nCreateCoerce(x,Source,Target)\$Lisp}
+
+To call a function from a {\bf Package} is relatively easy.
+
+The function ({\bf nCoerce} above) then uses the Axiom
+{\bf \$Lisp} syntax for calling a function.
+
+One item is a bit more difficult to solve. The existence of
+$\langle\langle\Sigma,S\rangle,S\rangle$ is implicit if a
+{\bf Domain} has special functions. It would also be possible to check
+if both source and target are members of a common {\bf Category}
+(using {\bf GETDATABASE}). It would even be possible to check that all
+the constructors of the source are from this {\bf Category}. Finally,
+it would be possible to ensure that this is the smallest such
+{\bf Category}.
+
+However, it would be most problematical to determine whether
+$\langle\langle\Sigma,S\rangle,S\rangle$ is a protecting extension of
+$\langle\langle\Delta,\mathcal{D}\rangle,\mathcal{D}\rangle$ or not.
+
+This is a more general problem than one which just applies to the
+automated coercion algorithm. This is due to the fact that Axiom
+believes everything that you say. One may produce a {\bf Category} and
+claim that it extends another. Yet if Axiom's {\bf Categories} were
+really varieties, specified by theories there would need to be some
+way of checking whether the equations in the original {\bf Category}
+still held in the new one. Similarly, {\bf Domains} need not model the
+theory specifing the variety ({\bf Category}) to which they have been
+declared to belong.
+
+The current situation in automated theorem proving means that Axiom
+will believe any false assertions like those mentioned in the previous
+paragraph. This is not a design flaw of either Axiom or the automated
+coercion algorithm; neither Axiom's designers nor I had any choice 
+automated theorem proving has not yet advanced sufficiently for us to
+take advantage of it. Similarly (and moreover) Axiom will believe that
+any function (which one may implement) called {\bf coerce} is a valid
+coercion.
+
+This means that in this implementation of the automated coercion
+algorithm in the current release of Axiom, it would be possible to
+create new ``coercions'' between (potentially) unrelated types or
+nonhomomorphically between similar types. Using the example from
+section \ref{DoyeSec7.5} we could create a ``coercion''
+$\mathbb{Z}_5\rightarrow\mathbb{Z}_3$
+
+The present state of automated theorem proving technology with special
+reference to Axiom is detailed in \cite{Mart97}. This paper details
+recent research and nearfuture directions for the subject.
+
+Other flaws which will be dealt with next including:
+\begin{enumerate}
+\item Some Axiom {\bf Categories} do not agree with our notion of
+varieties (specified by signatures or theories) (Sections
+\ref{DoyeSec9.2}, \ref{DoyeSec9.4}, \ref{DoyeSec9.5})
+\item Axiom {\bf Domains} have too much in common with their
+{\bf Categories}. There is a lack of distinction between operator
+symbols and operators. Similarly between sorts and carriers
+(Sections \ref{DoyeSec9.3}, \ref{DoyeSec9.6})
+\end{enumerate}
+
+\subsection{Conclusion}
+\label{DoyeSec8.8}
+
+We conclude that the automated coercion algorithm is probably
+implementable in the Axiom interpreter. It is certainly possible to
+create a version which works. However, it would take someone with
+deeper knowledge of the code to force a complete integration of the
+current implementation with the Axiom interpretation.
+
+\section{Making Axiom algebraically correct}
+\label{DoyeChap9}
+
+We will discuss various details which need to be changed to make a
+computer algebra system more ``algebraically correct''. By this we
+mean that Axiom's {\bf Categories} behave more like our concept of
+varieties (specified by ordersorted theories) and that the
+{\bf Domains} act more like our notion of ordersorted algebras more
+correctly.
+
+\subsection{Explicitly defined theories}
+\label{DoyeSec9.2}
+
+In Axiom, the {\bf Categories} were originally intended to be akin to
+varieties specified by signatures. The {\bf Domains} were then meant
+to be like algebras of those signatures.
+
+The {\bf Categories} do behave and look to the casual observer like
+they were specified by multisorted algebraic type theories, but there
+are some clear differences.
+
+\subsection{Operator symbols and names}
+\label{DoyeSec9.3}
+
+In Axiom, if a category defines an operator symbol
+$\sigma_{n,q,s}$ then for all domains in that category, that operator
+name $\alpha_{n,q,s}$ of $\sigma_{n,q,s}$ will be $\sigma_{n,q,s}$.
+
+It may appear to be not that much of a disadvantage to have such a
+restriction on operator names, but an important case in mind is that
+of the monoid. A ring, has two binary operators over which it forms a
+monoid. The only way in Axiom that we can ensure this is to have two
+different monoidal categories. A distinct disadvantage.
+
+If we allowed operator symbols to differ from operator names then
+another {\bf Category} could extend {\bf Monoid} in two different
+ways.
+
+Syntactically this would be most difficult. We would need a way of
+declaring the two operator symbols in {\bf Ring} (traditionally $+$
+and $*$) as being from different operator symbols in {\bf Group}
+(which extends {\bf Monoid}) and {\bf Monoid}.
+
+For example we could write something like the following
+
+{\bf Ring:Category $==$ with (M:Monoid, G:Group)}
+
+{\bf\quad $$ Operators from Monoid}\\
+\vskip 0.5cm
+{\bf\quad $*$: ($*$:(\%,\%) $>$ \%)\$M}\\
+\vskip 0.5cm
+{\bf\quad 1: (1:() $>$ \%)\$M}\\
+
+{\bf\quad $$ Operators from Group}\\
+\vskip 0.5cm
+{\bf\quad $+$: ($*$:(\%,\%) $>$ \%)\$G}\\
+\vskip 0.5cm
+{\bf\quad 0: (1:() $>$ \%)\$G}\\
+\vskip 0.5cm
+{\bf\quad inv: (inv:\% $>$ \%)\$G}\\
+\vskip 0.5cm
+$\ldots$
+
+This would identify $*$ and 1 with the binary operator and identity
+element, respectively, from {\bf Monoid}. Whereas $+$, 0, and
+{\bf inv} would be identified with the binary operator, identity
+element, and inverse function from {\bf Group}.
+
+Notice that both the operator symbol (e.g. $*$) and both the source
+arity (e.g. (\%,\%)) and target (e.g. \%) sort are needed to uniquely
+identify the operator. These correspond to $\sigma$, $q$ and $s$
+respectively. (we do not need to know $n$ since this is deducible from
+$1$).
+
+A function in Axiom (in either a {\bf Domain} or {\bf Category}) is
+currently represented by ({\bf name} ({\bf target} {\bf source})
+{\bf comments}). Function declarations in {\bf Categories} are
+normally of the form\footnote{$s$ and $q$ are reversed in Axiom's
+internal representation of a function.}
+\[(\sigma~(s~q)~ {\bf comments})\]
+and once exported by a ground type (i.e. genuine Axiom
+{\bf Domain} with all parameters to the {\bf Domain} fixed) it becomes
+\[(\alpha_{n,q,s,\sigma}~(A^s~A^q)~{\bf comments})\]
+where $\alpha_{n,q,s,\sigma}=\sigma$.
+
+For the coercion algorithm, we inserted special words in the comments
+field to try and mimic an operator symbol.
+
+Another approach might have been to declare other types e.g.
+{\bf Constructor(a,b)} which are subtypes of {\bf Mapping(a,b)}.
+
+A far better approach is to extend the information contained within
+the function construct. For initial definitions in {\bf Categories} 
+that is new operators which have come from this {\bf Category}, not
+ones which this {\bf Category} may extend  then the current
+declaration method suffices.
+
+However, as in the above {\bf Ring} example for {\bf Categories} which
+extend others then a better method may be
+\[(\sigma^\prime~(\sigma~(s~q)~\Sigma)~{\bf comments}\]
+where $\sigma^\prime$ is the new operator symbol corresponding to
+$\sigma$ a member of $\Sigma_{n,q,s}$ where this signature extends
+$\Sigma$.
+
+We have used variable names to avoid confusion. One may wish to define
+a {\bf Category} called {\bf DoubleMonoid} where {\bf G} is a
+{\bf Monoid} instead of a {\bf Group}. (Obviously no {\bf inv}
+operator would be available to such a {\bf Category}.)
+
+The same terminology could also be used to define specific algebras
+({\bf Domains}). For example, for all $n$ in $\mathbb{N}$,
+$n\mathbb{Z}$ (whose elements is the set
+$\{nz~\vert~z\in\mathbb{Z}\})$ is an additive group, whereas
+$S(n)$ (the symmetric group on $n$ elements) is usually considered to
+be a multiplicative group.
+
+So, for $n\mathbb{Z}$ we might write
+
+{\bf IntegersTimes(n:PositiveInteger):Group $==$}\\
+
+{\bf $+$ : ($*$ : (\%,\%) $>$ \%)}\\
+\vskip 0.5cm
+{\bf 0 : (1 : () $>$ \%)}\\
+\vskip 0.5cm
+{\bf  : (inv : \% $>$ \%)}\\
+\vskip 0.5cm
+\ldots
+
+However for $S(n)$ we might write:
+
+{\bf Symmetricgroup(n:PositiveInteger):Group $==$}\\
+
+{\bf $*$ : ($*$ : (\%,\%) $>$ \%)}\\
+\vskip 0.5cm
+{\bf () : (1 : () $>$ \%)}\\
+\vskip 0.5cm
+{\bf inv : (inv : \% $>$ \%)}\\
+\vskip 0.5cm
+\ldots
+
+In this example we can see the following proposed methodology for
+declaring operator names which correspond to operator symbols.
+\[(\alpha_{n,q,s,\sigma}~(\sigma~(s~q))~{\bf comments})\]
+
+The signature $\Sigma$ does not need to be mentioned in each function
+definition since the algebra is only declared to be a model of one
+signature.
+
+This does create more ``unnecessary'' confusion for
+{\bf Domain/Category} writers, but correctness should overrule
+easeofuse. It is also conceivable that this will have a negative
+effect on the amount of time it takes to compile a {\bf
+Domain}. However, this is true of all typechecking compilers.
+
+More inportantly, it should not have any effect on runtime speed of
+execution. This should definitely be the case if the internal
+representation is moved to something approximating Axiom's current
+order.
+\[(\alpha_{n,q,s,\sigma}~(s~q)~\sigma~{\bf comments})\]
+
+This puts the target and source closer (and less operations away) from
+being discovered.
+
+Clearly, in this proposed methodology the carriers of the same source
+and target are not mentioned explicitly in the function
+representation.
+
+To speed up functiontype lookups (modemap selection) each
+{\bf Domain} could provide a hash of sorts and carriers. Indeed, then
+the internal representation could be
+\[(\alpha_{n,q,s,\sigma}~(A^s~A^q)~\sigma~{\bf comments})\]
+and then modemap selection would be as fast as in the current version
+of Axiom, but the hash could be used (going in the other direction) to
+determine $s$ and $q$ for the automated coercion algorithm.
+
+\subsection{Moving certain operators}
+\label{DoyeSec9.4}
+
+Another factor which stops Axiom acting totally homomorphically, is
+that certain operators appear in {\bf Categories} too far ``up'' the
+inheritance lattice. This is best illustrated by an example.
+
+In Axiom, one often would like to be able to convert {\bf Lists} to
+{\bf Sets}. (The {\bf Domain} whose items are finite sets (or
+actually, sometimes classes), over some particular type is called
+{\bf Set} in Axiom.)
+
+{\bf Sets} and {\bf Lists} in Axiom are both certainly finite
+collections which can be built by adding in another element at a
+time. In {\bf List} this may be achieved using either {\bf cons} or
+{\bf append} (though obviously, {\bf cons} is far more efficient)
+whereas {\bf Sets} can be built using the (sometimes noneffective)
+command {\bf insert}\footnote{This operation inserts a (potentially)
+new element into a set. ${\bf insert}(x,s)=s\cup\{x\}=s;x$}.
+
+Axiom knows that {\bf Lists} are sorted whereas {\bf Sets} are
+not. The problem, which is immediately obvious, is that adding in a
+new element to a {\bf List} will always increase the length of the
+{\bf List}. This is not true of (Axiom's finite) {\bf Sets}. They both
+however get the same elementcountingoperator from the same
+{\bf Category}. This function, $\#$ comes from the {\bf Category},
+{\bf Aggregate}, which is the most general type of ``collection'' in
+Axiom.
+
+{\bf List(S)} (for some fixed {\bf S}) is a model of
+{\bf ListAggregate} and {\bf Set(S)} is a model of
+{\bf FiniteSetAggregate}. Both of these theories are extensions of the
+theory {\bf Aggregate}.
+
+Therefore if we had a homomorphism, $\phi$ from {\bf Lists} to
+{\bf Sets}, then the following equation should hold, yet it clearly
+does not,
+\[\phi(\#([1,1]))=\#(\phi([1,1]))\]
+since the left hand side is,
+\[\phi(2)=2\]
+and the right hand side is,
+\[\#(\{1\})=1\]
+and unless the carrier sort of collection length is not
+{\bf NonNegativeInteger} but a different type, one in which all
+elements are equal, we will not be able to create any homomorphisms
+from {\bf List} to {\bf Set}.
+
+In section \ref{DoyeSec7.3} we demanded that if the automated coercion
+algorithm was to be applicable (in this case) from {\bf List(S)} to
+{\bf Set(S)} then {\bf ListAggregate} would need to be a protecting
+extension of {\bf Aggregate}\footnote{Or an extension of
+{\bf Aggregate} which both {\bf ListAggregate} and
+{\bf FiniteSetAggregate} extends.}.
+
+It is clear that in {\bf ListAggregate} the following equation holds
+\[\#({\bf cons}(a,b))=1+\#(b)\]
+
+If this were a protecting extension then this equation would hold in
+{\bf Aggregate}. However, as we have already observed.
+\[\#({\bf insert}(a,b)\ne 1+\#(b)\]
+when $a\in b$.
+
+Thus {\bf ListAggregate} is not a protecting extension of
+{\bf Aggregate} and the automated coercion algorithm can not be
+applied.
+
+There are three obvious solutions:
+\begin{enumerate}
+\item Disallow coercions from {\bf List} to {\bf Set}. Although we
+would still allow a nonhomomorphic {\bf convert} operator
+\item Move the elementcountingoperation further down the
+{\bf Category} inheritance lattice until it does not appear in any
+{\bf Categories} to which {\sl both} {\bf List} and {\bf Set}
+belong. Or if they do both belong to this {\bf Category}, ensure that
+none of the part functions, constants, queries, or constructors are
+from this {\bf Category} or any of its ancestors.
+\item Move the addingnewelementoperation further down the lattice,
+in a similar manner. Thus {\bf cons} and {\bf insert} would not know
+anything about each other. In this case the automated coercion
+algorithm would still not be applicable
+\end{enumerate}
+
+This is merely one example of many such operators which could require
+moving.
+
+\subsection{Retyping certain sorts}
+\label{DoyeSec9.5}
+
+As in section \ref{DoyeSec9.4}, this is best illustrated by an
+example.
+
+In Axiom, the {\bf Category}, {\bf Ring} exports a function,
+\[{\bf characteristic:~()~>~NonNegativeInteger}\]
+(remember that Axiom does not differentiate between sorts and
+carriers). So imagine the natural ringepimorphism
+$\phi:\mathbb{Z}_6\rightarrow\mathbb{Z}_2$. Then the following
+equation should hold,
+\[{\bf characteristic}(\phi())=\phi({\bf characteristic}())\]
+yet clearly this is not the case, since $\phi$ must send the
+{\bf Void} sort to {\bf Void}, and thus the left hand side must equal
+the characteristic of $\mathbb{Z}_2$, which is 2. Whereas, for the
+right hand side, we have $\phi(6)$. This $\phi$ is the natural map
+from $\mathbb{N}\cup\{0\}$ to itself. This is, of course, the identity
+map, and hence the right hand side has the value 6.
+
+There is clearly something very wrong here. There are two solutions,
+the first of which is highly unsatisfactory:
+\begin{enumerate}
+\item Stop {\bf characteristic} from being a function. One could
+persuade it to be an attribute of the {\bf Ring}.
+\item Alter the carrier of the return type of {\bf characteristic}
+from {\bf NonNegativeInteger} to being a type with the same elements,
+but a different idea of equality.
+\end{enumerate}
+
+This is one of many such cases in Axiom.
+
+\subsection{Sorts and their order}
+\label{DoyeSec9.6}
+
+We have been discussing Axiom's {\bf Category} inheritance system as
+if it were a true attempt at modelling ordersorted algebra. There
+are, however, two areas which are distinctly missing from the Axiom
+model; these are, the sorts and their order.
+
+There is a distinct confusion in Axiom between sorts and carriers. The
+author believes that all {\bf Category} definitions (the signatures or
+theories which specify varieties) should not use genuine types at any
+point in the signatures, or any other point. These should only occur
+in the {\bf Domains} of that {\bf Category}.
+
+For example, many {\bf Categories} assume that the only booleanlike
+type is {\bf Boolean}. Similarly the types {\bf NonNegativeInteger},
+{\bf PositiveInteger}, and {\bf Integer} are often ``assumed'' and are
+not parameters of a type.
+
+For the types {\bf Boolean}, {\bf NonNegativeInteger}, and
+{\bf PositiveInteger} this is not normally a complete
+disadvantage. There are not likely to be other algebras in our system
+which behave similarly enough to replace these types.
+
+However, there are coercions between {\bf NonNegativeInteger},
+{\bf PositiveInteger}, and {\bf Integer} (in the obvious
+directions). This then imposes some order on the sorts of the type
+which is not explicitly mentioned.
+
+Some of the sorts of an algebra are defined. \% is always the
+principal sort, and any parameters of the {\bf Category} are there,
+too. Others, however, are merely mentioned in function prototypes
+(signatures). All should be listed in a sortlist (and/or
+sortlattice, see below).
+
+Neglected sorts normally include those which are carried by the four
+types mentioned above. However, other types are often neglected
+too. These include {\bf List} which is often present so that elements
+of the type may be constructed. (The underlying representation of most
+types in a Lispbased system are often lists). More seriously,
+particular polynomial representations are sometimes present.
+
+There is no real mechanism built into Axiom to order the sorts of a
+signature ({\bf Category}). The order is implicit in
+{\bf Categorical} inheritances, such as {\bf CoercibleTo} and
+{\bf RetractibleTo}, which give information on how the principal sort
+relates to some other sorts.
+
+I believe that a more sensible way would be to declare a lattice like
+arrangement with the declaration of a {\bf Category}. Indeed, this
+would then make the sortlist clear, too, since this is never
+explicitly defined either.
+
+For example, we could add the syntax, {\bf SortOrder} to be used as
+follows,
+
+{\bf ACategory(a:A,b:B,$\ldots$):Category $==$}
+
+{\bf\quad with~SortOrder\{}\\
+\vskip 0.5cm
+{\bf\quad\quad a $<$ \%;}\\
+\vskip 0.5cm
+{\bf\quad\quad \% $<$ b;}\\
+\vskip 0.5cm
+{\bf\quad\quad $\ldots$}\\
+\vskip 0.5cm
+{\bf\quad \}}
+
+{\bf\quad exportedFunction : List A $>$ \%;}
+
+$\ldots$
+
+or (better), {\bf SortOrder} could be a {\bf Category} which could be
+defined as (assuming this is compilable\footnote{According to
+Peter Broadberry ``One problem is that it may not be possible for the
+compiler to figure out exactly what this construct will export'' but
+it might still be implementable.}),
+
+{\bf SortOrder(ls:List Pair Type):Category $==$ \{}
+
+{\bf\quad for pr in ls repeat \{}\\
+\vskip 0.5cm
+{\bf\quad\quad coerce:first pr $>$ second pr;}
+\vskip 0.2cm
+{\bf\quad \}}
+\vskip 0.2cm
+{\bf \}}
+
+This {\bf for} loop would not build the entire sort lattice for any
+particular category. This would be better done by the compiler at
+compile time, on a per{\bf Category} or per{\bf Type} basis.
+
+Thus, any {\bf Category} which does not extend {\bf SortOrder} would
+be a nonordersorted signature.
+
+\subsection{Altering Axiom's databases}
+\label{DoyeSec9.7}
+
+Axiom has many built in databases for looking up comments, functions,
+attributes, etc. from each {\bf Category} or {\bf Domain}. These are
+usually text files, with character number keys for faster
+crossreferencing.
+
+Axiom could have some extra
+databases to aid the automated coercion algorithm. Specifically, there
+could be a database containing for each {\bf Category}, a list (of
+lists) of special functions exported by that algebra, but not its
+ancestors. This could just be also be a compiled fact about each
+algebra, but the lookup overhead would be greater.
+
+The restriction on only having functions from that {\bf Category} and
+not its ancestors' special functions allows for the dynamic nature of
+Axiom's {\bf Category} system. Without this restriction, altering a
+{\bf Category} further up the lattice could cause the database
+information to become outdated for all of its descendants.
+
+\subsection{Conclusion}
+\label{DoyeSec9.8}
+
+Axiom behaves very similarly to a language based on order sorted
+theories and the algebras that model them. However, there are some key
+areas in which Axiom differs from the mathematical notions.
+
+We summarise these areas in the following table.
+
+\begin{tabular}{ p{6cm}  p{6cm} }
+\hline
+{\bf Mathematical Notion} & {\bf Axiom}\\
+\hline
+\vskip 0.05cm
+Operator names need not be the same as operator symbols
+\vskip 0.05cm
+&
+\vskip 0.05cm
+Operator names are always the same as operator symbols
+\vskip 0.05cm\\
+\hline
+\vskip 0.05cm
+Coercions are homomorphisms and hence act homomorphically on all operators
+\vskip 0.05cm
+&
+\vskip 0.05cm
+Coercions need not act like homomorphisms at all. (If it were
+possible to implement a universal equation checker then Axiom
+would be alright)
+\vskip 0.05cm\\
+\hline
+\vskip 0.05cm
+A signature depends on its sortlist, and hence a sortlist is part of
+its definition
+\vskip 0.05cm
+&
+\vskip 0.05cm
+Category definitions do not explicitly list their sorts
+\vskip 0.05cm\\
+\hline
+\vskip 0.05cm
+No algebra are mentioned in a signature definition, only sorts
+\vskip 0.05cm
+&
+\vskip 0.05cm
+Category definitions do depend on specific Domains
+\vskip 0.05cm\\
+\hline
+\vskip 0.05cm
+The order on the sorts is part of the definition of a signature
+\vskip 0.05cm
+&
+\vskip 0.05cm
+Category definitions do not explictly order their sorts
+\vskip 0.05cm\\
+\hline
+\end{tabular}
+
+We have presented methods for addressing all of these differences.
+
+\section{Conclusions}
+\label{DoyeChap10}
+
+\subsection{Summary}
+\label{DoyeSec10.2}
+
+\subsubsection{Category theory and order sorted algebras as the bases for
+sound strongly typed computer algebra systems}
+\label{Doye10.2.1}
+
+We have shown why both category theory and order sorted algebra both
+provide solid models for the type systems found in computer algebra.
+
+In section \ref{DoyeSec3.3} we have demonstrated
+the correlation between a computer algebra type system and category
+theory.
+
+In section \ref{DoyeSec4.7} and \ref{DoyeSec5.2} we have shown how a
+computer algebra type system correlates with order sorted algebra. In
+section \ref{DoyeSec5.3} we extended the notion of order sorted
+signatures to cover conditional signatures which occur in Axiom.
+
+We have mentioned some of the correspondence between category theory
+and order sorted algebra (section \ref{DoyeSec5.4}). We have usually
+used order sorted algebra as a model. This is because order sorted
+algebra more readily corresponds to the algebraic inheritance
+mechanism. This is mainly due to the order on the sorts which is not
+available in category theory. Also category theory has more difficulty
+expressing higher order polymorphism.
+
+\subsubsection{Representation and syntax issues of an order sorted
+algebra based type system}
+\label{Doye10.2.2}
+In section \ref{DoyeChap9} we demonstrated various methodologies for
+extending Axiom's current type system so that it may more closely
+model order sorted signatures and algebra.
+
+In section \ref{DoyeSec9.3} we showed how Axiom's syntax may be
+extended so that a signature may extend another more than
+once\footnote{Thus thsi solves an interesting class of multiple
+inheritance problem.}. We also showed that this syntax could be used
+to uniquely identify operator names with operator symbols. This then
+allows operator symbols to differ from operator names.
+
+In section \ref{DoyeSec9.6} we discussed how both the sort list and
+the order on the sorts could be introduced to Axiom's signatures.
+
+Section \ref{DoyeSec9.4} commented on how the
+Axiom signature tree may be altered to allow coercions to act more
+homomorphically.
+
+Finally, we discussed how Axiom signatures could be compiled to
+contain extra information which would enhance the speed of the
+automated coercion algorithm (section \ref{DoyeSec9.7}).
+
+\subsubsection{On coherence}
+\label{Doye10.2.3}
+
+In section \ref{DoyeChap6} we first stated all the mathematics used by
+Weber to state and ``prove'' Weber's coherence conjuecture
+\ref{Doye6.3.7}.
+
+In section \ref{DoyeSec6.4} we then showed that this ``proof'' is not
+correct. We showed that altering a definition and adding a couple new
+assumptions that let us prove the coercion theorem \ref{Doye6.4.7}.
+
+In section \ref{DoyeSec6.5} we then showed that it was possible to
+relax one of the assumptions which Weber made, and still have a
+coherent type system. (The extended coherence theorem \ref{Doye6.5.4})
+
+\subsubsection{The automated coercion algorithm}
+\label{Doye10.2.4}
+In section \ref{DoyeSec7.2}
+we provided enough mathematics to show that the automated coercion
+algorithm \ref{Doye7.4.1} (section \ref{DoyeSec7.4}) is an algorithm
+which returns a function which is not only a homomorphism, but a
+coercion which we defined in definition \ref{Doye5.5.2}.
+
+This homomorphism is unique in a coherent type system, which we can
+guarantee providing we can satisfy all the assumptions of the extended
+coercion theorem \ref{Doye6.5.4}. The homomorphism created may be
+built from the four basic types of coercion given in the statement of
+that theorem.
+
+In section \ref{DoyeChap8} we showed that a demonstration
+implementation of this algorith is possible in Axiom.
+
+\subsection{Future work and extensions}
+\label{DoyeSec10.3}
+We have presented in this thesis the basis for a mathematically sound
+computer algebra system. We have also shown that it would be possible
+to implement the automated coercion algorithm in such a system.
+
+At present Axiom comes close but is not fully conforming.
+
+We have shown how Axiom's syntax could be extended to allow it to
+model an order sorted algebra system.
+
+Axiom's categories are not always abstract  that is they may contain
+implementations of functions\footnote{The ``not equals'' fuction is
+defined to be ``not(equals())''}. This is a good thing as it enforces
+certain truths about a particular function.
+
+Forcing any important facts by making a class which implements a
+particular inferface would then ruin any chance of reattaining
+multiple inheritance.
+
\chapter{Finite Fields in Axiom (Grabmeier/Scheerhorn)}
This was written by Johannes Grabmeier and Alfred Scheerhorn.
@@ 17579,7 +23132,7 @@ By now, it is well understood both theoretically and experimentally
that the full exact quantifier elimination is intrinsically difficult,
posing a formidable barrier to efforts for devising general but
efficient methods. One response to this is specialization, as we have
surveyed in the previous chapter. In this chapter, we see another
+surveyed in the previous section. In this section, we see another
response: {\sl approximation}.
In many applications (in particular in science and engineering),
@@ 17600,7 +23153,7 @@ approximated methods are much more efficient for a large class of
moderate size inputs.
The word ``approximate'' carries different meanings in different
contexts. In this chapter, we survey two different interpretations and
+contexts. In this section, we survey two different interpretations and
methods for them: {\sl generic} and {\sl volumeapproximate}.
\subsection{Generic Quantifier Elimination}
@@ 18923,7 +24476,7 @@ Diophantine Equations
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\cleardoublepage
\phantomsection
\addcontentsline{toc}{chapter}{Index}
+%\addcontentsline{toc}{chapter}{Index}
\printindex
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\end{document}
diff git a/changelog b/changelog
index ec81ad2..f27849e 100644
 a/changelog
+++ b/changelog
@@ 1,3 +1,7 @@
+20171009 tpd src/axiomwebsite/patches.html 20171009.02.tpd.patch
+20171009 tpd books/bookvol10.1 add Doye's Coercion Algorithm chapter
+20171009 tpd books/bookheader.tex add headers for Doye chapter
+20171009 tpd books/Makefile special case handling for Doye
20171009 tpd src/axiomwebsite/patches.html 20171009.01.tpd.patch
20171009 tpd books/bookvolbib add references
20170929 tpd src/axiomwebsite/patches.html 20170929.01.tpd.patch
diff git a/patch b/patch
index 9967af7..456e3bb 100644
 a/patch
+++ b/patch
@@ 1,132 +1,3 @@
books/bookvolbib add references
+books/bookvol10.1 add Doye's Coercion Algorithm chapter
Goal: Proving Axiom Correct

\index{Sturm, T.}
\begin{chunk}{axiom.bib}
@techreport{Stur95,
 author = "Sturm, T.",
 title = "A REDUCE package for firstorder logic",
 type = "technical report",
 institution = "Universitat Passau",
 year = "1995",
}

\end{chunk}

\index{Crole, R.L.}
\begin{chunk}{axiom.bib}
@book{Crol93,
 author = "Crole, R.L.",
 title = "Categories for Types",
 publisher = "Cambridge University Press",
 year = "1993",
 isbn = "9780521457019"
}

\end{chunk}

\index{Mendelson, Elliot}
\begin{chunk}{axiom.bib}
@book{Mend87,
 author = "Mendelson, Elliot",
 title = "Introduction to Mathematical Logic",
 publisher = "Wadsworth and Brooks/Cole",
 year = "1987",
 isbn = "9781482237726"
}

\end{chunk}

\index{Devlin, Keith J.}
\begin{chunk}{axiom.bib}
@book{Devl79,
 author = "Devlin, Keith J.",
 title = "Fundamentals of Contemporary Set Theory",
 publisher = "SpringerVerlag",
 year = "1979",
 isbn = "9780387904412"
}

\end{chunk}

\index{Davenport, James H.}
\begin{chunk}{axiom.bib}
@misc{Dave93a,
 author = "Davenport, James H.",
 title = "C9: Universal Algebra",
 year = "1993",
 comment = "Lecture Notes for 2nd year undergrad and mather's course
 in Universal Algebra",
 school = "University of Bath"
}

\end{chunk}

\index{Goguen, J.A.}
\index{Meseguer, J.}
\begin{chunk}{axiom.bib}
@article{Gogu82,
 author = "Goguen, J.A. and Meseguer, J.",
 title = "Completeness of Manysorted Equational Logic",
 journal = "ACM SIGPLAN Notices",
 volume = "17",
 number = "1",
 year = "1982",
 pages = "917",
 abstract =
 "The rules of deduction which are usually used for manysorted
 equational logic in computer science, for example in the study of
 abstract data types, are not sound. Correcting these rules by
 introducing explicit quantifiers yields a system which, although it is
 sound, is not complete; some new rules are needed for the addition and
 deletion of quantifiers. This note is intended as an informal, but
 precise, introduction to the main issues and results. It gives an
 example showing the unsoundness of the usual rules; it also gives a
 completeness theorem for our new rules, and gives necessary and
 sufficient conditions for the old rules to agree with the new.",
 paper = "Gogu82.pdf",
}

\end{chunk}

\index{Padawitz, Peter}
\begin{chunk}{axiom.bib}
@article{Pada80,
 author = "Padawitz, Peter",
 title = "New results on completeness and consistency of abstract data
 types",
 journal = "LNCS",
 volume = "88",
 pages = "460473",
 year = "1980",
 abstract =
 "If an algebraic specification is designed in a structured way, a
 small specification is stepwise enriched by more complex operations
 and their defining equations. Based on normalization properties of
 term reductions we present sufficient ``local'' conditions for the
 completeness and consistency of enrichment steps, which can be
 efficiently verified in many cases where other attempts to prove the
 enrichment property ``syntactically'' have failed so far."
}

\end{chunk}

\index{Kounalis, Emmanuel}
\index{Rusinowitch, Michael}
\begin{chunk}{axiom.bib}
@inproceedings{Koun90,
 author = "Kounalis, Emmanuel and Rusinowitch, Michael",
 title = "A Proof System for Conditional Algebraic Specifications",
 booktitle = "Conference Conditional and Typed Rewriting Systems",
 year = "1990",
 abstract =
 "Algebraic specifications provide a formal basis for designing
 datastructures and reasoning about their properties.
 Sufficientcompleteness and consistency are fundamental
 notions for building algebraic specifications in a modular way. We
 give in this paper effective methods for testing these properties for
 specifications with conditional axioms."
}

\end{chunk}
+Goal: Axiom Literate Programming
diff git a/src/axiomwebsite/patches.html b/src/axiomwebsite/patches.html
index 4ff3742..17126ff 100644
 a/src/axiomwebsite/patches.html
+++ b/src/axiomwebsite/patches.html
@@ 5828,6 +5828,8 @@ books/bookvolbib add references
books/bookvolbib add references
20171009.01.tpd.patch
books/bookvolbib add references
+20171009.02.tpd.patch
+books/bookvol10.1 add Doye's Coercion Algorithm chapter

1.9.1