Quando você tem uma expressão num lambda calculus e precisa renomear um determinado parâmetro para garantir que ele não conflite com uma variável "global". Exemplo: na expressão λx.λx.x, você precisa renomear uma das variáveis para não conflitar na hora de substituir. Ficaria: λy.λx.x, por exemplo.