2024/06/20 by Keisuke Nakano, Nakano, Keisuke, Munehiro Iwami +1
Computer Science · #03B40 (Primary) 68Q45 #68Q42 #68V05 (Secondary) #F.4.1 #F.4.2 #F.4.3 #FOS: Computer and information sciences #Formal Languages and Automata Theory (cs.FL) #Formal Methods in Verification #Logic in Computer Science (cs.LO) #Logic, programming, and type systems #semigroups and automata theory
paper · pdf · doi:10.48550/arxiv.2406.14305
openalex publication_date 2024/06/20 · openalex created_date 2024/06/22 · openalex updated_date 2026/07/28
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.