Implementation of three types of ordinals in Coq

José Grimm 1
1 MARELLE - Mathematical, Reasoning and Software
CRISAM - Inria Sophia Antipolis - Méditerranée
Abstract : One can define an inductive type T in Coq by the rules: zero is in T, and 'cons a n b' is in T when a, b are in T and n is an integer. One can embed this type with an ordering, and show that the subset of ''normal'' elements is well-ordered, thus corresponds to some ordinal, namely epsilon-zero, the least epsilon-ordinal of Cantor. The same construction can be applied to the case where cons take one more argument of type T; in this case we get the Feferman-Schütte ordinal Gamma-zero. These two type were implemented by Castéran in Coq. In these paper we present an implementation using the ssreflect library. One can consider the case where cons takes four arguments of type T and use the ordering function proposed by Ackermann. This gives some large ordinal. The proof in Coq that it is a well-ordering matches exactly that of Ackermann. Every limit ordinal in this type is (constructively) the supremum of a strictly increasing function. Finally, we show how these types are related to ordinals defined in an implementation of the theory of sets of Bourbaki (a variant of Zermelo-Fraenkel). The code is available on the Web, under http://www-sop.inria.fr/marelle/gaia
Type de document :
Rapport
[Research Report] RR-8407, INRIA. 2013, pp.74
Liste complète des métadonnées

Littérature citée [30 références]  Voir  Masquer  Télécharger

https://hal.inria.fr/hal-00911710
Contributeur : José Grimm <>
Soumis le : vendredi 29 novembre 2013 - 16:33:00
Dernière modification le : jeudi 11 janvier 2018 - 16:24:43
Document(s) archivé(s) le : lundi 3 mars 2014 - 20:20:34

Fichier

RR8407.pdf
Fichiers produits par l'(les) auteur(s)

Identifiants

  • HAL Id : hal-00911710, version 1

Collections

Citation

José Grimm. Implementation of three types of ordinals in Coq. [Research Report] RR-8407, INRIA. 2013, pp.74. 〈hal-00911710〉

Partager

Métriques

Consultations de la notice

457

Téléchargements de fichiers

283