非擦除唯一组合计算的终止性：基于树自动机的反证（完整版）
计算机科学中的逻辑
2024-06-21 v1 形式语言与自动机理论
摘要
我们研究唯一组合计算的终止性问题，该计算仅包含一个组合子。具体而言，通过寻找合适的树自动机（正如 Endrullis 和 Zantema 对项重写系统所做的那样），我们否定了非擦除组合子的终止性。我们改进了他们的技术，以适用于非擦除唯一组合计算，其中只需搜索具有最终汇聚状态的树自动机。我们的方法成功否定了8个组合子的终止性，这些组合子终止性一直是开放问题。
引用
@article{arxiv.2406.14305,
title = {Disproving Termination of Non-Erasing Sole Combinatory Calculus with Tree Automata (Full Version)},
author = {Keisuke Nakano and Munehiro Iwami},
journal= {arXiv preprint arXiv:2406.14305},
year = {2024}
}
备注
This is the full version of the corresponding CIAA 2024 paper