WST on Wednesday, July 14th

TBA

It is an extended abstract, therefore no abstract.

We present small improvements of Lee, Jones and Ben-Amram "size change termination principle" specialised to functional programming languages, where destructors come from pattern-matching. This allows for a finer analysis of call-graphs and yields a more precise test for termination.

In very recent work, we introduced a non-termination preserving transformation from logic programs with cut to definite logic programs. In this paper we extend the transformation such that logic programs with cut are transformed into dependency triple problems instead of definite logic programs. By the implementation of our new method and extensive experiments, we show that the power of automated termination analysis for logic programs with cut is increased substantially.

CHR, short for Constraint Handling Rules, is a rule-based programming language. In termination analysis of such languages, the concept of a cycle is often useful. There can be several advantages of using cycles in termination analysis, mostly due to the fact that an analysis based on cycles is more modular.

We have studied cycles in CHR, however, were confronted with multi-headed rules and a multiset semantics in CHR, making it hard to define a suitable notion of ``cycle''. One of our initial attempts was very intuitive and rather precise, but, as it turned out, the approach resulted in an infinite number of different minimal cycles. This is of course unacceptable. In this paper, we provide a less precise but useful definition of a cycle yielding a finite number of minimal cycles, and discuss its successful use in CHR termination analysis.

In the past five years, techniques have been developed to analyze the non-termination -- as opposed to termination -- of logic programs. The main motivation for this work is to provide precision results for termination analyzers. The first and most well-known non-termination analyzer is NTI. Recently, we developed a slightly more precise analyzer, P2P.

In this paper, we investigate limitations of current non-termination analyzers and we show that the inclusion of type information, non-failure information and program specialization in our non-termination analysis, allows to overcome these limitations.

This paper shows a sufficient condition for non-termination of constrained term rewriting systems. There is a distance in the non-termination proofs of constrained and unconstrained systems, e.g., constrained rewrite rules such that the right-hand sides are encompassments of the left-hand sides do not always cause non-termination. For such constrained rewrite rules, we characterize extra constraints that ensure non-termination caused by the constrained rewrite rules. We also show that such extra constraints sometimes can be obtained from the constraints of the constrained rewrite rules, by removing some closures from the disjunctive normal forms of the constraints.

Polynomial interpretations are a useful technique for proving termination of term rewrite systems. They come in various flavors: polynomial interpretations over $\NN$, $\QQ$ and $\RR$. In this note we show that there are term rewrite systems that are polynomially terminating over $\NN$ and $\RR$, but not over $\QQ$.

This submission is an extended abstract and, therefore, it does not have an abstract.

Match-bounds can be used to prove relative termination. We compare a recent such method (Zankl and Korp, RTA 2010) with earlier work (Waldmann, JALC 2007). We recall that matchbounds are related to interpretations in the fuzzy semi-ring (with operations min, max) that can be found by constraint solving. The order in the semi-ring (with zero at the top) is such that it supports the closure construction required in the RFC method.