On streams that are finitely red

DOI10.2168/LMCS-8(4:4)2012MaRDI QIDQ3166225zbMATH OpenFDO

Authors Marc Bezem, Keiko Nakata, Tarmo Uustalu

Publication date 22 October 2012

Published in Logical Methods in Computer Science (Search for Journal in Brave)

Full work available at URL https://arxiv.org/abs/1210.1200

zbMATH Keywords

coinductionconstructive mathematicsfinitenessinductionintuitionistic mathematicstype theory

Mathematics Subject Classification ID

Intuitionistic mathematics (03F55)

Abstract: Mixing induction and coinduction, we study alternative definitions of streams being finitely red. We organize our definitions into a hierarchy including also some well-known alternatives in intuitionistic analysis. The hierarchy collapses classically, but is intuitionistically of strictly decreasing strength. We characterize the differences in strength in a precise way by weak instances of the Law of Excluded Middle.

Recommendations

• Finite sets and infinite sets in weak intuitionistic arithmetic
• Finiteness and rational sequences, constructively
• Variations on Noetherianness
• scientific article; zbMATH DE number 5994597
• Finiteness in a Minimalist Foundation

Cited in

(5)

• A Decision Procedure for Regular Expression Equivalence in Type Theory
• Variations on Noetherianness
• A new coinductive confluence proof for infinitary lambda calculus
• Investigating streamless sets
• Finiteness and rational sequences, constructively

This page was built for publication: On streams that are finitely red

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q3166225)