Thursday December 12, 2013 at 13h00 in the Auditorium (room 200A.00.225)
Dept. Computerwetenschappen, Celestijnenlaan 200A, 3001 Heverlee.
Termination and Non-termination in Logic Programming
One of the central concerns of declarative programming is that it leads to less error-prone, more understandable and better maintainable programs. However, it is well-known that a declarative programming style also results in less efficient computations, and in the extreme case, in non-terminating computations. The latter problem has received considerable attention within the community. Much research has been done on termination analysis, loop detection and more recently, non-termination analysis.
Due to the nature of undecidability, there must be situations in which neither a termination proof nor a non-termination proof can apply; i.e., no sufficient termination/non-termination conditions are satisfied so that the user would get no conclusion. We observe that in such a situation, it is particularly useful to compute an approximate conclusion indicating possible termination or possible non-termination. To the best of our knowledge, however, no existing approximation approach was available before our work.
A first contribution of the thesis is the development of such an approximation approach called termination prediction. In the case that neither a termination nor a non-termination proof is applicable, we appeal to an approximation algorithm to predict possible termination or non-termination. The analysis constructs a finite symbolic derivation tree, representing the derivation for a class of queries. The termination behavior is then predicted by checking properties of this tree.
A second contribution of the thesis is a new non-termination analysis for logic programs. In the thesis, we define a non-termination analysis based on the symbolic derivation trees from the termination prediction approach. We show that this non-termination analysis improves on the results of the only nontermination analyzer developed before our work. We extend our non-termination analysis in several ways. Type information and use program specialization is incorporated to obtain a stronger non-termination analysis. Another extension we discuss, is an extension to handle programs using integer arithmetics. We implemented this non-termination analysis and we show its applicability on a benchmark of logic programs.
A final contribution of the thesis is the development of a termination analysis for the programming language Constraint Handling Rules (CHR). This termination analysis is the first approach without restrictions on the type of rules in the CHR program. We demonstrate the condition’s applicability on a set of terminating CHR programs, using a prototype analyzer.