The shortest beta-normalizer

April 13th, 2008 by Thorsten

I 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:

\begin{code}
data T = Var Int | Lam T | App T T
\end{code}

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:

\begin{code}
data V = Fun (V -> V)
\end{code}

It is easy to define application:

\begin{code}
app :: V -> V -> V
app (Fun f) v = f v
\end{code}

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

\begin{code}
eval :: T -> [V] -> V
eval (Var x) e = e !! x
eval (Lam t) e = Fun (\ v -> eval t (e++[v]))
eval (App t u) e = app (eval t e) (eval u e)
\end{code}

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

\begin{code}
quote :: V -> T
\end{code}

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:

\begin{code}
data V = Fun (V -> V) | NVar Int | NApp V V

app :: V -> V -> V
app (Fun f) v  = f v
app n v         = NApp n v
\end{code}
The code for eval remains unchanged. Now we can implement quote, though we need an extra parameter to keep track of the free variables:

\begin{code}
quote :: Int -> V -> T
quote x (Fun f)        = Lam (quote (x+1) (f (NVar x)))
quote x (NVar y)     = Var y
quote x (NApp n v)  = App (quote x n) (quote x v)
\end{code}
Now nf just evaluates and quotes the result:

\begin{code}
nf :: T -> T
nf t = quote 0 (eval t [])
\end{code}

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

One Response to “The shortest beta-normalizer”

  1. John Tromp Says:

    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

Leave a Reply