[Prev][Next][Index][Thread]
Re: note on graph vs. term reduction
Date: Thu, 1 Feb 90 17:28:45 EST
A note by John C. Mitchell is concerned with the correspondance between
graph-reduction and term reduction. This issue is obviously related to the
translation of lambda-expressions from string-representation to graph-
representation and vice versa. It is discussed to some extent in section
6.1 of my book "Lambda-calculus, Combinators, and Functional Programming".
In particular, on page 118 it is stated that the output routine to print
lambda-expressions in string format by traversing their graphs is precisely
the inverse of the parser which builds the graphs from the input strings.
The graph reduction rules presented in the next section are in one-to-one
correspondance with their string versions, hence the confluence property
of graph reduction follows immediately from the same property of the string
version.
I would say that "string-reduction" rather than "term-reduction" is, in fact,
the counterpart of "graph-reduction", since terms can be represented in both
ways.
If term-reduction is implemented by a sequence of more elementary graph-
reduction steps than, of course, these elementary steps must represent a
"compatible refinement" (see Barendregt) of the original reduction rules.
Best Regards,
- Gyorgy Revesz