Abstract
This paper introduces a new reduction order for the lambda calculus, called head order. It lends itself to a graph reduction implementation. The head normal form of a lambda expression corresponds closely to K. J. Greene's lazy normal form of his LNF-calculus, that is, the head order normal form will have the same variable (respectively, constant) as head and the same number of arguments as its normal form. In the context of future implementations, the head normal form is also called the head normal form skeleton (respectively, outline). This skeleton is produced first. Then the normal forms of the arguments are obtained and inserted into this skeleton concurrently, since they do not interact anymore. Head order reduction automatically exposes concurrent processes.
The procedure for generating a head normal form is described in terms of beta-reduction in-the-large, eta-extension in-the-large, and identity-reduction in-the-large. These in-the-large operations represent a new concept. They take sequences of bindings and/or applications as initial form, and produce a result in-the-large. They comprise a multitude of single reductions (e.g., beta, eta) occurring in a specific pattern.
A geometric, visual correspondence is described which pictures the process of obtaining a head normal form in terms of smoothing out a zigzag line (representing a lambda expression). The claim is that this image gives insight into the reduction process of very large lambda expressions. A formal definition is given to the concept of environment, which corresponds to a special zigzag line. An environment lookup corresponds to a selector function applied to a sequence of arguments.
Special attention is given to the problem of sharing. It is not generally possible, as opposed to the case of combinators, since an argument may contain free variables. They might get bound erroneously when the argument is substituted. Head order reduction has the advantage of normal order: no argument is reduced unless actually needed. How often an argument is copied depends on the occurrence of free variables and the number of different contexts it is substituted in. The implementation difficulties to make this information available on the run are touched upon.
Finally, some preliminary simulation results are reported. A set of lambda expressions was abstracted by K. J. Greene's abstraction algorithm. Then all combinators are expressed in terms of lambda expressions. Normal forms of the abstracted lambda expressions are compared to the normal forms of the original expressions. They are all respectively equal up to eta-conversion. This and a comparison of results obtained by the GMD string reduction machine give a fairly good indication of the correctness of the method.
Preview
Unable to display preview. Download preview PDF.
8. Bibliography
Abdali, S.K., “An Abstraction Algorithm for Combinatory Logic”, The Journal of Symbolic Logic 41, 1, March 1976, pp. 222–224.
Aiello, L. and Prini, G., “An Efficient Interpreter for the Lambda-Calculus”, Journal of Computer and System Sciences 23, pp. 383–424 (1981).
Barendregt, H.P., The Lambda Calculus: Its Syntax and Semantics, North-Holland Publishing Co., Amsterdam, Netherlands, 1981 and 1984.
Berkling, K.J., “Reduction Languages for Reduction Machines”, Proceedings of the 2nd International Symposium on Computer Architecture, Houston, January 1975, pp. 133–140.
Berkling, K.J., and Fehr, E., “A Consistent Extension of the Lambda Calculus as a Base for Functional Languages”, Information and Control 55, 1–3, pp. 89–101.
Church, A., The Calculi of Lambda-Conversion, 1941, Princeton University Press.
Clarke, T.J.W., Gladstone, P.J.S., Maclean, C.D., and Norman, A.C., “SKIM — S, K, I, Reduction Machine”, Proceedings 1980 Lisp Conference, Stanford, California, August 1980.
De Bruijn, N.G., “Lambda-calculus notation with nameless dummies: A tool for automatic formula manipulation with application to the Church-Rosser theorem”, Indag. Math. 34, pp. 381–392.
Hughes, R.J.M., “SUPER-COMBINATORS: A New Implementation Method for Applicative Languages”, 1982 ACM Symposium on Lisp and Functional Programming, Pittsburgh, Pennsylvania, August 1982.
Greene, K.J., “A Fully Lazy Higher Order Purely Functional Language with Reduction Semantics”, CASE Center Technical Report No. 8503, Syracuse University.
Johnsson, T., “The G-Machine: An Abstract Machine for Graph Reduction”, Chalmers University of Technolgy, Goteborg, Sweden, August 1983.
Kleene, S.C., Introduction to Metamathematics, Van Nostrand, New York, 1952.
Morris, F.L., “Computing Cyclic Liststructure”, School of Information and Computer Science, Report 2–80, Syracuse University, June 1980.
Scheevel, M., “NORMA: A Graph Reduction Processor”, 1986 ACM Conference on LISP and Functional Programming, August 1986.
Turner, D.A., “A New Implementation Technique for Applicative Languages”, Software—Practice and Experience 9, September 1979, pp. 31–49.
Wadsworth, C.P., Semantics and Pragmatics of the Lambda Calculus, Ph.D. Thesis, Oxford University, September 1971.
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 1987 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Berkling, K. (1987). Head order reduction: A graph reduction scheme for the operational lambda calculus. In: Fasel, J.H., Keller, R.M. (eds) Graph Reduction. GR 1986. Lecture Notes in Computer Science, vol 279. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-18420-1_48
Download citation
DOI: https://doi.org/10.1007/3-540-18420-1_48
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-18420-1
Online ISBN: 978-3-540-47963-5
eBook Packages: Springer Book Archive