Termination of Innermost-Terminating Right-Linear Overlay Term Rewrite Systems (Full Version)
Fuente:
arXiv
Enregistré dans:
| Auteur principal: | |
|---|---|
| Format: | Preprint |
| Publié: |
2026
|
| Sujets: | |
| Accès en ligne: | |
| Tags: |
Ajouter un tag
Pas de tags, Soyez le premier à ajouter un tag!
|
| _version_ | 1866914499395584000 |
|---|---|
| author | Nishida, Naoki |
| author_facet | Nishida, Naoki |
| contents | It has been shown that, regarding a terminating right-linear overlay term rewrite system (TRS), any rewrite sequence ending with a normal form can be simulated by the innermost reduction. In this paper, using this simulation property, we show that for a right-linear overlay TRS, there is no infinite minimal dependency-pair chain if and only if there is no infinite innermost minimal dependency-pair chain. This implies that a right-linear overlay TRS is terminating if and only if it is innermost terminating. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2604_20754 |
| institution | arXiv |
| publishDate | 2026 |
| record_format | arxiv |
| spellingShingle | Termination of Innermost-Terminating Right-Linear Overlay Term Rewrite Systems (Full Version) Nishida, Naoki Logic in Computer Science 68Q42 F.4.2 It has been shown that, regarding a terminating right-linear overlay term rewrite system (TRS), any rewrite sequence ending with a normal form can be simulated by the innermost reduction. In this paper, using this simulation property, we show that for a right-linear overlay TRS, there is no infinite minimal dependency-pair chain if and only if there is no infinite innermost minimal dependency-pair chain. This implies that a right-linear overlay TRS is terminating if and only if it is innermost terminating. |
| title | Termination of Innermost-Terminating Right-Linear Overlay Term Rewrite Systems (Full Version) |
| topic | Logic in Computer Science 68Q42 F.4.2 |
| url | https://arxiv.org/abs/2604.20754 |