Type-Based Termination with Sized Products
Type-Based Termination with Sized Products
复制标题
具有尺寸产品的基于类型的端接
DOI：
--
复制
发表时间：
2008
期刊：
影响因子：
--
通讯作者：
Colin Riba
中科院分区：
文献类型：
--
作者：
G. Barthe;B. Grégoire;Colin Riba
基于类型的终止是一种语义上直观的方法，通过跟踪数据类型元素的大小，并通过检查递归调用对较小参数的操作来确保递归定义的终止。然而，许多使用基于类型终止的系统依赖于语义异常来保证强规范化;即，它们强制数据类型的非递归元素（例如空列表）具有大小1而不是0。这种语义上的异常也阻止了像快速排序这样的函数得到精确的输入。
本文的主要贡献是一个类型的系统，纠正这种异常，并仍然确保终止。此外，我们的类型系统的特点前束阶段多态性，削弱存在量化阶段，是足够精确的类型quicksort作为一个非大小增加功能。此外，我们的系统适应阶段除了所有积极的归纳类型。
Type-based termination is a semantically intuitive method that ensures termination of recursive definitions by tracking the size of datatype elements, and by checking that recursive calls operate on smaller arguments. However, many systems using type-based termination rely on a semantical anomaly to guarantee strong normalization; namely, they impose that non-recursive elements of a datatype, e.g. the empty list, have size 1 instead of 0. This semantical anomaly also prevents functions such as quicksort to be given a precise typing.
The main contribution of this paper is a type system that remedies this anomaly, and still ensures termination. In addition, our type system features prenex stage polymorphism, a weakening of existential quantification over stages, and is precise enough to type quicksort as a non-size increasing function. Moreover, our system accomodate stage addition with all positive inductive types.