Archive for April, 2008

The shortest beta-normalizer

Sunday, 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.

Newton with scratch

Friday, April 4th, 2008 by Thorsten

I demonstrated how one can simulate Newtonian mechanics using scratch, a visual, impure language for children developed by people from MIT. My goal was to write a little program which shows that orbits are a consequence of Newton’s first law (inertia) and the law of gravity, which can be interpreted as a constant move towards the center of gravity. However, my first attempt has the problem that the planet always falls into the sun. The reason for this kind of friction is the discretisation of the movement. A little modification solves this problem but leads to an oscillating orbit. Nisse speculated (not entirely seriously) that this may be the real reason for the perihel movement of Mercury…