Hereditary substitutions

Aside Normalization-by-evaluation I told you about few blog posts ago, there's an another neat way to normalize expressions. I had already forgotten about this one but it's still neat. This thing produces a structurally recursive normalizer, which means the termination proof for it is straightforward.

I first describe the thing informally and then try to implement it.

Informal description

So lets pick the off-the-shelf simply typed lambda calculus that was presented in the paper as well. It's got lambdas, variables and application.

The algorithm ŋ-expands every variable. Basically, lets say you'd have this kind of context.

f:(a → b → c) ⊢ f

The ŋ-expansion would produce the following:

f:(a → b → c) ⊢ (λx.λy.f x y)

Note that if a and b are functions, they're also expanded in this way in the expression.

The next thing crucial for the algorithm is that applications are put into a spine. We can again take an example and illustrate:

λx.λy. (f x) y

If we add in De-bruijn indices, this expression transforms into:

Lambda (Lambda (Neut (S (S Z))
                     (Ap (Neut (S Z) Empty) (Ap (Neut Z Empty) Empty))))

This expression is in a normal form, and it's got one open variable. Lets try substitute it to something, lets say.. λx.λy.x.

So that term to substitute in would be:

Lambda (Lambda (Neut (S Z) Empty))

We could recursively climb up the expression with our substitution until.

(Neut (S (S Z))
      (Ap (Neut (S Z) Empty) (Ap (Neut Z Empty) Empty)))

At this point we can notice that the thing we're substituting in should go into the hole on the left. This means that we're going to apply the spine.

Lambda (Lambda (Neut (S Z) Empty))
(Ap (Neut (S Z) Empty) (Ap (Neut Z Empty) Empty))

(Neut (S Z) Empty)
[S Z := Neut (S Z) Empty]
[Z := Neut Z Empty]

(Neut (S Z) Empty)

And we can wrap the lambdas back in.

Lambda (Lambda (Neut (S Z) Empty))

ŋ-expansion ensures that the "napp" always has a lambda to open up. You get this structured recursion scheme that normalizes the expression.

Lets try implement it

I'll see if I can implement this in Haskell.

data Ty = Var Int
        | Arrow Ty Ty
        deriving (Show, Eq)

data Norm = Lambda Norm
          | Neut Int [Norm]
          deriving (Show, Eq)

napp :: Norm -> Norm -> Norm
napp (Lambda a) b = (sub 0 b) a

sub :: Int -> Norm -> Norm -> Norm
sub i a (Neut j neut) | (i <  j) = Neut (j-1)   (map (sub i a) neut)
sub i a (Neut j neut) | (i == j) = foldl napp a (map (sub i a) neut)
sub i a (Neut j neut)            = Neut j       (map (sub i a) neut)
sub i a (Lambda b)               = Lambda (sub (i+1) (wk 0 a) b)

wk :: Int -> Norm -> Norm
wk i (Lambda a) = Lambda (wk (i+1) a)
wk i (Neut j neut) | i > j = Neut j     (map (wk i) neut)
wk i (Neut j neut)         = Neut (j+1) (map (wk i) neut)

There's a catch on these structures, they're required to be in ŋ-long form.

check :: [Ty] -> Ty -> Norm -> Bool
check env (Arrow a b) (Lambda v)    = check (a:env) b v
check env (Var k)     (Neut i neut) = (nth i env >>= infer env neut) == Just k
check _   _           _             = False

infer :: [Ty] -> [Norm] -> Ty -> Maybe Int
infer env []     (Var k)     = Just k
infer env (x:xs) (Arrow a b) | check env a x
                             = infer env xs b
infer _   _      _           = Nothing

nth :: Int -> [a] -> Maybe a
nth 0 (x:_)          = Just x
nth n (_:xs) | n > 0 = nth (n-1) xs
nth _ _              = Nothing

The ŋ-long form requires that the neutral block doesn't produce a non-abstract term.

*HTS> check [] (Arrow (Var 0) (Var 0)) (Neut 0 [])
False
*HTS> check [] (Arrow (Var 0) (Var 0)) (Lambda (Neut 0 []))
True

*HTS> check [] (Arrow (Arrow (Var 0) (Var 1)) (Arrow (Var 0) (Var 1)))
      (Lambda (Neut 0 []))
False
*HTS> check [] (Arrow (Arrow (Var 0) (Var 1)) (Arrow (Var 0) (Var 1)))
      (Lambda (Lambda (Neut 1 [(Neut 0 [])])))
True

If you're using this to normalize lambda calculus, you need to produce n-long forms from variables.

reflect :: Int -> Ty -> [Ty] -> Norm
reflect n (Var _)     tys = Neut n (roll (length tys-1) tys)
reflect n (Arrow a b) tys = Lambda (reflect (n+1) b (tys ++ [a]))

roll :: Int -> [Ty] -> [Norm]
roll n [] = []
roll n (x:xs) = reflect n x [] : roll (n-1) xs

It'd seem a straightforward thing to implement.

When implementing the algorithm be careful with tracking scope changes. The verified implementation keeps track of the scope with the type system, but if you're implementing the algorithm in Haskell, it likely can contain some bugs.

The implementation of sum types with normalization-by-evaluation was quite hard. Lets see if it's hard with hereditary substitutions.

Lets try implement sum type normalization

First we need to extend the types and the language with sum types.

data Ty = Var Int
        | Arrow Ty Ty
        | Sum Ty Ty
        deriving (Show, Eq)

data Norm = Lambda Norm
          | Inl Norm
          | Inr Norm
          | Case Int [Norm] Norm Norm
          | Neut Int [Norm]
          deriving (Show, Eq)

It's fairly easy to catch the case block among any type.

napp :: Norm -> Norm -> Norm
napp (Lambda a) b = (sub 0 b) a
napp (Case i neut a b) c = (Case i neut (napp a c) (napp b c))

sub :: Int -> Norm -> Norm -> Norm
sub i a (Neut j neut) | (i <  j) = Neut (j-1)   (map (sub i a) neut)
sub i a (Neut j neut) | (i == j) = foldl napp a (map (sub i a) neut)
sub i a (Neut j neut)            = Neut j       (map (sub i a) neut)
sub i a (Lambda b)               = Lambda (sub (i+1) (wk 0 a) b)
sub i a (Inl b)                  = Inl (sub i a b)
sub i a (Inr b)                  = Inr (sub i a b)
sub i a (Case j neut b c) | (i < j)
    = Case (j-1) (map (sub i a) neut) (sub (i+1) (wk 0 a) b)
                                      (sub (i+1) (wk 0 a) c) 
sub i a (Case j neut b c) | (i == j)
    = case foldl napp a (map (sub i a) neut) of
        Inl z -> sub 0 z (sub (i+1) (wk 0 a) b)
        Inr z -> sub 0 z (sub (i+1) (wk 0 a) c)
        Case k neut p q -> let
            block = Case 0 [] (wk 0 (sub (i+1) (wk 0 a) b))
                              (wk 0 (sub (i+1) (wk 0 a) c))
            in Case k neut (sub 0 p block) (sub 0 q block)
sub i a (Case j neut b c)
    = Case j (map (sub i a) neut) (sub (i+1) (wk 0 a) b)
                                  (sub (i+1) (wk 0 a) c)

We get results that'd match with using just plain typed lambda calculus for normalising sum types.

Conclusion

Normalisation with sum types seem to add difficulty any way you put it.

Similar posts