<p>Although similar to a previously unanswered <a href="https://cstheory.stackexchange.com/questions/41810/locally-nameless-representation-normal-order-opening-with-a-bound-variable">question</a>, my query focuses on a different aspect of normalization. I'm trying to adjust the proof of strong normalization of STLC, given in Jeremy Avigad's <a href="https://www.cambridge.org/core/books/mathematical-logic-and-computation/300504EAD8410522CE0C27595D2825A2" rel="nofollow noreferrer">book</a>, to prove it in locally nameless representation. I'm referencing Arthur Chargueraud's <a href="https://chargueraud.org/research/2009/ln/main.pdf" rel="nofollow noreferrer">paper</a> for the locally nameless representation.. Until a lemma about lambda terms, everything fit well. But I couldn't figure out the following lemma.</p>
<blockquote>
<p><strong>Lemma 13.2.8.</strong> Suppose that whenever <span class="math-container">$s$</span> is strongly computable, <span class="math-container">$t[s/x]$</span> is strongly computable. Then <span class="math-container">$\lambda x. t$</span> is strongly computable.</p>
</blockquote>
<p>After some steps, proof involves a case analysis on the reducts of the application term <span class="math-container">$(\lambda x. t) s$</span>. One possibility is <span class="math-container">$(\lambda x. t')s$</span> where <span class="math-container">$t \rightarrow_1 t'$</span>, and inductive hypothesis gives the result. However, in locally nameless representation, the situation is different. If the reduction happens on first (lambda) part, it is of the form <span class="math-container">$\forall x \notin L,  t^x \rightarrow_1 t'^x$</span> where <span class="math-container">$L$</span> is a finite set. This is the definition (BETA-ABS) in Section 4.5 in the chapter. Here, <span class="math-container">$t^x$</span> denotes the variable opening (Section 3.1). About variable opening, we know from the paper:</p>
<blockquote>
<p>Variable opening turns some bound variables into free variables. It is used to investigate the body of an abstraction.</p>
</blockquote>
<p>Also, when a term <span class="math-container">$t$</span> is locally closed (Section 3.3), variable opening fixes the term, namely <span class="math-container">$t^x=t$</span>.</p>
<p>In the reduction step above, I know that <span class="math-container">$t$</span> is locally closed, so <span class="math-container">$t^x \rightarrow_1 t'^x$</span> becomes <span class="math-container">$t \rightarrow_1 t'^x$</span>. However, I'm not able to say it for <span class="math-container">$t'$</span> sure. That's why I'm not able to work with the induction like in the book. Therefore, I believe the lemma should be adapted to the locally nameless style. There is a relationship between substition and variable opening, but it's hard to explain for me. I have a vague sense.</p>
<p>How can we adjust the lemma (if we can) to obtain a criteria for strongly computable lambda terms?</p>
<p>EDIT: Following the idea in the comments and using the idea in the paper, I stated and proved the criteria for lambda terms as follows:</p>
<p><em>Suppose that whenever <span class="math-container">$s$</span> is strongly computable, <span class="math-container">$t^x[s/x]$</span> is strongly computable. Then <span class="math-container">$\lambda t$</span> is strongly computable.</em></p>
<p>As a corollary, I also have:</p>
<p><em>Suppose that whenever <span class="math-container">$u$</span> is strongly computable, <span class="math-container">$t^u$</span> is strongly computable. Then <span class="math-container">$\lambda t$</span> is strongly computable.</em></p>

CC BY-SA 4.0
2023-11-16T16:24:44.413Z
How do you know that $t$ is locally closed at the end? In general it wouldn't be, no? If the $t$ is the one in the statement of 13.2.8, then clearly the lemma should be about $t^x[s/x]$ or the like, not about locally closed $t$ (because the original lemma isn't about $t$ in which $x$ does not occur).
Dan Doel
CC BY-SA 4.0
2023-11-16T16:34:07.150Z
Also, as a side comment, I've become unconvinced that things like locally nameless are actually good when proving things. It is useful for avoiding mistakes that will not be caught in an ordinary programming setting. However, when you are proving your programs correct, you are not allowed to make such mistakes (the proof won't go through). So, it is not really helping you ensure correctness, but it is making your poofs harder by making (e.g.) inductive arguments more complicated.
Dan Doel
CC BY-SA 4.0
2023-11-17T02:04:57.817Z
@DanDoel As in the proof in the book, I can show $t$ is strongly computable. I've already shown strongly computable terms are locally closed because they are typed terms, I mean $t$ is a term of a type $T$ in a context $\Gamma$. So I have $t$ is locally closed. I'll try your suggestion, thanks.
phdstudent
CC BY-SA 4.0
2023-11-17T02:07:45.140Z
@DanDoel as for your comment, I agree with you. I'm just trying to do a Lean formalization about STLC in locally nameless style. And I would like to check how strong normalization is obtained in my case.
phdstudent
<lo.logic><lambda-calculus><typed-lambda-calculus><normalization>
Variable opening in locally-nameless representation
phdstudent
# Variable opening in locally-nameless representation

(Asked by: username_0 on 2023-11-16)

Although similar to a previously unanswered [question](https://cstheory.stackexchange.com/questions/41810/locally-nameless-representation-normal-order-opening-with-a-bound-variable), my query focuses on a different aspect of normalization. I'm trying to adjust the proof of strong normalization of STLC, given in Jeremy Avigad's [book](https://www.cambridge.org/core/books/mathematical-logic-and-computation/300504EAD8410522CE0C27595D2825A2), to prove it in locally nameless representation. I'm referencing Arthur Chargueraud's [paper](https://chargueraud.org/research/2009/ln/main.pdf) for the locally nameless representation.. Until a lemma about lambda terms, everything fit well. But I couldn't figure out the following lemma.

> **Lemma 13.2.8.** Suppose that whenever $s$ is strongly computable, $t[s/x]$ is strongly computable. Then $\lambda x. t$ is strongly computable.

After some steps, proof involves a case analysis on the reducts of the application term $(\lambda x. t) s$. One possibility is $(\lambda x. t')s$ where $t \rightarrow\_1 t'$, and inductive hypothesis gives the result. However, in locally nameless representation, the situation is different. If the reduction happens on first (lambda) part, it is of the form $\forall x \notin L, t^x \rightarrow\_1 t'^x$ where $L$ is a finite set. This is the definition (BETA-ABS) in Section 4.5 in the chapter. Here, $t^x$ denotes the variable opening (Section 3.1). About variable opening, we know from the paper:

> Variable opening turns some bound variables into free variables. It is used to investigate the body of an abstraction.

Also, when a term $t$ is locally closed (Section 3.3), variable opening fixes the term, namely $t^x=t$.

In the reduction step above, I know that $t$ is locally closed, so $t^x \rightarrow\_1 t'^x$ becomes $t \rightarrow\_1 t'^x$. However, I'm not able to say it for $t'$ sure. That's why I'm not able to work with the induction like in the book. Therefore, I believe the lemma should be adapted to the locally nameless style. There is a relationship between substition and variable opening, but it's hard to explain for me. I have a vague sense.

How can we adjust the lemma (if we can) to obtain a criteria for strongly computable lambda terms?

EDIT: Following the idea in the comments and using the idea in the paper, I stated and proved the criteria for lambda terms as follows:

*Suppose that whenever $s$ is strongly computable, $t^x[s/x]$ is strongly computable. Then $\lambda t$ is strongly computable.*

As a corollary, I also have:

*Suppose that whenever $u$ is strongly computable, $t^u$ is strongly computable. Then $\lambda t$ is strongly computable.*

**Tags:** lo.logic, lambda-calculus, typed-lambda-calculus, normalization
> **Comments:**
> **username_1**: How do you know that $t$ is locally closed at the end? In general it wouldn't be, no? If the $t$ is the one in the statement of 13.2.8, then clearly the lemma should be about $t^x[s/x]$ or the like, not about locally closed $t$ (because the original lemma isn't about $t$ in which $x$ does not occur).  
> **username_1**: Also, as a side comment, I've become unconvinced that things like locally nameless are actually good when proving things. It is useful for avoiding mistakes that will not be caught in an ordinary programming setting. However, when you are proving your programs correct, you are not allowed to make such mistakes (the proof won't go through). So, it is not really helping you ensure correctness, but it is making your poofs harder by making (e.g.) inductive arguments more complicated.  
> **username_0**: @DanDoel As in the proof in the book, I can show $t$ is strongly computable. I've already shown strongly computable terms are locally closed because they are typed terms, I mean $t$ is a term of a type $T$ in a context $\Gamma$. So I have $t$ is locally closed. I'll try your suggestion, thanks.  
> **username_0**: @DanDoel as for your comment, I agree with you. I'm just trying to do a Lean formalization about STLC in locally nameless style. And I would like to check how strong normalization is obtained in my case.  

---

## 0 answers

