would first translate into combinators S,K, then reduce those, and finally

convert the result back into lmabda calculus (which also involves applying

combinators to newly introduced variables), but I never figured you could

do this directly on lambda expressions.

Short lambda calculus reducers actually have an application in the

theory of Kolmogorov complexity, as I show in a paper

“Binary Lambda Calculus and Combinatory Logic” available from

http://www.cwi.nl/~tromp/cl/cl.html

With some luck I can use Thorsten’s reducer to significantly

improve the constant 1876 in (one half of) the Symmetry of

Information theorem in Section 5.

Thanks, Thorsten!

regards,

-John