[Prev][Next][Index][Thread]
Re: Note on graph vs. term reduction
Date: Mon, 5 Feb 90 13:49:47 -0500
To: types@theory.lcs.mit.edu, rewriting-list%loria.crin.FR@princeton.edu
The discussion of graph rewriting for functional programming has yet
to mention that graphs may contain directed cycles, due to the cyclic
Y-combinator reduction rule. In this case, one generally cannot map a
graph to a finite term; possibly infinite tress are the natural
substitute. The MITRE papers "A correctness proof for combinator
reduction with cycles", (to appear, Jan 1990 TOPLAS) and "Redex
capturing in term graph rewriting" (Tech Report M89-36, July 89,
submitted for publication) contain results on implementing term
rewriting systems with cyclic graph rewriting rules. The first paper
uses a simple trick to prove correctness for the Y-rule without any
use of infinite objects. The second paper formalizes a notion of
convergence for infinite tree rewritings sequences, and proves a
general result comparing cyclic graph rewriting to tree rewriting
sequences. The infinite rewriting development is related to work of
Dershowitz, Kaplan, and Plaisted from POPL-89 and ICALP-89.
-- Bill Farmer
-- John Ramsdell <last_name>@mitre.org
-- Ron Watro