Skip to main content
SpringerLink
Log in

Calculating Functional Programs

  • Chapter
  • First Online:
Algebraic and Coalgebraic Methods in the Mathematics of Program Construction

Part of the book series: Lecture Notes in Computer Science ((LNCS,volume 2297))

Abstract

Functional programs are merely equations; they may be manipulated by straightforward equational reasoning. In particular, one can use this style of reasoning to calculate programs, in the same way that one calculates numeric values in arithmetic. Many useful theorems for such reasoning derive from an algebraic view of programs, built around datatypes and their operations. Traditional algebraic methods concentrate on initial algebras, constructors, and values; dual co-algebraic methods concentrate on final co-algebras, destructors, and processes. Both methods are elegant and powerful; they deserve to be combined.

This is a preview of subscription content, log in via an institution to check access.

Access this chapter

Log in via an institution

Subscribe and save

Springer+ Basic
$34.99 /Month
  • Get 10 units per month
  • Download Article/Chapter or eBook
  • 1 Unit = 1 Article or 1 Chapter
  • Cancel anytime
Subscribe now

Buy Now

Chapter
USD 29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD 39.99
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 54.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

Similar content being viewed by others

References

  1. Roland Backhouse. An exploration of the Bird-Meertens formalism. In International Summer School on Constructive Algorithmics, Hollum, Ameland. STOP project, 1989. Also available as Technical Report CS 8810, Department of Computer Science, Groningen University, 1988.

    Google Scholar 

  2. R. S. Bird, C. C. Morgan, and J. C. P. Woodcock, editors. LNCS 669: Mathematics of Program Construction. Springer-Verlag, 1993.

    MATH  Google Scholar 

  3. Richard Bird. Personal communication, 1999.

    Google Scholar 

  4. Richard Bird and Oege de Moor. The Algebra of Programming. Prentice-Hall, 1996.

    Google Scholar 

  5. Richard S. Bird. Introduction to Functional Programming Using Haskell. Prentice-Hall, 1998.

    Google Scholar 

  6. Stephen Brookes and Shai Geva. Computational comonads and intensional semantics. In M. P. Fourman, P. T. Johnstone, and A. M. Pitts, editors, Categories in Computer Science, London Mathematical Society Lecture Notes, pages 1–44. Cambridge University Press, 1992. Also Technical Report CMU-CS-91-190, School of Computer Science, Carnegie Mellon University.

    Google Scholar 

  7. Stephen Brookes and Kathryn Van Stone. Monads and comonads in intensional semantics. Technical Report CMU-CS-93-140, CMU, 1993.

    Google Scholar 

  8. Rod Burstall and David Rydeheard. Computational Category Theory. Prentice-Hall, 1988.

    Google Scholar 

  9. Roy L. Crole. Categories for Types. Cambridge University Press, 1994.

    Google Scholar 

  10. B. A. Davey and H. A. Priestley. Introduction to Lattices and Order. Mathematical Textbooks Series. Cambridge University Press, 1990.

    Google Scholar 

  11. Maarten M. Fokkinga and Erik Meijer. Program calculation properties of continuous algebras. Technical Report CS-R9104, CWI, Amsterdam, January 1991.

    Google Scholar 

  12. Jeremy Gibbons and Geraint Jones. The under-appreciated unfold. In Proceedings of the Third ACM SIGPLAN International Conference on Functional Programming, pages 273–279, Baltimore, Maryland, September 1998.

    Google Scholar 

  13. J. A. Goguen, J. W. Thatcher, E. G. Wagner, and J. B. Wright. An introduction to categories, algebraic theories and algebras. Technical report, IBM Thomas J. Watson Research Centre, Yorktown Heights, April 1975.

    Google Scholar 

  14. J. A. Goguen, J. W. Thatcher, E. G. Wagner, and J. B. Wright. Initial algebra semantics and continuous algebras. Journal of the ACM, 24(1):68–95, January 1977.

    Article  MATH  MathSciNet  Google Scholar 

  15. Jeremy Gunawardena. Towards an applied mathematics for computer science. In M. S. Alber, B. Hu, and J. J. Rosenthal, editors, Current and Future Directions in Applied Mathematics. Birkhäuser, Boston, 1997.

    Google Scholar 

  16. Tatsuya Hagino. A Categorical Programming Language. PhD thesis, Department of Computer Science, University of Edinburgh, September 1987.

    Google Scholar 

  17. Tatsuya Hagino. A typed lambda calculus with categorical type constructors. In D. H. Pitt, A. Poigné, and D. E. Rydeheard, editors, LNCS 283: Category Theory and Computer Science, pages 140–157. Springer-Verlag, September 1987.

    Google Scholar 

  18. C. A. R. Hoare. Notes on data structuring. In Ole-Johan Dahl, Edsger W. Dijkstra, and C. A. R. Hoare, editors, Structured Programming, APIC studies in data processing, pages 83–174. Academic Press, 1972.

    Google Scholar 

  19. Graham Hutton. Fold and unfold for program semantics. In Proceedings of the Third ACM SIGPLAN International Conference on Functional Programming, Baltimore, Maryland, September 1998.

    Google Scholar 

  20. Graham Hutton. Personal communication, 1999.

    Google Scholar 

  21. Johan Jeuring, editor. LNCS 1422: Proceedings of Mathematics of Program Construction, Marstrand, Sweden, June 1998. Springer-Verlag.

    MATH  Google Scholar 

  22. Johan Jeuring and Erik Meijer, editors. LNCS 925: Advanced Functional Programming. Springer-Verlag, 1995. Lecture notes from the First International Spring School on Advanced Functional Programming Techniques, Båstad, Sweden.

    Google Scholar 

  23. Saunders Mac Lane. Categories for the Working Mathematician. Springer-Verlag, 1971.

    Google Scholar 

  24. Grant Malcolm. Algebraic Data Types and Program Transformation. PhD thesis, Rijksuniversiteit Groningen, September 1990.

    Google Scholar 

  25. Grant Malcolm. Data structures and program transformation. Science of Computer Programming, 14:255–279, 1990.

    Article  MathSciNet  MATH  Google Scholar 

  26. Lambert Meertens. Paramorphisms. Formal Aspects of Computing, 4(5):413–424, 1992.

    Article  MATH  Google Scholar 

  27. Erik Meijer, Maarten Fokkinga, and Ross Paterson. Functional programming with bananas, lenses, envelopes and barbed wire. In John Hughes, editor, LNCS 523: Functional Programming Languages and Computer Architecture, pages 124–144. Springer-Verlag, 1991.

    Google Scholar 

  28. Eugenio Moggi. Notions of computation and monads. Information and Computation, 93(1), 1991.

    Google Scholar 

  29. Bernhard Möller. Personal communication, 1995.

    Google Scholar 

  30. Bernhard Möller, editor. LNCS 947: Mathematics of Program Construction. Springer-Verlag, 1995.

    Google Scholar 

  31. Benjamin C. Pierce. Basic Category Theory for Computer Scientists. MIT Press, 1991.

    Google Scholar 

  32. John C. Reynolds. Semantics of the domain of flow diagrams. Journal of the ACM, 24(3):484–503, 1977.

    Article  MATH  MathSciNet  Google Scholar 

  33. David A. Schmidt. Denotational Semantics: A Methodology for Language Development. Allyn and Bacon, 1986.

    Google Scholar 

  34. M. B. Smyth and G. D. Plotkin. The category-theoretic solution of recursive domain equations. SIAM Journal on Computing, 11(4):761–783, November 1982.

    Article  MATH  MathSciNet  Google Scholar 

  35. Joseph Stoy. Denotational Semantics: The Scott-Strachey Approach to Programming Language Theory. MIT Press, 1977.

    Google Scholar 

  36. Doaitse Swierstra and Oege de Moor. Virtual data structures. In Bernhard Möller, Helmut Partsch, and Steve Schumann, editors, LNCS 755: IFIP TC2/WG2.1 State-of-the-Art Report on Formal Program Development, pages 355–371. Springer-Verlag, 1993.

    Google Scholar 

  37. Daniele Turi. Functorial Operational Semantics and its Denotational Dual. PhD thesis, Vrije Universiteit Amsterdam, June 1996.

    Google Scholar 

  38. Tarmo Uustalu and Varmo Vene. Primitive (co)recursion and course-of-value (co)iteration. Research Report TRITA-IT R 98:02, Dept of Teleinformatics, Royal Institute of Technology, Stockholm, January 1998.

    Google Scholar 

  39. J. L. A. van de Snepscheut, editor. LNCS 375: Mathematics of Program Construction. Springer-Verlag, 1989.

    MATH  Google Scholar 

  40. Varmo Vene and Tarmo Uustalu. Functional programming with apomorphisms (corecursion). Proceedings of the Estonian Academy of Sciences: Physics, Mathematics, 47(3):147–161, 1998. 9th Nordic Workshop on Programming Theory.

    Google Scholar 

  41. Philip Wadler. Comprehending monads. Mathematical Structures in Computer Science, 2(4):461–493, 1992. Earlier version appeared in ACM Conference on Lisp and Functional Programming, 1990.

    Article  MATH  MathSciNet  Google Scholar 

  42. Philip Wadler. The essence of functional programming. In 19th Annual Symposium on Principles of Programming Languages, 1992.

    Google Scholar 

  43. Philip Wadler. Monads for functional programming. In M. Broy, editor, Program Design Calculi: Proceedings of the Marktoberdorf Summer School, 1992. Also in [22].

    Google Scholar 

  44. R. F. C. Walters. Datatypes in distributive categories. Bulletin of the Australian Mathematical Society, 40:79–82, 1989.

    MATH  MathSciNet  Google Scholar 

  45. R. F. C. Walters. Categories and Computer Science. Computer Science Texts Series. Cambridge University Press, 1991.

    Google Scholar 

  46. R. F. C. Walters. An imperative language based on distributive categories. Mathematical Structures in Computer Science, 2:249–256, 1992.

    MATH  MathSciNet  Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Computing Laboratory, University of Oxford, Oxford

    Jeremy Gibbons

Authors
  1. Jeremy Gibbons
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. School of Computer Science and IT, University of Nottingham, Jubilee Campus, Wollaton Road, NG8 1BB, Nottingham, UK

    Roland Backhouse

  2. Dept. of Mathematics and Computer Science, University of Leicester, University Road, LE1 7RH, Leicester, UK

    Roy Crole

  3. Oxford University Computing Laboratory, Wolfson Building Parks Road, OX1 3QD, Oxford, UK

    Jeremy Gibbons

Rights and permissions

Reprints and permissions

Copyright information

© 2002 Springer-Verlag Berlin Heidelberg

About this chapter

Cite this chapter

Gibbons, J. (2002). Calculating Functional Programs. In: Backhouse, R., Crole, R., Gibbons, J. (eds) Algebraic and Coalgebraic Methods in the Mathematics of Program Construction. Lecture Notes in Computer Science, vol 2297. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-47797-7_5

Download citation

  • DOI: https://doi.org/10.1007/3-540-47797-7_5

  • Published:

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-540-43613-3

  • Online ISBN: 978-3-540-47797-6

  • eBook Packages: Springer Book Archive

Publish with us

Policies and ethics

Search

Navigation