From "Type Theory and Formal Proof, An Introduction" by Rob Nederpelt and Herman Geuvers:

Definition 1.5.1 (Renaming; $M^{x \to y}$; $=_{\alpha}$) Let $M^{x \to y}$ denote the result of replacing every free occurrence of $x$ in $M$ by $y$. The relation 'renaming', expressed with symbol $=_{\alpha}$, is defined as follows: $\lambda x . M =_{\alpha} \lambda y . M^{x \to y}$, provided that $y \notin FV(M)$ and $y$ is not a binding variable in $M$.

$FV$ denotes the set of free variables of a $\lambda$-term.

Are the conditions $y \notin FV(M)$ and $y$ is not a binding variable in $M$, the same as requiring that $y$ does occur in $M$? My understanding is that an occurrence of a variable can be either free, bound, or binding. If an occurrence of $y$ is bound in $M$, does this not also require that $y$ is a binding variable in $M$?


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.