[Prev][Next][Index][Thread]
Re: Note on graph vs. term reduction
Date: Fri, 2 Feb 90 13:24:40 GMT
In response to John Mitchell's question about the relationship between
term and graph reduction, see:
H.P. Barendregt, M.C.J.D. van Eekelen, J.R.W. Glauert, J.R. Kennaway,
M.J. Plasmeijer and M.R. Sleep.
Term graph rewriting, Proc. PARLE Conference, LNCS 259, 141-158, 1987.
or the slightly longer version with more proofs:
Term graph rewriting, Report 87, Department of Computer Science,
University of Nijmegen, and Report SYS-C87-01, School of Information
Systems, University of East Anglia.
Concerning Mitchell's axioms:
>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).
The above paper doesn't take an axiomatic approach, but it proves these
and other relationships between any weakly regular term rewrite system
and its obvious interpretation as a graph rewrite system. The
correspondence between evaluation strategies for term and graph systems
is also treated. Counterexamples are illustrated when weak regularity
does not hold.
>Question: is this sort of result well-known, or already
>published somewhere? References appreciated.
Presumably it has been known at least as folklore ever since the technique
was invented. For lambda calculus, it goes back to Wadsworth's 1971 thesis,
for term rewriting I dont know how old it is.
A similar question was recently asked on comp.lang.scheme citing the
above reference and also
P.M. van den Broek, and G.G. van der Hoeven
[1986] Combinatorgraph reduction and the Church-Rosser theorem, preprint
INF-86-15, Department of Informatics, Twente University of Technology.
Here is my (long) reply. There are a surprising number of references for
what, at least in the case of regular term rewrite systems, would seem
fairly obvious (and I say this although I'm the author or co-author of at
least two papers dealing with the matter :-)). For lambda calculus,
things are considerably less obvious - the basic question of whether you
can achieve Levy's "optimal" reduction of lambda expressions at all is
only recently solved, by one of the references below.
In message <387CZXC@cs.swarthmore.edu>, taylor@cs.swarthmore.edu (Brian
Taylor) writes:
> I'd also appreciate references to any particularly valuable articles in the
> literature providing a theoretical justification for the use of graph
> reduction in the interpretation of combinatory logic and lambda calculus.
I wont attempt to rank the following references by value, but here are those
I know of, besides the two cited by Taylor.
For graph reduction of the lambda calculus, the original reference is
%A Wadsworth, C.
%T Semantics and pragmatics of the lambda calculus
%R D.Phil. thesis
%I Programming Research Group, Oxford University
%D 1971
%X address of PRG is 8-11 Keble Road, Oxford OX1 3QD, U.K.
This describes a graph rewriting implementation of lambda calculus and proves
it correct. It does not achieve "optimal" sharing in Levy's sense (see
Barendregt's book on the lambda calculus for what this means); this has
recently been done by:
%A Lamping, John
%T An algorithm for optimal lambda calculus reduction
%B POPL 90 conference
%D 1990 January
%A Lamping, John
%T An algorithm for optimal lambda calculus reduction
%R unpublished
%I Xerox PARC
%D 1989
%X A longer version of the POPL paper, with more proofs.
The question of whether the bookkeeping overhead with Lamping's method
outweighs the improvement in sharing it gains is not yet settled.
For graph rewriting implementation of functional languages, see:
%A Peyton-Jones, S.L.
%T The Implementation of Functional Languages
%I Prentice-Hall
%D 1987
For the optimality properties of combinator graph reduction, there is a
series of three papers by Staples (which actually prove it for regular term
graph rewrite systems, of which combinatory logic is an example).
%A Staples, John
%T Computation on graph-like expressions
%J Th.Comp.Sci.
%V 10
%P 171-185
%D 1980
%A Staples, John
%T Optimal evaluations of graph-like expressions
%J Th.Comp.Sci.
%V 10
%P 297-316
%D 1980
%A Staples, John
%T Speeding up subtree replacement systems
%J Th.Comp.Sci.
%V 11
%P 39-47
%D 1980
Other references for the correctness of combinator graph reduction:
%A Lester, David
%T Combinator graph reduction: a congruence and its applications
%R D.Phil thesis, Technical Monograph PRG-73
%D 1989
%I Programming Research Group, Oxford University
%X (from the abstract) "This thesis may be read as a formal mathematical proof
that the G-machine is correct with respect to a denotational semantic
specification of a simple language. ... The G-machine is shown to be a
representation of the combinator graph reduction operational model."
%A Farmer, William M.
%A Ramsdell, John D.
%A Watro, Ronald J.
%T A correctness proof for combinator reduction with cycles
%R Report M88-53
%I MITRE
%D 1988 November
%A Farmer, William M.
%A Watro, Ronald J.
%T Redex capturing in term graph rewriting
%R unpublished
%I MITRE
%D 1989 June 16
The address of MITRE is:
The MITRE Corporation
Bedford
Massachusetts
U.S.A.
There are two papers using category theory to prove the same result:
%A Raoult, J.C.
%T On graph rewritings
%J Th.Comp.Sci.
%V 32
%P 1-24
%D 1984
%A Kennaway, J.R.
%T On 'On graph rewritings'
%J Th.Comp.Sci.
%V 52
%P 37-58
%D 1987
%X See also the minor corrigendum in v.61, pp.317-320 (but only if you really
need to study the proofs in detail).
The paper Taylor cited by van den Broek and van der Hoeven is based on a
different category-theoretic approach to general graph rewriting, developed by
the 'Berlin school' - see various papers in the following volumes:
Proc. (1st, 2nd, 3rd) Int. Workshop on Graph Grammars and their application to
computer science, eds. H.Ehrig et al (different als for the three volumes)
1978, 1982, 1986
Springer-Verlag LNCS 73, 153, 291
There will be a 4th conference in this series in Bremen, March 5-9 this year.
Proc. Int. Workshop WG80 on Graph Theoretic Concepts in Computer Science
ed. H. Noltemeier
Springer-Verlag LNCS 100, 1980.
These conferences are concerned with graph rewriting in general, not just the
particular application to functional language implementation. For the latter,
see
Proc. Workshop on Graph Reduction
eds. J.H. Fasel and R.M.Keller
Springer-Verlag LNCS 279, 1986.
There is also a paper either by v.d.Broek and v.d.Hoeven or their colleagues
at Twente on the relationship between the two different category-theoretic
definitions, but I can't find the exact reference at the moment.
The subject is also discussed in Revesz's book "Lambda-calculus,
Combinators, and Functional Programming".
It's some time since I last saw someone ask what LNCS means, but just in case,
it stands for "Lecture Notes in Computer Science".
--
Richard Kennaway SYS, University of East Anglia, Norwich, U.K.
Internet: jrk@sys.uea.ac.uk uucp: ...mcvax!ukc!uea-sys!jrk