A Characterization of Quasi-Decreasingness

TL;DR

This paper establishes a direct proof linking -termination of context-sensitive unravelings to quasi-decreasingness of DCTRSs, and reports experimental results on confluence-related problems.

Contribution

It provides a direct proof of the equivalence between -termination and quasi-decreasingness, and extends experimental analysis on confluence problems.

Findings

-termination implies quasi-decreasingness

Experimental results support theoretical findings

Extended analysis on confluence problems database

Abstract

In 2010 Schernhammer and Gramlich showed that quasi-decreasingness of a DCTRS R is equivalent to \mu-termination of its context-sensitive unraveling Ucs(R) on original terms. While the direction that quasi-decreasingness of R implies \mu-termination of Ucs(R) on original terms is shown directly; the converse - facilitating the use of context-sensitive termination tools like MU-TERM and VMTL - employs the additional notion of context-sensitive quasi-reductivity of R. In the following, we give a direct proof of the fact that \mu-termination of Ucs(R) on original terms implies quasi-decreasingness of R. Moreover, we report our experimental findings on DCTRSs from the confluence problems database (Cops), extending the experiments of Schernhammer and Gramlich.