Term Rewriting Seminar (TeReSe)

A festive TeReSe meeting will be organized at the occasion of the appearance of the book Term Rewriting Systems by Terese

date: Tuesday June 3, 2003
place: Vrije Universiteit Amsterdam, room S2.09

program:

13.30 Jan Willem Klop (VU): The book
13.50 Roel de Vrijer (VU): Proof terms
14.30 Christian Urban (Cambridge University): Nominal unification

15.10 break

15.40 Jaco van de Pol (CWI): ARS and LTS theory in PVS
16.20 Hans Zantema (TUE): Liveness in rewriting

17.00 end

Afterwards there will be the opportunity to eat out together
We propose to eat pancakes in Boerderij Meerzicht in the "Amsterdamse Bos" (from 17.30 to 19.30)

Further details to follow

Abstracts of the talks

• ARS and LTS theory in PVS (Jaco van de Pol)
  A library of core ARS theory has been developed in the theorem prover PVS, which is based on higher-order logic. The development contains basic definitions (many step reduction, commutation, confluence, weak/strong normalization) and a number of well known basic results, such as commutation theorems and Newman's Lemma. Other proven results are that increasing, confluent and weakly normalizing ARSs are strongly normalizing; if R between S and S* is diamond, then S is confluent; and Akama's criterion for modularity of the conjunction of confluence and strong normalization. The library is part of a much larger development on labeled transition systems, with strong and branching bisimulation. Their symbolic counter parts "linear process" from the process algebra muCRL is formalized. It is shown how invariants, state mappings, and various notions of confluence can be used to transform linear processes. Finally, we prove that these notions are preserved by those transformations in many cases. This can be viewed as a mechanical verification of the correctness of the optimization algorithms (not the code) in the muCRL toolset.
  
  
• Nominal unification (Christian Urban)
  I will present a generalisation of first-order unification to the practically important case of equations between terms involving binders. A substitution of terms for variables solves such an equation if it makes the equated terms alpha-equivalent. For the applications we have in mind, we must consider the simple, textual form of substitution in which names occurring in terms may be captured within the scope of binders upon substitution. We are able to take a `nominal' approach to binding in which bound entities are explicitly named (rather than using nameless, de Bruijn-style representations) and yet get a version of this form of substitution that respects alpha-equivalence and possesses good algorithmic properties.
  
  
• Liveness in Rewriting (Hans Zantema)
  We show how the problem of verifying liveness properties is related to termination of term rewrite systems (TRSs). By refining existing techniques for proving termination of TRSs we show how liveness properties can be verified automatically. As an example, we prove a liveness property of a waiting line protocol for a network of processes. This is joint work with Juergen Giesl from RWTH Aachen.
  
  
• Proof terms (Roel de Vrijer)
  Proof terms are constructed as explicit syntactic representations of rewrite steps and reduction sequences and also of sequences of parallel steps, multi-steps and the like. In rewriting logic proof terms represent proofs. In chapter 8 of the book proof terms have been put to use as a technical tool in the theory of term rewriting. Notions of equivalence of reduction can be defined via transformations on proof terms. In the talk we will demonstrate this for permutation equivalence and for projection equivalence. We will also indicate how proof terms can be elegantly used in the basic theory of orthogonal term rewriting.

Last modified: Thu May 22 09:12:42 CEST 2003