|
Journal description
All volumes of the corresponding journal
All issues of the corresponding volume
All articles of the corresponding issues
Details for article 1 of 1 found articles
| Title: |
TERMINATION OF TERM REWRITING BY SEMANTIC LABELLING |
| Author: |
Zantema, H. |
| Appeared in: |
Fundamenta informaticae |
| Paging: | Volume 24 (2011) nr. 1-2 pages 89-105 |
| Year: |
2011-02-08 |
| Contents: |
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 some 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 often 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 of having a model can slightly be weakened, yielding a remarkably simple termination proof of the system SUBST of [11] describing explicit substitution in λ-calculus. |
| Publisher: |
IOS Press |
| Source file: |
Elektronische Wetenschappelijke Tijdschriften |
Details for article 1 of 1 found articles