TY - GEN
T1 - Weak convergence and uniform normalization in infinitary rewriting
AU - Simonsen, Jakob Grue
PY - 2010
Y1 - 2010
N2 - We study infinitary term rewriting systems containing finitely many rules. For these, we show that if a weakly convergent reduction is not strongly convergent, it contains a term that reduces to itself in one step (but the step itself need not be part of the reduction). Using this result, we prove the starkly surprising result that for any orthogonal system with finitely many rules, the system is weakly normalizing under weak convergence if{f} it is strongly normalizing under weak convergence if{f} it is weakly normalizing under strong convergence if{f} it is strongly normalizing under strong convergence. As further corollaries, we derive a number of new results for weakly convergent rewriting: Systems with finitely many rules enjoy unique normal forms, and acyclic orthogonal systems are confluent. Our results suggest that it may be possible to recover some of the positive results for strongly convergent rewriting in the setting of weak convergence, if systems with finitely many rules are considered. Finally, we give a number of counterexamples showing failure of most of the results when infinite sets of rules are allowed.
AB - We study infinitary term rewriting systems containing finitely many rules. For these, we show that if a weakly convergent reduction is not strongly convergent, it contains a term that reduces to itself in one step (but the step itself need not be part of the reduction). Using this result, we prove the starkly surprising result that for any orthogonal system with finitely many rules, the system is weakly normalizing under weak convergence if{f} it is strongly normalizing under weak convergence if{f} it is weakly normalizing under strong convergence if{f} it is strongly normalizing under strong convergence. As further corollaries, we derive a number of new results for weakly convergent rewriting: Systems with finitely many rules enjoy unique normal forms, and acyclic orthogonal systems are confluent. Our results suggest that it may be possible to recover some of the positive results for strongly convergent rewriting in the setting of weak convergence, if systems with finitely many rules are considered. Finally, we give a number of counterexamples showing failure of most of the results when infinite sets of rules are allowed.
U2 - 10.4230/LIPIcs.RTA.2010.311
DO - 10.4230/LIPIcs.RTA.2010.311
M3 - Article in proceedings
T3 - Leibniz International Proceedings in Informatics (LIPIcs)
SP - 311
EP - 324
BT - Proceedings of the 21st International Conference on Rewriting Techniques and Applications,
A2 - Lynch, Christopher
PB - Schloss Dagstuhl - Leibniz-Zentrum für Informatik
T2 - 21st International Conference on Rewriting Techniques and Applications
Y2 - 11 July 2010 through 13 July 2010
ER -