N. Lindenstrauss and Y. Sagiv

The main project in the last couple of years has been TermiLog, a system for checking termination of queries to logic programs. This project has been supported in part by grants from the Israel Science Foundation. The system is implemented in SICStus Prolog. It accepts as input a Prolog program and a query pattern, and returns as answer either that queries with this pattern terminate or that the system cannot prove termination. In contrast with some other systems, the program does not have to satisfy any condition in order to be analyzed by TermiLog. The type of termination analyzed by the system is the termination of computing all the answers to a given query, using Prolog's computation rule. Because of the possibility of backtracking this is the relevant notion of termination for Prolog.

TermiLog and relevant papers are available at http://www.cs.huji.ac.il/~naomil/

Overview of the system

The system is based on ideas of abstract interpretation. Termination is proved by using well-founded orderings on terms. The system consists of three main parts: The first does the instantiation analysis. The instantiation analysis is done by means of a bottom-up abstract interpretation similar to groundness analysis; however, instantiation analysis checks that terms are rigid according to some symbolic norm rather than ground.

The second part is inference of constraints among argument sizes. The constraint inference is also used to find out whether a constraint is recursive or non-recursive. This distinction is used in order to deal automatically with some programs, such as mergesort, that previously were handled by means of some ad hoc transformations. We have developed an automatic transformation to deal with those programs; the transformation is based on the generation of rules that are adorned with the inferred constraints followed by unfolding of the non-recursive adorned rules.

The third part consists of constructing query-mapping pairs.

Results

We have applied TermiLog to more than 140 programs that were taken from the literature on termination and from some benchmarks. More than 80% of these programs were analyzed correctly by TermiLog (i.e., either the query pattern terminates and TermiLog says so, or it does not and TermiLog says it cannot prove termination); the analysis of those programs was completely automatic.

There is ongoing research in connection with the TermiLog system in several directions aimed at widening the applicability of TermiLog to larger programs, both by making the instantiation analysis more efficient and by using CLP. Furthermore, a graphical interface for TermiLog is planned, in order for the user to understand more clearly what might be potential causes of nontermination.

We are also working on an adaptation of TermiLog to detecting automatically termination of active rules in database management systems.

A second project is related to retrieving information from the Web. We use logic programming and abstract interpretation in order to implement algorithms that have been developed recently in the database area. Specifically, we are implementing techniques for describing heterogeneous information sources, and also implementing algorithms for view usability and query processing in the environment of the Web.