3
$\begingroup$

Notation:

  • Let $t$ and $u$ be terms in the $\lambda$-calculus, and $x$ be a variable name.

  • Let $[x\mapsto u]t$ be the substitution in $t$ of free variable $x$ for the term $u$. Specifically, I'm using the algorithm given in Functional Pearls: α-conversion is easy.

  • Let $t^\phi$ be the de Bruijn index–representation of a term $t$ in the $\lambda$-calculus (where $\phi$ is an injection from variable names to $\mathbb{N}$, with a sufficiently-large domain).

  • Let $[i \mapsto_{\textrm{dB}} u^\phi](t^\phi)$ be the substitution in $t^\phi$ of the free variable with index $i$ for the de Bruijn term $u^\phi$.


Question:

I've tried to search existing literature for a rigorous proof of the following (intuitively correct?) statement, but have come up empty:

$([x\mapsto u]t)^\phi = [\phi(x) \mapsto_{\textrm{dB}} u^\phi](t^\phi)$.

Specifically, I'm hoping for a proof that deals directly with the "normal" $\lambda$-calculus quotiented by $\alpha$-equivalence, instead of one that uses the Barengredt convention, nominal logic, etc.

Given that this lemma is left as an exercise in α-conversion is easy, I suspect that there may be no pre-existing answer to my question. (With that said, substitution doesn't actually use any of the paper's fancy new machinery.) If that's the case, I'm curious if there exists a "simple" definition of $[x\mapsto t]$ for which a proof exists (by "simple," I mean "doesn't use the Barengredt convention, nominal logic, etc."). If so, maybe I could use it as an intermediate step.


What I've Tried:

  • I think this is equivalent to Exercise 6.2.8 in Types and Programming Languages, but that proof isn't given explicitly. Also, I assume it relies on the Barendregt convention (like the rest of TAPL).

  • I've found a paper that seems to prove this statement by using a nominal logic–representation of the $\lambda$-calculus as an intermediary, but I guess I'm hoping for something more straightforward: Proof Pearl: De Bruijn Terms Really Do Work.

  • I've found another paper that uses a bespoke $\lambda_\textbf{x}$-calculus as an intermediary, although AFAICT it uses the Barengredt convention when proving the isomorphisms in question: Bridging de Bruijn Indices and Variable Names in Explicit Substitutions Calculi.

  • I've also proving the statement via induction on $t$, but without much luck (to wit, it's been a few weeks now and I'm still banging my head against it). Just for fun, I also tried induction on $\phi$, but it doesn't look promising.

$\endgroup$
3
  • $\begingroup$ How precisely have you defined $[x \mapsto u] t$? In particular, how did you deal with variable capture, precisely? The thankless lemmas you're trying to prove are very finicky. A small detail done clumsily or wrongly in the definitions will make them even more hellish. $\endgroup$ Aug 11, 2021 at 8:11
  • $\begingroup$ @AndrejBauer Oops, I should've clarified that—I've edited with more details. $\endgroup$ Aug 11, 2021 at 11:37
  • $\begingroup$ Upon reflection: Maybe I've been implicitly assuming that "if the definition of $[x\mapsto t]$ satisfies the substitution laws, then the proof will be the same regardless of its actual implementation." Or, maybe I've been so focused on understanding the de Bruijn side of things that I forgot about what I meant by "normal" substitution. Either way, I see now that my question wasn't very well-posed; hopefully it's better now. $\endgroup$ Aug 11, 2021 at 11:54

0

Your Answer

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

Browse other questions tagged or ask your own question.