LSV Seminar
The LSV seminar takes place on Tuesday at 11:00 AM. The usual location is the conference room at Pavillon des Jardins (venue). If you wish to be informed by e-mail about upcoming seminars, please contact Stéphane Le Roux and Matthias Fuegger.
The seminar is open to public and does not require any form of registration.
Past Seminars
Confluence of (non-terminating) layered rewrite systems by critical pair analysis
- Date
- Tuesday, March 17 2015 at 11:00AM
- Place
- Salle de Conférence (Pavillon des Jardins)
- Speaker
- Jean-Pierre Jouannaud (LIX, Ecole Polytechnique)
Knuth and Bendix showed long ago that confluence of a terminating first-order rewrite system can be reduced to the joinability of its finitely many critical pairs. But there are non-terminating critical pair free rewrite systems which are non-confluent, like R={f(x,c(x)) -> a, f(c(x),x) -> b, g -> c(g)}.
We investigate here the case of layered systems for which a given lefthand side cannot be overlapped by other lehthand sides unless at the root. We will also require that the maximal number of redexes along a path from root to leaves does not grow along reductions. R is a layered system. Using novel unification techniques in infinite trees, we show that layered systems are confluent provided their root critical pairs, in finite or infinite trees, have decreasing diagrams. We will also show that the redex-depth non-increasing condition is necessary.
This work is part of a program for designing new methods for showing confluence based on a critical pair analysis when reductions are non-terminating (as it is the case for type-theoretic raw terms, because of beta-reductions and elimination).