date: Thursday June 22, 2006
place: Vrije Universiteit
De Boelelaan 1085, 1081 HV Amsterdam
room F6.37
VU campus map (pdf)
contact: Roel de Vrijer, rdv at cs vu nl
13.00: Vincent van Oostrom (UU):
Random Descent
13.45: François-Régis Sinot (École Polytechnique, Paris):
Strategies of the Lambda-Calculus in Interaction Nets
14.30: tea break
15.00: Peter Schneider-Kamp (RWTH Aachen):
Automated Termination Analysis for Logic Programs by Term Rewriting
15.45: Hans Zantema (TUE):
Adding Constants to String Rewriting
16.30: Business meeting
17.00: end
Afterwards there will be the opportunity to eat out together. Restaurant still to be decided.
We introduce the notion of an ordered reduction diagram, which is a commutation diagram such that the east--south path from its source to its target is at least as long as its south--east path. We then introduce methods to compare rewrite strategies based only on verifying that some local commutation diagrams exist which are ordered. By the method being at the same level of abstraction (abstract rewriting systems) as Newman's Lemma, we expect it to have a similarly wide range of applications. To support this, we present several hitherto unrelated results as instances:
There are two major implementation models for the lambda-calculus:
abstract machines, used for instance for call-by-name and call-by-value;
and interaction nets, used for instance for optimal reduction. The
distributed nature of interaction nets does not allow in general to
describe precisely the implemented strategy, and these two models are
thus considered completely disconnected. This can be a problem, for
example if one wants to compare strategies implemented in different
models. In this talk, we exhibit a connexion between these two worlds by
showing that the usual strategies of the lambda-calculus can indeed be
encoded into interaction nets in a very simple and extensible way, and
in particular without requiring any notion of box. These encodings are
based on the simple idea of introducing an evaluation token, which gives
an explicit status to the evaluation flow and sequentialises some
reductions. We will deal with call by name, call by value, call by need
and the fully lazy strategy.
Transformational approaches for termination analysis of logic programs transform a logic program into a term rewrite system (TRS) and then analyze termination of the resulting TRS instead. Up to now, transformational approaches have only been applicable to restricted classes of logic programs.
We present an improved transformation from logic programs to TRSs
which is applicable for any logic program. Thus, in the TRS we have to
handle full unficiation by matching. To this end we introduce a modified
notion of term rewriting, so called infinitary constructor rewriting, and
show how to adapt state-of-the-art termination techniques to this notion.
We implemented our approach in AProVE and successfully evaluated it on a
large collection of examples.
We consider a signature where all symbols are either unary or constants. Then every term can be transformed into a corresponding string by just reading all symbols in the term from left to right, ignoring the optional variable. By lifting this transformation to rewrite rules, any TRS over such a signatures is transformed into a corresponding SRS.
We investigate which properties are preserved by this transformation. It turns out that any TRS over such a signature is terminating if and only if the corresponding SRS is terminating. In this way tools for proving termination of string rewriting like TORPA can be applied for proving termination of TRSs over such a signature. For other properties like CR, WCR, WN and UN we show that a corresponding preservation property does not hold.
This is joined work with Rene Thiemann, Juergen Giesl and Peter Schneider-Kamp.