2
$\begingroup$

Although similar to a previously unanswered question, 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, to prove it in locally nameless representation. I'm referencing Arthur Chargueraud's paper 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?

$\endgroup$
4
  • $\begingroup$ 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). $\endgroup$
    – Dan Doel
    Nov 16 at 16:24
  • $\begingroup$ 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. $\endgroup$
    – Dan Doel
    Nov 16 at 16:34
  • $\begingroup$ @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. $\endgroup$
    – phdstudent
    Nov 17 at 2:04
  • $\begingroup$ @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. $\endgroup$
    – phdstudent
    Nov 17 at 2:07

0

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge that you have read and understand our privacy policy and code of conduct.