Skip to main content
SpringerLink
Log in

Inverting Functions as Folds

  • Conference paper
  • First Online:
Book cover Mathematics of Program Construction (MPC 2002)

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

Included in the following conference series:

Abstract

This paper is devoted to the proof and applications of a theorem giving conditions under which the inverse of a partial function can be expressed as a relational hylomorphism. The theorem is a generalisation of a previous result, due to Bird and de Moor, that gave conditions under which a total function can be expressed a relational fold. The theorem is illustrated with three problems, all dealing with constructing trees with various properties.

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

Access this chapter

Log in via an institution
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.

References

  1. S. M. Abramov and R. Glück. The universal resolving algorithm: inverse computation in a functional language. In R. C. Backhouse and J. N. F. d. Oliveira, editors, Mathematics of Program Construction 2000, number 1837 in Lecture Notes in Computer Science, pages 187–212. Springer-Verlag, 2000.

    Chapter  Google Scholar 

  2. R. C. Backhouse, P. de Bruin, G. Malcolm, T. S. Voermans, and J. van der Woude. Relational catamorphisms. In B. Moller, editor, Proceedings of the IFIP TC2/WG2.1 Working Conference on Constructing Programs, pages 287–318. El-sevier Science Publishers B.V., 1991.

    Google Scholar 

  3. R. C. Backhouse and P. F. Hoogendijk. Elements of a relational theory of datatypes. In B. Moller, H. Partsch, and S. A. Schuman, editors, Formal Program Development. Proc. IFIP TC2/WG 2.1 State of the Art Seminar., number 755 in Lecture Notes in Computer Science, pages 7–42. Springer-Verlag, January 1992.

    Google Scholar 

  4. R. S. Bird. On building trees with minimum height. Journal of Functional Programming, 7(4):441–445, 1997.

    Article  MATH  MathSciNet  Google Scholar 

  5. R. S. Bird and O. de Moor. Algebra of Programming. International Series in Computer Science. Prentice Hall, 1997.

    Google Scholar 

  6. R. S. Bird, J. Gibbons, and S.-C. Mu. Algebraic methods for optimization problems. In R. C. Backhouse, R. Crole, and J. Gibbons, editors, Algebraic and Coalgebraic Methods in the Mathematics of Program Construction, number 2297 in Lecture Notes in Computer Science, pages 281–307. Springer-Verlag, January 2002.

    Chapter  Google Scholar 

  7. W. Chen and J. T. Udding. Program inversion: more than fun! Science of Computer Programming, 15:1–13, 1990.

    Article  MATH  MathSciNet  Google Scholar 

  8. T.-R. Chuang and B. Goldberg. Real-time deques, multihead Turing machines, and purely functional programming. In Conference on Functional Programming Languages and Computer Architecture, Copenhagen, Denmark, June 1993. ACM Press.

    Google Scholar 

  9. O. de Moor and J. Gibbons. Pointwise relational programming. In Proceedings of Algebraic Methodology and Software Technology 2000, number 1816 in Lecture Notes in Computer Science, pages 371–390. Springer-Verlag, May 2000.

    Chapter  Google Scholar 

  10. E. W. Dijkstra. Program inversion. Technical Report EWD671, Eindhoven University of Technology, 1978.

    Google Scholar 

  11. H. Doornbos and R. C. Backhouse. Induction and recursion on datatypes. In B. Moller, editor, Mathematics of Program Construction, 3rd International Conference, number 947 in Lecture Notes in Computer Science, pages 242–256. Springer-Verlag, July 1995.

    Google Scholar 

  12. J. Gibbons, G. Hutton, and T. Altenkirch. When is a function a fold or an unfold? In A. Corradini, M. Lenisa, and U. Montanari, editors, Coalgebraic Methods in Computer Science, number 44.1 in Electronic Notes in Theoretical Computer Science, April 2001.

    Google Scholar 

  13. J. Gibbons and G. Jones. Linear-time breadth-first tree algorithms: an exercise in the arithmetic of folds and zips. Technical report, University of Auckland, 1993. University of Auckland Computer Science Report No. 71, and IFIP Working Group 2.1 working paper 705 WIN-2.

    Google Scholar 

  14. D. Gries. The Science of Programming. Springer Verlag, 1981.

    Google Scholar 

  15. D. Gries and J. L. van de Snepscheut. Inorder traversal of a binary tree and its inversion. In E. W. Dijkstra, editor, Formal Development of Programs and Proofs, pages 37–42. Addison Wesley, 1990.

    Google Scholar 

  16. P. G. Harrison and H. Khoshnevisan. On the synthesis of function inverses. Acta Informatica, 29:211–239, 1992.

    Article  MATH  MathSciNet  Google Scholar 

  17. P. F. Hoogendijk and O. de Moor. Container types categorically. Journal of Functional Programming, 10(2):191–225, March 2000.

    Google Scholar 

  18. T. C. Hu and A. C. Tucker. Optimal computer search trees and variable-length alphabetical codes. SIAM Journal on Applied Mathematics, 21(4):514–532, 1971.

    Article  MATH  MathSciNet  Google Scholar 

  19. E. Knapen. Relational Programming, Program Inversion, and the Derivation of Parsing Algorithms. Master’s thesis, Eindhoven University of Technology, 23 November 1993.

    Google Scholar 

  20. R. E. Korf. Inversion of applicative programs. In Proceedings of the Seventh Intern. Joint Conference on Artificial Intelligence (IJCAI-81), pages 1007–1009. William Kaufmann, Inc., 1981.

    Google Scholar 

  21. C. Okasaki. Simple and efficient purely functional queues and deques. Journal of Functional Programming, 5(4):583–592, 1995.

    Article  Google Scholar 

  22. C. Okasaki. Breadth-first numbering: lessons from a small exercise in algorithm design. In Proceedings of the 2000 ACM SIGPLAN International Conference on Functional Programming, pages 131–136. ACM Press, September 2000.

    Google Scholar 

  23. C. Pareja-Flores and J. Á. Velázquez-Iturbide. Synthesis of functions by transformations and constraints. In Proceedings of the 1997 ACM SIGPLAN International Conference on Functional Programming, page 317, Amsterdam, The Netherlands, June 1997. ACM Press.

    Google Scholar 

  24. B. J. Ross. Running programs backwards: the logical inversion of imperative computation. Formal Aspects of Computing Journal, 9:331–348, 1997.

    Article  MATH  Google Scholar 

  25. B. Schoenmakers. Inorder traversal of a binary heap and its inversion in optimal time and space. In Mathematics of Program Construction 1992, number 669 in Lecture Notes in Computer Science, pages 291–301. Springer-Verlag, 1993.

    Google Scholar 

  26. J. L. van de Snepscheut. Inversion of a recursive tree traversal. Technical Report JAN 171a, California Institute of Technology, May 1991. Available online at ftp://ftp.cs.caltech.edu/tr/cs-tr-91-07.ps.Z.

Download references

Author information

Authors and Affiliations

  1. Programming Research Group, Oxford University, Wolfson Building, Parks Road, OX1 3QD, UK

    Shin-Cheng Mu & Richard Bird

Authors
  1. Shin-Cheng Mu
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Richard Bird
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. Computing Laboratory, University of Kent at Canterbury, CT2 7NF, Canterbury, Kent, UK

    Eerke A. Boiten

  2. Institut für Informatik, Universität Augsburg, Universitätsstr. 14, 86135, Augsburg, Germany

    Bernhard Möller

Rights and permissions

Reprints and permissions

Copyright information

© 2002 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Mu, SC., Bird, R. (2002). Inverting Functions as Folds. In: Boiten, E.A., Möller, B. (eds) Mathematics of Program Construction. MPC 2002. Lecture Notes in Computer Science, vol 2386. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-45442-X_13

Download citation

  • DOI: https://doi.org/10.1007/3-540-45442-X_13

  • Published:

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-540-43857-1

  • Online ISBN: 978-3-540-45442-7

  • eBook Packages: Springer Book Archive

Publish with us

Policies and ethics

Search

Navigation