WST on Tuesday, August 15th
(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.
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.
||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)
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.
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.
||Yi Wang (Nagoya University)
(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.
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.
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.
(Vrije Universiteit Amsterdam)
(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
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.
(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