Rewriting on cyclic structures: Equivalence between the operational and the categorical description

Andrea Corradini; Fabio Gadducci

RAIRO - Theoretical Informatics and Applications (2010)

  • Volume: 33, Issue: 4-5, page 467-493
  • ISSN: 0988-3754

Abstract

top
We present a categorical formulation of the rewriting of possibly cyclic term graphs, based on a variation of algebraic 2-theories. We show that this presentation is equivalent to the well-accepted operational definition proposed by Barendregt et al. – but for the case of circular redexes , for which we propose (and justify formally) a different treatment. The categorical framework allows us to model in a concise way also automatic garbage collection and rules for sharing/unsharing and folding/unfolding of structures, and to relate term graph rewriting to other rewriting formalisms.

How to cite

top

Corradini, Andrea, and Gadducci, Fabio. "Rewriting on cyclic structures: Equivalence between the operational and the categorical description." RAIRO - Theoretical Informatics and Applications 33.4-5 (2010): 467-493. <http://eudml.org/doc/222074>.

@article{Corradini2010,
abstract = { We present a categorical formulation of the rewriting of possibly cyclic term graphs, based on a variation of algebraic 2-theories. We show that this presentation is equivalent to the well-accepted operational definition proposed by Barendregt et al. – but for the case of circular redexes , for which we propose (and justify formally) a different treatment. The categorical framework allows us to model in a concise way also automatic garbage collection and rules for sharing/unsharing and folding/unfolding of structures, and to relate term graph rewriting to other rewriting formalisms. },
author = {Corradini, Andrea, Gadducci, Fabio},
journal = {RAIRO - Theoretical Informatics and Applications},
keywords = {Term graphs; directed acyclic graphs; term graph rewriting; categorical models; traced monoidal categories; 2-categories; algebraic theories; gs-monoidal theories.; cyclic term graphs; algebraic 2-theories; circular redexes; automatic garbage collection; sharing/unsharing; folding/unfolding; term graph rewriting},
language = {eng},
month = {3},
number = {4-5},
pages = {467-493},
publisher = {EDP Sciences},
title = {Rewriting on cyclic structures: Equivalence between the operational and the categorical description},
url = {http://eudml.org/doc/222074},
volume = {33},
year = {2010},
}

TY - JOUR
AU - Corradini, Andrea
AU - Gadducci, Fabio
TI - Rewriting on cyclic structures: Equivalence between the operational and the categorical description
JO - RAIRO - Theoretical Informatics and Applications
DA - 2010/3//
PB - EDP Sciences
VL - 33
IS - 4-5
SP - 467
EP - 493
AB - We present a categorical formulation of the rewriting of possibly cyclic term graphs, based on a variation of algebraic 2-theories. We show that this presentation is equivalent to the well-accepted operational definition proposed by Barendregt et al. – but for the case of circular redexes , for which we propose (and justify formally) a different treatment. The categorical framework allows us to model in a concise way also automatic garbage collection and rules for sharing/unsharing and folding/unfolding of structures, and to relate term graph rewriting to other rewriting formalisms.
LA - eng
KW - Term graphs; directed acyclic graphs; term graph rewriting; categorical models; traced monoidal categories; 2-categories; algebraic theories; gs-monoidal theories.; cyclic term graphs; algebraic 2-theories; circular redexes; automatic garbage collection; sharing/unsharing; folding/unfolding; term graph rewriting
UR - http://eudml.org/doc/222074
ER -

References

top
  1. Z.M. Ariola and J.W. Klop, Equational term graph rewriting. Fund. Inform.26 (1996) 207-240.  Zbl0854.68049
  2. Z.M. Ariola, J.W. Klop and D. Plump, Confluent rewriting of bisimilar term graphs, C. Palamidessi and J. Parrow, Eds., Expressiveness in Concurrency. Elsevier Sciences, Electron. Notes Theoret. Comput. Sci.7 (1997). Available at http://www.elsevier.nl/locate/entcs/volume7.html/.  Zbl0911.68090
  3. 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, J.W. de Bakker, A.J. Nijman and P.C. Treleaven, Eds., Parallel Architectures and Languages Europe. Springer Verlag, Lecture Notes in Comput. Sci.259 (1987) 141-158.  Zbl0681.68037
  4. L. Bernátsky and Z. Ésik, Semantics of flowchart programs and the free Conway theories. Theoret. Informatics Appl.32 (1998) 35-78.  
  5. G. Berry and J.-J. Lévy, Minimal and optimal computations of recursive programs. J. ACM26 (1979) 148-175.  Zbl0388.68012
  6. S. Bloom and Z. Ésik, Axiomatizing schemes and their behaviors. J. Comput. System Sci.31 (1985) 375-393.  Zbl0613.68013
  7. S. Bloom and Z. Ésik, Iteration Theories. EATCS Monographs on Theoretical Computer Science. Springer Verlag (1993).  
  8. S. Bloom and Z. Ésik, The equational logic of fixed points. Theoret. Comput. Sci.179 (1997) 1-60.  Zbl0920.03067
  9. S.L. Bloom, Z. Ésik, A. Labella and E.G. Manes, Iteration 2-theories, M. Johnson, Ed., Algebraic Methodology and Software Technology. Springer Verlag, Lecture Notes in Comput. Sci.1349 (1997) 30-44.  
  10. G. Boudol, Computational semantics of term rewriting systems, M. Nivat and J. Reynolds, Eds., Algebraic Methods in Semantics. Cambridge University Press (1985) 170-235.  
  11. A. Corradini, Term rewriting in CTΣ, M.-C. Gaudel and J.-P. Jouannaud, Eds., Trees in Algebra and Programming. Springer Verlag, Lecture Notes in Comput. Sci.668 (1993) 468-484.  
  12. A. Corradini and F. Drewes, (Cyclic) term graph rewriting is adequate for rational parallel term rewriting, Technical Report TR-97-14. Dipartimento di Informatica, Pisa (1997).  
  13. A. Corradini and F. Gadducci, A 2-categorical presentation of term graph rewriting, E. Moggi and G. Rosolini, Eds., Category Theory and Computer Science. Springer Verlag, Lecture Notes in Comput. Sci.1290 (1997) 87-105.  Zbl0889.68085
  14. A. Corradini and F. Gadducci, Rational term rewriting, M. Nivat, Ed., Foundations of Software Science and Computation Structures. Springer Verlag, Lecture Notes in Comput. Sci.1378 (1998) 156-171.  Zbl0908.68081
  15. A. Corradini and F. Gadducci, An algebraic presentation of term graphs, via gs-monoidal categories. Applied Categorical Structures, to appear.  Zbl0949.68121
  16. A. Corradini, U. Montanari, F. Rossi, H. Ehrig, R. Heckel and M. Löwe, Algebraic approaches to graph transformation I: Basic concepts and double pushout approach, G. Rozenberg, Ed., Handbook of Graph Grammars and Computing by Graph Transformation 1. World Scientific (1997).  
  17. A. Corradini and F. Rossi, Hyperedge replacement jungle rewriting for term rewriting systems and logic programming. Theoret. Comput. Sci.109 (1993) 7-48.  Zbl0781.68074
  18. Gh. Stefanescu, On flowchart theories: Part II. The nondeterministic case. Theoret. Comput. Sci.52 (1987) 307-340.  Zbl0642.68020
  19. Gh. Stefanescu, Algebra of flownomials. Technical Report SFB-Bericht 342/16/94 A. Technical University of München, Institut für Informatik (1994).  
  20. V.-E. Cazanescu and Gh. Stefanescu, Towards a new algebraic foundation of flowchart scheme theory. Fund. Inform.13 (1990) 171-210.  Zbl0705.68071
  21. V.-E. Cazanescu and Gh. Stefanescu, A general result on abstract flowchart schemes with applications to the study of accessibility, reduction and minimization. Theoret. Comput. Sci.99 (1992) 1-63.  Zbl0770.68037
  22. V.-E. Cazanescu and Gh. Stefanescu, Feedback, iteration and repetition, Gh. Paun, Ed., Mathematical Aspects of Natural and Formal Languages. World Scientific (1995) 43-62.  
  23. C.C. Elgot, Monadic computations and iterative algebraic theories, H.E. Rose and J.C. Shepherdson, Eds., Logic Colloquium 1973. North Holland, Stud. Logic Found. Math.80 (1975) 175-230.  
  24. C.C. Elgot, Structured programming with and without GO TO statements. IEEE Trans. Software Engrg.2 (1976) 41-54.  Zbl0348.68008
  25. C.C. Elgot, C.C. Bloom and R. Tindell, The algebraic structure of rooted trees. J. Comput. System Sci.16 (1978) 362-339.  Zbl0389.68007
  26. Z. Ésik, Identities in iterative theories and rational algebraic theories. Computational Linguistics and Computer Languages14 (1980) 183-207.  Zbl0466.68010
  27. Z. Ésik, Group axioms for iteration. Inform. and Comput.148 (1999) 131-180.  Zbl0924.68143
  28. Z. Ésik and A. Labella, Equational properties of iteration in algebraically complete categories. Theoret. Comput. Sci.195 (1998) 61-89.  Zbl0903.18003
  29. W.M. Farmer, J.D. Ramsdell and R.J. Watro, A correctness proof for combinator reduction with cycles. ACM Trans. Program. Lang. Syst.12 (1990) 123-134.  
  30. W.M. Farmer and R.J. Watro, Redex capturing in term graph rewriting, R.V. Book, Ed., Rewriting Techniques and Applications. Springer Verlag, Lecture Notes in Comput. Sci.488 (1991) 13-24.  Zbl0723.68057
  31. S. Ginali, Regular trees and the free iterative theory. J. Comput. System Sci.18 (1979) 222-242.  Zbl0495.68042
  32. J.A. Goguen, J.W. Tatcher, E.G. Wagner and J.R Wright, Initial algebra semantics and continuous algebras. J. ACM24 (1977) 68-95.  Zbl0359.68018
  33. I. Guessarian, Algebraic Semantics. Springer Verlag, Lecture Notes in Comput. Sci.99 (1981).  Zbl0474.68010
  34. M. Hasegawa, Models of Sharing Graphs. Ph.D. Thesis, University of Edinburgh, Department of Computer Science (1997).  Zbl1063.68599
  35. M. Hasegawa, Recursion from cyclic sharing: Traced monoidal categories and models of cyclic lambda-calculus, Ph. de Groote and R. Hindly, Eds., Typed Lambda Calculi and Applications. Springer Verlag, Lecture Notes in Comput. Sci.1210 (1997) 196-213.  
  36. B. Hoffmann and D. Plump, Implementing term rewriting by jungle evaluation. Theoret. Informatics Appl.25 (1991) 445-472.  Zbl0706.68061
  37. A. Joyal, R.H. Street and D. Verity, Traced monoidal categories. Math. Proc. Cambridge Philos. Soc.119 (1996) 425-446.  Zbl0845.18005
  38. G. Kelly, Basic Concepts of Enriched Category Theory. Cambridge University Press (1982).  Zbl0478.18005
  39. G.M. Kelly and R.H. Street, Review of the elements of 2-categories, G.M. Kelly, Ed., Sydney Category Seminar. Springer Verlag, Lecture Notes in Math.420 (1974) 75-103.  Zbl0334.18016
  40. J.R. Kennaway, On ``On Graph Rewritings". Theoret. Comput. Sci.52 (1980) 37-58.  Zbl0636.68028
  41. J.R. Kennaway, J.W. Klop, M.R. Sleep and F.J. de Vries, On the adequacy of graph rewriting for simulating term rewriting. ACM Trans. Program. Lang. Syst.16 (1994) 493-523.  
  42. J.W. Klop, Term rewriting systems, S. Abramsky, D. Gabbay and T. Maibaum, Eds. Oxford University Press, Handb. Log. Comput. Sci.1 (1992) 1-116.  
  43. N. Martí-Oliet and J. Meseguer, From Petri nets to linear logic through categories: A survey. Intrenat. J. Foundations Comput. Sci.4 (1991) 297-399.  Zbl0766.68100
  44. J. Meseguer, Conditional rewriting logic as a unified model of concurrency. Theoret. Comput. Sci.96 (1992) 73-155.  Zbl0758.68043
  45. J. Meseguer and U. Montanari, Petri nets are monoids. Inform. and Comput.88 (1990) 105-155.  Zbl0711.68077
  46. H. Miyoshi, Rewriting logic for cyclic sharing structures, T. Sato and A. Middeldorp, Eds., Fuji International Symposium on Functional and Logic Programming. World Scientific (1998) 167-186.  
  47. U. Montanari and F. Rossi, Contextual nets. Acta Inform.32 (1995) 545-596.  Zbl0835.68084
  48. M.J. Plasmeijer and M.C.J.D. van Eekelen, Functional Programming and Parallel Graph Rewriting. Addison Wesley (1993).  Zbl0788.68023
  49. A.J. Power, An abstract formulation for rewrite systems, D.H. Pitt, D.E. Rydehard, P. Dybjer, A.M. Pitts and A. Poigné, Eds., Category Theory and Computer Science. Springer Verlag, Lecture Notes in Comput. Sci.389 (1989) 300-312.  
  50. W. Reisig, Petri Nets: An Introduction. EACTS Monographs on Theoretical Computer Science. Springer Verlag (1985).  
  51. D.E. Rydehard and E.G. Stell, Foundations of equational deductions: A categorical treatment of equational proofs and unification algorithms, D.H. Pitt, A. Poigné and D.E. Rydehard, Eds., Category Theory and Computer Science. Springer Verlag, Lecture Notes in Comput. Sci.283 (1987) 114-139.  
  52. D. Scott, The lattice of flow diagrams, E. Engeler, Ed., Semantics of Algorithmic Languages, Springer Verlag, Lecture Notes in Math.182 (1971) 311-366.  
  53. M.R. Sleep, M.J. Plasmeijer and M.C. van Eekelen, Term Graph Rewriting: Theory and Practice. Wiley (1993).  Zbl0818.68099
  54. J. Staples, Computation of graph-like expressions. Theoret. Comput. Sci.10 (1980) 171-195.  Zbl0423.68007
  55. J. Staples, Optimal evaluation of graph-like expressions. Theoret. Comput. Sci.10 (1980) 297-316.  Zbl0426.68006
  56. J. Staples, Speeding up subtree replacement systems. Theoret. Comput. Sci.11 (1980) 39-47.  Zbl0438.68032
  57. R.H. Street, Categorical structures, M. Hazewinkel, Ed., Handbook of Algebra. Elsevier (1996) 529-577.  Zbl0854.18001
  58. D.A. Turner, A new implementation technique for applicative languages. Software: Practice and Experience9 (1979) 31-49.  Zbl0386.68009
  59. M. Wand, A concrete approach to abstract recursive definitions, M. Nivat, Ed., Automata, Languages and Programming. North Holland (1973) 331-341.  

NotesEmbed ?

top

You must be logged in to post comments.

To embed these notes on your page include the following JavaScript code on your page where you want the notes to appear.

Only the controls for the widget will be shown in your chosen language. Notes will be shown in their authored language.

Tells the widget how many notes to show per page. You can cycle through additional notes using the next and previous controls.

    
                

Note: Best practice suggests putting the JavaScript code just before the closing </body> tag.