Hostname: page-component-586b7cd67f-l7hp2 Total loading time: 0 Render date: 2024-11-20T11:40:14.250Z Has data issue: false hasContentIssue false
  • English
  • Français

Concrete stream calculus: An extended study

Part of: JFP Research Articles

Published online by Cambridge University Press:  18 January 2011

RALF HINZE
RALF HINZE*
Affiliation:
Computing Laboratory, University of Oxford, Wolfson Building, Parks Road, Oxford OX1 3QD, UK (e-mail: [email protected])
Rights & Permissions [Opens in a new window]

Abstract

Core share and HTML view are not available for this content. However, as you have access to this content, a full PDF is available via the ‘Save PDF’ action button.

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 smörgåsbord 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.

Type
Articles
Information
Journal of Functional Programming , Volume 20 , Special Issue 5-6: Dedicated to ICFP 2008 , November 2010 , pp. 463 - 535
Copyright
Copyright © Cambridge University Press 2011

References

Altenkirch, T. (2001) Representations of first order function types as terminal coalgebras. In Typed Lambda Calculi and Applications, TLCA 2001, Lecture Notes in Computer Science, vol. 2044. Springer-Verlag, pp. 62–78.Google Scholar
Backhouse, R. (2001) Galois Connections and Fixed Point Calculus. Lecture Notes.CrossRefGoogle Scholar
Backhouse, R. & Fokkinga, M. (2001) The associativity of equivalence and the towers of Hanoi problem, Inf. Process. Lett., 77: 71–76.CrossRefGoogle Scholar
Backhouse, R. & Michaelis, D. (2005) A Calculational Presentation of Impartial Two-Person Games. Abstract presented at RelMiCS8.Google Scholar
Bartels, F. (2003) Generalised coinduction, Math. Struct. Comp. Sci., 13: 321–348.CrossRefGoogle Scholar
Bird, R. (1998) Introduction to Functional Programming using Haskell, 2nd ed.Prentice Hall, Europe.Google Scholar
Bird, R. & Meertens, L. (1998) Nested datatypes. In Proceedings of the Fourth International Conference on Mathematics of Program Construction, MPC'98, Marstrand, Sweden, Jeuring, J. (ed), Lecture Notes in Computer Science, vol. 1422. Springer-Verlag, pp. 52–67.Google Scholar
Bird, R. (1987) An introduction to the theory of lists. In Proceedings of the NATO Advanced Study Institute on Logic of Programming and Calculi of Discrete Design, Marktoberdorf, Germany, Broy, M. (ed), Springer-Verlag, pp. 5–42.CrossRefGoogle Scholar
Coquand, T. (1994) Infinite objects in type theory. In Types for Proofs and Programs, International Workshop TYPES'93, Nijmegen, The Netherlands, May 24–28, 1993, Selected Papers, Barendregt, H. & Nipkow, T. (eds), Lecture Notes in Computer Science, vol. 806. Springer-Verlag, pp. 62–78.CrossRefGoogle Scholar
Danvy, O. (1999) An extensional characterization of lambda-lifting and lambda-dropping. In Proceedings of the 4th Fuji International Symposium on Functional and Logic Programming (FLOPS'99), Tsukuba, Japan, Middeldorp, A. & Sato, T. (eds), Lecture Notes in Computer Science, vol. 1722. Springer-Verlag, pp. 241–250.Google Scholar
Fokkinga, M. M. (1992) Law and Order in Algorithmics. PhD thesis, University of Twente.Google Scholar
Gibbons, J. & Hutton, G. (2005) Proof methods for corecursive programs. Fundam. Inform. (Special Issue on Program Transformation) 66 (4): 353–366.Google Scholar
Gill, A. & Hutton, G. (2009) The worker/wrapper transformation, J. Funct. Program., 19 (2): 227–251.CrossRefGoogle Scholar
Graham, R. L., Knuth, D. E. & Patashnik, O. (1994) Concrete Mathematics, 2nd edn.Addison-Wesley Publishing Company.Google Scholar
Hinze, R. (2000a) Functional Pearl: Perfect trees and bit-reversal permutations, J. Funct. Program., 10 (3): 305–317.CrossRefGoogle Scholar
Hinze, R. (2000b) Memo functions, polytypically!. In Proceedings of the 2nd Workshop on Generic Programming. Jeuring, J. (ed), Ponte de Lima, Portugal,. pp. 17–32. The proceedings appeared as a technical report of Universiteit Utrecht, UU-CS-2000-19.Google Scholar
Hinze, R. (2008) Functional Pearl: Streams and unique fixed points. In Proceedings of the 13th ACM SIGPLAN International Conference on Functional Programming (ICFP '08). Thiemann, P. (ed), ACM Press, pp. 189–200.CrossRefGoogle Scholar
Hinze, R. (2009) Functional Pearl: The Bird tree, J. Funct. Program., 19 (5): 491–508.CrossRefGoogle Scholar
Hinze, R. (to appear a) Scans and convolutions—a calculational proof of Moessner's Theorem. In Post-proceedings of the 20th International Symposium on the Implementation and Application of Functional Languages (IFL 2008), University of Hertfordshire (UK, September 10–12, 2008). Scholz, S.-B. (ed), Lecture Notes in Computer Science, vol. 5836. Springer-Verlag.Google Scholar
Hinze, R. (2010) Lifting operators and laws. Available at: http://www.comlab.ox.ac.uk/ralf.hinze/Lifting.pdf.Google Scholar
Hinze, R. (to appear b) Type fusion. In Proceedings of the 13th International Conference on Algebraic Methodology And Software Technology (AMAST2010), Pavlovic, D. & Johnson, M. (eds), Lecture Notes in Computer Science, vol. 6486. Springer-Verlag.Google Scholar
Hinze, R. & Löh, A. (2008) Guide2lhs2TeX (for version 1.13). Available at: http://people.cs.uu.nl/andres/lhs2tex/.Google Scholar
Karczmarczuk, J. (1997) Generating power of lazy semantics, Theor. Comput. Sci., (Special volume on computer algebra), 187 (1–2): 203–219.CrossRefGoogle Scholar
Knuth, D. E. (1998) The Art of Computer Programming, Volume 3: Sorting and Searching, 2nd edn.Addison-Wesley Publishing Company.Google Scholar
Mac Lane, S. (1998) Categories for the Working Mathematician, 2nd edn. Graduate Texts in Mathematics. Springer-Verlag.Google Scholar
McBride, C. & Paterson, R. (2008) Functional Pearl: Applicative programming with effects, J. Funct. Program. 18 (1): 1–13.CrossRefGoogle Scholar
McIlroy, M. D. (1999) Power series, power serious, J. Funct. Program., 3 (9): 325–337.CrossRefGoogle Scholar
McIlroy, M. D. (2001) The music of streams, Inf. Process. Lett., 77 (2–4): 189–195.CrossRefGoogle Scholar
Milner, R. (1989) Communication and Concurrency. International Series in Computer Science. Prentice Hall International.Google Scholar
Moessner, A. (1951) Eine Bemerkung über die Potenzen der natürlichen Zahlen. In Aus den Sitzungsberichten der Bayerischen Akademie der Wissenschaften. Mathematisch-naturwissenschaftliche Klasse, Nr. 3 March: 29.Google Scholar
Niqui, M. & Rutten, J. (2010) Sampling, splitting and merging in coinductive stream calculus. In Proceedings of the 10th International Conference on Mathematics of Program Construction (MPC '10), Bolduc, C., Desharnais, J. & Ktari, B. (eds), Lecture Notes in Computer Science, vol. 6120. Springer-Verlag, pp. 310–330.Google Scholar
Paasche, I. (1952) Ein neuer Beweis des Moessnerschen Satzes. In Aus den Sitzungsberichten der Bayerischen Akademie der Wissenschaften. Mathematisch-naturwissenschaftliche Klasse, Nr. 1 February:1–5.Google Scholar
Perron, O. (1951) Beweis des Moessnerschen Satzes. Aus den Sitzungsberichten der Bayerischen Akademie der Wissenschaften. Mathematisch-naturwissenschaftliche Klasse, Nr. 4 May: 31–34.Google Scholar
Peyton Jones, S. (2003) Haskell 98 Language and Libraries. Cambridge University Press.Google Scholar
Rutten, J. (2003) Fundamental study: Behavioural differential equations: A coinductive calculus of streams, automata, and power series, Theor. Comput. Sci., 308: 1–53.CrossRefGoogle Scholar
Rutten, J. (2005) A coinductive calculus of streams, Math. Struct. Comp. Sci., 15: 93–147.CrossRefGoogle Scholar
Röjemo, N. (1995) Garbage Collection, and Memory Efficiency, in Lazy Functional Languages. PhD thesis, Chalmers University of Technology.Google Scholar
Salié, H. (1952) Bemerkung zu einem Satz von Moessner. In Aus den Sitzungsberichten der Bayerischen Akademie der Wissenschaften. Mathematisch-naturwissenschaftliche Klasse, Nr. 2 February: 7–11.Google Scholar
Silva, A. & Rutten, J. (2010) A coinductive calculus of binary trees, Inf. Comput., 208: 578–593.CrossRefGoogle Scholar
Sloane, N. J. A. (2009) The on-line encyclopedia of integer sequences [online]. Available at: http://www.research.att.com/~njas/sequences/.Google Scholar
Stewart, I. (1999) The Magical Maze: Seeing the World Through Mathematical Eyes. Wiley. ISBN 0471350656.Google Scholar
Submit a response

Discussions

No Discussions have been published for this article.