终止转换：一种灵活的通用递归终止方法
Termination Casts: A Flexible Approach to Termination with General Recursion
摘要：
本文提出了一个类型和效果系统Teqt，它区分终止项和全函数与可能的发散项和部分函数，适用于具有一般递归和等式类型的λ演算.其中心思想是包含一个原始类型形式“Terminates t”，表示术语t是终止的;然后允许术语t被强制从可能发散到总和，使用Terminates t的证明。我们将这种递归函数称为终止类型转换，并展示如何使用它们实现终止递归。对于元理论的系统，我们描述了一个翻译从Teqt终止一般递归，简单类型的功能的逻辑理论。Teqt的每一个类型判断都被转化为一个定理，该定理表达了Teqt项的计算部分的适当终止性质。
英文摘要：
This paper proposes a type-and-effect system called Teqt, which distinguishes terminating terms and total functions from possibly diverging terms and partial functions, for a lambda calculus with general recursion and equality types. The central idea is to include a primitive type-form "Terminates t", expressing that term t is terminating; and then allow terms t to be coerced from possibly diverging to total, using a proof of Terminates t. We call such coercions termination casts, and show how to implement terminating recursion using them. For the meta-theory of the system, we describe a translation from Teqt to a logical theory of termination for general recursive, simply typed functions. Every typing judgment of Teqt is translated to a theorem expressing the appropriate termination property of the computational part of the Teqt term.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
