Abstract
In constructive mathematics, several nonequivalent notions of finiteness exist. In this paper, we continue the study of Noetherian sets in the dependently typed setting of the Agda programming language. We want to say that a set is Noetherian, if, when we are shown elements from it one after another, we will sooner or later have seen some element twice. This idea can be made precise in a number of ways. We explore the properties and connections of some of the possible encodings. In particular, we show that certain implementations imply decidable equality while others do not, and we construct counterexamples in the latter case. Additionally, we explore the relation between Noetherianness and other notions of finiteness.
| Original language | English |
|---|---|
| Pages (from-to) | 76-88 |
| Number of pages | 13 |
| Journal | Electronic Proceedings in Theoretical Computer Science, EPTCS |
| Volume | 207 |
| DOIs | |
| Publication status | Published - 1 Apr 2016 |
| Event | 6th Workshop on Mathematically Structured Functional Programming, MSFP 2016 - Eindhoven, Netherlands Duration: 8 Apr 2016 → … |
Bibliographical note
Funding Information:This research was supported by the Estonian Ministry of Education and Research institutional research grant no. IUT33-13, the Estonian Science Council personal research grant no. PUT763 and the Estonian Science Foundation grant no. 9475.
Publisher Copyright:
� 2016, Open Publishing Association. All rights reserved.