~ohad-kammar/ohads-thesis/trunk

\Section{Universal algebra and equational logic}\sectionlabel{univ alg}
This section briefly recounts standard notions and results from
universal algebra. For a thorough introduction, see, e.g., Burris and
Sankappanavar~\cite[Chapter II, Sections~1
  and~8]{burris-ankappanavar:a-course-in-universal-algebra}.

A \defterm{signature} $\uaSignature$ is a pair $\pair
\uaOpset\uaArities$ where
\begin{itemize}
\item $\uaOpset$ is a set whose elements $\uamop$, $\uamopv$,
  $\uamopw$ we call \defterm{operation symbols}; and
\item $\uaArities$ assigns to each $\uamop$ in $\uaOpset$ a natural
  number $\uaArities(\uamop)$ called its \defterm{arity}.
\end{itemize}
When $\uaArities(\uamop) = n$, we say that $\uamop \of n$ in
$\uaSignature$. Operation symbols with arity $n$ are called $n$-ary
operations, and nullary operations, $\uamop \of 0$, are called
\defterm{constants}.


\begin{example}
  The signature for semilattices consists of a single binary operation
  $\orop \of 2$ called \defterm{join}.
\end{example}

\begin{example}
  The signature for monoids consists of a binary operation $\mdot{}
  \of 2$ called \defterm{multiplication}, and a constant $\munit \of
  0$ called \defterm{unit}.
\end{example}

\begin{example}\examplelabel{mnemoid signature}
  Let $\StorVal = \set{\mval_1, \ldots, \mval_n}$ be a finite set, $n
  \geq 2$ denoting storable values. The signature for
  \defterm{mnemoids}\footnote{Paul-Andr\'e Melli\`es coined the term
    `mnemoid' in unpublished work from 2010.} consists of an $n$-ary
  operation symbol $\lookupop \of n$ and $n$ different unary operation
  symbols $\updateop_{\mval_i} \of 1$, for all $i = 1, \ldots,
  n$. Note that this signature depends on the enumeration order of
  $\StorVal$.
\end{example}

Let $\uaSignature$ be a signature, and $\mX$ be any set. We consider
the elements of $\mX$ as \defterm{variables}, and define the set of
\defterm{$\uaSignature$-terms over $\mX$},
$\TermAlgebra[\mX]\uaSignature$ by induction:
\begin{itemize}
\item For every variable $\mx \in \mX$, we have $\mx \in
  \TermAlgebra[\mX]\uaSignature$.
\item For every $\uamop \of n$, if  $\mterm_1,
  \ldots, \mterm_n \in \TermAlgebra[\mX]\uaSignature$, then $\uamop(\mterm_1, \ldots, \mterm_n)
  \in \TermAlgebra[\mX]\uaSignature$.
\end{itemize}
Given a $\uaSignature$-term $\mterm$ over $\mX$, we define the set
$\varset\mterm \subset\mX$ of variables appearing in $\mterm$ by
induction:
\begin{itemize}
\item $\varset\mx \definedby \set{\mx}$; and
\item $\varset{\uamop(\mterm_1, \ldots, \mterm_n)} \definedby \Union_{i=1}^n\varset{\mterm_i}$.
\end{itemize}
A \defterm{$\uaSignature$-equation $\uaeq$ over $\mX$} is a pair
$\pair\mterm\mtermv$ of two $\uaSignature$-terms over $\mX$, written
as $\mterm = \mtermv$. This notation may cause confusion between an
equation such as $\munit \mdot \tx = \tx$ and syntactic equality which
differentiates $\munit\mdot\tx$ from $\tx$. In the following, we
explicitly note when we refer to syntactic equality between terms. We
extend the variable-set function to equations by setting
$\varset{\mterm = \mtermv} \definedby
\varset\mterm\union\varset\mtermv$.

We will henceforth fix a countably infinite set of {variables}
$\VarSet$, whose elements are denoted by $\tx$, $\ty$, $\tz$ and their
subscripts and superscripts $\tx_1$, $\ty^2$, $\tz^1_2$, etc. Thus, $\TermAlgebra\uaSignature$ refers to
$\TermAlgebra[\VarSet]\uaSignature$.

\begin{definition} A \defterm{presentation $\Ax$} is a pair
  $\pair\uaSignature\uaEq$ consisting of a signature $\uaSignature$
  and a set $\uaEq$ of $\uaSignature$-equations (over the distinguished set of
  variables $\VarSet$).
\end{definition}

We will usually define presentations by specifying their equations
only, when their signature can be inferred.

\begin{example}\examplelabel{semilattice presentation}
  The presentation of semilattices consists of the associativity,
  commutativity and idempotency equations:
  \begin{align*}
  \tx \orop (\ty \orop \tz) &= (\tx \orop \ty) \orop \tz &
  \tx \orop \ty             &= \ty \orop \tx             &
  \tx \orop \tx             &= \tx
  \end{align*}
\unhangdisplay{}
\end{example}

\begin{example}
  The presentation of monoids consists of the associativity equation and
  neutrality of the unit:
  \begin{align*}
      \tx \mdot (\ty \mdot \tz) &= (\tx \mdot \ty) \mdot \tz &
      \munit \mdot \tx          &= \tx                       &
      \tx \mdot \munit          &= \tx
  \end{align*}
\unhangdisplay{}
\end{example}

The following presentation of mnemoids is due to
Melli\'es~\cite{mellies:segal-condition-meets-computational-effects}:
\begin{example}\examplelabel{mnemoid presentation}
  Let $\StorVal = \set{\mval_1, \ldots, \mval_n}$ be a finite non-empty set denoting storable values
  and $\GlobalStateSignature$ be the signature for $\StorVal$-mnemoids
  given in \exampleref{mnemoid signature}. The presentation for mnemoids
  consists of the following three equation schemas:
  \begin{align*}
  \lookupop(\updateop_{\mval_1}(\tx), \ldots, \updateop_{\mval_n}(\tx)) &= \tx                      \\
  \updateop_{\mval_i}(\lookupop(\tx_1, \ldots, \tx_n))                &= \updateop_{\mval_i}(\tx_i) \\
  \updateop_{\mval}(\updateop_{\mvalv}(\tx))                         &= \updateop_{\mvalv}(\tx)
  \end{align*}
  These three equations have an operational reading in terms of
  interactions with a single global memory $\StorVal$-cell. The first
  equation states that a computation that first reads the state, and,
  depending on the stored value $\mval$, updates the cell to contain
  $\mval$, and then carries on executing $\tx$ is identical to the
  computation that immediately executes $\tx$. The second equation
  states that a look-up proceeding an update yields the updated
  value. The last equation states that more recent updates erase
  previous updates.
\end{example}

Let $\uaSignature$ be a signature. We call the presentation $\pair
\uaSignature\emptyset$ the \defterm{free presentation over
  $\uaSignature$}.

\begin{example}
  Let $\Char = \set{\mchar_1, \ldots, \mchar_n}$ be a finite set
  denoting I/O terminal characters. The presentation of terminal I/O
  is the free presentation over the signature consisting of the an
  $n$-ary operation $\inputop \of n$ and $n$ unary operations
  $\outputop_{\mchar_1}$, $\ldots$ , $\outputop_{\mchar_n}$. This
  presentation has the same signature as the mnemoid presentation, but
  no equations.
\end{example}
\begin{example}
  Let $\Exc$ be any non-empty set, possibly infinite, denoting
  possible exceptions. The presentation of $\Exc$-exceptions is the
  free presentation over the signature consisting of a constant
  $\raiseop_{\mexc}$ for every $\mexc \in \Exc$.
\end{example}

Let $\uaSignature$ be a signature. A \defterm{$\uaSignature$-algebra
  $\uaAlgebra$} is a pair $\pair{\carrier\uaAlgebra}{\algebra}$
consisting of a set $\carrier\uaAlgebra$, and an assignment mapping each
$\uamop \of n$ in $\uaSignature$ to a function $\algebra[\uaAlgebra][\uamop] \of
\carrier\uaAlgebra^n \to \carrier\uaAlgebra$. The set
$\carrier\uaSignature$ is called the \defterm{carrier} of the
algebra. The set
$\TermAlgebra[\mX]\uaSignature$ has an evident $\uaSignature$-algebra
structure, which we call the \defterm{term algebra}.

Let $\uaAlgebra$ be a $\uaSignature$-algebra and $\mX$ a set. A
\defterm{valuation over $\mX$ in $\uaAlgebra$} is a function
$\valuation \of \mX \to \carrier\uaAlgebra$. Given a term $\mterm$, we
say that a valuation over $\mX$ \defterm{suffices for $\mterm$}
provided $\varset\mterm \subset \mX$. We define valuations
sufficing for equations similarly. We can
extend any valuation $\valuation$ over $\mX$ in $\uaAlgebra$ to a
function $\uaalgebra[\uaAlgebra][\placeholder]\valuation \of
  \TermAlgebra[\mX]\uaSignature \to \carrier\uaAlgebra$ inductively as follows:
\begin{itemize}
\item $\uaalgebra[\uaAlgebra][\tx]\valuation \definedby
  \valuation(\tx)$
\item $\uaalgebra[\uaAlgebra][\uamop(\mterm_1, \ldots,
  \mterm_n)]\valuation \definedby
  \uaalgebra[\uaAlgebra][\uamop](\uaalgebra[\uaAlgebra][\mterm_1]\valuation,
  \ldots, \uaalgebra[\uaAlgebra][\mterm_n]\valuation)$
\end{itemize}

Let $\mterm = \mtermv$ be a $\uaSignature$-equation, $\uaAlgebra$ a
$\uaSignature$-algebra, and $\valuation$ a valuation in $\uaAlgebra$
sufficient for $\uaeq$. We say that $\mterm = \mtermv$ is \defterm{true under
the valuation $\valuation$} if $\uasem\mterm\valuation = \uasem\mtermv\valuation$.
We say that a $\uaSignature$-equation is \defterm{true in a
$\uaSignature$-algebra} if it is true under all valuations sufficient
for it.

\begin{definition}
  Let $\Ax = \pair\uaSignature\uaEq$ be a presentation. An $\Ax$-model
  is a $\uaSignature$-algebra in which all the equations in
  $\uaEq$ are true.
\end{definition}

The models for the semilattice presentation are precisely the
semilattices, and similarly for monoids. We call models of the mnemoid
presentation mnemoids.

Let $\Ax$ be a presentation. We say that $\Ax$ \defterm{entails} an
equation $\uaeq$, and write $\Ax \entails \uaeq$, if the equation $\uaeq$
is valid in all $\Ax$-models.

The following observation is due to
Melli\'es~\cite{mellies:segal-condition-meets-computational-effects}:
\begin{example}
  The presentation for mnemoids entails the following equation:
  \[
  \lookupop(\lookupop(\tx^1_1, \ldots, \tx^1_n), \ldots,
  \lookupop(\lookupop(\tx^n_1, \ldots, \tx^n_n))
  =
  \lookupop(\tx^1_1, \ldots,  \tx^n_n)
  \]
  The operational reading of this equation is that the memory cell
  does not change its contents between consecutive look-ups.
\end{example}

Let $\uaAlgebra$, $\uaAlgebrav$ be two $\uaSignature$-algebras. A
\defterm{homomorphism $\uahomo \of \uaAlgebra \to \uaAlgebrav$} is a
function $\uahomo \of \carrier\uaAlgebra \to \carrier\uaAlgebrav$ such that,
for every $\uamop \of n$ in $\uaAlgebra$ and $\malg_1, \ldots, \malg_n
\in \carrier\uaAlgebra$:
\[
\uahomo(\algebra[\uaAlgebra][\uamop](\malg_1, \ldots, \malg_n)) =
\algebra[\uaAlgebrav][\uamop](\uahomo(\malg_1), \ldots, \uahomo(\malg_n))
\]
Let $\Ax =
\pair\uaSignature\uaEq$ be a presentation. A
\defterm{homomorphism between two $\Ax$-models} is a homomorphism
between them as $\uaSignature$-algebras.

Let $\Ax$ be a presentation and $\mX$ a set. A \defterm{free
  $\Ax$-model over $\mX$} is a pair $\pair\uaAlgebra\unit$ consisting
of an $\Ax$-model $\uaAlgebra$ and a function $\unit \of \mX \to
\carrier\uaAlgebra$ such that for every other such pair
$\pair\uaAlgebrav\mmorph$ there exists a unique homomorphism $\uahomo
\of \uaAlgebra \to \uaAlgebrav$ satisfying $\uahomo \compose \unit =
\mmorph$. The free $\Ax$-model over any set always exists, and it is
unique up to a unique isomorphism preserving $\unit$.

\begin{example}
  The carrier of the free semilattice over a set $\mX$ is given by the non-empty
  finite powerset $\NonemptyFinitePowerset\mX$. The join operation is
  given by union.
\end{example}

\begin{example}
  The carrier of the free monoid over a set $\mX$ is given by the set $\Kleene\mX$
  of finite sequences of $\mX$-elements. The monoid unit is the empty
  sequence, $\seq{}$. The monoid multiplication is concatenation,
  $\concat$.
\end{example}

The following three examples are due to Plotkin and
Power~\cite{plotkin-power:notions-of-computation-determine-monads}:
\begin{example}
  Let $\StorVal = \set{\mval_1, \ldots, \mval_n}$ be a finite set with
  at least two elements denoting storable values. The carrier of the
  free mnemoid $\Monad\mX$ over a set $\mX$ is given by ${(\StorVal\times\mX)^{\StorVal}}$. The $\lookupop$ operation is given
  by:
\begin{mapdef*}
\lookupop \of &\parent{\Monad\mX}^{n} &\to
{\Monad\mX}
\\
\lookupop \of
&\lam{i}{\parent{\lam{\mval}{\pair{\mvalv_{i,\mval}}{\mvx_{i,\mval}}}}}
&\mapsto \lam {\mval_i}{\pair{\mvalv_{i,\mval_i}}{\mvx_{i,\mval_i}}}
\end{mapdef*}%
For every $\mval_0 \in \StorVal$, the $\updateop_{\mval_0}$ operation
is given by:
\begin{mapdef*}
\updateop_{\mval_0} \of &\parent{\Monad\mX} &\to
{\Monad\mX}
\\
\updateop_{\mval_0} \of &\mcomp &\mapsto {\lam \mval{\mcomp
(\mval_0)}}
\end{mapdef*}%
Compare these operations with the algebraic operations for the global
state monad given in \exampleref{global state operations}.
\end{example}

\cats{}Let $\Ax$ be a presentation. Denote by $\ModCat\Ax\Set$ the
category consisting of $\Ax$-models as objects and homomorphisms
between them. Consider the forgetful functor $\U_{\Ax} \of \ModCat\Ax\Set \to \Set$
forgetting the algebra structure. The free model over $\mX$
is a universal arrow from $\mX$ to $\U$. The existence of the free $\Ax$-model implies that $\U_{\Ax}$ always has a
left adjoint $\F_{\Ax} \leftadjointto \U_{\Ax}$ given on objects by the free
algebra.

\nocats{}The entailment relation forms a semantic notion of
validity. We now discuss syntactic validity via
\defterm{provability}. Given a signature $\uaSignature$, a
\defterm{substitution $\uasub$ from a set $\mX$ to a set $\mY$}
assigns to each element in $\mX$ a $\uaSignature$-term over $\mY$. Thus,
substitutions from $\mX$ to $\mY$ are valuations over $\mX$ in the
term algebra $\TermAlgebra[\mY]\uaSignature$. Therefore, we may say
that a substitution suffices for a term or an equation. When $\uasub$
suffices for $\mterm$, we write $\mterm\uasub$ for the term resulting
from performing the substitution, and similarly for an equation
$\uaeq$. A \defterm{renaming} is a substitution to $\mY$ assigning
only variables in $\mY$.

Given a presentation $\Ax = \pair\uaSignature\uaEq$,
\figureref{provability relation} inductively defines the provability
relation $\Ax \proves \mterm = \mtermv$ over $\uaSignature$-equations.
The provability relation is thus the least congruence relation, with
respect to the operations in $\uaSignature$, that contains $\uaEq$, and that
is closed under substitution. When the presentation is
\emph{free}, i.e., $\uaEq = \emptyset$, the provability relation
coincides with syntactic equality.

\begin{figure}
\begin{mathpar}
\inferrule[Axiom:]{}{\uaeq \in \uaEq \implies \Ax \proves \uaeq}
\\
\inferrule[refl:]{}{
\Ax \proves \mterm = \mterm}

\inferrule[symm:]{\Ax \proves \mterm  = \mtermv}
                {\Ax \proves \mtermv = \mterm }

\inferrule[Trans:]{\Ax \proves \mterm = \mtermv \qquad \Ax\proves\mtermv = \mtermu}
        {\Ax \proves \mterm                     =                \mtermu}

\inferrule[subst:]{\Ax \proves \uaeq\/\hphantom{\uasub}}
                  {\Ax \proves \uaeq\/\uasub}
\quad (\text{$\uasub$ suffices for $\uaeq$})

\inferrule[cong:]{\text{for all $\tx \in \varset\mterm$: } \Ax \proves \uasub_1(\tx) = \uasub_2(\tx)}
                 {\Ax \proves \mterm\uasub_1 = \mterm\uasub_2}
\quad (\text{$\uasub_1$, $\uasub_2$ suffice for $\mterm$})
\end{mathpar}
\caption{\figurelabel{provability relation}equational logic}
\end{figure}

We extend the provability relation from $\TermAlgebra\uaSignature$ to
terms over any set $\mX$ by defining $\Ax \proves \mterm = \mtermv$ if
and only if there exist provably equal $\uaSignature$-terms $\mterm'$,
$\mtermv'$ (over $\VarSet$) and a renaming $\uasub$ to $\mX$
sufficient for $\mterm' = \mtermv'$ such that $\mterm'\uasub$ and
$\mtermv'\uasub$ are syntactically equivalent to $\mterm$ and
$\mtermv$, respectively.  The extended provability relation is then
the least
congruence over the term algebra $\TermAlgebra[\mX]\uaSignature$, with respect to its
operations, contains all instances of equations in $\uaEq$, and
closed under substitution. We can therefore quotient each term algebra
$\TermAlgebra[\mX]\uaSignature$ by the provability relation, with the
operations factoring through the congruence relation. The resulting
algebra $\F \mX$ is then an $\Ax$-model called the \defterm{term model over
  $\mX$}.

\begin{theorem}\theoremlabel{term model}
  Let $\Ax = \pair\uaSignature\uaEq$ be a presentation, and $\mX$ is a
  set.  The term model over $\mX$, with the function mapping each
  variable in $\mX$ to its equivalence class, is the free $\Ax$-model
  over $\mX$.  Moreover, every $\uaSignature$-equation over $\mX$ is
  provable if and only if it is valid in the term model $\F\mX$.
\end{theorem}

In particular, entailment and provability coincide:

\begin{theorem}[soundness and completeness]\theoremlabel{soundness and
  completeness}
  For every presentation $\Ax$:
  \[
  \Ax \entails \uaeq \qquad \iff \qquad \Ax \proves \uaeq
  \]
\end{theorem}

\begin{example}
  The free semilattice $\NonemptyFinitePowerset\mX$ can be viewed as
  the term model where each set $\set{\mx_1, \ldots, \mx_n}$
  corresponds to the equivalence class of $\mx_1\orop\ldots\orop \mx_n$.
\end{example}

\begin{example}
  The free monoid $\Kleene\mX$ can be viewed as the term model where
  each finite sequence $\seq{\mx_1, \ldots, \mx_n}$, $n \geq 0$, corresponds to the
  equivalence class of $\mx_1 \cdots \mx_n$.
\end{example}

\begin{example}\examplelabel{idempotency equation for mnemoids}
  Let $\StorVal = \set{\mval_1, \ldots, \mval_n}$, $n \geq 2$ be a finite
  set denoting storable values.
  The free mnemoid $\parent{\StorVal\times\mX}^{\StorVal}$ can be
  viewed as the term model where each function
  $\lam{\mval}{\pair{\mvalv_{\mval}}{\mx_{\mval}}}$ corresponds to the
  equivalence class of the following term:
  \[
  \lookupop(\updateop_{\mval_1}(\mx_{\mval_1}), \ldots, \updateop_{\mval_n}(\mx_{\mval_n}))
  \]
  \unhangdisplay
\end{example}

We say that a presentation $\Ax$ is \defterm{equationally inconsistent} if $\Ax
\proves \tx = \ty$. A presentation that is not inconsistent is
consistent. \theoremref{soundness and completeness} implies that if
$\Ax$ is inconsistent, every $\Ax$-model has at most one element. In
this case, if $\Ax$ has no constant symbols, the free model over the
empty set is the empty set. If $\Ax$ does contain at least one
constant symbol, the free model over the empty set is also a
singleton.

Finally, we discuss morphisms between presentations. The following
notions are \emph{not} standard. Let $\uaSignature$, $\uaSignature'$
be signatures. A \defterm{translation of signatures $\Translation \of
  \uaSignature \to \uaSignature'$} is an assignment assigning to every
$\uamop \of n$ in $\uaSignature$ a $\uaSignature'$-term
$\Translation(\uamop)$ over $\set{\tx_1, \ldots, \tx_n}$.  Note that
every translation $\Translation$ extends uniquely to a homomorphism
${\Translation \of \TermAlgebra\uaSignature \to
  \TermAlgebra{\uaSignature'}}$ between the term algebras of the
corresponding signatures (without any equations).

Let $\Ax = \pair\uaSignature\uaEq$,
$\Ax'=\pair{\uaSignature'}{\uaEq'}$ be presentations. A
\defterm{translation of presentations ${\Translation \of \Ax \to \Ax'}$}
is a translation ${\Translation \of \uaSignature \to \uaSignature'}$
such that, for every $\mterm = \mtermv$ in $\uaEq$, $${\Ax' \proves
\Translation(\mterm) = \Translation(\mtermv)}$$

The category of
presentations $\PresentationCat$ is given by presentations and
translations between them. The identities are the translations mapping
each $\uamop \of n$ to $${\Translation(\uamop) \definedby \uamop(\tx_1,
\ldots, \tx_n)}$$ Composition $\Translation_2 \compose \Translation_1$
is given by composing the homomorphic extension of $\Translation_2$
with $\Translation_1$.

\begin{example}\examplelabel{alternative group presentation}
  Let $\AbGrpAx$ be the presentation of Abelian groups whose signature
  $\AbGrpSig$ consists of a binary operation $+ \of 2$, a constant $0
  \of 0$, a unary operation $- \of 1$, and whose equations are
  \begin{align*}
  \tx + \ty &= \ty + \tx &
  \tx + (-\tx) &= 0 \\
  (\tx + \ty) + \tz &= \tx + (\ty + \tz) &
  \tx + 0 &= \tx
  \end{align*}
  Let $\AbMinusAx$ be the presentation whose signature $\AbMinusSig$ consists of a
  binary operation $- \of 2$, a constant $0 \of 0$, and whose
  equations are
  \begin{align*}
    \tx - \parent{\ty - \parent{\tz - \parent{\tx - \ty}}} &= \tz &
    \tx - \tx &= 0
  \end{align*}

  Define the following translation $\Translation \of \AbMinusSig \to \AbGrpSig$:
  \begin{align*}
    \Translation(0) &\definedby 0&
    \Translation(-) &\definedby \tx_1 + (-\tx_2)
  \end{align*}
  Then $\Translation$ is also a translation $\Translation \of
  \AbMinusAx \to \AbGrpAx$.

  Define the following translation $\inv\Translation \of \AbGrpSig
  \to \AbMinusSig$:
  \begin{align*}
    \inv\Translation(0) &\definedby 0&
    \inv\Translation(+) &\definedby \tx_1 - (0-\tx_2) &
    \inv\Translation(-) &\definedby 0 - \tx_1
  \end{align*}
  Tarski~\cite{tarski:ein-beitrag-zur-axiomatik-der-abelschen-gruppen}
  showed that the Abelian group axioms follow from the two axioms of
  $\AbMinusSig$, and therefore $\inv\Translation \of \AbGrpAx \to
  \AbMinusAx$ is a translation.

  The two compositions are given by:
  \begin{align*}
    \inv\Translation\compose\Translation(0) &= 0
    &&\begin{aligned}[t]
    \inv\Translation\compose\Translation(-) &= \inv\Translation(\tx_1
    + (-\tx_2))
    \\&= \tx_1 - (0 - (0 - \tx_2))
    \end{aligned}\\
    \\
    \Translation\compose\inv\Translation(0) &= 0
    &&\begin{aligned}[t]
    \Translation\compose\inv\Translation(+) &= \Translation(\tx_1 - (0
    - \tx_2)) \\&= \tx_1 + (-(0 + (0 + (-\tx_2))))
    \end{aligned}
    \\
    &&\mathclap{\Translation\compose\inv\Translation(-) = \Translation(0 - \tx_1)
    = 0 + (0 - \tx_1)}
  \end{align*}
  Note that $\inv\Translation\compose \Translation(0)$ and
  $\id(0)$ are syntactically equivalent,  but
  $\inv\Translation\compose\Translation(-)$ and $\id(-)$ are not, and
  therefore $\inv\Translation\compose\Translation$ is \emph{not} the
  identity translation. However, the following does hold:
  \[\AbMinusAx \proves \inv\Translation\compose\Translation(-) =
  \id(-)
  \]
  \unhangdisplay
\end{example}

The previous example suggests an alternative for translations. Given two
presentations $\Ax$, $\Ax'$, we define the relation $\TransEq$ over
translations $\Translation_1, \Translation_2 \of \Ax \to \Ax'$ by
$\Translation_1 \TransEq \Translation_2$ if and only if for every
$\uamop \of n$ in $\Ax$:
\[
\Ax' \proves \Translation_1(\uamop) = \Translation_2(\uamop)
\]
For example, the translations from \exampleref{alternative group
  presentation} satisfy $\inv\Translation\compose\Translation \TransEq
\id$ and ${\Translation\compose\inv\Translation \TransEq
\id}$. Therefore, it is natural to consider the category $\TheoryCat$ consisting of
presentations together with equivalence classes of translations as
morphisms between them. We will do so in the next section using
Lawvere theories and monads. The advantage of our chosen notion of
translations is that their equality can be decided syntactically.

We will be mainly concerned with a particular kind of translation. An
\defterm{extension} is a translation $\Translation \of \Ax \to \Ax'$
such that for every $\uamop \of n$ in $\Ax$ there is a unique $\uamop' \of
n$ in $\Ax'$ such that $\Translation (\uamop) = \uamop'(\tx_1, \ldots,
\tx_n)$ syntactically, and, moreover, if $\uamop_1' = \uamop_2'$ then $\uamop_1 =
\uamop_2$.

\begin{example}\examplelabel{environment presentation}
  Let $\StorVal = \set{\mval_1, \ldots, \mval_n}$ be a finite set with at lest two elements denoting
  storable values. The \defterm{environment presentation} is given by
  the two equations:
  \begin{align*}
    \lookupop(\tx, \ldots, \tx) &= \tx \\
    \lookupop(\lookupop(\tx^1_1, \ldots, \tx^1_n), \ldots,
    \lookupop(\tx^n_1, \ldots, \tx^n_n)) &= \lookupop(\tx^1_1, \ldots,
    \tx^n_n)
  \end{align*}

  Then, by \exampleref{idempotency equation for mnemoids}, we have an
  extension from the environment presentation to the mnemoid
  presentation mapping $\lookupop$ to $\lookupop$.
\end{example}
As in the previous example, the extension will usually be obvious.  In
this case we simply say that $\Ax'$ is an extension of $\Ax$.