From Linear Term Rewriting to Graph Rewriting with Preservation of Termination

TL;DR

This paper demonstrates that PBPO+ graph rewriting formalism can encode linear term rewriting systems while preserving global termination, facilitating the modeling of complex rewriting systems like lambda calculus.

Contribution

It introduces a method to encode linear TRS rules into PBPO+ graph rewriting, maintaining termination properties, which was not possible with previous encodings.

Findings

PBPO+ allows encoding of linear TRS rules with preserved termination.

The encoding can model higher-order rewriting systems like lambda calculus.

Potential to extend TRS termination techniques to graph rewriting formalism.

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.