Bottom-up β-reduction: Uplinks and γ-DAGs

• Autorzy: Shivers O. , Wand M.
• Języki publikacji: EN

Abstrakty

EN

If we represent a γ-calculus term as a DAG rather than a tree, we can efficiently represent the sharing that arises from β-reduction, thus avoiding combinatorial explosion in space. By adding uplinks from a child to its parents, we can efficiently implement β-reduction in a bottom-up manner, thus avoiding combinatorial explosion in time required to search the term in a top-down fashion. We present an algorithm for performing â-reduction on ë-terms represented as uplinked DAGs; describe its proof of correctness; discuss its relation to alternate techniques such as Lamping graphs, explicitsubstitution calculi and director strings; and present some timings of an implementation. Besides being both fast and parsimonious of space, the algorithm is particularly suited to applications such as compilers, theorem provers, and type-manipulation systems that may need to examine terms in between reductions—i.e., the “readback” problem for our representation is trivial. Like Lamping graphs, and unlike director strings or the suspension ë calculus, the algorithm functions by sideeffecting the term containing the redex; the representation is not a “persistent” one. The algorithm additionally has the charm of being quite simple; a complete implementation of the data structure and algorithm is 180 lines of SML.

• Wydawca: Polskie Towarzystwo Matematyczne
• Czasopismo: Fundamenta Informaticae
• Rocznik: 2010
• Tom: Vol. 103, nr 1-4
• Strony: 247--287
• Opis fizyczny: Bibliogr. 17 poz., tab., wykr.

Twórcy

autor

Shivers O.

autor

Wand M.

• College of Computer and Information Science, Northeastern University, 360 Huntington Avenue, Room 202 WVH, Boston, MA 02115, USA,

Bibliografia

• [1] Andrea Asperti and Stefano Guerrini. The Optimal Implementation of Functional Programming Languages. Cambridge University Press, 1999.
• [2] Henk Barendregt. The Lambda Calculus. North Holland, revised edition, 1984.
• [3] Alan Bawden. Personal communication, November 2002. Alan wrote the compiler, a toy exercise for Scheme, sometime in the late 1980's.
• [4] N. Bourbaki. Théorie des ensembles. Hermann & C. Editeurs, 1954.
• [5] Alonzo Church. The Calculi of Lambda Conversion. Princeton University Press, 1941.
• [6] Georges Gonthier, Mart´ın Abadi and Jean-Jacques Lévy. The geometry of optimal lambda reduction. In Conference Record of the Nineteenth Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, pages 15-26, January 1992.
• [7] Richard A. Kelsey. A correspondence between continuation-passing style and static single assignment form. In ACM SIGPLAN Workshop on Intermediate Representations, SIGPLAN Notices, vol. 30, no. 3, pages 13-22, January 1995.
• [8] J. R. Kennaway and M. R. Sleep. Director strings as combinators. ACM Transactions on Programming Languages and Systems, 10, pages 602-626, (October 1988).
• [9] John Lamping. An algorithm for optimal lambda-calculus reduction. In Proceedings of the Seventeenth Annual ACM Symposium on Principles of Programming Languages, pages 16-30, January 1990.
• [10] Jean-Jacques Lévy. Réductions Correctes et Optimales dans le Lambda-calcul. Th`ese d' ´ Etat, Université de Paris VII, Paris, France, 1978.
• [11] R. Milner, M. Tofte, R. Harper, D. MacQueen. The Definition of Standard ML (Revised). MIT Press, 1997.
• [12] Gopalan Nadathur and Debra Sue Wilson. A notation for lambda terms: A generalization of environments. Theoretical Computer Science 198(1-2):49-98, May 1998.
• [13] Simon L. Peyton Jones. The Implementation of Functional Programming Languages. Prentice-Hall, 1987.
• [14] Zhong Shao and Andrew W. Appel. A type-based compiler for Standard ML. In Proceedings of the ACM SIGPLAN'95 Conference on Programming Language Design and Implementation (PLDI), SIGPLAN Notices 30(6), pages 116-129, June 1995.
• [15] Zhong Shao, Christopher League, and Stefan Monnier. Implementing typed intermediate languages. In Proceedings of the 1998 ACM SIGPLAN International Conference on Functional Programming Languages, September 1998.
• [16] D. Tarditi, G. Morrisett, P. Cheng, C. Stone, R. Harper and P. Lee. TIL: A type-directed optimizing compiler for ML. In Proceedings of the ACM SIGPLAN'96 Conference on Programming Language Design and Implementation (PLDI), SIGPLAN Notices 31(5), pages 181-192, May 1996.
• [17] C. P. Wadsworth. Semantics and pragmatics of the lambda-calculus. PhD dissertation, Oxford University, 1971.