NP-completeness of a combinator optimization problem

Abstract

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 β-η- 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. © 1995, Duke University Press. All Rights Reserved.