Abstract
Encodings of term rewriting systems (TRSs) into graph rewriting systems usually lose global termination, meaning the encodings do not terminate on all graphs. A typical encoding of the terminating TRS rule a(b(x)) → b(a(x)), for example, may be indefinitely applicable along a cycle of a’s and b’s. Recently, we introduced PBPO+, a graph rewriting formalism in which rules employ a type graph to specify transformations and control rule applicability. In the present paper, we show that PBPO+ allows for a natural encoding of linear TRS rules that preserves termination globally. This result is a step towards modeling other rewriting formalisms, such as lambda calculus and higher order rewriting, using graph rewriting in a way that preserves properties like termination and confluence. We moreover expect that the encoding can serve as a guide for lifting TRS termination methods to PBPO+ rewriting.
| Original language | English |
|---|---|
| Pages (from-to) | 19-34 |
| Number of pages | 16 |
| Journal | Electronic Proceedings in Theoretical Computer Science, EPTCS |
| Volume | 350 |
| Early online date | 21 Dec 2021 |
| DOIs | |
| Publication status | Published - 2021 |
| Event | 12th International Workshop on Graph Computational Models, GCM 2021 - Virtual, Online Duration: 22 Jun 2021 → … |
Bibliographical note
Funding Information:We thank anonymous reviewers for useful suggestions and corrections. Both authors received funding from the Netherlands Organization for Scientific Research (NWO) under the Innovational Research Incentives Scheme Vidi (project. No. VI.Vidi.192.004).
Publisher Copyright:
© R. Overbeek & J. Endrullis
Funding
We thank anonymous reviewers for useful suggestions and corrections. Both authors received funding from the Netherlands Organization for Scientific Research (NWO) under the Innovational Research Incentives Scheme Vidi (project. No. VI.Vidi.192.004).