结合类型和大小约束用于检查高阶条件重写系统终止性
计算机科学中的逻辑
2016-08-16 v2
摘要
在之前的工作中，第一作者将类型中的大小注释扩展到高阶重写和依赖类型，采用一种称为类型或基于大小的终止性证明技术的终止性证明方法，最初developed for ML-like 程序。这里，我们进一步考虑条件重写和显式量化以及大小注释上的约束。这允许更准确地描述函数输出大小如何取决于其输入大小。因此，我们可以检查更多函数的终止性。我们首先给出一种基于约束求解的通用类型检查算法。然后，我们给出一种带有 Presburger 算术约束的终止性准则。据我们了解，这是首个考虑条件在终止性中的条件的高阶条件重写系统的终止性准则。
关键词
引用
@article{arxiv.cs/0609013,
title = {Combining typing and size constraints for checking the termination of higher-order conditional rewrite systems},
author = {Frédéric Blanqui and Colin Riba},
journal= {arXiv preprint arXiv:cs/0609013},
year = {2016}
}