Termination of Innermost-Terminating Right-Linear Overlay Term Rewrite Systems (Full Version)

TL;DR

This paper proves that for right-linear overlay TRSs, termination is equivalent to innermost termination, based on a simulation property linking rewrite sequences and dependency pairs.

Contribution

It establishes a new equivalence between termination and innermost termination for right-linear overlay TRSs using dependency pair analysis.

Findings

Termination and innermost termination are equivalent for right-linear overlay TRSs.

A simulation property links rewrite sequences ending in normal forms to innermost reductions.

No infinite minimal dependency-pair chain exists if and only if no infinite innermost minimal dependency-pair chain exists.

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.