WST on Tuesday, August 15th

Welcome to WST 2006 (08:50‑09:00)

Invited Talk (09:00‑10:00)

09:00‑10:00

Byron Cook (Microsoft Research Cambridge) Program termination analyses for free! [ppt] I will describe an easy-to-follow recipe for the construction of automatic program termination analyses. The recipe's primary ingredient is an abstract-interpretation-based program analysis for invariance properties - any one will do. If we change the underlying program analysis, we get a different program termination analysis.

Break (10:00‑10:30)

Session 1: Logic Programming (10:30‑11:30)

10:30‑11:00

Peter Schneider-Kamp (RWTH Aachen) Juergen Giesl (RWTH Aachen) Alexander Serebrenik (TU Eindhoven) Rene Thiemann (RWTH Aachen) Termination Analysis for Logic Programs by Term Rewriting Revisited There are two kinds of approaches for termination analysis of logic programs: "transformational" and "direct" ones. Direct approaches prove termination directly on the basis of the logic program. Transformational approaches transform a logic program into a term rewrite system (TRS) and then analyze termination of the resulting TRS instead. Thus, transformational approaches make all methods previously developed for TRSs available for logic programs as well. However, the applicability of most existing transformations is quite restricted, as they can only be used for certain subclasses of logic programs. (Most of them are restricted to well-moded programs.) In this paper we improve these transformations such that they become applicable for any definite logic program. Moreover, we show that our transformation results in TRSs which are indeed suitable for automated termination analysis. In contrast to most other methods for termination of logic programs, our technique is also sound for logic programming without occur check, which is typically used in practice. We implemented our approach in the termination prover AProVE and successfully evaluated it on a large collection of examples.

11:00‑11:30

Manh Thang Nguyen (DTAI group, Department of Computer Science, K.U.Leuven, Belgium.) Maurice Bruynooghe (DTAI group, Department of Computer Science, K.U.Leuven, Belgium) Danny De Schreye (DTAI group, Department of Computer Science, K.U.Leuven, Belgium) Michael Leuschel (Heinrich-Heine-Universität Düsseldorf) Program Specialisation as a Pre-processing Step for Termination Analysis Analysing the structure of logic programs may provide useful information for termination analysis in Logic Programming (LP). In this paper, we present a simple transformation technique for termination analysis in LP based on the structural information of the program. We report on an extensive experiment which shows that this technique can significantly improve the precision of termination analysis and can be applied as a pre-processing step in any LP termination analyser.

Session 2: Narrowing; Non-Termination (11:30‑12:30)

11:30‑12:00

Naoki Nishida (Nagoya University) Koichi Miura (Nagoya University) Dependency Graph Method for Proving Termination of Narrowing Term rewriting systems with extra variables are useful to represent operators for inverse computation. Their ground rewrite sequences can be simulated by narrowing sequences starting from the same initial terms. In this paper we refine the dependency pair method for proving termination of narrowing, and extend the dependency graph method for proving termination of rewriting to a method for narrowing.

12:00‑12:30

Yi Wang (Nagoya University) Masahiko Sakai (Graduate School of Infomation Science, Nagoya University) On Non-looping Term Rewriting Proving non-termination is important for instance if one wants to decide termination for a given class of TRSs. Although the usual method is to find looping reduction sequences, there are non-looping infinite reduction sequences. We find some new interesting non-looping examples and propose new definitions to classify them. We also show the undecidability of existence of non-looping sequence.

Lunch break (12:30‑14:00)

Session 3: Higher-Order Rewriting (14:00‑15:00)

14:00‑14:30

Frederic Blanqui (INRIA) Higher-order dependency pairs Art and Giels proved that the termination of a first-order rewrite system can be reduced to the study of its ``dependency pairs''. We extend these results to rewrite systems on simply typed lambda-terms by using Tait's computability technique.

14:30‑15:00

Wojciech Moczydlowski (Cornell University) Normalization of intuitionistic set theories IZF is a well-investigated impredicative constructive counterpart of Zermelo-Fraenkel set theory. We define weakly-normalizing lambda calculus $\lambda Z$ corresponding to proofs in an intensional version of IZF with Replacement according to the Curry-Howard isomorphism principle. By adapting a counterexample invented by M. Crabbe, we show that $\lambda Z$ does not strongly normalize. Moreover, we prove that the calculus corresponding to a non-well-founded IZF does not even weakly normalize. Thus $\lambda Z$ and IZF are positioned on the fine line between weak, strong and lack of normalization.

Termination Competition (15:00‑15:30)

15:00‑15:30

Claude Marche and Hans Zantema Report on termination competition 2006

Break (15:30‑16:00)

Session 4: String Rewriting (16:00‑17:00)

16:00‑16:30

Joerg Endrullis (Vrije Universiteit Amsterdam) Dieter Hofbauer (Univ. Kassel) Johannes Waldmann (HTWK Leipzig, FB IMN) Decomposing Terminating Rewrite Relations We decompose an arbitrary rewrite relation into the product of a context-free system and an inverse context-free system with empty right-hand sides. By requiring both of these relations to be terminating, we lose computational completeness and arrive at the class of deleting rewriting systems. Our new treatment allows to efficiently construct the rewrite closure of a regular language with respect to deleting or match-bounded rewriting. Previous implementations of this method either used a complete but inefficient decomposition algorithm leading to impracticable resource consumption, or incomplete approximation algorithms. Our new algorithm is both efficient and exact, thereby improving the power of automated termination provers that use the method of match-bounds.

16:30‑17:00

Hans Zantema (Technische Universiteit Eindhoven) Termination of Extended String Rewriting We extend string rewriting in such a way that in the rules also variables may occur that may be replaced by arbitrary strings. This is a natural format occurring in text editing and pattern matching. We investigate termination behaviour of these extended string rewriting systems.

Business Meeting (17:00‑18:00)