[TYPES] Strong normalization of overlapping rewrite rules

[Frederic Blanqui]

Hello Andreas.

In fact, all the works I know on the combination of (typed) 
lambda-calculus and first or higher-order rewriting consider arbitrary 
rewrite rules, thus including non-left-linear and overlapping rules. 
This includes the works of Breazu-Tannen, Gallier, Okada, Barbanera, 
Dougherty, Jouannaud, Fernandez, Geuvers, Barthe, Rubio, Walukiewicz, 
... and myself. You can for instance find some references in my MSCS'05 
paper, pages 5-6.

Frederic.

Le 11/12/2012 08:34, Andreas Abel a écrit :
> [ The Types Forum, 
> http://lists.seas.upenn.edu/mailman/listinfo/types-list ]
>
> The typical normalization proof for a typed lambda calculus with 
> rewrite rules requires the rules to be left-linear and 
> non-overlapping.  What is known about left-linear but /overlapping/ 
> rewriting?  [References appreciated.]
>
> Best,
> Andreas
>