半连续尺寸类型和终止
Semi-continuous Sized Types and Termination
摘要：
一些基于类型的终止方法使用大小类型：数据结构大小的序数界限存储在其类型中。如果在类型系统中可见递归调用仅在较小的大小上发生，则接受大小调整类型上的递归函数。这种方法只有在递归函数的类型是可接受的情况下才是合理的，即，在某种程度上取决于大小指数。为了探索空间的容许函数在存在较高的kinded数据类型和impredicative多态性，语义的大小类型被解释为从序数到强规范化的条款集的功能。结果表明，上半连续的这种功能是一个充分的语义准则的可容许性。为了提供一个语法标准，半连续函数的演算。
英文摘要：
Some type-based approaches to termination use sized types: an ordinal bound for the size of a data structure is stored in its type. A recursive function over a sized type is accepted if it is visible in the type system that recursive calls occur just at a smaller size. This approach is only sound if the type of the recursive function is admissible, i.e., depends on the size index in a certain way. To explore the space of admissible functions in the presence of higher-kinded data types and impredicative polymorphism, a semantics is developed where sized types are interpreted as functions from ordinals into sets of strongly normalizing terms. It is shown that upper semi-continuity of such functions is a sufficient semantic criterion for admissibility. To provide a syntactical criterion, a calculus for semi-continuous functions is developed.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
