论大小终止与语义标注的关系
On the relation between size-based termination and semantic labelling
摘要：
我们调查两个独立开发的终止技术之间的关系。一方面，基于大小类型的终止（sized-typesbasedtermination，SBT）使用带有大小表达式和Girard的reductioncandidates注释的类型，并且仅适用于使用构造函数匹配的系统。另一方面，语义标记通过用其参数的语义注释每个函数符号来转换重写系统，并且适用于任何重写系统。首先，我们介绍了一个简化版本的SBT的简单类型的Alzuda演算。然后，我们给出了新的证明的正确性SBT使用语义标签，在第一和高阶的情况下。因此，我们表明，SBT可以扩展到使用定义的符号（例如，关联函数）匹配的系统。
英文摘要：
We investigate the relationship between two independently developed termination techniques. On the one hand, sized-types based termination (SBT) uses types annotated with size expressions and Girard's reducibility candidates, and applies on systems using constructor matching only. On the other hand, semantic labelling transforms a rewrite system by annotating each function symbol with the semantics of its arguments, and applies to any rewrite system. First, we introduce a simplified version of SBT for the simply-typed lambda-calculus. Then, we give new proofs of the correctness of SBT using semantic labelling, both in the first and in the higher-order case. As a consequence, we show that SBT can be extended to systems using matching on defined symbols (e.g. associative functions).
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
