Document Open Access Logo

Investigating Streamless Sets

Author Erik Parmann

PDF

File

Thumbnail PDF
PDF
LIPIcs.TYPES.2014.187.pdf
  • Filesize: 484 kB
  • 15 pages

Document Identifiers

Subject Classification

Keywords
  • Type theory
  • Constructive Logic
  • Finite Sets

Metrics

  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    0
    PDF Downloads
    0
    Metadata Views

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.

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

Author Details

Erik Parmann

References

  1. Michael Beeson. Goodman’s theorem and beyond. Pacific Journal of Mathematics, 84(1):1-16, 1979. Google Scholar
  2. 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.
  3. The Coq Development Team. The Coq Reference Manual, version 8.4, August 2012. Available electronically at URL: http://coq.inria.fr/doc.
  4. 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. Google Scholar
  5. 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. Google Scholar
  6. Per Martin-Löf and Giovanni Sambin. Intuitionistic type theory, volume 17. Bibliopolis Naples, 1984. Google Scholar
  7. F. P. Ramsey. On a problem of formal logic. Proceedings of the London Mathematical Society, 2(1):264-286, 1930. Google Scholar
  8. F. Richman and G. Stolzenberg. Well quasi-ordered sets. Advances in Mathematics, 97(2):145-153, 1993. Google Scholar
  9. Anne Sjerp Troelstra and Dirk Van Dalen. Constructivism in mathematics, volume 2. Elsevier, 1988. Google Scholar
  10. The Univalent Foundations Program. Homotopy Type Theory: Univalent Foundations of Mathematics. http://homotopytypetheory.org/book, Institute for Advanced Study, 2013.
  11. 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. Google Scholar
  12. Dimitrios Vytiniotis, Thierry Coquand, and David Wahlstedt. Stop when you are almost-full. In Interactive Theorem Proving, pages 250-265. Springer, 2012. Google Scholar
Any Issues?
X

Feedback on the Current Page

CAPTCHA

Thanks for your feedback!

Feedback submitted to Dagstuhl Publishing

Could not send message

Please try again later or send an E-mail
© 2023-2025 Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact