Le séminaire du LSV

Le séminaire du LSV a lieu le mardi à 11h00. Le lieu habituel est la salle de conférences au Pavillon des Jardins (plan d'accès). Pour être informé par email des prochains séminaires, contacter Stéphane Le Roux and Matthias Fuegger.

Le séminaire du LSV est public et ne nécessite aucune inscription préalable.

Séminaires passés

Confluence of (non-terminating) layered rewrite systems by critical pair analysis

Visiter le site web pour cet événement | Exporter cet événement au format iCalendar

 Jean-Pierre Jouannaud
Le mardi 17 mars 2015 à 11:00
Salle de Conférence (Pavillon des Jardins)
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).

À propos du LSV

Agenda des séminaires

Exporter l'agenda au format iCalendar | Les séminaires précédents

mar. 19 février

Les séminaires précédents