The Funded Proposals from MathFIT 2001

Below are the proposals funded by MathFIT as a result of the MathFIT 2001 Call (text is included to give a flavour of the intended research).

• Accurate Simplication of Elementary Functions
  Investigators: Professor J.H. Davenport, Dr. R.J. Bradford (University of Bath)

  "That 'the square root of z squared equals z' is not always true: consider when z is equal to –1. What of 'the square root of (z squared - 1) equals the square root of (z - 1) multiplied by the square root of (z + 1)'? While algebraic identities have been much studied, there are essentially no formal methods for studying identities between functions, complete with branch cuts and special cases. This project proposes to develop some, based on analysing, using techniques from quantifier elimination and cylindrical algebraic decomposition, the geometry of C (or C to the power n) induced by the various branch cuts, and hence determining the truth (or falsity) of the proposed identity on each region."

• Geometry of Interaction and the Foundations of Reversible and Quantum Computing
  Investigator: Professor S. Abramsky (Oxford University)

  "We will develop a structural approach to quantum computing, using ideas from Geometry of Interaction and Linear Logic. We will seek a form of Curry-Howard correspondence for quantum computation, and more generally to develop logics, type theories and process calculi with a quantum-computational interpretation, as a basis for a high-level approach to programming quantum computations. The semantic and logical basis for these formalisms will come from a quantum version of Geometry of Interaction. The mathematical aspects of these models will be studied using tools from inverse semigroup theory and category theory. We will also seek implicit characterizations of quantum complexity classes, similar to what has been done for classical complexity classes with logical systems such as Light Linear Logic. We will also be concerned to relate our high-level approach to concrete issues in quantum algorithms and implementation."

• Modelling and Optimising Reliabilty in Dynamic Communications Networks
  Investigators: Dr. J. van den Heuvel (LSE) Mr. S. Hurley, Dr. S.M. Allen, Dr. R.M. Whitaker (Cardiff University)

  "We aim to devise computational, provably efficient methods for the design of dynamic communications networks. Much work has been on the development of algorithms and theoretical metrics for reliable network design. However there is an increasing requirement to take into account dynamic aspects of networks, for example either through node movement or edge or node failure. The proposed research will initially formulate a suitable mathematical model taking into account both the theoretical mathematical and computational issues. This will then be used for the simulation of dynamic networks and will include a realistic traffic model. Suitable reliability metrics based on connectivity measures will be developed together with the deviation of lower and upper bounds on these metrics. This information will be incorporated into an effective optimisation algorithm for the design process. In particular the optimisation algorithm will probably be based on a multi stage process incorporating meta-heuristic methods. The initial stage would generate an initial reasonably good network that aims to partially satisfy some of the objectives. The second optimise stage takes the initial network design and aims to produce a design that satisfies all the objectives as well as possible by using more computationally intensive local search."

• New Factoring-Based Cryptosystems
  Investigators: Dr. S.D. Galbraith, Dr. J.F. McKee (Royal Holloway, University of London)

  "There are numerous public key cryptosystems using composite integers, however the security of the cryptosystems depends on the hardness of computational problems which are different from the integer factorisation problem. Some of these problems have only recently been explicitly stated and it is an important problem in computer science to determine the security of these cryptosystems. The expertise needed to study these problems is not generally available in the computer science community and so a new interaction between mathematics and computer science is needed. This project will apply the full power of computational number theory and algebraic geometry to study these new computational problems. The results of this study will determine the security of the corresponding cryptosystems and will be of great interest to computer science and the wider applications of cryptography in the business world."

• Pythagorus: Machine Support for Semi-Formalised Proof Oriented Mathematics
  Investigators: Professor Z. Luo (University of Durham), Professor P. Aczel (University of Manchester)

  "Machine support for both numerical and symbolic computational mathematics has been very successfully used in mathematics, science and education. This proposal aims to investigate the issues involved in the achievement of such support for proof oriented mathematics. We believe that the theory and technology of interactive theorem proving can be effectively applied to building tools to help research mathematicians as well as students of mathematics in their proof development effort. We believe that a key to this is to focus not on the full formalisation of mathematics but on what we here call semi-formalised mathematics. This is mathematics which is completely formal as far as the formulation of definitions and results is concerned, but where proofs are allowed to have steps which may not be instances of rules of inference, but instead are documented with various kinds of less formal evidence for the step. We shall study the theory and techniques needed to build supporting computer environments for the development and presentation of semi-formal mathematics. Our method is to implement a generic environment based on an existing proof development system. We will develop and implement techniques of meta-variables in multiple-contexts that will provide effective support for the representation and development of semi-formal proofs. The evaluation will be conducted via case studies for educational uses of our tools in Mathematics and Computer Science courses."

• Quantum Computing and Algorithms in Group Theory
  Investigators: Dr. A.J. Duncan, Dr. S.E. Rees (University of Newcastle), Professor S.L. Braunstein (Bangor University)

  "We propose to develop quantum algorithms in the setting of computational group theory. We shall survey existing quantum algorithms (based mostly on Shor’s and Grover’s algorithms) to see how these may be applied to problems in computational group theory. We shall go on to develop new quantum models to address problems of group theory. We shall consider in particular algorithms for the word problem in free groups, where previous results suggest we should expect advances. This should lead to consideration of algorithms for other problems in finitely presented groups: for example the conjugacy or power problem. The eventual aim is an efficient quantum version of Makanin’s algorithm for equations in a free group (or semigroup). Routines for integer matrix manipulation, which play a large part in computational group theory as well as having many other applications, will also be considered. Once we have developed new quantum algorithms we shall compare their complexity to traditional procedures. This is of particular interest where random or parallel algorithms address the problem in question. We shall develop computer simulations for quantum algorithms and use these to compare them experimentally to traditional methods. Once we have established a reasonable library of quantum algorithms we shall try to understand how to transform standard algorithms into corresponding fast quantum algorithms."

• Sources of Long Range Dependence in Internet Traffic and their Relative Importance in Networks
  Investigators: Professor D.K. Arrowsmith, Professor J.M. Pitts (Queen Mary, University of London), Professor M.M. Dodson, Professor M.J. Smith (University of York)

  "Data from existing and from new sources will be analysed to determine whether LRD (Long Range Dependence) is present. This analysis will encompass single machines and applications to see which applications may lead directly or indirectly to LRD and multifractal behaviour. The collected data will be compared with the output of iterated maps which have long been used as a source of LRD behaviour. Parameters will be chosen to replicate the statistical nature of real traffic as closely as possible. Simulation results will be used with a new simulation model to provide insight into the aggregation of LRD processes. The parameters of the simulation will be informed by our earlier measurements (see above) and a variety of network topologies will be investigated. An existing mathematical model of TCP traffic will be extended to allow the investigation of the interaction between co-existing flows on the same infrastructure. This mathematical model will be investigated using parameters from our real measurements (see above)."

• Surface Reconstruction from Gauss Maps
  Investigators: Professor E.R. Hancock, Dr. R.C. Wilson, Dr. I. McIntosh (University of York)

  "The proposed research aims to develop the computational and mathematical framework for reconstructing surfaces from their Gauss maps. The main challenge here is to find curvature on energy minimising paths through the Gauss map. Once this path is to hand, then the height reconstruction process is a straightforward one which involves only the application of Eulers method. At York, we have already developed a computationally effective algorithm for this process which uses a graph-spectral characterisation based on the leading eigenvector of a curvature property matrix. The research proposed here aims to establish a mathematical framework for the process. We will commence by using stochastic geometry to pose the recovery of a curvature minimising path in a variational setting using stochastic differential equations. To apply this apparatus to the location of curvature minimising paths, we will require a probabilistic characterisation of the Guass-maps and the site transitions undergone by the path. Finally, we will demonstrate the utility of the resulting surface reconstruction algorithms on surface normal data delivered by shape-from-shading and shape-from-texture."