Skip to main content
SpringerLink
Log in

Problems in rewriting applied to categorical concepts by the example of a computational comonad

  • Regular Papers
  • Conference paper
  • First Online:
Rewriting Techniques and Applications (RTA 1995)

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

Included in the following conference series:

Abstract

We present a canonical system for comonads which can be extended to the notion of a computational comonad [BG92] where the crucial point is to find an appropriate representation. These canonical systems are checked with the help of the Larch Prover [GG91] exploiting a method by G. Huet [Hue90a] to represent typing within an untyped rewriting system. The resulting decision procedures are implemented in the programming language Elf [Pfe89] since typing is directly supported by this language. Finally we outline an incomplete attempt to solve the problem which could be used as a benchmark for rewriting tools.

sponsored by the Austrian Science Foundation (FWF) under ESPRIT BRP 6471 MEDLAR II, and by the American National Science Foundation under Grant No. CCR-9303383

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

Access this chapter

Log in via an institution

Institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. L. Bachmair. Canonical Equational Proofs. Progress in Theoretical Computer Science. Birkhäuser, 1991.

    Google Scholar 

  2. S. Brookes and S. Geva. Computational Comonads and Intensional Semantics. In M.P. Fourman and P.T. Johnstone and A.M. Pitts, editor, Categories in Computer Science, number 177 in London Mathematical Society Lecture Notes, pages 1–44. Cambridge University Press, 1992.

    Google Scholar 

  3. R. Bündgen. Reduce the Redex → ReDuX. In C. Kirchner, editor, Rewriting Techniques and Applications, number 690 in Lecture Notes in Computer Science, pages 446–450. Springer-Verlag, 1993.

    Google Scholar 

  4. M. Barr and C. Wells. Toposes, Triples and Theories. Number 278 in Grund-lehren der mathematischen Wissenschaften. Springer-Verlag, 1985.

    Google Scholar 

  5. A. Filinski. Representing Monads. In Proceedings of the 21st Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, pages 446–457. ACM, 1994.

    Google Scholar 

  6. P.J. Freyd and A. Sčedrov. Categories, Allegories. Elsevier Science Publishers, 1990.

    Google Scholar 

  7. W. Gehrke. Proof of the Decidability of the Uniform Word Problem for Monads Assisted by Elf. Technical Report 94-66, RISC, 1994.

    Google Scholar 

  8. S.J. Garland and J.V. Guttag. A Guide to LP, The Larch Prover. MIT, 1991.

    Google Scholar 

  9. G. Huet. Confluent Reductions. Journal of the Association for Computing Machinery, 24(4):797–821, October 1980.

    Google Scholar 

  10. G. Huet. Cartesian closed categories and lambda-calculus. In [Hue90b], pages 7–23. Addison Wesley, 1990.

    Google Scholar 

  11. G. Huet. Logical Foundations of Functional Programming. University of Texas at Austin Programming Series. Addison Wesley, 1990.

    Google Scholar 

  12. D. Kapur and H. Zhang. RRL: Rewrite Rule Laboratory User's Manual, revised edition, May 1989.

    Google Scholar 

  13. D.S. Lankford. On proving term rewriting systems are Noetherian. Technical report, Louisiana Technical University, Ruston, LA, 1979.

    Google Scholar 

  14. E. Manes. Algebraic Theories. Number 26 in Graduate Texts in Mathematics. Springer-Verlag, 1976.

    Google Scholar 

  15. S. Mac Lane. Categories for the Working Mathematician. Number 5 in Graduate Texts in Mathematics. Springer-Verlag, 1971.

    Google Scholar 

  16. E. Moggi. Computational Lambda-calculus and Monads. In Fourth Annual Symposium on Logic in Computer Science, pages 14–23. IEEE, June 1989.

    Google Scholar 

  17. T. Nipkow. Higher Order Critical Pairs. In Sixth Annual Symposium on Logic in Computer Science, pages 342–349. IEEE, July 1991.

    Google Scholar 

  18. F. Pfenning. Elf: a language for verified meta-programming. In Fourth Annual Symposium on Logic in Computer Science, pages 313–322. IEEE, June 1989.

    Google Scholar 

  19. E. Vogel. Unifikation von Morphismen (in German). Diplomarbeit, Universitat Karlsruhe, 1978.

    Google Scholar 

  20. P. Wadler. Monads for functional programming. In M. Broy, editor, Program Design Calculi, volume 118 of NATO ASI Series F: Computer and System Sciences, pages 233–264. Springer-Verlag, 1993.

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Research Institute for Symbolic Computation, Johannes Kepler University, A-4040, Linz, Austria

    Wolfgang Gehrke

Authors
  1. Wolfgang Gehrke
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Jieh Hsiang

Rights and permissions

Reprints and permissions

Copyright information

© 1995 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Gehrke, W. (1995). Problems in rewriting applied to categorical concepts by the example of a computational comonad. In: Hsiang, J. (eds) Rewriting Techniques and Applications. RTA 1995. Lecture Notes in Computer Science, vol 914. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-59200-8_58

Download citation

  • DOI: https://doi.org/10.1007/3-540-59200-8_58

  • Published:

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-540-59200-6

  • Online ISBN: 978-3-540-49223-8

  • eBook Packages: Springer Book Archive

Publish with us

Policies and ethics

Search

Navigation