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.
@InProceedings{endrullis_et_al:LIPIcs.RTA.2015.160, author = {Endrullis, J\"{o}rg and Zantema, Hans}, title = {{Proving non-termination by finite automata}}, booktitle = {26th International Conference on Rewriting Techniques and Applications (RTA 2015)}, pages = {160--176}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-939897-85-9}, ISSN = {1868-8969}, year = {2015}, volume = {36}, editor = {Fern\'{a}ndez, Maribel}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.RTA.2015.160}, URN = {urn:nbn:de:0030-drops-51952}, doi = {10.4230/LIPIcs.RTA.2015.160}, annote = {Keywords: non-termination, finite automata, regular languages} }
Feedback for Dagstuhl Publishing