Disproving Termination of Non-Erasing Sole Combinatory Calculus with Tree Automata (Full Version)
Fuente:
arXiv
Salvato in:
| Autori principali: | , |
|---|---|
| Natura: | Preprint |
| Pubblicazione: |
2024
|
| Soggetti: | |
| Accesso online: | |
| Tags: |
Aggiungi Tag
Nessun Tag, puoi essere il primo ad aggiungerne!!
|
| _version_ | 1866909228149506048 |
|---|---|
| author | Nakano, Keisuke Iwami, Munehiro |
| author_facet | Nakano, Keisuke Iwami, Munehiro |
| contents | 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. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2406_14305 |
| institution | arXiv |
| publishDate | 2024 |
| record_format | arxiv |
| spellingShingle | Disproving Termination of Non-Erasing Sole Combinatory Calculus with Tree Automata (Full Version) Nakano, Keisuke Iwami, Munehiro Logic in Computer Science Formal Languages and Automata Theory 03B40 (Primary) 68Q45, 68Q42, 68V05 (Secondary) F.4.1; F.4.2; F.4.3 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. |
| title | Disproving Termination of Non-Erasing Sole Combinatory Calculus with Tree Automata (Full Version) |
| topic | Logic in Computer Science Formal Languages and Automata Theory 03B40 (Primary) 68Q45, 68Q42, 68V05 (Secondary) F.4.1; F.4.2; F.4.3 |
| url | https://arxiv.org/abs/2406.14305 |