Disproving Termination of Non-Erasing Sole Combinatory Calculus with Tree Automata (Full Version)
Keisuke Nakano, Munehiro Iwami
TL;DR
The termination of sole combinatory calculus, which consists of only one combinator, is disproven by finding a desirable tree automaton with a SAT solver as done for term rewriting systems by Endrullis and Zantema.
Abstract
We study the termination of sole combinatory calculus, which consists of only one combinator. Specifically, the termination for non-erasing combinators is disproven by finding a desirable tree automaton with a SAT solver as done for term rewriting systems by Endrullis and Zantema. We improved their technique to apply to non-erasing sole combinatory calculus, in which it suffices to search for tree automata with a final sink state. Our method succeeds in disproving the termination of 8 combinators, whose termination has been an open problem.