Comments on: The shortest beta-normalizer http://sneezy.cs.nott.ac.uk/fplunch/weblog/?p=95 abstracting the pain away Tue, 17 May 2011 07:05:56 +0100 hourly 1 http://wordpress.org/?v=3.0.3 By: John Tromp http://sneezy.cs.nott.ac.uk/fplunch/weblog/?p=95#comment-15808 John Tromp Thu, 17 Apr 2008 19:08:38 +0000 http://sneezy.cs.nott.ac.uk/fplunch/weblog/?p=95#comment-15808 This is very neat! I have written lambda calculus reducers before that 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 This is very neat! I have written lambda calculus reducers before that
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

]]>