[ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list ]
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
