LIPIcs.TYPES.2014.187.pdf
- Filesize: 484 kB
- 15 pages
Document
Investigating Streamless Sets
Author
-
Part of:
Volume:
20th International Conference on Types for Proofs and Programs (TYPES 2014)
Series: Leibniz International Proceedings in Informatics (LIPIcs)
Conference: International Conference on Types for Proofs and Programs (TYPES) - License:
Creative Commons Attribution 3.0 Unported license
- Publication Date: 2015-10-12
Cite As Get BibTex
Erik Parmann. Investigating Streamless Sets. In 20th International Conference on Types for Proofs and Programs (TYPES 2014). Leibniz International Proceedings in Informatics (LIPIcs), Volume 39, pp. 187-201, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2015)
https://doi.org/10.4230/LIPIcs.TYPES.2014.187
Abstract
In this paper we look at streamless sets, recently investigated by Coquand and Spiwack. A set is streamless if every stream over that set contain a duplicate. It is an open question in constructive mathematics whether the Cartesian product of two streamless sets is streamless. We look at some settings in which the Cartesian product of two streamless sets is indeed streamless; in particular, we show that this holds in Martin-Loef intentional type theory when at least one of the sets have decidable equality. We go on to show that the addition of functional extensionality give streamless sets decidable equality, and then investigate these results in a few other constructive systems.
Subject Classification
Keywords
- Type theory
- Constructive Logic
- Finite Sets
Metrics
- Access Statistics
-
Total Accesses (updated on a weekly basis)
0PDF Downloads
References
-
Michael Beeson. Goodman’s theorem and beyond. Pacific Journal of Mathematics, 84(1):1-16, 1979.
- M. Bezem, K. Nakata, and T. Uustalu. On streams that are finitely red. Logical Methods in Computer Science, 2011. URL: http://www.cs.ioc.ee/~keiko/papers/finiteness.pdf.
- The Coq Development Team. The Coq Reference Manual, version 8.4, August 2012. Available electronically at URL: http://coq.inria.fr/doc.
-
Thierry Coquand and Arnaud Spiwack. Constructively finite? In Contribuciones científicas en honor de Mirian Andrés Gómez, pages 217-230. Universidad de La Rioja, 2010.
-
Per Martin-Löf. An intuitionistic theory of types: predicative part. In H. E. Rose and J. C. Shepherdson, editors, Proceedings of the Logic Colloquium 1973, volume 80 of Studies in Logic and the Foundations of Mathematics, pages 73-118. North-Holland, 1975.
-
Per Martin-Löf and Giovanni Sambin. Intuitionistic type theory, volume 17. Bibliopolis Naples, 1984.
-
F. P. Ramsey. On a problem of formal logic. Proceedings of the London Mathematical Society, 2(1):264-286, 1930.
-
F. Richman and G. Stolzenberg. Well quasi-ordered sets. Advances in Mathematics, 97(2):145-153, 1993.
-
Anne Sjerp Troelstra and Dirk Van Dalen. Constructivism in mathematics, volume 2. Elsevier, 1988.
- The Univalent Foundations Program. Homotopy Type Theory: Univalent Foundations of Mathematics. http://homotopytypetheory.org/book, Institute for Advanced Study, 2013.
-
Wim Veldman and Marc Bezem. Ramsey’s theorem and the pigeonhole principle in intuitionistic mathematics. Journal of the London Mathematical Society, 2(2):193-211, 1993.
-
Dimitrios Vytiniotis, Thierry Coquand, and David Wahlstedt. Stop when you are almost-full. In Interactive Theorem Proving, pages 250-265. Springer, 2012.