Ralf Hinze.
Concrete Stream Calculus: An Extended Study.
Journal of Functional Programming,
20(5-6):463-535,
November 2010.
ISSN: 0956-7968, 1469-7653.
Keyword(s): coinduction,
Haskell.
Abstract: |
This paper shows how to reason about streams concisely and precisely. Streams, infinite sequences of elements, live in a coworld: they are given by a coinductive datatype, operations on streams are implemented by corecursive programs, and proofs are typically concocted using coinduction. This paper offers an alternative to coinduction. Suitably restricted, stream equations possess unique solutions. This property gives rise to a simple and attractive proof technique, essentially bringing equational reasoning to the coworld. We redevelop the theory of recurrences, finite calculus and generating functions using streams and stream operators, building on the cornerstone of unique solutions. The paper contains a smo extasciidieresis rg\r{}asbord of examples: we study recursion elimination, investigate the binary carry sequence, explore Sprague-Grundy numbers and present two proofs of Moessner's Theorem. The calculations benefit from the rich structure of streams. As the type of streams is an applicative functor we can effortlessly lift operations and their properties to streams. In combination with Haskell's facilities for overloading, this greatly contributes to conciseness of notation. The development is indeed constructive: streams and stream operators are implemented in Haskell, usually by one-liners. The resulting calculus or library, if you wish, is elegant and fun to use. |
@article{hinzeConcreteStreamCalculus2010,
title = {Concrete Stream Calculus: {{An}} Extended Study},
author = {Hinze, Ralf},
year = {2010},
month = nov,
volume = {20},
pages = {463--535},
issn = {0956-7968, 1469-7653},
doi = {10.1017/S0956796810000213},
abstract = {This paper shows how to reason about streams concisely and precisely. Streams, infinite sequences of elements, live in a coworld: they are given by a coinductive datatype, operations on streams are implemented by corecursive programs, and proofs are typically concocted using coinduction. This paper offers an alternative to coinduction. Suitably restricted, stream equations possess unique solutions. This property gives rise to a simple and attractive proof technique, essentially bringing equational reasoning to the coworld. We redevelop the theory of recurrences, finite calculus and generating functions using streams and stream operators, building on the cornerstone of unique solutions. The paper contains a smo extasciidieresis rg\r{}asbord of examples: we study recursion elimination, investigate the binary carry sequence, explore Sprague-Grundy numbers and present two proofs of Moessner's Theorem. The calculations benefit from the rich structure of streams. As the type of streams is an applicative functor we can effortlessly lift operations and their properties to streams. In combination with Haskell's facilities for overloading, this greatly contributes to conciseness of notation. The development is indeed constructive: streams and stream operators are implemented in Haskell, usually by one-liners. The resulting calculus or library, if you wish, is elegant and fun to use.},
url = {https://wcl.cs.rpi.edu/pilots/library/papers/TAGGED/4389-Hinze (2010) - Concrete stream calculus.pdf},
journal = {Journal of Functional Programming},
keywords = {coinduction,Haskell},
number = {5-6}
}
Taylor.
A Lambda Calculus for Real Analysis.
Journal of Logic and Analysis,
2010.
ISSN: 17599008.
Keyword(s): calculus,
reals.
Abstract: |
Abstract Stone Duality is a new paradigm for general topology in which computable continuous functions are described directly, without using set theory, infinitary lattice theory or a prior theory of discrete computation. Every expression in the calculus denotes both a continuous function and a program, and the reasoning looks remarkably like a sanitised form of that in classical topology. This is an introduction to ASD for the general mathematician, with application to elementary real analysis. |
@article{taylorLambdaCalculusReal2010,
title = {A Lambda Calculus for Real Analysis},
author = {{Taylor}},
year = {2010},
issn = {17599008},
doi = {10.4115/jla.2010.2.5},
abstract = {Abstract Stone Duality is a new paradigm for general topology in which computable continuous functions are described directly, without using set theory, infinitary lattice theory or a prior theory of discrete computation. Every expression in the calculus denotes both a continuous function and a program, and the reasoning looks remarkably like a sanitised form of that in classical topology. This is an introduction to ASD for the general mathematician, with application to elementary real analysis.},
url = {https://wcl.cs.rpi.edu/pilots/library/papers/TAGGED/4527 - Taylor (2010) - A lambda calculus for real analysis.pdf},
journal = {Journal of Logic and Analysis},
keywords = {calculus,reals},
}