[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]
Re: Combinators & Compilation
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