• View
• Edit
• History
• Print

ExactRealNumberComputationInAgda

Exact real number computation in Agda

When computing, real numbers are usually approximated by floating point numbers, and it is then necessary to keep the resulting round off errors under control. An alternative approach is however to work with exact computable real numbers. These are infinite sequences (for example Cauchy sequences) which provide arbitrarily close approximations of the number. These sequences are then be implemented as functions or as lazy lists. See for example http://www.dcs.ed.ac.uk/home/mhe/plume/index.html which shows how to implement exact real number computations using streams in Haskell.

Agda is a functional programming language with dependent types. Its type system is more expressive than Haskell, and gives the user the possiblility to express more or less arbitrary logical properties.

The task of this project is to develop a library of functions on real numbers in Agda, and to use the type system to express simple properties on them. Such a library could be used for teaching beginning university students about real numbers and the elements of calculus. In a futuristic approach to teaching, we envisage freshman level mathematics being taught together with functional programming, logic, and numerical analysis. Part of the project could involve thinking about how such a curriculum could be structured.

There is already a substantial literature on the topic of exact real number computations, both in connection with functional languages and in connection with dependent types.

contact person: Peter Dybjer