Proving Looping and Non-Looping Non-Termination by Finite Automata

TL;DR

This paper introduces an automated method using finite automata and SAT solving to prove non-termination in term rewriting systems, successfully handling cases where previous techniques failed.

Contribution

It presents a novel automata-based approach for non-termination proofs, expanding the toolkit for analyzing term rewriting systems.

Findings

Successfully proves non-termination for complex examples like the S-rule.

Automates the process using SAT formulas and finite automata.

Outperforms earlier techniques on challenging cases.

Abstract

A new technique is presented to prove non-termination of term rewriting. The basic idea is to find a non-empty regular language of terms that is closed under rewriting and does not contain normal forms. It is automated by representing the language by a tree automaton with a fixed number of states, and expressing the mentioned requirements in a SAT formula. Satisfiability of this formula implies non-termination. Our approach succeeds for many examples where all earlier techniques fail, for instance for the S-rule from combinatory logic.