Nottingham FP Lab Blog

The shortest beta-normalizer

by Thorsten on April 13, 2008.
Tagged as: Lunches.

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.