\section{Theory of Algebraic Specification}
\begin{definition}[Strings on an Alphabet] Given a non-empty set $A$ we denote
\begin{enumerate}
\item $A^+$ the set of non-empty strings $a_1 a_2 \ldots a_r$ with
the $a_i \in A$ and
\item $A^*$ the set $\{\lambda\} \cup S^+$ where $\lambda$ denotes the
empty string.
\end{enumerate}
\end{definition}
\begin{definition}[Signature] A signature $\Sigma=(S,\Omega)$ consists
of a set $S$, the set of sort symbols, and a set $\Omega$ of
constant and operation symbols. The set $\Omega$ is the union of pairwise
disjoint subsets:
\begin{enumerate}
\item $K_{s}$, the set of constant symbols of sorts $s \in S$
\item $\Omega_{W,s}$, set of operation symbols with argument sorts
$W$ and range sort $s$, for all $s \in S$ and $W \in S^+$,
where $S^+$ denotes the set of non-empty strings on the
alphabet $S$.
\end{enumerate}
\end{definition}
\begin{remarks}
\begin{enumerate}
\item The set of constants symbols (resp. operation symbols) are given by
$$
K=\cup_{s \in S}K_{s} \;\;\;\;\; (\Omega=K \cup_{W \in S^+, s \in S}\;\Omega_{W,s}).
$$
Using the notation $\Omega_{\lambda,s}=K_s$, where $\lambda \in S^*$ is the
empty string, we could more succinctly write:
$$
\Omega=K \cup_{W \in S^*,s \in S}\;\Omega_{W,s}).
$$
\item Constant symbols $N \in K$ ( resp. operation symbols $N \in \Omega_{W,s}$, with
$W=s_1 s_2 \ldots s_n$) are written as $N:\rightarrow s$ (resp.
$N: W \rightarrow s$ or $N: s_1 s_2 \ldots s_n \rightarrow s$),
where N is called the {\em name} and $\rightarrow s$ (resp.
$s_1 s_2 \ldots s_n \rightarrow s$) the {\em declaration} of the
constant (resp. operation) symbol. Because of the
$\Omega_{\lambda,s}=K_s$ constant symbols are also called
operation symbols of arity $0$.
\end{enumerate}
\end{remarks}
\begin{example} \label{Nat_sig}Consider the signature $Nat=(S,\Omega)$ with sorts symbols
$S=\{\mathbf{nat}\}$ and operations symbols
$$
\Omega=\{\mathbf{zero}:\rightarrow \mathbf{nat}, \mathbf{succ}: \mathbf{nat} \rightarrow \mathbf{nat} \}.
$$
\end{example}
\begin{definition}[Algebra] An algebra $A=(S_A, \Omega_A)$ of a signature
$\Sigma=(S,\Omega)$, also called a $\Sigma-algebra$, is given by two families
of $S_A=\{A_s\}_{s \in S}$ and $\Omega_A=\{N_A\}_{N \in \Omega}$ where
\begin{enumerate}
\item $A_s$ are sets for all $s \in S$, called the {\em carrier sets} or
{\em domains} of $A$.
\item $N_A$ are elements of $A_S$ for all constant symbols $N \in K_s$
{\em i.e.} $N: \rightarrow s$ and $s \in S$. They are called the
{\em constants} of $A$. {\bf Note}: Constants can be considered as
operations of arity $0$ because of the fact that there is
a bijective correspondence between elements $N_A \in A_s$ and
functions $N_A: \{\lambda\} \rightarrow A_s$.
\item $N_A: A_{s_1} \times A_{s_2} \ldots \times A_{s_n} \rightarrow A_s$
are functions for all operation symbols
$N \in \Omega_{s_1 s_2 \ldots s_n, s}$ ({\em i.e.}
$N: s_1 s_2 \ldots s_n \rightarrow s$) and
$w=s_1 s_2 \ldots s_n \in S^+$, $s \in S$, where $\times$
denotes the cartesian product of sets. The functions $N_A$
are called operations of $A$.
\end{enumerate}
\end{definition}
\begin{example} \label{Nat_alg} Following example \ref{Nat_sig}, we consider
the $\mathbf{nat}$-algebra $A$ defined by the assigments:
$$
A_{\mathbf{nat}}:=\mathbb{N}\mbox{, } \mathbf{zero}_{A}:=0 \mbox{ and }
\mathbf{succ}_{A}:= succ:\mathbb{N} \rightarrow \mathbb{N},
$$
where $succ$ is the usual succesor function on $\mathbb{N}$.
So, $A:=\{\{ A_{\mathbf{nat}}\}, \{\mathbf{zero}_{A}, \mathbf{succ}_{A}\}\}$.
\end{example}
\begin{definition}[Variables and Terms] Let $\Sigma=\{S,\Omega\}$ be a
signature and $X_s$ a set, for each $s \in S$. Furthermore, we assume that the
sets $X_s$ are pairwise disjoint and also disjoint with $\Omega$. The union
$$
X = \bigcup_{s \in S} X_s
$$
is called the set of variables with respect to $\Sigma$.
The sets $T_{\Omega,s}(X)$ of {\em terms of sort $s$} are inductively defined by:
\begin{enumerate}
\item the {\em basic terms} $X_s \bigcup K_s \subset T_{\Omega,s}(X)$,
where $K_s$ is the set of constant symbols of sort $s$.
\item the {\em composite terms} $N(t_1,\ldots,t_n) \in T_{\Omega,s}(X)$
for all operation symbols $N \in \Omega$ with
$N:s_1 \dots s_1 \rightarrow s$ and all terms
$t_1 \in T_{\Omega,s_1}(X),\ldots,t_n \in T_{\Omega,s_n}(X)$.
\item No further terms of sort $s$ are present in $T_{\Omega,s}(X)$.
The set $T_{\Omega,s}$ of terms without variables of sort $s$,
also called ground terms of sort $s$, is defined as
$$
T_{\Omega,s}=T_{\Omega,s}(X:=\emptyset).
$$
The set of terms $T_{\Omega}(X)$ (resp. the set of terms without variables
$T_{\Omega}$) is defined as
$$
T_{\Omega}(X) := \bigcup_{s \in S} T_{\Omega,s}(X) \;\;\;\; \mbox{(resp. } T_{\Omega} := \bigcup_{s \in S} T_{\Omega,s} \mbox{).}
$$
\end{enumerate}
\end{definition}
\begin{definition} [Evaluation of Terms] Let $\Sigma=(S,\Omega)$ be a signature
and $A$ a $\Sigma$-algebra.
\begin{enumerate}
\item Let $T_{\Omega}$ the set of ground terms over $\Sigma$. The
{\em evaluation} $eval: T_{\Omega} \rightarrow A$ is defined
by
\begin{enumerate}
\item $eval(N) = N_A$ for all constant symbols $N \in K$.
\item $eval(N(t_1,\ldots,t_n)) = N_A(eval(t_1),\ldots,eval(t_n))$
for all $N(t_1,\ldots,t_n) \in T_{\Omega}$.
\end{enumerate}
\item Given a set of variables $X$ for $\Sigma$ and an {\em assigment}
$ass:X \rightarrow A$, where $ass=(ass:X_s \rightarrow A_s)_{s \in S}$
is a consistlection of functions. The {\em extended assigment}
$\overline{ass}:T_{\Omega}(X) \rightarrow A$ of the assigment $ass$
is recursively defined by
\begin{enumerate}
\item $\overline{ass}(x):=ass(x)$ for all $x \in X$;
\item $\overline{ass}(N):=N_A$ for all constant symbols $N \in K$;
\item $\overline{ass}(N(t_1,\ldots,t_n)):=N_A(\overline{ass}(t_1),\ldots,\overline{ass}(t_n))$
for all $N(t_1,\ldots,t_n) \in T_{\Omega}(X)$.
\end{enumerate}
\end{enumerate}
\end{definition}
\begin{remarks}
\begin{enumerate}
\item In case the $X=\emptyset$ there is exactly one assigment, the
empty assigment $\emptyset$, and $\overline{ass}=eval$.
\item Though a functional notation is used to denote $eval$ and $\overline{ass}$
they in fact are families of fuctions
$eval=(eval_s: T_{\Omega,s} \rightarrow A_s)_{s \in S}$ and
$\overline{ass}l=(\overline{ass}_s: T_{\Omega,s}(X) \rightarrow A_s)_{s \in S}$.
Moreover, $eval$ is the restriction of $\overline{ass}$ to
$T_{\Omega}$.
\end{enumerate}
\end{remarks}
\begin{definition}[Equations]
Let $\Sigma=(S,\Omega)$ be a signature and $X$ set of variables with respect to
$\Sigma$.
\begin{enumerate}
\item A triple $e=(X,L,R)$ with $L, R \in T_{\Omega,s}(X)$ for some
$s \in S$ is called an equation of sort $s$ with respect to
$\Sigma$.
\item The equation $e=(X,L,R)$ is called {\em valid} in a $\Sigma$-algebra
$A$ if for all assigment $ass: X \rightarrow A$ we have
$$
\overline{ass}(L)=\overline{ass}(R)
$$
where $\overline{ass}$ is the extended assigment
\end{enumerate}
\end{definition}
\begin{definition}[Homomorphisms and Isomorphism of $\Sigma$-algebras]
Let $A$ and $B$ be $\Sigma$-algebras of the same signature
$\Sigma=(S,\Omega)$.
\end{definition}
\begin{definition}[Institution] An institution $I=(\mathbf{Sign}_{I})$ consist of:
\begin{itemize}
\item a category $\mathbf{Sign}_{I}$ of {\em signatures};
\item a functor $\mathbf{Sen}_{I}:\mathbf{Sign}_{I} \rightarrow \mathbf{Set}$
giving a set $\mathbf{Sen}_{I}(\Sigma)$ of $\Sigma$-{\em sentences} for
each signature $\Sigma \in \|\mathbf{Sign}_{I}\|$;
\item a functor $\mathbf{Sen}_{I}:\mathbf{Sen}_{I}^{op} \rightarrow \mathbf{Cat}$
giving a category $\mathbf{Mod}_{\Sigma}$ of $\Sigma$-models for each
signature $\Sigma \in \mathbf{Sign}_{I}$; and
\item for each $\Sigma \in \mathbf{Sign}_{I}$, a {\em satisfaction relation}
\end{itemize}
\end{definition}
\section{Context Theory}
We follow an Object Oriented Programming (OOP) approach to model theories.
For us a theory $A$ is analogous to a class in an object oriented language.
A theory-class contains methods. Methods can be of different types. Namelly,
we allow methods of type:
\begin{enumerate}
\item symbol. They define OpenMath symbols. A symbol can be public
or private.
public symbols are know to descendant of the theory.
private symbols are unknown to the descendants.
\item axiom. An essential property over a group of symbols defined in the
theory is stated.
\item definition. A definition for a symbol (or group of symbols).
\item assertion. Assertions can be of different types (follow omdoc model):
corollary, theorem, proposition, conjecture, false-conjecture,
etc. That distintion is not important because the same assertion
can be of a different type in different theories (a theorem in
one theore may be just a corollary in other). So we should
allow the type to be changed by inheristance and so forth.
\item exercise.
\item example. Examples. (omdoc model).
\item algorithm. Algorithms of a theory.
\end{enumerate}
We will use the terms theory and class in an interchangable manner.
All methods within a class are identified by a unique name (id in the
\xml{} representation). That is the class possess a unique namespace
for its methods.
As methods do in OOP classes. our theory methods may accept parameters. What is this
useful for? If well programmed, a method may be highly customizable. For instance,
suppose the following axiom belongs to a theory of modoids groups
(we use a an \xml{} format for descrbing our theories, see the implementation
section for more explanation):
{
\small
\begin{verbatim}
For all ${vars.var("a")},
${vars.var("b")} and
${vars.var("c")}
in ${symbols.symbol("set")},
the equation
${symbols.symbol("eq")}
${symbols.symbol("op")}
${vars.var("a")}
${symbols.symbol("op")}
${vars.var("b")}
${vars.var("c")}
${symbols.symbol("op")}
${symbols.symbol("op")}
${vars.var("a")}
${vars.var("b")}
${vars.var("c")}
holds.
\end{verbatim}
}
The axiom is parameterized in terms of the variables a, b and c, with default
values \BET{OMV name="a"}, \BET{OMV name="b"} and \BET{OMV name="c"},
respectively. In case we want another presentation for the axiom we
just need to "call" the axiom method with different parameters
(e.g. a="\BET{OMV name="H"}", b="\BET{OMV name="G"}", b="\BET{OMV name="W"}" ).
Classes will have to be instancated in order to acces their methods.
An instance of a class (theory) will be called an object. In order to access
the methods of a class we will have to create an object of that class.
\subsection{Theory Inheritance}
\label{susect:theory_inheritance}
{\bf Simple inheritace}: A theory $A$ inherits a theory $B$ by inheriting all their
symbols, axioms, definitions, (assertions?, exercises?, examples?). Nothing is
changed in class $B$.
{\bf Simple inheritance via theory morphisms}: The class $A$ inherits the class
$B$ but there is an injective function
$$
f: S \subset symb(A) \rightarrow symb(B)
$$
where $symb(*)$ denote the set of symbols of $*$. A tipical example for this case
is the definition of a theory of rings $R$ by inheriting the theory of monoids $M$
and groups $G$ via the following morphisms:
$$\{R.starset \rightarrow M.set, R.times \rightarrow M.op, R.one \rightarrow M.neut\}$$
and
$$\{R.set \rightarrow G.set, R.plus \rightarrow G.op, R.zero \rightarrow G.neut\}.$$
where $X.*$ denotes the symbol $*$ in the theory $X$. The symbol
R.starset denotes the support set of a ring without the zero (commonly denoted
as $R^*$).
Note: special care will have to be taken with namespace conventions in
inheritance. For instance, in case in the case of the theory of rings $R$
the axiom op\_associative from monoid will be inherited twice once
with monoid and once with group (mind that group inherits monoid).
\subsection{Parametric Theories}
\label{susect:theory_inheritance}
Theories may accept other theories as global parameters. Examples:
\begin{itemize}
\item a theory of vector spaces take as parameters an integer (the dimension) and
an instance of a field (the base field). An instance of a vector space
is is given by specifying a integer and a concrete field.
\item a theory of a polinomial ring in one variable may acept a ring as
a parameters.
\item Finite fields are parameterized by a prime number and by an irreducible
polynomial over the prime field $\mathbb{F}_p$ (or what amounts
to the same the ideal generated by that polynomial).
\item Finite fields modulo isomorphism are parameterized by a number $q=p^N$,
where $p$ is a (positive) prime number and $N>0$.
\end{itemize}
What can a global parameter be?
\begin{itemize}
\item maybe we need basic data types as integer, floats, strings, etc.
Maybe as \om{} OMI, OMSTR, OMF, etc.
\item An instance (object) of a given class. (How do we handle the
example of an Ideal?)
\end{itemize}
\section{Context Implementation}
- element.
Attr: id=""