Mardi 19/03/2013, à partir de 14h, en salle Byron Blanc.
Orateur : José Grimm.
Titre : Ordinaux et récursivité.
Résumé :
Dans la théorie des ensembles de Zermelo Fraenkel on peut définir un type particulier d’ensembles, les ordinaux, avec des opérations (somme, produit, puissance), et une relation d’ordre compatible avec les opérations. Les ordinaux généralisent les entiers naturels. Beaucoup de preuves se font par induction transfinie (une variante de l’induction sur les entiers). Il y a beaucoup trop d’ordinaux pour en faire un ensemble (ou un type Coq). On peut définir (par induction transfinie) des suites d’ordinaux epsilon(x), Gamma(x), etc. Si E est l’ensemble des ordinaux plus petits que epsilon(0) ou Gamma(0), E est stable par addition, multiplication, exponentiation, et est dénombrable. On peut le définir dans Coq comme un sous-type inductif via un constructeur constant zero, et un autre de type E→nat→E→E ou E→E→nat→E→E. Je montrerai le lien entre mon implémentation des ordinaux de Bourbaki, et les travaux de Pierre Castéran.
