On Singleton Self-Loop Removal for Termination of LCTRSs with Bit-Vector Arithmetic

TL;DR

This paper introduces a new dependency pair processor for logically constrained term rewrite systems with bit-vector arithmetic, improving termination proofs by analyzing self-loop dependency pairs through acyclic graphs.

Contribution

It proposes a novel DP processor based on acyclic graphs to handle singleton self-loop problems in BV-LCTRSs, enhancing termination analysis methods.

Findings

A sufficient condition for the existence of an acyclic graph is provided.

The method simplifies the analysis for specific cases.

The approach improves termination proofs for BV-LCTRSs.

Abstract

As for term rewrite systems, the dependency pair (DP, for short) framework with several kinds of DP processors is useful for proving termination of logically constrained term rewrite systems (LCTRSs, for short). However, the polynomial interpretation processor is not so effective against LCTRSs with bit-vector arithmetic (BV-LCTRSs, for short). In this paper, we propose a novel DP processor for BV-LCTRSs to solve a singleton DP problem consisting of a dependency pair forming a self-loop. The processor is based on an acyclic directed graph such that the nodes are bit-vectors and any dependency chain of the problem is projected to a path of the graph. We show a sufficient condition for the existence of such an acyclic graph, and simplify it for a specific case.