利用高度为 omega 的转移不变量证明终止性
计算机科学中的逻辑
2014-07-18 v1
摘要
Podelski 和 Rybalchenko 的终止定理指出，从任何初始状态出发均终止的归约关系，恰恰是那些其传递闭包（限制在可达状态上）包含于某些良基关系有限并集中的归约关系。该定理的另一种表述是：终止的归约关系正是那些具有“析取良基转移不变量”的关系。基于此结果，这些作者与 Byron Cook 设计了一种算法，用于检查 while-if 程序终止的充分条件。该算法寻找一个由高度为 omega 的良基关系构成的析取良基转移不变量，若找到，则利用终止定理推导该 while-if 程序的终止性。这引发了一个有趣的问题：具有析取良基转移不变量（其中每个关系的高度均为 omega）的归约关系处于何种地位？回答这个问题可以刻画终止算法能够证明终止的 while-if 程序集合。本工作的目标是证明，它们恰恰是那些具有高度 （对于某个 ）的归约关系集合。此外，如果转移不变量中的所有关系都是原始递归的，且归约关系是某个原始递归映射限制在某个原始递归集合上的图，则最终状态可由某个关于初始状态的原始递归映射计算得出。作为推论，我们得出：至少在 Podelski-Rybalchenko while-if 语言中拥有一种实现（其具有析取良基转移不变量且每个关系高度为 omega）的函数集合，恰恰是原始递归函数集合。
引用
@article{arxiv.1407.4692,
title = {Proving termination with transition invariants of height omega},
author = {Stefano Berardi and Paulo Oliva and Silvia Steila},
journal= {arXiv preprint arXiv:1407.4692},
year = {2014}
}