Symbolic computation (also known as computer algebra)
refers to the study and development of algorithms and software for manipulating mathematical expressions and objects.
It leads to exact answers, and is distinct from numerical computation which uses floating point arithmetic to give approximate results.
Instead of decimals symbolic systems use integers (whole numbers) which may be combined to represent rational numbers (fractions).
We can go further and represent algebraic numbers by describing them as the roots of polynomials,
(such as defining √2 to be the positive root of x2-2).
A Visualisation of the algebraic numbers in the complex plane by Stephen J. Brooks. Click on the image for more details.
There is a wide variety of computer algebra software available,
with a comparison of the features here. I mostly work with Maple,
but our research is applicable to generic systems.
Symbolic computation has been applied in many areas, such as space technology (engineering CanadaArm) and animation (Dreamworks movies).
For a more thorough introduction see this presentation by Stephen Watt.
The image of CanadaArm2 is from NASA (click on the image for more details).
a decomposition - splits the domain into connected cells;
algebraic - each cell is described by polynomial relations;
cylindrical - the cells are arranged in a useful structure.
CADs are usually constructed in increasing dimension. For example, the plot shows how a CAD for a sphere comes first from a CAD of the line and then the plane.
Usually CADs are constructed so that given polynomials are sign-invariant (either positive, negative or zero) on each cell.
The first algorithm was given in the 70s and since then there have been many improvements and refinements.
Even so, CADs still usually contain far more information (decomposes into more cells) than required for most applications.
Application of CAD
The potential applications of CAD are huge: almost any problem that can be described by polynomials!
It was originally introduced for quantifier elimination and simplification of logical formulas.
This in turn has numerous applications, ranging from engineering to epidemic modelling.
CAD itself has been used for equation solvers (for example in Maple)
One application pursued by our group is improvements to the algebraic simplification of elementray function identities via branch cut analysis, (see the research section below).
We are also considering applications to robot motion planning, (with the robots and their environment described by polynomials).
The image is a CAD produced to study the problem of moving a ladder round a right angled corridor. Robots encounter this type of situation and need to find the best path.
Bath has much expertise in the field of robotics in the Robotics and Autonomous Systems Lab.
The main topics of my research in this area are summarised below.
The references refer to papers listed under Publications.
TTICAD
Truth table invariant CAD
In [BDEMW13] we have developed a new CAD algorithm which instead of producing sign-invariant CADs gives one that is truth-table invariant - clauses of formulae have constant truth value (true or false) on each cell.
This gets far closer to the minimal information required for most applications.
For example suppose we care about the truth of
\Phi:= (f1 = 0 /\ g1 < 0 ) \/ (f2 = 0 /\ g2 < 0 )
where f1 and f2 are the circles below and g1 and g2 the hyperbolas.
The new algorithm only identifies the solid green lines when projecting down while a sign-invariant algorithm would also identify the dotted lines.
The algorithm has implemented in Maple as part of the ProjectionCAD package described below. We recently extended the algorithm to work in the most general cases in [BDEMW14].
Problem Formulation
Problem formulation for CAD algorithms
All CAD algorithms are sensitive to problem formulation. For example, the images below represent two CADs for the same curve, which differ only in the ordering of the variables used.
Assuming y>x leads to a CAD with 11 cells while x>y leads to a CAD with 3 cells. For more complicated problems the formulation can determine the feasbility of producing a CAD.
In [BDEW13] we consider these issues introducing a new measure of CAD complexity and heuristics to use when formulating problems for CAD algoriothms.
Then in [HEWDP14] we evaluate these heuristics on a large data set, while in [HEWDPB14] we investigate how machine learning can be used to build a meta heuristics superior to the individual ones.
More generally, in [WDEB13] we show how an alternative logical formulation of the piano mover's problem can change the feasbility of studying the problem using CAD.
[England14] is a survey article on the issue of problem formulation for CAD.
Note also that the alternative CAD computation scheme based on regular chains has its own issues of problem formulation (see that section below).
Sub-CAD
Sub-CAD
We define a Sub-CAD as a subset of the set of cells of a CAD. In [WBDE14] we presented algorithms to produce sub-CADs of cells lying on prescribed varieties and sub-CADs of cells with a prescribed dimension or higher.
For example, the first image below identifies all cells in a CAD (with a black circle) while the second only the full dimensional ones (with different colours).
Sub-CADs can be sufficient to solve certain problems (for example, systems of strict inequalities will have solutions described by full dimensional CAD cells only).
We have also investigated how they may be used as heuristics for choices of problem formulation in [WEBD14].
ProjectionCAD
The ProjectionCAD Package in Maple
We have developed a Maple package titled ProjectionCAD for producing CADs via projection and lifting.
The package is in contrast to the built-in Maple CAD command which uses the theory of Regular Chains. However, it makes use of some RegularChains commands, giving output in the same format.
The functionality and implementation is discussed in [EWBD14], with more details in the technical reports [England13a, England13b].
The ProjectionCAD webpage has hosts the latest code.
The code can produce CADs which are: sign-invariant, order-invariant, invariant with respect to equational constraint and truth-table invariant. There are also commands for choosing the best problem formulation for the CAD algorithms.
[England13a] describes how this package is the only implementation of McCallum's delineating polynomials and the only package to offer order-invariant output.
[England13b] describes how the equational constraints commands offer not only improved projection but also improved lifting, as well as extensions to the original TTICAD algorithm.
CAD by RegularChains
CAD by RegularChains
Recently an alternative construction scheme for CAD was developed.
Instead of projecting down through real space and then building solutions back up, it instead first creates a cylindrical complex decomposition (CCD) of complex space (upon which the real root isolation is applied to refine to a CAD).
The CCD is built using the theory of triangular decomposition by regular chains (and the well developed technology of the RegularChains Library for Maple.
We recently worked with the authors of the RegularChains Library to develop there technology to produce TTICADs, described in [BCDEMW14]
The implementation is now part of the RegularChains Library. The regular chains construction is also sensitive to the variable ordering, an issue studied in [EBDW14].
However, the incremental nature of the construction means it is sensitive to a new issue, the order in which constraints are presented, as studied in [EBCDMW14].
These studies developed new heuristics for the individual problems, but an open question is how best to address the issues in tandem.
Simplification
Algebraic simplification
Many formulae thought universally true are in fact not. For example √(x)√(y) = √(xy) is not true for x=y=-1, (where √(x) is refering to the positive root).
Mathematically this is because there are actually two choices of root and in this case the formula requires the other.
However, computer algebra systems tend to work with the single valued counterparts of such multi-valued functions, leading to these problems.
As a result, most computer algebra software is very cautious about simplifying formulae, often leading to answers more complicated than may be neccessary.
Key to understanding when such formulae hold are branch cuts - lines over which inverse functions like square root are discontinuous.
They can be thought of as the curves where the different sheets of a multi-valued function come together, such as in this figure for the Riemann surface of the square root function.
We are working on improving simplification technology using CAD.
The rough scheme is to (1) identify branch cuts as polynomial relations (2) construct from these a CAD (3) test the proposed simplification in each cell.
[DBEW12] examines how such technology could affect programming with complex numbers.
Branch Cuts
Branch cut calculation and visualisation
To build the simplification technology we need to first calculate the branch cuts of mathematical expressions.
We have considered various algorithms leading to a classification of the types of cuts.
A package of code has been developed, distributed with Maple 17, which calculates and visualises the branch cuts of univariate functions;
either directly through a 3d numerical plot or implicitly by a 2d interpretation of the algebraic output. The work is described in [EBDW13, EC-TBDW14].
Useful Links
•
A key textbook gathering together much of the research into CAD and quantifier elimination is this 1998 text.
•
The original algorithm of Collins is described in this freely available report by Arnon, Collins and McCallum.
•
There are various CAD implementations such as QEPCAD a freely available interactive command line program that implements partial CAD.
Another key implementation is that in Maple which uses a different approach via Regular Chains.
Other implementations include Mathematica,
Redlog and SyNRAC.
