论文标题
递归方案的无限性：更简单的系统
Unboundedness for Recursion Schemes: A Simpler Type System
论文作者
论文摘要
Clemente，Parys，Salvati和Walukiewicz（2016）建立了无限制和同时无限制和同时无限制问题（又称对角线问题）的可决定性（对角线问题）。然后，Parys提出了最佳复杂性的程序（2017）；此过程使用复杂的类型系统，涉及多个标志和标记。我们在这里提出一个更简单，更直观的类型系统，具有相同的目的。我们证明，这种类型的系统允许解决一个被称为递归方案的子类（称为安全方案）的无界度问题。对于不安全的递归方案，我们只有类型系统的合理性：如果可以建立一种类型的派生，声称递归方案是没有绑定的，那么它确实是无限的。不安全递归方案的类型系统的完整性是一个空旷的问题。再进一步，我们讨论了类型系统的扩展，该系统允许处理同时无限制问题。 我们还设计和实施了一种算法，该算法将完全自动检查给定递归方案的无限制，并在短时间内完成各种输入。
Decidability of the problems of unboundedness and simultaneous unboundedness (aka. the diagonal problem) for higher-order recursion schemes was established by Clemente, Parys, Salvati, and Walukiewicz (2016). Then a procedure of optimal complexity was presented by Parys (2017); this procedure used a complicated type system, involving multiple flags and markers. We present here a simpler and much more intuitive type system serving the same purpose. We prove that this type system allows to solve the unboundedness problem for a widely considered subclass of recursion schemes, called safe schemes. For unsafe recursion schemes we only have soundness of the type system: if one can establish a type derivation claiming that a recursion scheme is unbounded then it is indeed unbounded. Completeness of the type system for unsafe recursion schemes is left as an open question. Going further, we discuss an extension of the type system that allows to handle the simultaneous unboundedness problem. We also design and implement an algorithm that fully automatically checks unboundedness of a given recursion scheme, completing in a short time for a wide variety of inputs.
