# LIP6 2003/009

- Habilitation

Programmer le Calcul Formel, de L'Algorithmique à la Sémantique - R. Rioboo
- 118 pages - 12/18/2002- document en - http://www.lip6.fr/lip6/reports/2003/lip6.2003.009.pdf - 903 Ko
- Contact : Renaud.Rioboo (at) nulllip6.fr
- Ancien Thème : CALFOR
- Keywords : Computer Algebra, FoC, real numbers
- Publisher : David.Massot (at) nulllip6.fr

My research work has always been centered in Computer Algebra. This is automatic manipulation of mathematical formulas. In order to be able to design algorithms which work on formulas we are lead to use ``exact arithmetics''. We thus work with ``numbers'' whose size is no more fixed.

The first part of this document deals with real algebraic numbers which are a computer algebra approximation of usual real numbers. When computing with roots of polynomials, real algebraic numbers are the analogous of usual real numbers and computations with sequences limits. It is well known that exact arithmetics is decidable over this subset of the real numbers. However none of the techniques used in major computer algebra systems enables to perform ``big computations'' with these numbers.

The main reason for this limitation is that is difficult to express the alternative representations I propose inside inside those systems. By now Axiom is the only language in which we can express efficient algorithms to perform real algebraic numbers manipulations.

When implementing complicated algorithms a programmer is concerned about correction of his program. We want to perform exact manipulations and we have prove the methods we use. We must completely understand the semantics of the programming language we use in order to assimilate the mathematics we prove and the program we implement.

The second part of this document presents the basics of the FoC (http://www-calfor.lip6.fr/foc/) project which purpose is studying tools to program certified algorithms for computer algebra. The programming language offers the programmer a unified framework where he can both state the algorithms and their specifications.

The first part of this document deals with real algebraic numbers which are a computer algebra approximation of usual real numbers. When computing with roots of polynomials, real algebraic numbers are the analogous of usual real numbers and computations with sequences limits. It is well known that exact arithmetics is decidable over this subset of the real numbers. However none of the techniques used in major computer algebra systems enables to perform ``big computations'' with these numbers.

The main reason for this limitation is that is difficult to express the alternative representations I propose inside inside those systems. By now Axiom is the only language in which we can express efficient algorithms to perform real algebraic numbers manipulations.

When implementing complicated algorithms a programmer is concerned about correction of his program. We want to perform exact manipulations and we have prove the methods we use. We must completely understand the semantics of the programming language we use in order to assimilate the mathematics we prove and the program we implement.

The second part of this document presents the basics of the FoC (http://www-calfor.lip6.fr/foc/) project which purpose is studying tools to program certified algorithms for computer algebra. The programming language offers the programmer a unified framework where he can both state the algorithms and their specifications.