NP-completeness of a combinator optimization problem. (English) Zbl 0837.03015

Joy, M. S.; Rayward-Smith, V. J.

Notre Dame J. Formal Logic 36, No. 2, 319-335 (1995).

Summary: We consider a deterministic rewrite system for combinatory logic over combinators \(S, K, I, B\), \(C, S', B'\), and \(C'\). Terms will be represented by graphs so that reduction of a duplicator will cause the duplicated expression to be “shared” rather than copied. To each normalizing term we assign a weighting which is the number of reduction steps necessary to reduce the expression to normal form. A lambda- expression may be represented by several distinct expressions in combinatory logic, and two combinatory logic expressions are considered equivalent if they represent the same lambda-expression (up to \(\beta\)- \(\eta\)-equivalence). The problem of minimizing the number of reduction steps over equivalent combinator expressions (i.e., the problem of finding the “fastest running” combinator representation for a specific lambda-expression) is proved to be NP-complete by reduction from the “Hitting Set” problem.

MSC:

03B40	Combinatory logic and lambda calculus
68Q42	Grammars and rewriting systems
68Q25	Analysis of algorithms and problem complexity

Keywords:

deterministic rewrite system; combinatory logic; normal form; lambda- expression; NP-complete

References:

[1]	Barendregt, H. P., The Lambda Calculus, its Syntax and Semantics , North-Holland, Amsterdam, 1981. · Zbl 0467.03010
[2]	Batini, C., and A. Pettorossi, Some Properties of Subbases in Weak Combinatory Logic , Report 75–04, Istituto di Automatica, Roma, 1975. · Zbl 0332.02033
[3]	Clarke, T. J. W., P. J. S. Gladstone, C. D. MacLean and A. C. Norman, “SKIM—The S,K,I Reduction Machine” in Conference Record of the 1980 LISP Conference , Stanford University, 1980.
[4]	Curry, H. B., W. Craig and R. C. Feys, Combinatory Logic , vol. 1, North-Holland, Amsterdam, 1958. · Zbl 0081.24104
[5]	Curry, H. B., J. R. Hindley and J. P. Seldin, Combinatory Logic , vol. 2, North-Holland, Amsterdam, 1972. · Zbl 0242.02029
[6]	Garey, M. R., and D. S. Johnson, Computers and Intractability: A Guide to the Theory of NP-Completeness , W. H. Freeman, San Francisco, 1979. · Zbl 0411.68039
[7]	Glaser, H., C. Hankin and D. Till, Principles of Functional Programming , Prentice-Hall, Englewood Cliffs, 1984. · Zbl 0649.68002
[8]	Hindley, J. R., and J. P. Seldin, Introduction to Combinators and \(\lambda\)-Calculus, Cambridge University Press, Cambridge, 1986. · Zbl 0614.03014
[9]	Joy, M. S., On the Efficient Implementation of Combinators as an Object Code for Functional Programs , PhD Thesis, University of East Anglia, Norwich, 1985.
[10]	Joy, M. S., V. J. Rayward-Smith and F. W. Burton, “Efficient combinator code,” Computer Languages , vol. 10 (1985), pp. 221–224.
[11]	Kennaway, J. R., “The complexity of a translation of \(\lambda \)-calculus to combinators,” Internal Report CS/82/023/E, University of East Anglia, Norwich, 1982.
[12]	Klop, J. W., Combinatory Reduction Systems , Mathematisch Centrum, Amsterdam, 1980. · Zbl 0466.03006
[13]	Stoye, W. R., “The implementation of functional languages using custom hardware,” Technical Report 81, University of Cambridge Computer Laboratory, Cambridge, 1985.
[14]	Turner, D. A., “Another algorithm for bracket abstraction,” The Journal of Symbolic Logic , vol. 44, (1979), pp. 67–70. JSTOR: · Zbl 0408.03013 · doi:10.2307/2273733
[15]	Turner, D. A., “A new implementation technique for applicative languages,” Software—Practice and Experience , vol. 9 (1979), pp. 31–49. · Zbl 0386.68009 · doi:10.1002/spe.4380090105
[16]	Turner, D. A., “Combinator reduction machines,” in Proceedings of the International Workshop on High Level Computer Architecture , Los Angeles, 1984.