Following up on this post denoting $(x \leftrightarrow y)$ the permutation of $x$ and $y$ and $P[x \leftrightarrow y]$ the term obtained from the term $P$ by permuting $x$ and $y$ (so for example if $P = \lambda x. \lambda y. x y$ then we have $P[x \leftrightarrow y] = \lambda y. \lambda x. y x$) (note that such transformation is immune from potential variable capture unlike those based on substitutions $y \leftarrow x$ or $x \leftarrow y$), then it appears to me that when $x \ne y$, a term $\lambda x. P$ is alpha equivalent to a term $\lambda y. Q$ if and only if $y$ is not free in $P$ and $Q$ is alpha equivalent to $P[y \leftrightarrow x]$. I find this observation interesting because it lends itself to a simple recursion in order to establish alpha-equivalence (as opposed to using an algorithm based on de Bruijn indices). I would like to know whether anyone thinks this observation is wrong, or whether it is true (a proof sketch or counterexample is welcome), or whether while true, it is not very interesting because the complexity of the recursive computation would be worse than a solution based on de Bruijn indices (each step requires determining whether $y$ is free in $P$ and permuting variable $x$ and $y$ in $P[x \leftrightarrow y]$).

  • 2
    $\begingroup$ I'm sorry, I'd misread your question. I don't have time to write a proper answer now, but in a nutshell, yes, the property is correct; it's the key fact in proving that the definition of alpha equivalence using capture-avoiding substitution and the definition of alpha equivalence using permutations. Implementations of alpha equivalence often work that way, but you still have the burden of doing renamings, and they can be costly because you aren't ever skipping terms protected by binders. $\endgroup$ – Gilles 'SO- stop being evil' Jun 12 '17 at 16:24
  • $\begingroup$ @Gilles I am very grateful for your time, thank you! $\endgroup$ – Sven Williamson Jun 12 '17 at 16:29
  • $\begingroup$ May I ask what you're after? Alpha equivalence has been beaten to death. $\endgroup$ – Andrej Bauer Jun 12 '17 at 18:13
  • $\begingroup$ @AndrejBauer I wanted to have confirmation that the property I have indicated was true, with possibly some insight about it which Gilles has given me. $\endgroup$ – Sven Williamson Jun 12 '17 at 18:26
  • $\begingroup$ That is perfectly all right. I just wanted to point out that you shouldn't waste time reinventing alpha equivalence if you're really after something larger. It's better to just reuse what is known. $\endgroup$ – Andrej Bauer Jun 12 '17 at 18:49

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.