Polytool: Polynomial interpretations as a basis for termination analysis of logic programs

AbstractOur goal is to study the feasibility of porting termination analysis techniques developed for one programming paradigm to another paradigm. In this paper, we show how to adapt termination analysis techniques based on polynomial interpretations—very well known in the context of term rewrite systems—to obtain new (nontransformational) termination analysis techniques for definite logic programs (LPs). This leads to an approach that can be seen as a direct generalization of the traditional techniques in termination analysis of LPs, where linear norms and level mappings are used. Our extension generalizes these to arbitrary polynomials. We extend a number of standard concepts and results on termination analysis to the context of polynomial interpretations. We also propose a constraint-based approach for automatically generating polynomial interpretations that satisfy the termination conditions. Based on this approach, we implemented a new tool, called Polytool, for automatic termination analysis of LPs.

Download Full-text

On termination of meta-programs

Theory and Practice of Logic Programming ◽

10.1017/s1471068404002248 ◽

2005 ◽

Vol 5 (3) ◽

pp. 355-390 ◽

Cited By ~ 8

Author(s):

ALEXANDER SEREBRENIK ◽

DANNY DE SCHREYE

Keyword(s):

Broad Class ◽

The Other ◽

Writing Programs ◽

Logic Programs ◽

Termination Analysis ◽

Rewrite Systems ◽

Term Rewrite Systems ◽

Meta Programming

The term meta-programming refers to the ability of writing programs that have other programs as data and exploit their semantics. The aim of this paper is presenting a methodology allowing us to perform a correct termination analysis for a broad class of practical meta-interpreters, including negation and performing different tasks during the execution. It is based on combining the power of general orderings, used in proving termination of term-rewrite systems and programs, and on the well-known acceptability condition, used in proving termination of logic programs. The methodology establishes a relationship between the ordering needed to prove termination of the interpreted program and the ordering needed to prove termination of the meta-interpreter together with this interpreted program. If such a relationship is established, termination of one of those implies termination of the other one, i.e. the meta-interpreter preserves termination. Among the meta-interpreters that are analysed correctly are a proof trees constructing meta-interpreter, different kinds of tracers and reasoners.

Download Full-text

Proving Properties of Term Rewrite Systems via Logic Programs

Rewriting Techniques and Applications - Lecture Notes in Computer Science ◽

10.1007/978-3-540-25979-4_12 ◽

2004 ◽

pp. 170-184 ◽

Cited By ~ 7

Author(s):

Sébastien Limet ◽

Gernot Salzer

Keyword(s):

Logic Programs ◽

Rewrite Systems ◽

Term Rewrite Systems

Download Full-text

Transformation techniques for context-sensitive rewrite systems

Journal of Functional Programming ◽

10.1017/s0956796803004945 ◽

2004 ◽

Vol 14 (4) ◽

pp. 379-427 ◽

Cited By ~ 31

Author(s):

JÜRGEN GIESL ◽

AART MIDDELDORP

Keyword(s):

Functional Programming ◽

Term Rewriting ◽

Lazy Evaluation ◽

Transformation Techniques ◽

Termination Analysis ◽

Rewrite Systems ◽

Context Sensitive ◽

Term Rewrite Systems ◽

Huge Variety

Context-sensitive rewriting is a computational restriction of term rewriting used to model non-strict (lazy) evaluation in functional programming. The goal of this paper is the study and development of techniques to analyze the termination behavior of context-sensitive rewrite systems. For that purpose, several methods have been proposed in the literature which transform context-sensitive rewrite systems into ordinary rewrite systems such that termination of the transformed ordinary system implies termination of the original context-sensitive system. In this way, the huge variety of existing techniques for termination analysis of ordinary rewriting can be used for context-sensitive rewriting, too. We analyze the existing transformation techniques for proving termination of context-sensitive rewriting and we suggest two new transformations. Our first method is simple, sound, and more powerful than the previously proposed transformations. However, it is not complete, i.e., there are terminating context-sensitive rewrite systems that are transformed into non-terminating term rewrite systems. The second method that we present in this paper is both sound and complete. All these observations also hold for rewriting modulo associativity and commutativity.

Download Full-text