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.