The next TeReSe (Term Rewriting Seminar), an afternoon with presentations on rewriting, will take place on Thursday November 19, 2009 at:
Location University College Utrecht, Campusplein 7, 3584 ED Utrecht Directions link UCU-page, google maps, map Utrecht Room UCU-Descartes-J
TeReSes take place, usually twice a year, at locations with an active rewriting community, in or close to the Netherlands (such as: Aachen, Amsterdam, Eindhoven, Utrecht, Nijmegen).
time speaker(s) title 13.15 - 13.30 arrival, setting up connections with the beamer 13.30 - 14.15 Carsten Fuhs Termination Analysis by Dependency Pairs and Inductive Theorem Proving 14.15 - 15.00 Albert Visser, Vincent van Oostrom, Joop Leo, Clemens Grabmayer On the termination of Russell's description elimination algorithm 15.00 - 15.30 break with coffee and tea 15.30 - 16.15 Cynthia Kop Higher Order Path Orderings 16.15 - 17.00 Hans Zantema Transformations for well-definedness of streams 17.00 - 17.20 TeReSe business meeting
Afterwards there will be the opportunity to have a TeReSe-dinner out together. It will take place in Indonesian Restaurant Djakarta in Utrecht (route in Utrecht city center).
Current techniques and tools for automated termination analysis of term rewrite systems (TRSs) are already very powerful. However, they fail for algorithms whose termination is essentially due to an inductive argument. Therefore, we show how to couple the dependency pair method for TRS termination with inductive theorem proving. As confirmed by the implementation of our new approach in the tool AProVE, now TRS termination techniques are also successful on this important class of algorithms.
In `On Denoting' (1905) B. Russell introduced a theory for denoting
phrases like `the author of Waverly' and `the present King of France'
that is based on `a reduction of propositions in which denoting phrases
occur to forms in which no such phrases occur'. A logical formulation
of denoting phrases as description terms, and their elimination from
formulas by using paraphrases was given in Principica Mathematica (1910).
While the adequacy of Russell's theory of descriptions for analysing denoting phrases still is very much under discussion, it turns out that even the logical-technical part of the theory remains a source of interesting questions. For example, Kripke (2005) stressed that the ambiguity of scope of description terms in formulas can be the reason for non-termination of the elimination algorithm, for a certain choice of paraphrase in a predicate logical language with Sheffer stroke.
We analyse the situation from a term rewriting perspective, and provide a reasonably complete picture of the termination behaviour of description elimination for formulas with ambiguous-scope, and with disambiguated-scope description terms. Our results link termination/non-termination of the respective description-elimination (higher-order) rewrite system to the syntactic form of the chosen paraphrase, confirm Kripke's claim, but also establish that `good' paraphrases (entailing termination) can always be found independently of the connectives available.
The talk will zoom in, on the one hand, on the background of the problem in Analytical Philosophy, and on the other hand, on the term rewriting methods we applied for analysing the termination behaviour of description elimination.
(The article is available as Preprint 280 in the Logic Group Preprint series.)
The higher-order recursive path ordering (HORPO) defined by Jouannaud and Rubio provides a method to prove termination of higher-order rewriting. We extend on this method in two ways. First, by defining an iterative version by means of an auxiliary term rewriting system, following an approach originally due to Bergstra and Klop. Second, we define a transitive variation of the recursive path ordering, using some of the techniques from the iterative version.
Streams are infinite sequences over a given data type.
A stream specification is a set of equations intended to define a stream.
A most fundamental question is whether the stream is well-defined by the equations. This follows from productivity (as was studied extensively in the Infinity project), or from termination of the observational variant, as presented at RTA09. But what to do if both approaches fail, like for the Fibonacci stream specified by the three equations fib = f(fib), f(0:s) = 0:1:f(s), f(1:s) = 0:f(s)?
We investigate semantics preserving transformations, by which such a stream specification is transformed to another one for which the earlier approaches succeed. In this way we can prove well-definedness of the non-productive fib specification, and many other examples.
We hope to see you in Utrecht,
Vincent van Oostrom and Clemens Grabmayer.