Université de Limoges
The aim of this tutorial is to illustrate how ``soft'' (or ``approximate'') type specifications can be used in Computer Algebra as a frame for exact computations.
Recent results prove that a specification can be defined in a finite number of steps by an ``approximation'' method. The initial specification may be restricted to the main features, at the cost of some errors in less significant details. These errors may be corrected later during the approximation process, ending up with an exact type specification. These results rely on sketch theory.
First, sketch theory is presented by means of examples of type specifications: either usual types, like booleans and natural numbers, or less usual ones, like algebraic numbers.
Then ``soft'' specifications are introduced, together with the main features of the "approximation" process, on examples involving error handling, partiality, overloading, subsorts, global variables.
Sketch theory was introduced by C. Ehresmann in the sixties, and the work presented here is done in collaboration with J.-C. Reynaud, C. Lair, H. Kirchner, among others.