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.
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.
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.
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 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. |
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.
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".
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.
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.
The theory behind the system can be found in the paper
Thanks are due to Alexander Serebrenik, Tal Reichert, Chana Slutzkin and Tomer Klainer for their help.