WST on Wednesday, July 14th

09:00‑10:00 Invited Talk
Location: IF G.03
09:00 Elvira Albert (Complutense University of Madrid)
From Termination to Cost (in Object-Oriented Languages)


10:30‑12:30 Programming Languages
Location: IF G.03
10:30 Samir Genaim and Damiano Zanardini
The Acyclicity Inference of COSTA

It is an extended abstract, therefore no abstract.

11:00 Christophe Raffalli and Pierre Hyvernat
Improvements on the "Size Change Termination Principle" in a functional language

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.

11:30 Thomas Stroeder, Jürgen Giesl and Peter Schneider-Kamp
Termination Analysis of Logic Programs with Cut Using Dependency Triples

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.

12:00 Paolo Pilozzi and Danny De Schreye
Scaling termination proofs by a characterisation of cycles in CHR

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.

14:00‑15:00 Non-Termination Analysis
Location: IF G.03
14:00 Dean Voets and Danny De Schreye
Non-termination analysis of Logic Programs using Types

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.

14:30 Naoki Nishida, Masahiko Sakai and Tatsuya Hattori
On Disproving Termination of Constrained Term Rewriting Systems

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.

15:30‑17:00 Term Rewriting
Location: IF G.03
15:30 Friedrich Neurauter and Aart Middeldorp
Polynomial Termination over N and R does not imply Polynomial Termination over Q

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$.

16:00 Michael Codish, Carsten Fuhs, Jürgen Giesl and Peter Schneider-Kamp
Lazy abstraction for size-change termination

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

16:30 Dieter Hofbauer and Johannes Waldmann
Match-Bounds for Relative Termination

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.