cTI

Home

Download

cTI: A Termination Inference Engine

Welcome to the home page of the cTI system. cTI is the first bottom-up left-termination inference tool for ISO-Prolog.


News

Mar 14, 2003 cTI 1.0 released!
This is the first public release of the system.
Sep 08, 2003 Web site improved and extended
More information is now available on cTI and what is behind it. More download options are also available.

Termination Inference

When does a logic program terminate? Termination inference, a new kind of program analysis, answers this question with a compact formula, called a 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, i.e., if A is 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.''

cTI's Architecture

cTI relies on two representations of the analyzed program: PN and PB In PN all terms have been mapped to expressions in N (the set of natural numbers) 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 makes heavy use of abstract interpretation techniques. The current implementation, written in SICStus Prolog, relies most notably on the Parma Polyhedra Library and the SICStus Prolog libraries CLP(Q) and CLP(B). For further details, please refer to the literature.

The cTI System

cTI (constraint based Termination Inference) infers classes of universally terminating programs for the leftmost selection rule (Prolog style execution). You can use cTI via the WWW, or immediately look at the benchmark collection. The TU Wien site also attempts to prove that the inferred conditions are optimal.

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

Sample Programs

Here are some programs with which you can test cTI:
  • som4 has a rather complex termination condition;
  • exp is a simple grammar with a very large cycle (same grammar as DCG);
  • reach is Example 7.6.2c from L.Plümer, Termination Proofs for Logic Programs, LNAI 446, 1990;
  • append3, naive reverse, and permutation are from K. R. Apt, From Logic Programming to Prolog, Prentice-Hall, 1997.
In addition, here is a benchmark collection that includes the collection of Naomi Lindenstrauss.

Contributors

Fred Mesnard
original idea, design, most implementation, maintenance, non-termination.
Ulrich Neumerkel
debugging, web interface of the TU Wien site, non-termination.
Serge Colin
implementation of the boolean mu-calculator.
Roberto Bagnara
cTI/PPL interface.
Etienne Payet
non-termination.
Alexander Forst-Rakoczy
human guide to HTML and Apache.

Literature

[Mesnard93] F. Mesnard, Etude de la terminaison des programmes logiques avec contraintes, au moyen d'approximations, PhD thesis, Université Paris VI, 1993.

[Mesnard96] F. Mesnard, Inferring left-terminating classes of queries for constraint logic programs by means of approximations. In M. J. Maher, editor, Logic Programming: Proceedings of the Joint International Conference and Symposium on Logic Programming, MIT Press Series in Logic Programming, Bonn, Germany, 1996. The MIT Press. Pages 7-21.

[NeumerkelM99] U. Neumerkel and F. Mesnard, Localizing and explaining reasons for non-terminating logic programs with failure-slices. In G. Nadathur, editor, Principles and Practice of Declarative Programming, volume 1702 of Lecture Notes in Computer Science, Paris, France, 1999. Springer-Verlag, Berlin. Pages 328-341.

[MesnardN01] F. Mesnard and U. Neumerkel, Applying static analysis techniques for inferring termination conditions of logic programs. In P. Cousot, editor, Static Analysis: 8th International Symposium, SAS 2001, volume 2126 of Lecture Notes in Computer Science, Paris, France, 2001. Pages 93-110.

[MesnardPN02] F. Mesnard, E. Payet, and U. Neumerkel, Detecting optimal termination conditions of logic programs. In M. V. Hermenegildo and G. Puebla, editors, Static Analysis: 9th International Symposium, SAS 2002, volume 2477 of Lecture Notes in Computer Science, Madrid, Spain, 2002. Springer-Verlag, Berlin. Pages 509-525.

[MesnardR03] F. Mesnard and S. Ruggieri, On proving left termination of constraint logic programs. ACM Transactions on Computational Logic, 4(2):1-26, 2003.

Related Systems

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

TerminWeb: Termination analyser by Michael Codish, Samir Genaim, and Cohavit Taboch.

LPTP: A Logic Program Theorem Prover (proving left termination and other properties) by Robert Stärk.

Ciao: Prolog development system with an upper-bound complexity analyzer (upper-bound complexity analysis encompasses termination analysis).

Mercury contains a termination analyser (see the manual).

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

[Page last updated on January 20, 2013, 16:47:51.]

© Fred Mesnard

Home | Download