Disproving Termination of Non-Erasing Sole Combinatory Calculus with Tree Automata (Full Version)

TL;DR

This paper demonstrates that the termination of non-erasing sole combinatory calculus can be disproven using an improved tree automaton approach, solving previously open problems about combinator termination.

Contribution

It extends the tree automaton technique to non-erasing sole combinatory calculus, successfully disproving termination for 8 previously unresolved combinators.

Findings

Disproved termination for 8 combinators.

Extended tree automaton method to non-erasing calculus.

Solved open problems in combinator termination.

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.