\documentclass[runningheads]{llncs}
\RequirePackage{url}
\usepackage{graphicx}
\usepackage{alltt}
\input{thol.tex}
\begin{document}
\author{Cezary Kaliszyk and Freek Wiedijk}
\title{Certified Computer Algebra on top of an Interactive Theorem Prover}
\institute{
\{\texttt{cek},\texttt{freek}\}\texttt{@cs.ru.nl} \\
Institute for Computing and Information Sciences,\\
Radboud University Nijmegen, the Netherlands}
\date{\today}
\maketitle{}
\begin{abstract}
We present a prototype of a computer algebra system that is built on top of
a proof assistant, {HOL Light}. This architecture
guarantees that one can be certain that the system will make no
mistakes. All expressions in the system will have precise semantics, and
the proof assistant will check the correctness of all simplifications
according to this semantics. The system actually \emph{proves} each
simplification performed by the computer algebra system.
Although our system is built on top of a proof assistant, we designed the
user interface to be very close in spirit to the interface of systems like
{Maple} and {Mathematica}. The system, therefore, allows the user
to easily probe the underlying automation of the proof assistant for
strengths and weaknesses with respect to the automation of mainstream
computer algebra systems. The system that we present is a
prototype, but can be straightforwardly scaled up to a practical computer
algebra system.
\end{abstract}
\section{Introduction}
%\subsection{Motivation}
% In this paper we study the relationship between two important classes of
% computer programs that manipulate mathematical formulas: proof assistants and
% computer algebra systems.
% A computer algebra system (or `CAS') has at its core a set of algorithms,
% which is made available to the user through a friendly interface. The
% formulas the algorithms of a computer algebra system manipulate generally do
% not have precise semantics. They are simplified in a way that resembles the
% style a mathematician simplifies expressions on paper, but for that the
% symbols that occur in those formulas do not need a mathematical definition
% inside the system.
% On the other hand, the mathematical symbols that occur in proof assistants
% always have precisely defined semantics. Proof assistants not only manipulate
% symbolic expressions, but also theorems that are stated using those symbols.
% The basic activity in a proof assistant is not simplification of expressions
% but proving of theorems. A proof assistant generally does not have many
% algorithms available for automating the application of those theorems, and to
% make use of those that are there one needs to have good knowledge of the
% prover environment. The interface to a proof assistant is generally less
% friendly to a naive user than that of a CAS.
Computer algebra systems do not always give correct answers. This happens
because those systems do not certify the operations
performed. There can be various reasons for errors in a CAS: assumptions can
be lost, types of expressions can be forgotten \cite{aslaksen}, the system
might get confused between branches of `multi-valued' functions, and of course
the algorithms of the system themselves may contain implementation errors
\cite{wester}.
As an example of the kind of error that we are talking about here,
consider the following \textsc{Maple} \cite{maple} session that tries to compute
$\int_0^\infty {e^{-(x-1)^2}\over\sqrt{x}} dx$
numerically in two different ways:
\begin{alltt}
> int(exp(-(x-t)^2)/sqrt(x), x=0..infinity);
\end{alltt}
$${{1\over 2} {e^{-t^2} \Big({-{3 (t^2)^{1\over 4} \pi^{1\over 2} 2^{1\over 2} e^{t^2\over 2} K\!_{3\over 4\rlap{\phantom{\tiny g}}}({t^2\over 2}) \over t^{2\rlap{\phantom{x}}}}} + {\textstyle (t^2)^{1\over 4} \pi^{1\over 2} 2^{1\over 2} e^{t^2\over 2} K\!_{7\over 4}({t^2\over 2})} \Big) \over \pi^{1\over 2}}}$$
\begin{alltt}
> subs(t=1,%);
\end{alltt}
$${{1\over 2} {e^{-1} \big({-3 \pi^{1\over 2} 2^{1\over 2} e^{1\over 2} K\!_{3\over 4}({1\over 2})} + \pi^{1\over 2} 2^{1\over 2} e^{1\over 2} K\!_{7\over 4}({1\over 2})\big) \over \pi^{1\over 2}}}$$
\begin{alltt}
> evalf(%);
\end{alltt}
$$0.4118623312$$
\begin{alltt}
> evalf(int(exp(-(x-1)^2)/sqrt(x), x=0..infinity));
\end{alltt}
$$1.973732150$$
(We are showing \textsc{Maple} here, but all major computer algebra systems
make errors like this.)
To be sure that results are correct, one may use a proof assistant instead of
a CAS. But in that case even calculating simple things, like adding fractions
or calculating a derivative of a polynomial becomes a non-trivial activity,
which requires significant experience with the system.
%\subsection{Approach}
Our approach is to implement a computer algebra system on top of a proof
assistant. For our prototype we chose the LCF-style theorem prover \textsc{HOL
Light} \cite{hollight}. Thanks to this, we obtain a CAS system where the
user can be sure of the correctness of the results. Such a system has strong
semantics, that is all variables have types, all functions have precise
definitions in the logic of the prover and for every simplification there is a
theorem that ensures the correctness of this simplification.\footnote{In
\textsc{HOL Light} \emph{simplification} is implemented through
what in the LCF world is called \emph{conversions}. A {conversion} is a
function that takes a term and returns an equational theorem. The theorem
has the given term on its left side and a simplified version of the term on
the right side.
In this paper `simplification' should \emph{not} be taken to be a fixed
reduction hard-wired into the logic of the proof assistant, the way it is in type
theoretical systems like \textsc{Coq} \cite{coqman}.}
The interface of our computer algebra system resembles most CAS systems. It
has a simple read-evaluate-print loop. The language of the formulas typed into
the system is as close as possible to the language in which formulas are
generally entered in CAS and to the language in which mathematics is done on
paper. Interaction with the system currently looks like this\footnote{
The `\texttt{\&}', `\texttt{Cx}' and `\texttt{\#}' are coercions to real, complex and floating point numbers
}:
\begin{holnb}
In1 := (3 + 4 DIV 2) EXP 3 * 5 MOD 3
Out1 := 250
In2 := vector [\&2; \&2] - vector [\&1; \&0] + vec 1
Out2 := vector [\&2; \&3]
In3 := diff (diff (\Lam{}x. \&3 * sin (\&2 * x) + \&7 + exp (exp x)))
Out3 := \Lam{}x. exp x pow 2 * exp (exp x) + exp x * exp (exp x) +
-- \&12 * sin (\&2 * x)
In4 := N (exp (\&1)) 10
Out4 := #2.7182818284 + ... (exp (\&1)) 10 F
In5 := 3 divides 6 \Conj{} EVEN 12
Out5 := T
In6 := Re ((Cx (\&3) + Cx (\&2) * ii) / (Cx (-- \&2) + Cx (\&7) * ii))
Out6 := \&8 / \&53
\end{holnb}
\begin{holnb}
In7 := x + \&1 - x / \&1 + \&7 * (y + x) pow 2
Out7 := \&7 * x pow 2 + \&14 * x * y + \&7 * y pow 2 + \&1
In8 := sum (0,5) (\Lam{}x. \&x * \&x)
Out8 := \&30
\end{holnb}
%\subsection{Related work}
One can distinguish three categories of systems that try to fill
the gap between computer algebra and proof assistants:
\begin{itemize}
\item Theorem provers inside computer algebra systems:
\begin{itemize}
\item \textsc{Analytica} \cite{analytica98}, %analytica92
\item \textsc{Theorema} \cite{theorema00},
\item \textsc{RedLog} \cite{redlog}, % - logical extension of \textsc{Reduce}
\item logical extension of \textsc{Axiom} \cite{logicalaxiom}.
\end{itemize}
\item Frameworks for mathematical information exchange between systems:
\begin{itemize}
\item \textsc{MathML} \cite{mathml03},
\item \textsc{OpenMath} \cite{openmath},
\item \textsc{OMSCS} \cite{omscs},
\item \textsc{MathScheme} \cite{mathscheme},
\item \textsc{Logic Broker} \cite{logicbroker}.
\end{itemize}
\item Bridges between theorem provers and computer algebra systems, also
referred to as ad-hoc information exchange solutions:
\begin{itemize}
\item \textsc{PVS} and \textsc{Maple} \cite{maplepvs},
\item \textsc{HOL} and \textsc{Maple} \cite{maplehol98},
\item \textsc{Isabelle} and \textsc{Maple} \cite{mapleisabelle},
\item \textsc{NuPrl} and \textsc{Weyl} \cite{weylnuprl},
\item \textsc{Omega} and \textsc{Maple/GAP} \cite{sapper},
\item \textsc{Isabelle} and \textsc{Summit} \cite{isabellesumit}.
\end{itemize}
\end{itemize}
An important distinction that one can make within the category of bridges is
the \emph{degree of trust} between the prover and the CAS. In some of these
solutions the prover uses the simplification of the CAS as an axiom, i.e.,
without checking its correctness. But in other solutions the prover takes the
CAS output and then builds a verified theorem out of it. In this case there
are again two possibilities: either the result is verified independently of
how the CAS obtained it, or the system takes a trace of the rules that the CAS
applied, and then uses that as a suggestion for what theorems should be used
to construct a proof of the result.
In the work that we referred to here either the proof assistant is built
inside the CAS, or the proof assistant and the CAS are next to each other. In
our work however, we have the CAS inside the proof assistant.
Of course in many proof assistants there already is CAS-like functionality,
in particular many proof assistants have arithmetic
procedures or even powerful decision procedures. However, we do not just
provide the functionality, but also build a \emph{system} that can be used in
a similar way as most other computer algebra systems are used.
In our system it is the first time that anyone pursued the
combination of a CAS \emph{inside} a proof assistant (in which all simplifications
are validated), with an interface that has the customary CAS look and feel.
Our way of combining theorem proving and computer algebra has advantages
over the ones presented above. All calculations done by our system are
certified by the architecture of our system. All formulas defined inside it
have types assigned, all defined operators have explicit semantics and all
simplifications performed have theorems associated with them. No translation
of formulas or semantics is needed, as the CAS shares the internal data
structures of the proof assistant. There is no need to worry about mistakes in
the implementation of the CAS, since all conversions are certified using the
logic of the underlying prover. There is no verification required after the
result is obtained, thanks to the creation of theorems alongside with the
results. All simplifications performed by our architecture are completely
certified, that is if a certificate for a particular simplification does not
exist \cite{henk} it can not be performed.
All variables used in \textsc{HOL Light} conversions have to be typed, so
working in a proof assistant might seem less flexible than a traditional CAS
implementation, but the abundance of decision procedures for HOL show that
this probably is not a strong limitation.
%\subsection{Contents}
The paper is organized as follows: in Section \ref{arch} we present the
architecture of the system. In Section \ref{knowledge} we talk about the
knowledge base. Finally in Section \ref{conclusion} we present a conclusion.
\section{Architecture}\label{arch}
We present a general architecture for a certified computer algebra system, and
we will describe an implementation prototype. The source for the prototype is
available from \url{http://www.cs.ru.nl/~cek/holcas/}. For the implementation
we chose the proof assistant \textsc{HOL Light} \cite{hollight}. The factors
that influenced our choice were: the possibility to manipulate terms to create
the conversions, prove theorems and implement the system in the same
language\footnote{\textsc{HOL Light} is written in \textsc{OCaml} and is
provided as an extension of it}, as well as a good library of analysis and
algebra. The system created is rather a proof of concept than a real product,
which is why the efficiency of the underlying prover was not a decisive
factor. In particular we perform all computations inside the proof assistant's
logic, sometimes with the help of decision procedures.
Our system is divided in three independent parts (Fig. 1): the user interface
(input-response loop), the abstract algorithm of dealing with a formula (we
will call this \textit{the CAS conversion}), and the knowledge that is
specific to the CAS system. That architecture allows the user both to use it
as a computer algebra system, as well as making it usable in the context of
theorem proving\footnote{\textit{The CAS conversion} can be applied to a goal
to be proved using \texttt{CONV\_TAC}.}.
\begin{figure}[htb]
\centering
\includegraphics[width=.9\textwidth]{arch}
\caption{Architecture of a CAS inside a TP system with responsibilities of the
parts of our implementation marked. The prover is not marked on the figure,
since all parts make use of it, by using it's type of terms and theorems, as
well as tactics and conversions to build them.}
\end{figure}
\subsection{Input-response loop}
The system displays a prompt, where one can write expressions to be simplified
and commands. It is necessary to distinguish expressions to be computed or
simplified from commands that represent actions that do not evaluate anything,
like listing theorems or modifying and printing assumptions.
Every expression that is not recognized as a command is passed to \textit{the
CAS conversion}, which will try to compute or simplify the expression. The
theorem given back by \textit{the CAS conversion} is the certificate that the
output is correct. If \textit{the CAS conversion} is not able to simplify the
term, it returns an instance of reflexivity, and the result is then the same
as the input.
In most CASs variables can be used without declaring them, but for certain
algebraic operations one can define a variable to be of a particular type
(necessary for example in \textsc{Magma}). Our system can handle expressions
in both ways. The free variables are typed using \textsc{HOL Light} type
inference, but one can also require a specific type with the
\texttt{assumetype} command (described in section 3.4).
Most computer algebra systems allow one to reuse previously typed in
expressions and calculated outputs. One may calculate \texttt{In1 + Out2}. The
loop has to have access to all expressions entered, theorems proved and
outputs. In our framework every expression entered is stored with its type, so
when it is reused, parsing the same expression, even in a different context,
gives the same type.
\subsection{Abstract CAS conversion}
To be able to benefit from the CAS simplification in theorem proving, it is
useful to have the CAS functionality available as a single conversion (that we
call here \textit{the CAS conversion}). Since the underlying prover can be
further developed and new theorems can be proved later, it is useful to
separate \textit{the CAS conversion} from the knowledge that it uses. For
this reason \textit{the CAS conversion} is parametrized. The general idea
behind \textit{the CAS conversion} is to try to apply all sub-conversions from
the knowledge base at all positions in the term until it is saturated
(Fig. 2). Applying the same conversions to a modified term is necessary, since
some conversions return terms, parts of which can be again simplified.
Particular implementations may include mechanisms to increase efficiency or to
provide termination of simplification.
We are not particularly aiming at completeness for the algorithms in \textit{the CAS conversion}, since completeness in practice can
only be realized for rather basic theories.
However any mathematically correct algorithm that exists for
existing computer algebra systems can be implemented as a \textsc{HOL Light} conversion too,
that does the calculation while building the correctness proof in parallel.
Examples include conversions that perform algorithms for
integration, conversions that perform splitting and joining for branching calculations,
or conversions that simplify terms involving higher order operations (like
summation).
\begin{figure}[htb]
\centering
\includegraphics[width=.9\textwidth]{casconv}
\caption{Our implementation of \textit{the CAS conversion} first tries to look
up the term in a built-in cache (for efficiency). If the term is an application
or an abstraction, then it tries to simplify subterms recursively (not
performed if the term is known not to be expandable or is a suggestion that
should not be expanded, for example \texttt{NUMERAL} or
\texttt{assuming}). Finally it tries to apply all conversions from the knowledge
base to the term.}
\end{figure}
\section{CAS-like knowledge}\label{knowledge}
%The knowledge of a computer algebra system is substantially different from
%that of a proof assistant. Usually the main part of a CAS's knowledge
%consists of algorithms that just manipulate formulas, and usually the theory
%on which they are based is not represented inside the system. On the other
%hand, the primary part of a proof assistant is a large collection of
%definitions and theorems.
%There are different possible approaches we implement to the creation of
%theorems that certify correctness of algorithms implementing CAS-style
%simplifications. In certain cases a theorem is built alongside with the term
%analyzed. Sometimes it is sufficient to do a calculation in \textsc{OCaml}
%code and only verify the result in the logic. For example a factorization of
%big integers or polynomials can be simply verified by multiplying them
%out. This is where our approach is similar to the ``bridge'' approach. The
%important difference is that an algorithm for a calculation \emph{together}
%with a certification form a single conversion that can be introduced in the
%knowledge base.
%\subsection{Knowledge base}
The knowledge base is a separate part of the system. The knowledge is kept in
a discrimination net (a structure that allows matching a term to a number of
patterns efficiently). There is an interface on the theorem prover level that
allows introducing knowledge to the knowledge base in the following three
forms:
\begin{itemize}
\item Rewrite rules, for example:\\
\texttt{|- \Fa{}z. abs (norm z) = norm z}
\item Conditional rewrite rules, for example:\\
\texttt{|- \Fa{}x. \&0 <= x ==> abs x = x}
\item Conversions meant to be used with an argument that matches a certain
pattern and return ad-hoc rewrite rules. An ad-hoc rewrite rule is a
theorem that is generated to be used for rewriting the formula, but it is not
added to the knowledge base (although our implementation keeps all rewritten
theorems in cache, implemented as a hash-table, for efficiency reasons).
For example the \textsc{HOL Light} conversion \texttt{DIVIDES\_CONV} takes terms that match the pattern
\texttt{n divides m} and then returns ad-hoc rewrite rules for the given data like
\texttt{|- 33 divides 123453 <=> T}.
\end{itemize}
\textit{The CAS conversion} has to check whether the given term matches one of the
rewrite rules and ad-hoc rewrite rules in the knowledge base. For
efficiency it keeps all theorems and conversions included in the knowledge
base in a discrimination net. To allow matching conversions with even less overhead,
optional patterns for matching associated with conversions can be provided. The
discrimination net is not changed, the particular used instances are only added to
the cache.
%\subsection{Knowledge representation}
To resemble a CAS system, the formulas processed by the system should be in the
``evaluation'' form and not in ``verification'' form.
Let us compare the ways in which one writes differentiation in the
\textsc{HOL Light} library and the way it is written in our CAS:
\begin{alltt}
\Fa{}x. (f diffl (g x)) x \Func{} diff f = g
(f diffl (g x)) x \Func{} diff f x = g x
\end{alltt}
In \textsc{HOL Light} the \texttt{diffl} predicate takes three arguments: the
function (on the left of the predicate), the value of its derivative and the
point. To write a general derivative we need to generalize the point and
replace the value with the derivative function in this point. Even then it is
still a binary predicate.
In most computer algebra systems there exists a simple \texttt{diff} operator,
that takes a function and returns its derivative. Using the Hilbert's choice
operator, we created a such function, defined:
\texttt{diff f = \Lam{}x. \Hilbert{}v. (f diffl v) x}.
We also created a conversion that is able to calculate the derivative of a function, if
\textsc{HOL Light}'s \texttt{DIFF\_CONV} can.
Just like we defined a functional form of differentiation,
we also defined a functional integration operator.
Using these we can then compute the following
expressions in the system:
\begin{holnb}
In9 := dint (\&1,\&2) sin
Out9 := -- \&1 * cos (\&2) + cos (\&1)
In10 := dint (\&1,\&2) (\Lam{}x. x pow n)
Out10 := \&1 / \&(n + 1) * \&2 pow (n + 1) +
-- \&1 * \&1 / \&(n + 1) * \&1 pow (n + 1)
In11 := diff (diff (\Lam{}x. \&3 * sin (\&2 * x) + \&7 + exp (exp x))) (\&2)
Out11 := exp (exp (\&2)) * exp (\&2) pow 2 + exp (exp (\&2)) * exp (\&2) +
-- \&12 * sin (\&4)
In12 := diff (\Lam{}x. dint (x,x + \&2) (\Lam{}x. x pow 3))
Out12 := \Lam{}x. \&6 * x pow 2 + \&12 * x + \&8
\end{holnb}
%If a function is not differentiable, or the system does not know how to
%differentiate it, then the conversion is not able to simplify it, and the input is
%returned unchanged.
Our differentiation and integration definitions
do not work well with partial functions. An approach for defining them in such a way that
partial functions are handled better will be described in Section \ref{conclusion}.
\subsection{Numerical approximations}
In complex calculations computer algebra systems provide users with numerical
approximations. They are usually implemented with an approximation algorithm,
which keeps an error bound with every calculation. In a proof assistant a
numerical approximation must have its semantics completely defined, and the
algorithm has to respect the approximation definition and theorems that specify
its properties.
The two main ways of rounding a real number are down to an integer and towards
the nearest integer. Both these operations do
not give rise to a computable function (see for example \cite{lester}). In
\cite{vuillemin} it is shown that if one computes non-deterministically either one
of those values then one does get a computable function. We will use a conversion
that calculates the value rounded both down and to nearest value, that terminates
when one of those calculations terminate.
We propose to define the numerical approximation of a given number \texttt{x}
to a precision \texttt{p} as identical to the number itself: \texttt{N x p =
x}. It is only a hint for the system that the number has to be simplified to
a decimal fraction plus a rest. It is the rest, that determines in which form
is the number given: rounded down or rounded to the nearest. For rest defined
in this way we provide a theorem, that states that the approximation can be
different from the exact value only on the last digit, and the difference
is less than one.
In the following \textsc{HOL Light} definitions, \verb|N| is the numerical
approximation of a number to a precision (following the convention of
\textsc{Mathematica}) and \verb|...| is the rest of a number to the given
precision with an additional argument that specifies the form of the
rest. \verb|T| stands for rounding to nearest and \verb|F| stands for rounding
down.
\begin{holnb}
... x p F = x - floor (&10 pow p * x) / &10 pow p
... x p T = x - floor (&10 pow p * x + &1 / &2) / &10 pow p
|- abs(... x p v - x) < &1 / &10 pow p
\end{holnb}
The system is able to compute some numerical approximations with this scheme:
\begin{holnb}
In13 := N (\&1 / \&3) 8
Out13 := #0.33333333 + ... (\&1 / \&3) 8 F
In14 := N (sqrt #5.123456789) 8
Out14 := #2.26350542 + ... (sqrt #5.123456789) 8 F
In15 := N (dint (#0.1,#0.4) exp) 7
Out15 := #0.3866537 + ... (-- \&1 * exp #0.1 + exp (\&2 / \&5)) 7 F
\end{holnb}
\subsection{Assumptions}
In most CASs there is a possibility to make type assumptions or binary
assumptions about variables. Examples include assuming a variable to be
greater than zero, greater than another variable, natural or real. There are
various methods of introducing assumptions in computer algebra systems:
\begin{itemize}
\item Assumptions associated with a simplification\\
in \textsc{Mathematica}: \verb|Simplify[Sin[n Pi], Element[n,Integers]]|
\item Global list of assumptions\\
in \textsc{Maple}: \verb|assume(x>0); sqrt(x*x);|
\item Asking the user for conditions on variables (e.g. \textsc{Maxima})
\item Adding assumptions automatically and silently to the prover environment
(e.g. \textsc{MathXpert})
\end{itemize}
In our system we keep a global list of assumptions, which are Boolean
properties that may be later used to instantiate assumptions of rewrite rules
and ad-hoc rewrite rules. In a big CAS the number of rules that can be used is
so big that asking the user seems not to be a good choice. Also automated
assuming will probably not behave too well in such a situation.
An assumption can be introduced by the user either using \texttt{assume},
which takes a Boolean, or \texttt{assumetype} which takes a typed variable.
An assumption associated with a single simplification of a sub-term may be
also introduced using \texttt{assuming}. The latter method temporarily changes
the assumptions list to simplifying the sub-expression. The assumptions will
be added to the assumptions of the theorem generated by \textit{the CAS
conversion}, which is why changing the assumptions list is only useful at
the top-level of the expression to simplify.
The global list of assumptions is used by the conversions from the knowledge
base, therefore we consider is a part of the latter. To ensure the usage of
variables with correct types, type checking has to have access to this list.
When an expression is typed in the system it is type-checked in a particular
context. This context includes types already assigned to all free variables
from the assumptions list, as well as all variables for which types have been
assumed with \verb|assumetype|. To do this, the latter are kept in another
global list.
\looseness=-1
For example, $\sqrt{x^2}$ cannot be simplified to $x$, since we don't know whether
$x$ is positive or not. Also $\frac{x}{x}$ cannot be simplified to $1$, since
it is possible that $x = 0$.
\begin{holnb}
In16 := sqrt (x * x)
Out16 := abs x
In17 := x / x
Out17 := x * inv x
\end{holnb}
When an assumption about $x$ is introduced, stating that it is greater then
$1$, numeric things about $x$ can be proved, and both of the above formulas
can be simplified:
\begin{holnb}
In18 := assume (x > \&1)
Out18 := T
In19 := x > #0.5
Out19 := T
In20 := sqrt (x * x)
Out20 := x
In21 := x / x
Out21 := \&1
\end{holnb}
There are two ways in which assumptions are used: direct and indirect. The
first way is to use an assumption directly in the derivation in unchanged
form. It can be used to a prove a reflexive theorem or to fill the requirement
of a certain conditional rewrite rule (or a conditional ad-hoc rewrite rule).
An assumption may be used as an indirect step in the derivation, for
example simplifying $abs(x)$ to $x$ requires $x \ge 0$, and the assumption $x
> 1$ can be used for this.
\subsection{Manipulating assumptions}
A CAS has to provide a mechanism for adding assumptions and listing defined
assumptions. In our prototype we added the \texttt{assumptions} and
\texttt{about} commands, which resemble their \textsc{Maple} equivalents.
\begin{holnb}
Command: about Argument: x
`x > &1`
\end{holnb}
An issue that is hard to handle in any approach are errors that may be caused
by incorrect parsing and printing. We try to be as close as possible to the
original \textsc{HOL Light}'s parsing and printing mechanism. In fact, the
system currently uses HOL's term printing (with special output for errors)
but, when parsing, the system has to add typing information and distinguish
commands from terms. Special output is added, so that the user always knows
when a given string has been interpreted as a command.
To further lower the risk of parsing and printing problems, we add the
\texttt{theorems} command. It allows printing all theorems defined in a
session. The standard \textsc{HOL Light} theorem printing function is used for
this. It is especially useful for conversions that use assumptions, because in
that it case the assumptions that have been actually used will be shown.
Below are the first five theorems proved by the examples from this document:
\begin{holnb}
Command: theorems
|- (3 + 4 DIV 2) EXP 3 * 5 MOD 3 = 250
|- vector [&2; &2] - vector [&1; &0] + vec 1 = vector [&2; &3]
|- diff (diff (\Lam{}x. &3 * sin (&2 * x) + &7 + exp (exp x))) =
(\Lam{}x. exp x pow 2 * exp (exp x) + exp x * exp (exp x) +
-- &12 * sin (&2 * x))
|- N (exp (&1)) 10 = #2.7182818284 + ... (exp (&1)) 10 F
|- 3 divides 6 \Conj{} EVEN 12 <=> T
\end{holnb}
\section{Conclusion}\label{conclusion}
Our work integrates computer algebra and proof assistant technology. We will
now look at how our architecture compares with what one gets by just having a
CAS or a proof assistant.
Developing a system according to our architecture (i.e., where the algorithms
not only generate the results, but also generate certificates of the
correctness of those results) will be slower than the development of
traditional CAS systems (because that only has to generate the results). As
far as the performance of the system is concerned, our architecture will be
somewhat slower than a traditional CAS as well. This is mostly because
generating the certificates for all simplifications also takes time.
However, we expect this slow-down over traditional CAS
to only multiply the running time by a constant factor. Our expectation is not
experiment based, but based on the architecture, we trace what a traditional
CAS does and provide proofs for every step.
When we compare our architecture to the way that one normally does CAS-like
manipulations in an interactive theorem prover, the main difference is the
interaction model. Our CAS system does not interactively work on propositions
that are to be proved, but instead takes an expression and automatically
simplifies it.
%\subsection{Future work}
Our primary focus is to extend the knowledge base with a formalization of
multivalued functions, to be able to handle more complicated expressions, like
the \textsc{Maple} example of a complex function with multiple branches given
in the introduction.
Another important feature that we plan to investigate are the coercions that
many proof assistants use, like the embedding of the integers in the real
numbers or the real numbers in the complex numbers. Currently a user of our
prototype needs to use the `\texttt{\&}' and `\texttt{Cx}' symbols for this
(as is customary in the \textsc{HOL Light} library). A small improvement to
the current situation might be to overload the `\texttt{\&}' operator, but we
would rather not make the user write these functions at all.
An issue that our approach does not cover is completeness of the conversions.
In the case of rewrite rules the completeness is clear. But in the case of
arbitrary algorithms, it is not guaranteed by our architecture that a given
conversion will always terminate and never fail.
%\subsection{Outlook}
% We presented an architecture for a certified computer algebra system, and
% addressed some issues that were encountered when using this architecture. We
% also presented the details of a prototype of our architecture that was
% implemented on top of a state-of-the-art proof assistant. Although the
% prototype is not a powerful CAS at the moment, we believe it can be extended
% into one, just by extending the knowledge base that the system uses.
We believe that both computer algebra systems and proof assistants currently
have a problem. In computer algebra the lack of explicit semantics and the
lack of verification of the results inside the system makes the systems less
reliable than one would like them to be. In proof assistants the powerful
symbolic manipulations that are taken for granted in computer algebra often
are missing and, even when present, it takes work and expertise to make use of
it.
We claim that the architecture that we present here can solve both problems
simultaneously. The computer algebra systems will get explicit semantics and
certification. And the proof assistants will get CAS-like functionality that
will make them more powerful and easier to use than they are today.
\bibliographystyle{plain}
\bibliography{all}
\end{document}