Locally-nameless normalization

Question

This paper on locally-nameless (Charguéraud, Arthur: The locally nameless representation, Journal of Automated Reasoning (2012): 1-46) describes how to perform beta-reduction by "opening", but it's unclear to me how to normalize under abstractions. For example how would one normalize the following expression, with the locally-nameless operations:

$\lambda((\lambda\lambda(1 \; 0)) \; 0)$

Answer 1

A good rule of thumb with locally nameless is "pattern matching on a binder is opening". In particular, take a naive call-by-name normalization algorithm on terms with named binders that ignores variable capture (in OCaml syntax):

 let rec norm t = match t with
     | Var v -> Var v
     | Lambda (v, t') -> Lambda (v, norm t')
     | App(t, u) -> let t' = norm t in
                    let u' = norm u in
                    match t' with
                       | Lambda (v, t'') -> norm (subst v u' t'')
                       | _               -> App (t', u')

The locally nameless version is exactly the same, except that you need to open the lambdas right after pattern matching on one, i.e. instantiate the top level deBruijn index with a name. What name do you want to open with? Well it probably needs to be a name you haven't opened with "above", aka a fresh variable.

Well darn. We were kind of hoping to not have to care about generating fresh variables with locally nameless. No such luck. In OCaml, you can cheat a little and create a statefull fresh : unit -> name function that always produces a never-seen-before name.

You don't actually need to do this with the second pattern match! When opening a term and immediately substituting, you can skip a step and call instantiate directly. This mentions no names (and works on a "scope", a non "opened term" with 1 deBruijn variable still in it).

But then you have the fresh names in the normal form! You need to abstract over the name again before applying the Lambda constructor. This gives

 let rec norm t = match t with
     | Var v -> Var v
     | Lambda t' -> let v = fresh () in
                    let t'' = instantiate (Var v) t' in
                    Lambda (abstract v (norm t''))
     | App(t, u) -> let t' = norm t in
                    let u' = norm u in
                    match t' with
                       | Lambda t'' -> norm (instantiate u' t'')
                       | _               -> App (t', u')

Easy peezy (except for the implementation of fresh, which can be tricky)!