jrk@sys.uea.ac.uk (Richard Kennaway CMP RA) (02/02/90)
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