other.tex

\section{A Challenge Example for Blending} \label{galois}

\subsection{Computational Creativity via Blending}

The examples shown thus far in the paper have been examples of
blending in mathematics whose mechanisation has helped to identify
some novel and unexpected results. The blending itself was a one-stage
process where human input was required to identify the input
concepts. A more ambitious aim of the approach of applying blending to
the problem of computational creativity in mathematics, is to allow
search to be done over multiple blends and for the {\em process} of
blending to be controlled mechanically. In this section we describe
very informally a mathematical domain that seems in some ways a
natural candidate for a blending approach. 
% A fuller mathematical
% exposition would be required to support such an enterprise.


\subsection{Galois Theory}

%% This example is developed in a less formal manner than the previous.
%% It is included both to highlight some outstanding technical issues,
%% and to develop some broader theoretical points about the future
%% prospects and applications of our approach.  

% In its most straightforward formulation, 
Galois theory develops a relationship between a polynomial $p(x)$ with
coefficients in some field $F$, the extension of $K$ of $F$ (written
``$K/F$'') containing all of the roots of $p(x)$ in the algebraic
closure of $F$, and the group $\mathbf{Gal}(K)$ of automorphisms of
$K/F$ that fix the elements of $F$.  The fundamental theorem of Galois
theory states that there is a bijection between the subfields of $K/F$
and the subgroups of $\mathbf{Gal}(K)$; namely, subgroups correspond
to their fixed fields.  Using this correspondence, properties of
polynomials can be derived, most famously the fact that quintic
polynomials cannot be solved by algebraic operations and the
extraction of roots.

We do not propose to reconstruct much of the theory here, but note
that already in this basic account there are several steps that seem
compellingly ``blend-like.''

In the first place, 
%that would describes 
% we can describe
% the notion of a field
% extension quite well.  
for field extension, $E$ is an extension of $F$ if $F$ is a subfield of $E$.
We could derive the extension relationship from the input concepts $E$
and $F$ by ``taking everything additional from $E$ and adding it to
$F$.''  This is made specific in the process of \emph{adjoining}
elements,
%elements to a field, 
which simply means to augment 
the field 
%it
with all
fractions of
formal finite sums and products of the adjoined elements with
coefficients in the base field.

Second, the notion of the \emph{splitting field} of a polynomial,
namely the special extension $K/F$ containing all of the roots of
$p(x)$.  This could be formed conceptually by combining the concept
``\emph{the roots of a polynomial $p(x)$ with coefficients in a field
  $F$}'' and the concept ``\emph{a field extension $E/F$ formed by
  adjoining certain elements to $F$}.'' 
% Formally, the roots of $p(x)$
% are not part of the second concept, and they must be put in
% correspondence with the ``certain elements.''  Note that formulating
% the concept of a splitting field in this way is different from proving
% that a splitting field always exists.  It does exist, however, and the proof
% (by induction on the degree of the polynomial) works by successively
% adjoining elements to $F$.  This gives an inkling of the idea that
% blending could be used as a proof step.

As above, we could then form the concept of $\mathbf{Gal}(K)$ by blending
at the conceptual level.  This time, there would be several constituent pieces:
``\emph{the roots of a polynomial $p(x)$ with coefficients in a field $F$},''
``\emph{the splitting field of $p(x)$},''
``\emph{the group of automorphisms of a field extension $E$},''
``\emph{the automorphisms that fix $F$}.''

Finally, assuming that we have built $\mathbf{Gal}(K)$ in this
fashion, we would like to know some of its properties.  Consider the
claim that \emph{elements of $\mathbf{Gal}(K)$ permute the roots of
  $f$}.  This time, instead of being purely conceptual, we want to
work at the \emph{process} level, and consider before-and-after
descriptions of the result of applying $\varphi\in\mathbf{Gal}(K)$ to
some $r$ with the property $p(r)=0$.  This is similar in some ways to
the ``Riddle of the Buddhist Monk'', popularised by \textcite{Koestler64},
which is cited as
an example of the power of blending.\footnote{
  ``A Buddhist monk begins at dawn one day
  walking up a mountain, reaches the top at sunset, meditates at the
  top for several days until one dawn when he begins to walk back to
  the foot of the mountain, which he reaches at sunset.  Making no
  assumptions about his starting or stopping or about his pace during
  the trips, prove that there is a place on the path which he occupies
  at the same hour of the day on the two separate journeys.''}
However, this time the generic space is not a simple geometric machine,
but rather an algebraic machine with several moving parts.

The proof of the claim is as follows.  If $p(r)=0$, then $\varphi
p(r)=\varphi 0$.  Since $\varphi$ is an automorphism, $\varphi 0 = 0$;
and furthermore $\varphi$ distributes over the sums and products that
make up the polynomial $p(x)$ and fixes its coefficients, therefore
$\varphi p(r)=p(\varphi r)$.  Chaining the equalities together, we
have $p(\varphi r)=0$.

In short, the proof is a fairly direct result of combining the
definitions.  \textcite{Goguen92sheafsemantics} suggests that
``combination is colimit.''  Can we realise the proof through (one or
several) colimit operations?  And is there anything special about this
proof?  Apart from these more theoretical questions, the foregoing
discussion raises the following technical issues:

\begin{description}
\item[Field Extension] When reasoning about polynomials, it is useful
  to distinguish the three separate types -- those of $E$, those of
  $F$ and those of $E/F$ as a supertype. Using blending machinery
  removes the distinction between these types.
\item[Splitting Field Extension Theorem] A challenging but creative
  step is to discover the theorem that extending $F$ {\em only} with
  the roots of $f(x)$ forms a field.
\item[Automorphisms] As mentioned in the background section,
  currently there is no way of computing colimits if automorphisms
  are characterised in higher-order logic. An alternative specification,
  or an implementation of colimit computation for higher-order
  logic is needed.

\end{description}

% \input{other-issues}

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