[Applications, cTI system, help, architecture, contributors, literature, related systems]

Termination inference

When does a logic program terminate? Termination inference, a new kind of program analysis, answers this question with a compact formula, called termination condition. All queries whose termination has been proven are described by this condition. For example, the condition app(A,B,C) terminates_if b(A);b(C) is inferred for program app/3. Here, b(A) is true if the term size of A is bound, e.g. finite and ground. Disjunctions are denoted as ;. Thus, app/3 has been proven to terminate, if the first or the last argument is bound.

Termination inference is an annotation free generalization of termination analysis/checking. It shifts the programmer's focus away from particular cases to the whole relation. Traditionally, a termination analyzer tries to prove that a given class of queries terminates. This class must be provided by the user, which is rather cumbersome if the programs have been written previously without any annotations. With termination inference no annotations are necessary. All provably terminating classes to all related predicates are inferred at once, illustrating the `multi-directionality' of predicates. This means that predicates can be used safely in several `directions'.

Applications of termination inference

The cTI system

cTI_lt (constraint based termination inference for left termination) infers classes of universally terminating programs for the left most selection rule (Prolog style execution). You can use cTI_lt via the WWW (Help), or immediately look at the benchmark collection. The most recent version is located at the University of Parma site.

cTI_lt has been integrated into GUPU, a Prolog programming environment for beginners used at TU Wien and Univ. de La Réunion. cTI_lt explains compactly the (provable) properties of termination of all predicates and improves a slicing-system in explaining reasons of nontermination.

Sample programs

som4
a rather complex termination condition
exp
a simple grammar with a very large cycle, same grammar as DCG
reach
example 7.6.2c from L.Plümer, Termination Proofs for Logic Programs, LNAI 446, 1990.
APPEND3, NAIVE REVERSE, PERMUTATION
from K.R.Apt, From Logic Programming to Prolog, Prentice-Hall, 1997.
Benchmark collection
including collection of Naomi Lindenstrauss

Architecture

cTI relies on two representations of the analyzed program: PN and PB. In PN all terms have been mapped to expressions in N according to a symbolic term size norm. The semantics of PN is estimated and some control informations are inferred. PB represents only the information whether an argument is bound, allowing to propagate boundedness information over the program.

To determine the corresponding models, cTI uses heavily abstract interpretations. The current implementation uses SICStus Prolog relying most notably on its libraries CLP(Q) (to perform calculations in N) and CLP(B). For further details, please refer to the literature.

Contributors

Fred Mesnard
idea, design, most implementation, maintenance
Ulrich Neumerkel
TNA, web interface, NTI
Serge Colin
implementation of mu-calculus
Antoine Rauzy
help and advice for boolean parts (mu-calculus)
Sébastien Hoarau
uses termination inference for static goal reordering
Alexander Forst-Rakoczy
human guide to HTML and Apache

Literature

[Mes96] F. Mesnard, Inferring left-terminating classes of queries for constraint logic programs. JICSLP'96, 7-21, MIT Press, 1996.

[HoaMes98] S. Hoarau and F. Mesnard, Inferring and Compiling Termination for Constraint Logic Programs. LOPSTR 1998, 240-254, LNCS 1559, Springer-Verlag, 1999.

[NeuMes99] U. Neumerkel and F. Mesnard, Localizing and explaining reasons for nonterminating logic programs with failure slices. PPDP'99, 328-341, LNCS 1702, Springer-Verlag, 1999.

[MesNeu01] F. Mesnard and U. Neumerkel, Applying static analysis techniques for inferring termination conditions of logic programs. SAS'01, 93-110, LNCS 2126, Springer-Verlag, 2001.

[MesPayNeu02] F. Mesnard, E. Payet, and U. Neumerkel, Detecting Optimal Termination Conditions of Logic Programs. SAS'02, 509-525, LNCS 2477, Springer-Verlag 2002.

Related systems

Web based

TermiLog (without frames). Termination analyzer by Naomi Lindenstrauss.

TerminWeb. Termination analyser by Michael Codish and Cohavit Taboch.

TALP. Automatic termination proofs for well-moded logic programs.

AProVE.

Offline

LPTP. Logic program theorem prover (proving left termination and other properties) by Robert Stärk.

Ciao. Prolog development system with an upper-bound complexity analyzer. If the property steps_ub/2 with a finite upper-bound has been proven, also termination has been proven. Upper-bound analysis therefore generalizes termination analysis in another direction.

Mercury contains a termination analyser (Manual).

Hasta-La-Vista. Termination analyser for logic programs equipped with numerical computations.

Polytool


Valid HTML 3.2Fred Mesnard (Université de La Réunion), Ulrich Neumerkel (Technische Universität Wien)