Lorsque l'on effectue des raisonnements formels sur une notion mathématique, il est utile de disposer de plusieurs points de vue sur les notions envisagées. Certains points de vue pourront être plus adaptés pour faire des calculs tandis que d'autres pourront être plus adaptés pour faire des démonstrations pour des calculs. Un exemple connu est celui des entiers naturels, pour lesquels Péano a fourni des axiomes qui donnent un point de vue très pratique pour des faire des démonstrations et mais pas très efficace pour faire des calculs. Une autre représentation, basée sur la numération binaire, fournit des algorithmes d'addition, de multiplication, et de division bien plus efficaces, mais impose des structures de raisonnements par récurrence moins naturelles. Néanmoins, un système de démonstration sur ordinateur comme Coq, fournit typiquement les deux representations.
Pour les nombres rationnels, l'usage est de les représenter comme des paires d'entiers, la paire p,q représentant le nombre p/q. L'ennui avec cette représentation est que cette représentation n'est pas injective. Nous avons trouvé une famille de représentations mieux adaptées, qui peuvent être mises aisément en relation avec l'algorithme d'Euclide-Gauss pour calculer le plus grand diviseur commun de deux nombre et avec les fractions continues.
L'objectif de ce stage est de formaliser complètement ces nouvelles représentations des nombres rationnels dans le système preuve Coq de façon à montrer que cette représentation est adéquate. Une connaissance raisonnable de l'arithmétique est nécessaire et un goût prononcé pour la preuve sur ordinateur telle qu'on peut la faire dans Coq est préférable.
Tel: 04 92 38 77 39
E-mail: Yves.Bertot@sophia.inria.fr
Station de travail ou PC
2 mois extensible
[1] G. Huet, G. Kahn, C. Paulin-Mohring, The Coq Proof Assistant : A Tutorial : Version 6.1, Rapport Technique INRIA 0204, août 1997.
[2] V. Ménissier-Morain, Arbitrary precision real arithmetic: design and algorithms, soumis pour publication à Journal of Symbolic Computation.