{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,27]],"date-time":"2025-10-27T20:30:39Z","timestamp":1761597039206},"reference-count":34,"publisher":"Cambridge University Press (CUP)","issue":"3","license":[{"start":{"date-parts":[[2007,6,1]],"date-time":"2007-06-01T00:00:00Z","timestamp":1180656000000},"content-version":"unspecified","delay-in-days":0,"URL":"https:\/\/www.cambridge.org\/core\/terms"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Math. Struct. Comp. Sci."],"published-print":{"date-parts":[[2007,6]]},"abstract":"<jats:p>The Rewriting Calculus (\u03c1-calculus, for short) was introduced at the end of the 1990s and fully integrates term-rewriting and \u03bb-calculus. The rewrite rules, acting as elaborated abstractions, their application and the structured results obtained are first class objects of the calculus. The evaluation mechanism, which is a generalisation of beta-reduction, relies strongly on term matching in various theories.<\/jats:p><jats:p>In this paper we propose an extension of the \u03c1-calculus, called \u03c1<jats:sub>g<\/jats:sub>-calculus, that handles structures with cycles and sharing rather than simple terms. This is obtained by using recursion constraints in addition to the standard \u03c1-calculus matching constraints, which leads to a term-graph representation in an equational style. Like in the \u03c1-calculus, the transformations are performed by explicit application of rewrite rules as first-class entities. The possibility of expressing sharing and cycles allows one to represent and compute over regular infinite entities.<\/jats:p><jats:p>We show that the \u03c1<jats:sub>g<\/jats:sub>-calculus, under suitable linearity conditions, is confluent. The proof of this result is quite elaborate, due to the non-termination of the system and the fact that \u03c1<jats:sub>g<\/jats:sub>-calculus-terms are considered modulo an equational theory. We also show that the \u03c1<jats:sub>g<\/jats:sub>-calculus is expressive enough to simulate first-order (equational) left-linear term-graph rewriting and \u03b1-calculus with explicit recursion (modelled using a letrec-like construct).<\/jats:p>","DOI":"10.1017\/s0960129507006093","type":"journal-article","created":{"date-parts":[[2007,7,6]],"date-time":"2007-07-06T13:51:23Z","timestamp":1183729883000},"page":"363-406","source":"Crossref","is-referenced-by-count":9,"title":["A rewriting calculus for cyclic higher-order term graphs"],"prefix":"10.1017","volume":"17","author":[{"given":"PAOLO","family":"BALDAN","sequence":"first","affiliation":[]},{"given":"CLARA","family":"BERTOLISSI","sequence":"additional","affiliation":[]},{"given":"HORATIU","family":"CIRSTEA","sequence":"additional","affiliation":[]},{"given":"CLAUDE","family":"KIRCHNER","sequence":"additional","affiliation":[]}],"member":"56","published-online":{"date-parts":[[2007,6,1]]},"reference":[{"key":"S0960129507006093_ref28","doi-asserted-by":"crossref","unstructured":"Parigot M. (1992) \u03bb\u03bc-Calculus: An Algorithmic Interpretation of Classical Natural Deduction. In: Voronkov A. (ed.) Proceedings of LPAR'92, Logic Programming and Automated Reasoning, St Petersburg, Russia, July 1992. Springer-Verlag Lecture Notes in Artificial Intelligence 624 190\u2013201.","DOI":"10.1007\/BFb0013061"},{"key":"S0960129507006093_ref27","doi-asserted-by":"publisher","DOI":"10.1007\/BFb0052358"},{"key":"S0960129507006093_ref22","doi-asserted-by":"publisher","DOI":"10.1016\/S0304-3975(96)00171-5"},{"key":"S0960129507006093_ref32","volume-title":"Term graph rewriting: theory and practice","author":"Sleep","year":"1993"},{"key":"S0960129507006093_ref12","doi-asserted-by":"publisher","DOI":"10.1016\/S1571-0661(05)82526-5"},{"key":"S0960129507006093_ref17","doi-asserted-by":"publisher","DOI":"10.1051\/ita:1999128"},{"key":"S0960129507006093_ref16","unstructured":"Corradini A. and Drewes F. (1997) (Cyclic) Term Graph Rewriting is Adequate for Rational Parallel Term Rewriting. Technical Report TR-97-14, Dipartimento di Informatica, Pisa."},{"key":"S0960129507006093_ref25","unstructured":"Klop J. W. (1980) Combinatory Reduction Systems, Ph.D. thesis, CWI."},{"key":"S0960129507006093_ref11","first-page":"77","volume-title":"Springer-Verlag Lecture Notes in Computer Science","volume":"2051","author":"Cirstea","year":"2001"},{"key":"S0960129507006093_ref21","doi-asserted-by":"publisher","DOI":"10.1145\/177492.177577"},{"key":"S0960129507006093_ref29","doi-asserted-by":"publisher","DOI":"10.1145\/322248.322251"},{"key":"S0960129507006093_ref13","doi-asserted-by":"crossref","unstructured":"Cirstea H. , Liquori L. and Wack B. (2003) Rewriting Calculus with Fixpoints: Untyped and First-order Systems. In: Berardi S. , Coppo M. and Damian F. (eds.) Types for Proofs and Programs (TYPES). Springer-Verlag Lecture Notes in Computer Science 3085 147\u2013171.","DOI":"10.1007\/978-3-540-24849-1_10"},{"key":"S0960129507006093_ref14","unstructured":"Colmerauer A. (1984) Equations and Inequations on Finite and Infinite Trees. In: Proceedings of FGCS'84 85\u201399."},{"key":"S0960129507006093_ref23","doi-asserted-by":"publisher","DOI":"10.1006\/inco.1995.1075"},{"key":"S0960129507006093_ref10","first-page":"427","article-title":"The rewriting calculus \u2014 Part I and II","volume":"9","author":"Cirstea","year":"2001","journal-title":"Logic Journal of the Interest Group in Pure and Applied Logics"},{"key":"S0960129507006093_ref24","volume-title":"Unification","author":"Kirchner","year":"1990"},{"key":"S0960129507006093_ref15","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-56610-4_83"},{"key":"S0960129507006093_ref26","unstructured":"Lankford D. S. and Ballantyne A. (1977) Decision procedures for simple equational theories with permutative axioms: complete sets of permutative reductions. Technical report, Univ. of Texas at Austin, Dept. of Mathematics and Computer Science."},{"key":"S0960129507006093_ref20","doi-asserted-by":"publisher","DOI":"10.1137\/0215084"},{"key":"S0960129507006093_ref3","doi-asserted-by":"publisher","DOI":"10.1006\/inco.1997.2651"},{"key":"S0960129507006093_ref19","doi-asserted-by":"publisher","DOI":"10.1145\/322217.322230"},{"key":"S0960129507006093_ref4","unstructured":"Barendregt H. (1984) The Lambda-Calculus, its syntax and semantics, Second edition, Studies in Logic and the Foundation of Mathematics, Elsevier Science Publishers."},{"key":"S0960129507006093_ref18","doi-asserted-by":"crossref","unstructured":"Courcelle B. (1980) Infinite Trees in Normal Form and Recursive Equations having a unique solution. Math. Syst. Theory.","DOI":"10.1007\/BF01744293"},{"key":"S0960129507006093_ref1","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796800000186"},{"key":"S0960129507006093_ref2","doi-asserted-by":"crossref","first-page":"207","DOI":"10.3233\/FI-1996-263401","article-title":"Equational term graph rewriting","volume":"26","author":"Ariola","year":"1996","journal-title":"Fundamenta Informaticae"},{"key":"S0960129507006093_ref9","doi-asserted-by":"publisher","DOI":"10.1016\/j.entcs.2004.06.029"},{"key":"S0960129507006093_ref6","doi-asserted-by":"publisher","DOI":"10.1145\/604131.604152"},{"key":"S0960129507006093_ref5","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-17945-3_8"},{"key":"S0960129507006093_ref7","unstructured":"Bertolissi C. (2005) The graph rewriting calculus: properties and expressive capabilities, Th\u00e8se de Doctorat d'Universit\u00e9, Institut National Polytechnique de Lorraine, Nancy, France."},{"key":"S0960129507006093_ref31","doi-asserted-by":"publisher","DOI":"10.1142\/9789812815149_0001"},{"key":"S0960129507006093_ref8","doi-asserted-by":"publisher","DOI":"10.2307\/2266170"},{"key":"S0960129507006093_ref30","unstructured":"Peyton-Jones S. (1987) The implementation of functional programming languages, Prentice Hall."},{"key":"S0960129507006093_ref33","first-page":"31","article-title":"A new implementation technique for applicative languages","volume":"9","author":"Turner","year":"1979","journal-title":"Software:Practice and Experience"},{"key":"S0960129507006093_ref34","unstructured":"Wack B. (2005) Typage et d\u00e9duction dans le calcul de r\u00e9\u00e9criture, Th\u00e8se de doctorat, Universit\u00e9 Henri Poincar\u00e9 \u2013 Nancy I."}],"container-title":["Mathematical Structures in Computer Science"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/www.cambridge.org\/core\/services\/aop-cambridge-core\/content\/view\/S0960129507006093","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,4,24]],"date-time":"2020-04-24T03:17:53Z","timestamp":1587698273000},"score":1,"resource":{"primary":{"URL":"https:\/\/www.cambridge.org\/core\/product\/identifier\/S0960129507006093\/type\/journal_article"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2007,6]]},"references-count":34,"journal-issue":{"issue":"3","published-print":{"date-parts":[[2007,6]]}},"alternative-id":["S0960129507006093"],"URL":"https:\/\/doi.org\/10.1017\/s0960129507006093","relation":{},"ISSN":["0960-1295","1469-8072"],"issn-type":[{"value":"0960-1295","type":"print"},{"value":"1469-8072","type":"electronic"}],"subject":[],"published":{"date-parts":[[2007,6]]}}}