Service interruption on Monday 11 July from 12:30 to 13:00: all the sites of the CCSD (HAL, Epiciences, SciencesConf, AureHAL) will be inaccessible (network hardware connection).
Skip to Main content Skip to Navigation
Preprints, Working Papers, ...

The Algebra of Infinite Sequences: Notations and Formalization

Abstract : We propose some convenient notations for expressing complicated properties of finite and infinite, ordinal-indexed sequences. The algebra of ordinal-indexed sequences is being implemented in the proof-assistant Coq, together with the algebra of ordinals represented in Cantor normal form. 1 Purpose In infinite combinatorics, program verification, and other subjects of mathematical interest, one often encounters a need to describe properties of finite and infinite sequences. For example, a "good" sequence in well-quasi-ordering (wqo) theory is an infinite sequence containing at least one element that is related (in a quasi-ordering) to a subsequent element. We have been seeking convenient notations and operations that would enable us to easily express properties of sequences that are of interest. Not finding anything suiting our needs, we propose some in this note. In programming and proof development, the idea of dependent types has established itself as most useful for various applications. In practice, such types depend either on natural numbers, such as lists depending on a natural number expressing their length, or on a proposition whose proof is required for type-checking purposes. Infinite lists, as studied in this note, will depend instead on ordinals. This paper therefore contains a formalization in Coq of ordinals in Cantor normal form, and their use for formalizing infinite sequences. Proofs of most statements are provided in the online supplement. 2 Finite Paths We begin with the simpler finite case. Let V be a (finite or infinite) alphabet, which we call points (akin to vertices), and let V n be all n-tuples of points, thought of as n-element sequences, which we refer to as paths. The length of a path s 0 , s 1 ,. .. , s n−1 is n, the number of its
Document type :
Preprints, Working Papers, ...
Complete list of metadata

Cited literature [14 references]  Display  Hide  Download
Contributor : Jean-Pierre Jouannaud Connect in order to contact the contributor
Submitted on : Monday, May 11, 2020 - 10:52:25 AM
Last modification on : Sunday, June 26, 2022 - 2:49:37 AM


Files produced by the author(s)


  • HAL Id : hal-02569232, version 1


Nachum Dershowitz, Jean-Pierre Jouannaud, Qian Wang. The Algebra of Infinite Sequences: Notations and Formalization. 2020. ⟨hal-02569232⟩



Record views


Files downloads