TermiLog

TermiLog is a system for proving termination of logic programs written in Prolog.

TermiLog was written at the Hebrew University and is implemented in SICStus Prolog.

Note that the version of TermiLog on the web is not the full version.

What kind of termination is considered?

We consider termination of the computation of all answers to the query, using the leftmost selection rule. This is equivalent to finiteness of the LD-tree constructed for the query and program.


How can it be done?

It is a known fact that termination of a Turing machine (which is a model of a computer) is undecidable. Since a Turing machine can be described by a Prolog program this means that termination of Prolog programs is undecidable.
However, in Prolog the problem of termination is somehow simpler than in the general case, as the only reason for programs not to stop is infinite recursion.
TermiLog checks the recursions in the program, and tries to find an argument whose size is constantly decreasing at each recursive call (technically what it checks is that each circular variant has a forward positive cycle).
TermiLog either answers that there is termination or that there may be non-termination. In the latter case either there really is non-termination or TermiLog is not strong enough to prove termination.
It should be remembered that TermiLog assumes correct unification, so before submitting a Prolog program to it one should check that it is free from occur-check problems.


What is the meaning of the answers returned by TermiLog?

TermiLog may answer that your program terminates. In this case, if we wrote it correctly, TermiLog should be right. If it was wrong, please write us.
TermiLog may answer that it could not prove termination of your program. This can mean one of two things:
Your program does not terminate Your program really does not terminate. TermiLog will display the suspicious predicate.
Your program terminates TermiLog, using your preferences, could not prove the termination of your program, but your program does terminate.


What is a Norm?

TermiLog measures the size of the terms in your program by using a norm. Two norms may be used: the term size norm, which is sufficient in most cases, and the list size norm, which makes it possible to deal with arguments that are not necessarily ground. For instance, from termination of append(b,b,f) with list size norm, we may conclude that append([X,Y],[Z,U,V],L) terminates.
There is also a version of TermiLog for general linear norms, that is not available on the WWW.



How is a Query represented?

You have to give a query pattern by giving a predicate with arguments that are b or f. In the case of the term size norm b means "ground", while in the case of the list size norm it means a list with fixed length. In both cases f means "anything".


What is Constraint Inference?

Constraint inference uses abstract interpretation to find size relations between arguments of atoms that follow logically from the program. If termination can be proved without constraint inference this should be preferred because it is faster. However, there are cases, like quicksort, where it is not possible to prove termination without constraint inference.


Why can't I find my file on the list?

Your file probably ends with a ".pl". In the list, you might see only "*.html" files. The way to see all files depends on your browser. What you should look for is a Filter field or button.


Additional Information

The theory behind the system can be found in the paper

N.Lindenstrauss and Y. Sagiv, Automatic Termination Analysis of Logic Programs, ICLP'97

and a more detailed discussion in

N.Lindenstrauss and Y. Sagiv, Checking Termination of Queries to Logic Programs

For more information consult Dr. Naomi Lindenstrauss .

Related Links


Thanks

Thanks are due to Alexander Serebrenik, Tal Reichert, Chana Slutzkin and Tomer Klainer for their help.