Weak convergence and uniform normalization in infinitary rewriting

Jakob Grue Simonsen

doi:10.4230/LIPIcs.RTA.2010.311

Weak convergence and uniform normalization in infinitary rewriting

Jakob Grue Simonsen

Department of Computer Science

4 Citations (Scopus)

10 Downloads (Pure)

Abstract

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.

Original language	English
Title of host publication	Proceedings of the 21st International Conference on Rewriting Techniques and Applications,
Editors	Christopher Lynch
Number of pages	14
Publisher	Schloss Dagstuhl - Leibniz-Zentrum für Informatik
Publication date	2010
Pages	311-324
ISBN (Electronic)	978-3-939897-18-7
DOIs	https://doi.org/10.4230/LIPIcs.RTA.2010.311
Publication status	Published - 2010
Event	21st International Conference on Rewriting Techniques and Applications - Edinburgh, United Kingdom Duration: 11 Jul 2010 → 13 Jul 2010

Conference

Conference	21st International Conference on Rewriting Techniques and Applications
Country/Territory	United Kingdom
City	Edinburgh
Period	11/07/2010 → 13/07/2010

Series	Leibniz International Proceedings in Informatics (LIPIcs)
Volume	6
ISSN	1868-8969

Access to Document

10.4230/LIPIcs.RTA.2010.311Licence: CC BY-NC-ND

Simonsen_2010_Weak_convergenceFinal published version, 161 KBLicence: CC BY-NC-ND

Cite this

Simonsen, J. G. (2010). Weak convergence and uniform normalization in infinitary rewriting. In C. Lynch (Ed.), Proceedings of the 21st International Conference on Rewriting Techniques and Applications, (pp. 311-324). Schloss Dagstuhl - Leibniz-Zentrum für Informatik. Leibniz International Proceedings in Informatics (LIPIcs) Vol. 6 https://doi.org/10.4230/LIPIcs.RTA.2010.311

Weak convergence and uniform normalization in infinitary rewriting. / Simonsen, Jakob Grue.

Proceedings of the 21st International Conference on Rewriting Techniques and Applications,. ed. / Christopher Lynch. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2010. p. 311-324 (Leibniz International Proceedings in Informatics (LIPIcs), Vol. 6).

Research output: Chapter in Book/Report/Conference proceeding › Article in proceedings › Research › peer-review

Simonsen, JG 2010, Weak convergence and uniform normalization in infinitary rewriting. in C Lynch (ed.), Proceedings of the 21st International Conference on Rewriting Techniques and Applications,. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, Leibniz International Proceedings in Informatics (LIPIcs), vol. 6, pp. 311-324, 21st International Conference on Rewriting Techniques and Applications, Edinburgh, United Kingdom, 11/07/2010. https://doi.org/10.4230/LIPIcs.RTA.2010.311

@inproceedings{1ab57337781245cbaee6c733b1ccc027,

title = "Weak convergence and uniform normalization in infinitary rewriting",

abstract = "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. ",

author = "Simonsen, {Jakob Grue}",

year = "2010",

doi = "10.4230/LIPIcs.RTA.2010.311",

language = "English",

series = "Leibniz International Proceedings in Informatics (LIPIcs)",

publisher = "Schloss Dagstuhl - Leibniz-Zentrum f{\"u}r Informatik",

pages = "311--324",

editor = "Christopher Lynch",

booktitle = "Proceedings of the 21st International Conference on Rewriting Techniques and Applications,",

note = "21st International Conference on Rewriting Techniques and Applications ; Conference date: 11-07-2010 Through 13-07-2010",

}

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 -