Implementation of three types of ordinals in Coq - Archive ouverte HAL Access content directly
Reports (Research Report) Year : 2013

Implementation of three types of ordinals in Coq

(1)
1

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
Fichier principal
Vignette du fichier
RR8407.pdf (672.99 Ko) Télécharger le fichier
Origin : Files produced by the author(s)
Loading...

Dates and versions

hal-00911710 , version 1 (29-11-2013)

Identifiers

  • HAL Id : hal-00911710 , version 1

Cite

José Grimm. Implementation of three types of ordinals in Coq. [Research Report] RR-8407, INRIA. 2013, pp.74. ⟨hal-00911710⟩
542 View
497 Download

Share

Gmail Facebook Twitter LinkedIn More