Editing infinitary rewriting

'''Infinitary rewriting''' is an extension of [[abstract rewriting]] featuring:

* [[infinitary terms]], ''i.e.'' terms that may be infinitely deep,
* infinitary sequences of rewriting steps.

Notice that {{Quotes|infinitary}} means {{Quotes|finite or infinite}}.

== General definition ==

== Converging reduction sequences ==

=== Weak convergence ===

=== Strong convergence ===

== Coinductive presentation ==

== References ==
Historical references:

* {{Bib Article
| id = DerKapPla1991
| author = N. Dershowitz, S. Kaplan and D. A. Plaisted
| title = Rewrite, rewrite, rewrite, rewrite, rewrite, …
| journal = Theoretical Computer Science
| year = 1991
| doi = 10.1016/0304-3975(91)90040-9
| volume = 83
| number = 1
}} First published work on infinitary rewriting, where only weak convergence is considered. (A conference version had been presented at POPL'89.)
* {{Bib Article
| id = FarWat1990
| author = W. M. Farmer and R. J. Watro
| title = Redex capturing in term graph rewriting
| journal = International Journal of Foundations of Computer Science
| year = 1990
| doi = 10.1142/S0129054190000266
| volume = 1
| number = 4
}} First introduction of strong convergence.
* {{Bib Article
| id = KenKloSleDeV1995
| author = R. Kennaway, J. W. Klop, R. Sleep, F.-J. de Vries
| title = Transfinite Reductions in Orthogonal Term Rewriting Systems
| journal = Information and Computation
| year = 1995
| doi = 10.1006/inco.1995.1075
| volume = 119
| number = 1
}} Where strongly convergent infinitary rewriting is first extensively studied. (A conference version had been presented at RTA'91.)