TY - JOUR
T1 - Variations on noetherianness
AU - Firsov, Denis
AU - Uustalu, Tarmo
AU - Veltri, Niccol�
N1 - 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.
PY - 2016/4/1
Y1 - 2016/4/1
N2 - 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.
AB - 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.
UR - http://www.scopus.com/inward/record.url?scp=84991672233&partnerID=8YFLogxK
U2 - 10.4204/EPTCS.207.4
DO - 10.4204/EPTCS.207.4
M3 - Conference article
AN - SCOPUS:84991672233
SN - 2075-2180
VL - 207
SP - 76
EP - 88
JO - Electronic Proceedings in Theoretical Computer Science, EPTCS
JF - Electronic Proceedings in Theoretical Computer Science, EPTCS
T2 - 6th Workshop on Mathematically Structured Functional Programming, MSFP 2016
Y2 - 8 April 2016
ER -