Proving and Disproving Termination of Higher-Order Functions
Proving and Disproving Termination of Higher-Order Functions
复制标题
证明和反驳高阶函数的终止
DOI：
--
复制
发表时间：
2005
期刊：
影响因子：
--
通讯作者：
Peter Schneider
中科院分区：
文献类型：
--
作者：
J. Giesl;René Thiemann;Peter Schneider
依赖对技术是一个强大的模块化方法的自动终止证明的术语重写系统（TRS）。我们提出了两个重要的扩展这项技术：首先，我们展示了如何证明终止高阶函数使用依赖对。为此，依赖对技术扩展到处理（无类型）应用TRS。其次，我们介绍了一种利用依赖对证明非终止性的方法，而到目前为止，依赖对只用于验证终止性。我们的研究结果导致一个框架相结合的终止和非终止技术的第一和高阶函数在一个非常灵活的方式。我们在自动终止证明器AProVE中实施并评估了我们的结果。
The dependency pair technique is a powerful modular method for automated termination proofs of term rewrite systems (TRSs). We present two important extensions of this technique: First, we show how to prove termination of higher-order functions using dependency pairs. To this end, the dependency pair technique is extended to handle (untyped) applicative TRSs. Second, we introduce a method to prove non-termination with dependency pairs, while up to now dependency pairs were only used to verify termination. Our results lead to a framework for combining termination and non-termination techniques for first- and higher-order functions in a very flexible way. We implemented and evaluated our results in the automated termination prover AProVE.