License: Creative Commons Attribution 3.0 Unported license (CC BY 3.0)
When quoting this document, please refer to the following
DOI: 10.4230/LIPIcs.TYPES.2014.187
URN: urn:nbn:de:0030-drops-54971
URL: http://dagstuhl.sunsite.rwth-aachen.de/volltexte/2015/5497/
Go to the corresponding LIPIcs Volume Portal

Parmann, Erik

Investigating Streamless Sets

pdf-format:
11.pdf (0.5 MB)

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.

BibTeX - Entry

@InProceedings{parmann:LIPIcs:2015:5497,
  author =	{Erik Parmann},
  title =	{{Investigating Streamless Sets}},
  booktitle =	{20th International Conference on Types for Proofs and Programs (TYPES 2014)},
  pages =	{187--201},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-88-0},
  ISSN =	{1868-8969},
  year =	{2015},
  volume =	{39},
  editor =	{Hugo Herbelin and Pierre Letouzey and Matthieu Sozeau},
  publisher =	{Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{http://drops.dagstuhl.de/opus/volltexte/2015/5497},
  URN =		{urn:nbn:de:0030-drops-54971},
  doi =		{10.4230/LIPIcs.TYPES.2014.187},
  annote =	{Keywords: Type theory, Constructive Logic, Finite Sets}
}

Keywords: Type theory, Constructive Logic, Finite Sets
Collection: 20th International Conference on Types for Proofs and Programs (TYPES 2014)
Issue Date: 2015
Date of publication: 12.10.2015

DROPS-Home | Fulltext Search | Imprint | Privacy Published by LZI