## The shortest beta-normalizer

April 13th, 2008 by ThorstenI presented the shortest implementation of a normalizer for beta equality for untyped lambda calculus which is based on Normalisation by Evaluation.

We start with the definition of lambda terms using de Bruijn levels:

The reason for using de Bruijn levels is that weakening comes for free. The other side of the coin is that one has to reindex bound variables when substituting. However, this is not an issue because we never do that.

We define values by solving a negative domain equation:

It is easy to define application:

We can evaluate lambda terms in the Value domain using a list of values as the environment:

All we have to do now is to invert evaluation, i.e. to define a function

To be able to do this we have first to extend values with variables. Then to be able to extend app, we also have to represent stuck applications, or neutral values:

The code for eval remains unchanged. Now we can implement quote, though we need an extra parameter to keep track of the free variables:

Now nf just evaluates and quotes the result:

We discussed how to verify such a normalisation function – I suggested to use the partiality monad.

April 17th, 2008 at 7:08 pm

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