# 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).