[Prev][Next][Index][Thread]
Note on graph vs. term reduction
A note on term and graph reduction
John C. Mitchell
Stanford
In texts on functional programming such as Peyton Jones,
it seems to be assumed implicitly that since the untyped
lambda calculus is confluent, so is graph reduction on
any reasonable "enhanced" lambda calculus, such as lambda
calculus with booleans and natural numbers. While Mitschke's
"delta reduction" theorem (see [Barendregt]) implies that
term reduction for various enhanced lambda calculi is
confluent, it does not seem immediately clear that this
follows for the corresponding notion of graph reduction.
Rather than discuss the machinery of graph reduction in
detail, let us take an axiomatic approach. The main benefit
is that there many ways we might implement term reduction
by graph reduction, and our results will apply to any
such implementation satisfying the general conditions
below.
To begin with, we assume there are functions
G: Terms --> Graphs
T: Graphs --> Terms
with T o G = id. In addition, we need the following properties.
Intuitively, the first says that "every term reduction has
a corresponding graph reduction," and the second that
"every graph reduction has a corresponding set of term
reductions."
Property 1.
If term t -> s, and T(g) = t, then there is some graph
h with g -> h and s ->> T(h).
Property 2.
If graph g -> h, then T(g) ->> T(h).
Under the assumption that these properties hold, we have
the following theorem.
Theorem.
If term reduction is confluent on terms with normal forms,
then graph reduction is confluent on all graphs representing
such terms.
It can be argued that this restricted form of confluence
is sufficient for most implementation considerations,
but it would also be interesting to identify the properties
of graph implementation that would make term confluence
imply graph confluence. (I conjecture that this is true
under plausible general conditions.)
Question: is this sort of result well-known, or already
published somewhere? References appreciated.