Are combinatory logic terms always larger?

Question

So there is an algorithm to convert lambda calculus terms to combinatory logic using SK combinators. It produces things that explode in size. I would like to know more about this explosion in size. I can't seem to think of a better algorithm however. I have heard of functional languages being practically compiled to combinators so it seems that a better algorithm must exist. I looked up David Turner's paper on the topic and he basically just says to apply a few optimizations and that they cause a "considerable improvement".

Does "considerable improvement" mean that the size drops to only a polynomial increase? Is there a known way to convert lambda terms to combinatory logic with only a polynomial (or less?) increase in size? If such an algorithm exists is it practical?

Answer 1

not an expert on this but here are two historical papers that seem to be closely relevant to the question and it is possibly a semi active area of research. Turner proposed a set of combinators that can be reduced to SK combinators. this next paper argues that Turner combinators even not reduced to SK combinators leads to exponential blowup (and that presumably the reduction would to SK terms be even larger). but then the 2nd paper says there is an efficient O(n log n) space algorithm based on Turner combinators. (it appears maybe that claims have been made about polynomial efficiency that are regarded as not fully demonstrated/ unproved & are therefore regarded as conjectures...?) anyway apparently real functional evaluation in applied languages typically does not use combinator method so implementors are not too concerned with issues of theoretical efficiency of evaluation of functional expressions by combinator translation.

• What is an Efficient Implementation of the λ-calculus? / Frandsen, Sturtivant (1991) (see p.18)

  Furthermore, we show that implementations based upon Turner Combinators or Hughes Super-combinators have complexities $2^{Ω(ν)}$, i.e. an exponential lower bound. It is open whether any implementation of polynomial complexity, $ν^{O(1)}$, exists, although some implementations have been implicitly claimed to have this complexity.

• Translation of Turner Combinators in O(n log n) space / Noshita (1985)

  A practical method for representing Turner Combinators is presented, which needs only O(n log n) space in the worst case for translating lambda expressions of length n.