Checking Termination of Queries to Logic Programs
Checking Termination of Queries to Logic Programs
复制标题
检查逻辑程序查询的终止
DOI：
--
复制
发表时间：
1996
期刊：
影响因子：
--
通讯作者：
Y. Sagiv
中科院分区：
文献类型：
--
作者：
Naomi Lindenstrauss;Y. Sagiv
程序的终止是不可判定的。然而，在逻辑程序的情况下，其中唯一可能的原因是非终止的无限递归，终止实际上可以证明自动为一大类程序。本文描述了一种自动检查逻辑程序查询终止性的算法。给定一个程序和查询，算法要么回答查询终止，要么回答由于无限递归而可能存在非终止。该算法可以使用一个广泛的家庭的范数证明终止性的任何范数。它已在SICStus Prolog中实现。该实现可以自动处理大多数的例子，我们遇到的文献中终止的逻辑程序，约有一半的程序在一个集合的基准，这原本是用于其他目的而不是终止（11的24个程序终止可以自动决定和3个以上，它可以决定后，适当的转换或分割部分）。该算法由三个主要部分组成|实例化分析、约束推理以及与程序和查询相关联的查询-映射对的构造。它使用加权规则图，提取程序规则中关于参数规范的信息。约束推理的一个副产品是递归单调性约束与非递归约束的分离。这使我们能够发现能够在展开后证明终止的程序。
Termination of programs is known to be undecidable. However in the case of logic programs , where the only possible cause for non-termination is innnite recursion, termination can actually be proved automatically for a large class of programs. This paper describes an algorithm for automatically checking termination of queries to logic programs. Given a program and query the algorithm either answers that the query terminates or that there may be non-termination due to innnite recursion. The algorithm can use any norm of a wide family of norms for proving termination. It has been implemented in SICStus Prolog. The implementation can handle automatically most of the examples we encountered in the literature on termination of logic programs, and about half the programs in a collection of benchmarks, which were originally used for purposes other than termination (for 11 of the 24 programs termination can be decided automatically and for 3 more it can be decided after suitable transformation or division to parts). The algorithm consists of three main parts| instantiation analysis, constraint inference, and construction of the query-mapping pairs associated with the program and query. It uses weighted rule graphs, which extract the information about argument norms that is in the program rules. A by-product of the inference of constraints is the separation of recursive monotonicity constraints from nonrecursive ones. This enables us to spot programs for which we will be able to prove termination after unfolding.