Skip to Main content Skip to Navigation

# The Algebra of Infinite Sequences: Notations and Formalization

4 DEDUCTEAM - Deduction modulo, interopérabilité et démonstration automatique
Inria Saclay - Ile de France, LSV - Laboratoire Spécification et Vérification
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]

https://hal.inria.fr/hal-02569232
Contributor : Jean-Pierre Jouannaud <>
Submitted on : Monday, May 11, 2020 - 10:52:25 AM
Last modification on : Wednesday, June 2, 2021 - 3:41:06 AM

### File

AlgebraOfInfiniteSequences.pdf
Files produced by the author(s)

### Identifiers

• HAL Id : hal-02569232, version 1

### Citation

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

Record views

Files downloads