Section. Applicative-order normalisation [nbe-nf0]

Now let's start with a simple-minded normaliser. We would like to define a function

nf0 :: Tm -> Tm

that takes in an arbitrary lambda term, which is allowed to have free variables, and should produce a normal form beta-equivalent to the input. Recall that the definition of a term t being in normal form is given inductively as follows:

1. t is a variable applied to zero or more arguments, where each argument is in normal form, i.e. t ≡ v a_1 a_2 ... a_n where v is a variable, n ≥ 0, and each a_i is in normal form (the base case of a normal form is when n = 0).

2. t is a lambda abstraction applied to a normal form, i.e. t ≡ \x. b where b is in normal form.

When the input to nf0 is a variable, we are already done:

nf0 (Var n) = Var n

When the input is a lambda abstraction, we can just recursively compute the normal form of the function body:

nf0 (Abs b) = Abs (nf0 b)

The interesting case is when the input is an application f a. A simple idea is to first recursively compute the normal forms f' and a' of f and a respectively, and then

1. if f' is a lambda abstraction \x. b, f' a' is not a normal form because (\x. b) a' is beta-reducible, so we can do this beta-reduction and re-normalise the result;

2. if f' is not a lambda abstraction, it is a variable applied to a (possibly empty) list of normal forms, sometimes called a spine. In this case, adding one more argument a' keeps it normal.

In total, we have

nf0 (App f a) =
   let f' = nf0 f
       a' = nf0 a
   in case f' of
        Abs b -> nf0 (beta b a')
        _ -> App f' a'

Let's do some basic sanity checks of our naive normaliser using Church numerals. This article is written as a .hs file so that I can use haskell-language-server to run small tests on the fly. Unfortunately you can't do this if you are reading the generated html file. If you want to play with the code more interactively, you can download the source code here and load it into your editor.

-- Church numeral increment
cinc :: Tm
cinc = Abs (Abs (Abs (Var 2 `App` Var 1 `App` (Var 1 `App` Var 0))))

-- Church numeral 0
c0, c1, c2 :: Tm
c0 = Abs (Abs (Var 0))
c1 = cinc `App` c0
c2 = cinc `App` c1

-- >>> nf0 c1
-- \x0. \x1. x0 x1

-- >>> nf0 c2
-- \x0. \x1. x0 (x0 x1)

-- Church numeral addition
cadd :: Tm
cadd = Abs $ Abs $ Abs $ Abs $
  Var 3 `App` Var 1 `App` (Var 2 `App` Var 1 `App` Var 0)

-- >>> nf0 (cadd `App` c2 `App` c2)
-- \x0. \x1. x0 (x0 (x0 (x0 x1)))

-- Church numeral multiplication
cmul :: Tm
cmul = Abs $ Abs $ Abs $ Abs $
  Var 3 `App` (Var 2 `App` Var 1) `App` Var 0

-- >>> nf0 (cmul `App` c2 `App` (cinc `App` c2))
-- \x0. \x1. x0 (x0 (x0 (x0 (x0 (x0 x1)))))

-- >>> nf1 ((cmul `App` c2 `App` (cinc `App` c2)) `App` Var 0 `App` Var 1)
-- x1 (x1 (x1 (x1 (x1 (x1 x0)))))

-- >>> nf1 (Var 0 `App` Var 1)
-- x1 x0

-- >>> nf0 ((cmul `App` c2 `App` (cinc `App` c2)) `App` Var 0 `App` Var 1)
-- x1 (x1 (x1 (x1 (x1 (x1 x0)))))

Great, basic tests check out! The normaliser nf0 always reduces the argument of a function application to normal form before applying it to the function body. For this reason, it is usually called applicative-order normalisation.