Skip to main content
SpringerLink
Log in
Book cover

International Conference on Category Theory and Computer Science

CTCS 1997: Category Theory and Computer Science pp 87–105Cite as

A 2-categorical presentation of term graph rewriting

  • Conference paper
  • First Online:

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

Abstract

It is well-known that a term rewriting system can be faithfully described by a cartesian 2-category, where horizontal arrows represent terms, and cells represent rewriting sequences. In this paper we propose a similar, original 2-categorical presentation for term graph rewriting. Building on a result presented in [8], which shows that term graphs over a given signature are in one-to-one correspondence with arrows of a gs-monoidal category freely generated from the signature, we associate with a term graph rewriting system a gs-monoidal 2-category, and show that cells faithfully represent its rewriting sequences. We exploit the categorical framework to relate term graph rewriting and term rewriting, since gs-monoidal (2-)categories can be regarded as “weak” cartesian (2-) categories, where certain (2-)naturality axioms have been dropped.

Research partly supported by the EC TMR Network GETGRATS (General Theory of Graph Transformation Systems) through the Technical University of Berlin. A. Corradini is on leave from Dipartimento di Informatica, Pisa, Italy, and he is also partly supported by the EC Fixed Contribution Contract n. EBRFMBICT960840.

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

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. Z.M. Ariola and J.W. Klop. Equational Term Graph Rewriting. Fundamenta Informaticae, 26:207–240,1996.

    MATH  MathSciNet  Google Scholar 

  2. H.P. Barendregt, M.C.J.D. van Eekelen, J.R.W. Glauert, J.R. Kennaway, M.J. Plasmeijer, and M.R. Sleep. Term graph reduction. In Proceedings PARLE, volume 259 of LNCS, pages 141–158. Springer Verlag, 1987.

    Google Scholar 

  3. M. Barr and C. Wells. Category Theory for Computing Science. Prentice Hall, 1990.

    Google Scholar 

  4. S. Bloom and Z. Èsik. Iteration Theories. EATCS Monographs on Theoretical Computer Science. Springer Verlag, 1991.

    Google Scholar 

  5. G. Boudol. Computational semantics of term rewriting systems. In M. Nivat and J. Reynolds, editors, Algebraic Methods in Semantics, pages 170–235. Cambridge University Press, 1985.

    Google Scholar 

  6. L. Budach and H.-J. Hoenke. Automaten and Functoren. Akademie-Verlag, 1975.

    Google Scholar 

  7. A. Corradini. Concurrent Graph and Term Graph Rewriting. In U. Montanari and V. Sassone, editors, Proceedings CONCUR'96, volume 1119 of LNCS, pages 438–464. Springer Verlag, 1996.

    Google Scholar 

  8. A. Corradini and F. Gadducci.An algebraic presentation of term graphs, via ps-monoidal categories.Submitted for publication. Available at http://www.di.unipi.it/~gadducci/papers/aptg.ps, 1997.

    Google Scholar 

  9. A. Corradini, F. Gadducci, and U. Montanari. Relating two categorical models of term rewriting. In Rewriting Tecniques and Applications, volume 914 of LNCS, pages 225–240. Springer Verlag, 1995.

    Google Scholar 

  10. A. Corradini and F. Rossi. Hyperedge Replacement Jungle Rewriting for Term Rewriting Systems and Logic Programming. Theoret. Comput. Sci., 109:7–48, 1993.

    Article  MATH  MathSciNet  Google Scholar 

  11. G. Gadducci. On the Algebraic Approach to Concurrent Term Rewriting. PhD thesis, University of Pisa — Department of Computer Science, 1996.

    Google Scholar 

  12. J.A. Goguen, J.W. Tatcher, E.G. Wagner, and J.R Wright. Some Fundamentals of Order-Algebraic Semantics. In Mathematical Foundations of Computer Science, volume 45 of LNCS, pages 153–168. Springer Verlag, 1976.

    Google Scholar 

  13. B. Hofmann and D. Plump. Implementing Term Rewriting by Jungle Evaluation. Informatique thèorique et Applications/Theoretical Informatics and Applications, 25:445–472, 1991.

    Google Scholar 

  14. G. Huet and J-J. Lévy. Computations in Orthogonal Rewriting Systems, I. In J.-L. Lassez and G. Plotkin, editors, Computational Logic: Essays in honour of J. A. Robinson, pages 395–414. MIT Press, 1991.

    Google Scholar 

  15. B. Jacobs. Semantics of Weakening and Contraction. Annals of Pure and Applied Logic, 69:73–106, 1994.

    Article  MATH  MathSciNet  Google Scholar 

  16. G.M. Kelly and R.H. Street. Review of the elements of 2-categories. volume 420 of Lecture Notes in Mathematics, pages 75–103. Springer Verlag, 1974.

    Google Scholar 

  17. J.R. Kennaway, J.W. Klop, M.R. Sleep, and F.J. de Vries. On the Adequacy of Graph Rrewriting for Simulating Term Rewriting. ACM Trans. Program. Lang. Syst., 16:493–523, 1994.

    Article  Google Scholar 

  18. A. Kock and G.E. Reyes. Doctrines in Categorical Logic. In J. Bairwise, editor, Handbook of Mathematical Logic, pages 283–313. North Holland, 1977.

    Google Scholar 

  19. Y. Lafont. Equational Reasoning with 2-dimensional Diagrams. In Term Rewriting, French Spring School of Theoretical Computer Science, volume 909 of LNCS, pages 170–195. Springer Verlag, 1995.

    Google Scholar 

  20. C. Laneve and U. Montanari. Axiomatizing permutation equivalence in the λ-λ-calculus. Mathematical Structures in Computer Science, 6:219–249, 1996.

    Article  MATH  MathSciNet  Google Scholar 

  21. F.W. Lawvere. Functorial Semantics of Algebraic Theories. Proc. National Academy of Science, 50:869–872, 1963.

    Article  MATH  MathSciNet  Google Scholar 

  22. S. Mac Lane. Categories for the working mathematician. Springer Verlag, 1971.

    Google Scholar 

  23. J. Meseguer. Conditional rewriting logic as a unified model of concurrency. Theoret. Comput. Sci., 96:73–155, 1992.

    Article  MATH  MathSciNet  Google Scholar 

  24. M.J. Plasmeijer and M.C.J.D. van Eekelen. Functional Programming and Parallel Graph Rewriting. Addison Wesley, 1993.

    Google Scholar 

  25. A.J. Power. An abstract formulation for rewrite systems. In Proceedings Category Theory in Computer Science, volume 389 of LNCS, pages 300–312. Springer Verlag, 1989.

    Google Scholar 

  26. D.E. Rydehard and E.G. Stell. Foundations of equational deductions: A categorical treatment of equational proofs and unification algorithms. In Proceedings Category Theory in Computer Science, volume 283 of LNCS, pages 114–139. Springer Verlag, 1987.

    Google Scholar 

  27. M.R. Sleep, M.J. Plasmeijer, and M.C. van Eekelen, editors. Term Graph Rewriting: Theory and Practice. Wiley, London, 1993.

    MATH  Google Scholar 

  28. J. Staples. Computation of graph-like expressions. Theoret. Comput. Sci., 10:171–195, 1980.

    Article  MATH  MathSciNet  Google Scholar 

  29. J.G. Stell. Categorical Aspects of Unification and Rewriting. PhD thesis, University of Manchester, 1992.

    Google Scholar 

  30. R. Street. Categorical structures. In M. Hazewinkel, editor, Handbook of Algebra, pages 529–577. Elsevier, 1996. *** DIRECT SUPPORT *** A0008C33 00003

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. CWI, Kruislaan 413, 1098SJ, Amsterdam, The Netherlands

    A. Corradini

  2. TUB, Fachbereich 13 Informatik, Franklinstraße 28/29, 10587, Berlin, Germany

    F. Gadducci

Authors
  1. A. Corradini
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. F. Gadducci
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Eugenio Moggi Giuseppe Rosolini

Rights and permissions

Reprints and permissions

Copyright information

© 1997 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Corradini, A., Gadducci, F. (1997). A 2-categorical presentation of term graph rewriting. In: Moggi, E., Rosolini, G. (eds) Category Theory and Computer Science. CTCS 1997. Lecture Notes in Computer Science, vol 1290. Springer, Berlin, Heidelberg. https://doi.org/10.1007/BFb0026983

Download citation

  • DOI: https://doi.org/10.1007/BFb0026983

  • Published:

  • Publisher Name: Springer, Berlin, Heidelberg

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

  • Online ISBN: 978-3-540-69552-3

  • eBook Packages: Springer Book Archive

Publish with us

Policies and ethics

Search

Navigation