On streams that are finitely red. (English) Zbl 1267.03058

Bezem, Marc; Nakata, Keiko; Uustalu, Tarmo

Log. Methods Comput. Sci. 8, No. 4, Paper No. 4, 20 p. (2012).

The article analyses the notion of finiteness in the context of intuitionistic mathematics. Precisely, given an infinite sequence of red or blue elements, the paper compares different definitions of the concept ‘the sequence contains a finite number of red elements’.
Even assuming the sequences to be searchable, it turns out that there are at least six strictly different notions of finiteness, of distinct strength and meaning in a constructive setting. The six variations are: (1) eventually all blue; (2) boundedly red; (3) almost always red; (4) streamless red positions; (5) not not eventually all blue; (6) not infinitely often red. It is shown that (1) implies (2), (2) implies (3), (3) implies (4), (3) implies (5), (4) implies (6), and (5) implies (6). Reverse implications hold when additional assumptions are made, e.g., weak forms of the law of excluded middle, thus revealing the required additional power to prove them.
Finally, the paper compares the above achievements with Coquand and Spiwack’s analysis of finiteness in Bishop’s set theory, obtaining some improved results when the considered sets are assumed to be decidable.
This work gives some non-evident insights to the constructive meaning of finiteness, a recurring theme when results from constructive mathematics are applied to real problems, e.g., in functional programming. Although no application is directly envisaged, the paper provides a clear view of the application of (co)inductive techniques to study constructively a concept. In this sense, the paper is addressed both to constructive mathematicians and to theoretical computer scientists, as both can profitably use its content in their respective fields.

Reviewer: Marco Benini (Buccinasco)

MSC:

03F55

Intuitionistic mathematics

Keywords:

type theory; constructive mathematics; induction; coinduction; finiteness; intuitionistic mathematics