4
$\begingroup$

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)$

$\endgroup$
  • $\begingroup$ When you refer to a paper, please specify it. Just saying "the paper on ..." isn't enough. $\endgroup$ – Andrej Bauer Sep 15 '17 at 9:11
3
$\begingroup$

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)!

$\endgroup$
  • $\begingroup$ Thanks a lot, yeah you're exactly right that I was hoping I would not need to generate fresh names. Am I right in thinking that the new name only needs to be fresh in the body of the binder? So one could get the free names in the body and then choose a new name that's not in that set? $\endgroup$ – Labbekak Sep 15 '17 at 6:50
  • 1
    $\begingroup$ @Labbekak you are correct, names only need to be fresh "from below". As a side note, this fantastic paper does go into fresh name generation, so there's inspiration to be had there. $\endgroup$ – cody Sep 15 '17 at 14:21

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.