Infinitary Rewriting and Cyclic Graphs
Richard Kennaway · Electronic Notes in Theoretical Computer Science · 1995
Infinitary rewriting allows infinitely large terms and infinitely long reduction sequences. There are two computational motivations for studying these: the infinite data structures implicit in lazy functional programming, and the use of rewriting of possibly cyclic graphs as an implementation technique for functional languages. We survey the fundamental properties of infinitary rewriting in orthogonal term rewrite systems, and its relation to cyclic graph rewriting.