O que seria alpha conversion e LC?

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.

\ L x F(x) ==alfa==> \ L y F(y) Algo assim