[ 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 -- Andreas Abel <>< Du bist der geliebte Mensch. Theoretical Computer Science, University of Munich Oettingenstr. 67, D-80538 Munich, GERMANY [email protected] http://www2.tcs.ifi.lmu.de/~abel/
