background.tex

\section{Background}
\label{sec:background}

\subsection{Blending in Mathematics}
\label{subsec:mathblend}

%Lakoff and N{\'u}{\~n}ez \citep{Lak00} 
\textcite{Lak00} 
are among the first to present
a cognitive account of the origin and development of mathematical
ideas,\footnote{This is lamented by Lakoff and N{\'u}{\~n}ez, who
claim that (prior to their work), ``there was still no discipline of
mathematical idea analysis from a cognitive perspective''
\citep{Lak00}.} arguing against the ``romance of mathematics'' in which
mathematics is presented as an ever-increasing set of universal,
absolute, certain truths which exist independently of humans. They
present the thesis that human mathematics is grounded in bodily
experience of a physical world, and mathematical entities inherit
properties which objects in the world have, such as being consistent
or stable over time.  Exploring the physical world of object
collection might lead to concepts like the empty collection and rules
like ``adding a collection of $n$ objects to an empty collection
yields a collection with $n$ objects''. People then form grounding
metaphors between the physical world and an abstract mathematical
world, allowing us to project from everyday experiences onto abstract
concepts, thus leading to the concept of zero and the axiom that $n +
0 = n$. Lakoff and N{\'u}{\~n}ez posit that blending different
mathematical metaphors leads to more complex ideas (see
also~\textcite{alexander11}). 

Alongside this account of mathematical cognition, mainstream
contemporary mathematics has developed its own methodology and
foundations, enjoying an exceptional place among scientific
disciplines. Its methods, objects of study and sometimes astonishing
results have widespread, if not universal, acceptance.

In conclusion, mathematics is a scientific discipline having not only
a fundamental cognitive component, necessary in its development, but
also possessing a collection of general principles and structures
going beyond a particular school of thought.  Among these general
processes we want to highlight in this paper the importance that
conceptual blending has in mathematics, incorporating both cognitive and
mathematically specific aspects in order to create new mathematical concepts.


%% \subsection{Some mathematical concepts}
%% In this paper we draw on Lakoff and N{\'u}{\~n}ez's ideas to produce a
%% computational model of blending in abstract mathematics. We present
%% three illustrative examples: the mathematical notion of infinity,
%% prime ideals and Galois theory. The first of these is the idea of a
%% number, process etc without limits or end. The latter two are concepts
%% from abstract algebra, which explores groups and related objects and
%% their properties. 

%% A {\em prime ideal} is a subset of a ring, which certain
%% properties, and Galois theory draws an important connection between
%% fields and groups, which can be used to simplify problems in field
%% theory. 

\subsection{Terminology for conceptual blending}
Our notion of conceptual blending is informed by Category theory, and
highly influenced by Goguen's work on concepts \parencite{Gog05b}. In
this paper we use the terminology below, and elucidate the terminology
by means of a running example -- discovering a version of the integers
(in the sense of providing a partial approach to the genuine integers)
using blending.

{\bf Conceptual spaces} are partial and temporary representational
structures which are constructed on the fly when talking about a
particular situation, which are informed by the knowledge structures
associated with a domain. These are influenced by Boden's idea of a
concept space which is mapped, explored and transformed by
transcending mapped boundaries \parencite{boden}, and form the input spaces
to our blend. 

As an example of two conceptual spaces, consider one as a theory
$\SIdIndex{Nat}$ --
a theory of the natural numbers, and $\SIdIndex{Func}$ -- a theory of a total
unary function with an inverse. 
%The terminology here used obviously refers to the fact that these two
%conceptual spaces are partial representations of the genuine concepts
%employed by mathematicians.  
We will refer back to these theories in this exposition.

(Many-sorted) First-order {\bf Axioms} are the criteria which will be
used here to delineate the conceptual
spaces. The axiomatic method has been a fundamental aspect of
mathematical research since Euclid, and various axiom changes have led
to revolutions in mathematics. For instance, 
%relaxing the axioms
%defining numbers led to negative and imaginary numbers, and 
rejecting
the parallel postulate opened up fascinating new areas of
non-Euclidean geometry.

The precise formulations for $\SIdIndex{Nat}$ and $ \SIdIndex{Func}$ can
be found in Listings~\ref{fig:nats} and \ref{fig:inv}. 
Notice that these formulations obviously refer to 
%the fact that these two conceptual spaces are 
partial representations of the genuine concepts
employed by mathematicians.  
In the conceptual space with theory $\SIdIndex{Nat}$, an example of an axiom is 
%$\forall x. \neg s(x) = 0$ -- that is that zero is not a successor element.
$\forall x. \neg \: 0 = \Id{s}(x)$ -- that is that zero is not a successor element.
%the least element of the natural numbers. 
The conceptual space with theory $\SIdIndex{Func}$ has an axiom
%$\forall x.\;f(f^{-1}) x = x$. 
$\forall x.\:\:\Id{f}(\Id{finv}(x)) = x$. 
%where heuristics for transformation, such as {\em consider
%the negative} and {\em drop a constraint}, are suggested.

{\bf Signature morphisms} between conceptual spaces are mappings from
the symbols of the source conceptual space into the symbols of the other
conceptual space. 
%
%For example $\SIdIndex{Nat}$ contains a function $\lambda
%x:\Id{Nat}.\;\Id{s}(x)$ to denote the successor, and $\SIdIndex{Func}$ contains a function
%$\lambda x:\Id{X}.\;\Id{f}(x)$. 
%A theory $G$ common to both may contain a function
%%$\lambda x:\sigma.\;g(x)$. 
%$\lambda x:\Id{N}.\;\Id{func}(x)$. 
For example $\SIdIndex{Nat}$ contains a function $\lambda
x:\Id{Nat}.\;\Id{s}(x)$ that maps $x$ to its successor, and
$\SIdIndex{Func}$ contains a function defined over a set $X$ that maps
each element to an image $\lambda x:\Id{X}.\;\Id{f}(x)$.  A theory $G$
with a morphism to both $\SIdIndex{Nat}$ and $\SIdIndex{Func}$ might
contain a function $\lambda x:\Id{N}.\;\Id{func}(x)$ that takes every
number in some set $\Id{N}$ to its image under $\Id{func}$.
%
When we show a mapping % in this paper 
we write 
this as
\begin{align}
  \Id{s}&&\leftarrow_{\phi(G,\SIdIndex{Nat})}&&\Id{func}&&\rightarrow_{\phi(G,\SIdIndex{Func})}&&\Id{f}\\
  \Id{Nat}&&\leftarrow_{\phi(G,\SIdIndex{Nat})}&&\Id{N}&&\rightarrow_{\phi(G,\SIdIndex{Func})}&&\Id{X}
\end{align}
\noindent The mapping $\phi(G,\SIdIndex{Nat})$ is a signature morphism from
$G$ to $\SIdIndex{Nat}$. Note that associated types are also mapped.

{\bf Input Spaces} refer to two or more conceptual spaces of
interest. 

{\bf Generic spaces} are conceptual spaces that possess commonality
between input spaces. 

%{\bf Colimits} are conceptual spaces representing a blend of input
%spaces with respect to a given generic space and set of signature
%morphisms. These are uniquely computed given a generic space and set of
%morphisms. Here is a diagrammatic representation of such a computation
%in our example using theories $\SIdIndex{Nat}$ and $\SIdIndex{Func}:$
{\bf Colimits} are conceptual spaces representing a blend of input
spaces with respect to a given generic space and a set of signature
morphisms. These are uniquely computed given a generic space and a set of
morphisms. Here is a diagrammatic representation of such a computation
in our example using theories $\SIdIndex{Nat}$ and $\SIdIndex{Func}:$
%\begin{center}
%  \begin{diagram}[size=7mm]
%    &       &   $G$   &       & \\
%    & \ldTo^{\rotatebox{-45}{$\phi(G,\SIdIndex{Nat})$}} &       &
%    \rdTo^{\rotatebox{45}{$\phi(G,\SIdIndex{Func})$}} &          \\
%    \SIdIndex{$\SIdIndex{Nat}$} &       &   &       &
%    \SIdIndex{$\SIdIndex{Func}$} \\
%    & \rdTo_{\rotatebox{45}{$\phi(B,\SIdIndex{Nat})$}} &       &
%    \ldTo_{\rotatebox{-45}{$\phi(B,\SIdIndex{Func})$}} &  \\
%    & & $Colimit$ & & 
%  \end{diagram}
%\end{center}
\begin{center}
  \begin{tikzcd}[column sep=normal, row sep=small]
    & \textrm{Colimit}
    \\
    \SIdIndex{Nat} \arrow{ur}{\phi(B,\SIdIndex{Nat})} & & \SIdIndex{Func} \arrow{ul}[swap]{\phi(B,\SIdIndex{Func})} \\
    & G \arrow{ul}{\phi(G,\SIdIndex{Nat})}
    \arrow{ur}[swap]{\phi(G,\SIdIndex{Func})}
  \end{tikzcd}
\end{center}
The conceptual space represented by the Colimit is often referred to
as the {\em blend}. 

{\bf Internal Evaluation} constitutes a variety of techniques to determine whether a computed colimit is viable as a conceptual space. In our example, since the conceptual spaces are mathematical theories, we can exploit the notion of consistency. This is a way of evaluating whether a
blend is not only creative, but also valid. In the example of theories
$\SIdIndex{Nat}$ and $\SIdIndex{Func}$,
the computed blend is inconsistent due to the emergent axioms in the
computed colimit. The only type existing within the colimit is from now
on referred to as $\mathbb{Z}$ to distinguish it from the natural
numbers. Notice that in the colimit it holds that:
%\begin{eqnarray*}
%  \forall x: \mathbb{Z}. \neg\; \Id{zero} &=&\Id{s}(x)\\
%%\forall x:\mathbb{Z}.\;s(s^{-1}( x)) &=& x
%\forall x:\mathbb{Z}.\; \Id{s}(\Id{sinv}( x)) &=& x
%\end{eqnarray*}
%\[
%  \begin{array}{lc@{\: = \:}c}
%    \forall x: \mathbb{Z}. \neg & \Id{zero} & \Id{s}(x)\\
%    \forall x: \mathbb{Z}. & \Id{s}(\Id{sinv}(x)) & x \\
%  \end{array}
%\]
\begin{center}
  $\forall x: \mathbb{Z}. \neg \:\:   \Id{zero} = \Id{s}(x)$
\end{center}
\begin{center}
  $\forall x: \mathbb{Z}. \:\: \Id{s}(\Id{sinv}(x)) = x$ \:.
\end{center}
This is an inconsistency, as from the second axiom we see 
that there is an
element for which 0 is the successor.

{\bf Weakening} refers to the process of weakening the input
theories by removing symbols or axioms. If we remove the axiom 
$$
\forall x: \Id{Nat}. \neg \:\: \Id{zero} = \Id{s}(x)
$$
then the resulting computed colimit contains a mathematical theory
which is consistent.  

\textcite{MartinezEtAl14} provides an algorithm to explore the space
of blends resulting from given input spaces and a given generic space, where
weakening is achieved by omitting axioms.  The algorithm returns the
blends which are consistent, and maximally so, among those in this
space of blends.  This algorithm assumes that consistency of relevant
theories can be checked, so is not always effective.

{\bf Running the blend} refers to elaborating or completing a
mathematical theory. Sometimes there are missing definitions which
need to be discovered. For example in the new theory 
%the following axioms exists
the following axiom appears
\begin{eqnarray*}
%\forall x,y:\mathbb{Z}. \: s(x) + y &=& s(x+y)
  \forall x,y:\mathbb{Z}. \:\: \Id{s}(x) + y &=& \Id{s}(x+y) \:,
\end{eqnarray*}
%but we also are interested in additional axioms such as
but we also are interested in theorems such as
\begin{eqnarray*}
%\forall x,y:\mathbb{Z}. s^{-1}(x) + y &=& s^{-1}(x+y)
  \forall x,y:\mathbb{Z}. \:\: \Id{sinv} (x) + y &=& \Id{sinv} (x+y) \:.
\end{eqnarray*}
Finding suitable theorems is an example of running the blend, and from which it
is possible to discover and prove 
%such 
theorems such as
\begin{eqnarray*}
%\forall x,y:\mathbb{Z}. s^{-1}(x) + s(y) &=& x+y
  \forall x,y:\mathbb{Z}. \:\: \Id{sinv}(x) + \Id{s}(y) &=& x+y \:.
\end{eqnarray*}

\subsection{Technologies}

The approach explained above corresponds to Goguen's
proposal \parencite{Gog99} for implementing blending, but slightly
simplified % (as in \textcite{Kutz2012} and \textcite{KuMoNeCo14}): 
(as in \textcite{KuMoNeCo14}): 
we use
the normal colimit construction, rather than $\frac{3}{2}$-colimits
(both described in \textcite{Gog99}).

%In the examples here considered we will be using colimits of V-shaped
%diagrams (cf.~Figure??). Thus, in each of the cases we have to specify
%two morphisms between a source conceptual space and a target conceptual
%space, with the restriction that both morphisms share the same source
%conceptual space.

Additionally we assume that the conceptual spaces involved are % always
given using a CASL specification \parencite{astesiano2002casl} and that the
morphisms are theorem preserving (i.e.\ map theorems to theorems).
% (but perhaps not axiom preserving). 
The reason for these assumptions is that in these cases
it is well-known how to compute % colimits \parencite{Mo98a}; 
colimits: the colimit
specification essentially corresponds to the disjoint union of the two
target conceptual spaces except for not repeating the symbols given in
the common source conceptual space.  Moreover, we will be using the
HETS system \parencite{MossakowskiEA06} to compute such colimits.
The code for the implemented examples in this paper
is available on-line.%
\footnote{See: \texttt{\url{https://github.com/ewenmaclean/ICCC2015_hetsfiles}}}

The use of CASL specifications means that we deal with first-order
logic; CASL is supported in the HETS system, and colimits here can be
computed in the current implementation of HETS. Although higher-order
logic (with Henkin semantics) is available in HETS (indeed in CASL)
and the colimits are well-known to exist (because higher-order in this
form is reducible to many-sorted first-order logic), it is worth
noticing that the calculus of such colimits is not currently available
in HETS.  This restricts the formalisms that can be used directly for
our purposes, where computation of colimits is central to our
approach.


%%% Local Variables: 
%%% mode: latex
%%% TeX-master: "mathsICCC"
%%% End: