Termination of Innermost-Terminating Right-Linear Overlay Term Rewrite Systems (Full Version)
Logic in Computer Science
2026-04-23 v1
Abstract
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.
Cite
@article{arxiv.2604.20754,
title = {Termination of Innermost-Terminating Right-Linear Overlay Term Rewrite Systems (Full Version)},
author = {Naoki Nishida},
journal= {arXiv preprint arXiv:2604.20754},
year = {2026}
}
Comments
9 pages, full version of a submission to WST 2026