<p>A good rule of thumb with locally nameless is &quot;pattern matching on a binder is opening&quot;. In particular, take a naive call-by-name normalization algorithm on terms with <em>named</em> binders that ignores variable capture (in OCaml syntax):</p>
<pre><code> let rec norm t = match t with
     | Var v -&gt; Var v
     | Lambda (v, t') -&gt; Lambda (v, norm t')
     | App(t, u) -&gt; let t' = norm t in
                    let u' = norm u in
                    match t' with
                       | Lambda (v, t'') -&gt; norm (subst v u' t'')
                       | _               -&gt; App (t', u')
</code></pre>
<p>The locally nameless version is exactly the same, except that you need to <em>open</em> 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 &quot;above&quot;, aka a <em>fresh variable</em>.</p>
<p>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 <code>fresh : unit -&gt; name</code> function that always produces a never-seen-before name.</p>
<p>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 <code>instantiate</code> directly. This mentions no names (and works on a &quot;scope&quot;, a non &quot;opened term&quot; with 1 deBruijn variable still in it).</p>
<p>But then you have the fresh names in the normal form! You need to abstract over the name again before applying the <code>Lambda</code> constructor. This gives</p>
<pre><code> let rec norm t = match t with
     | Var v -&gt; Var v
     | Lambda t' -&gt; let v = fresh () in
                    let t'' = instantiate (Var v) t' in
                    Lambda (abstract v (norm t''))
     | App(t, u) -&gt; let t' = norm t in
                    let u' = norm u in
                    match t' with
                       | Lambda t'' -&gt; norm (instantiate u' t'')
                       | _               -&gt; App (t', u')
</code></pre>
<p>Easy peezy (except for the implementation of <code>fresh</code>, which can be tricky)!</p>

CC BY-SA 3.0
2017-09-15T06:50:26.943Z
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?
Labbekak
CC BY-SA 3.0
2017-09-15T14:21:04.363Z
@Labbekak you are correct, names only need to be fresh "from below". As a side note, [this fantastic paper](https://pdfs.semanticscholar.org/1df1/a0b5e9d14855e24deb7cd602bdef9445a435.pdf) does go into fresh name generation, so there's inspiration to be had there.
cody
CC BY-SA 4.0
2017-09-14T20:27:08.483Z
2023-10-16T18:46:06.777Z
2023-10-16T18:46:06.777Z
cody
<p>This paper on locally-nameless (Charguéraud, Arthur: <a href="https://www.chargueraud.org/research/2009/ln/main.pdf" rel="nofollow noreferrer"><em>The locally nameless representation</em></a>, 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:</p>

<p>$\lambda((\lambda\lambda(1 \; 0)) \; 0)$</p>

<lambda-calculus>
Locally-nameless normalization
Labbekak
# Locally-nameless normalization

(Asked by: username_0 on 2017-09-14)

This paper on locally-nameless (Charguéraud, Arthur: [*The locally nameless representation*](https://www.chargueraud.org/research/2009/ln/main.pdf), 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)$

**Tags:** lambda-calculus


---

## 1 answers

### Answer by username_1 on 2017-09-14. Score: 4 | Accepted answer

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

> **Comments:**
> **username_0**: 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?  
> **username_1**: @username_0 you are correct, names only need to be fresh "from below". As a side note, [this fantastic paper](https://pdfs.semanticscholar.org/1df1/a0b5e9d14855e24deb7cd602bdef9445a435.pdf) does go into fresh name generation, so there's inspiration to be had there.  

---

