Representations of stream processors using nested fixed points

DOI10.2168/LMCS-5(3:9)2009MaRDI QIDQ3401133zbMATH OpenFDO

Authors Peter Hancock, Neil Ghani, Dirk Pattinson

Publication date 28 January 2010

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

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

zbMATH Keywords

continuous functionsfinal coalgebrasinitial algebrasstreams

Mathematics Subject Classification ID

Logic in computer science (03B70) Functional programming and lambda calculus (68N18) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30)

Abstract: We define representations of continuous functions on infinite streams of discrete values, both in the case of discrete-valued functions, and in the case of stream-valued functions. We define also an operation on the representations of two continuous functions between streams that yields a representation of their composite. In the case of discrete-valued functions, the representatives are well-founded (finite-path) trees of a certain kind. The underlying idea can be traced back to Brouwer's justification of bar-induction, or to Kreisel and Troelstra's elimination of choice-sequences. In the case of stream-valued functions, the representatives are non-wellfounded trees pieced together in a coinductive fashion from well-founded trees. The definition requires an alternating fixpoint construction of some ubiquity.

Recommendations

• Continuous functions on final coalgebras
• Continuous functions on final coalgebras
• scientific article; zbMATH DE number 7297867
• scientific article; zbMATH DE number 3903936
• A coinductive approach to computing with compact sets

Cited in

(17)

• Categorical Büchi and parity conditions via alternating fixed points of functors
• Continuity of Gödel's system T definable functionals via effectful forcing
• Continuous functions on final coalgebras
• A coalgebraic view of bar recursion and bar induction
• Continuous functions on final coalgebras
• Stream differential equations: specification formats and solution methods
• scientific article; zbMATH DE number 3903936 (Why is no real title available?)
• Nonflatness and totality
• Representing continuous functions between greatest fixed points of indexed containers
• scientific article; zbMATH DE number 7168147 (Why is no real title available?)
• Well-founded recursion with copatterns and sized types
• Stream processors and comodels
• Hypernormalisation in an abstract setting
• Coalgebras in functional programming and type theory
• \(\text{TT}^\Box_{\mathcal{C}}\): a family of extensional type theories with effectful realizers of continuity
• Comodule representations of second-order functionals
• A saturation-based unification algorithm for higher-order rational patterns

This page was built for publication: Representations of stream processors using nested fixed points

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