### Abstract

A new kind of transformation of term rewriting systems (TRS) is proposed, depending on a choice for a model for the TRS. The labelled TRS is obtained from the original one by labelling operation symbols, possibly creating extra copies of same rules. This construction has the remarkable property that the labelled TRS is terminating if and only if the original TRS is terminating. Although the labelled version has more operation symbols and may have more rules (sometimes infinitely many), termination is of ten easier to prove for the labelled TRS than for the original one. This provides a new technique for proving termination, making classical techniques like path orders and polynomial interpretations applicable even for non-simplifying TRS's. The requirement ofhaving a model can slightly be
weakened, yielding a remarkably simple termination proof of the system SUBST of [11] describing explicit substitution in ¿-calculus.

Original language | English |
---|---|

Pages (from-to) | 89-105 |

Journal | Fundamenta Informaticae |

Volume | 24 |

Issue number | 1-2 |

Publication status | Published - 1995 |

## Fingerprint Dive into the research topics of 'Termination of term rewriting by semantic labelling'. Together they form a unique fingerprint.

## Cite this

Zantema, H. (1995). Termination of term rewriting by semantic labelling.

*Fundamenta Informaticae*,*24*(1-2), 89-105.