Marco Ordoñez

Conversión alfa en el cálculo lambda

El acto de reemplazar una variable ligada por otra lo conocemos como conversión alfa.

Cuando \(y \notin FV(M)\) decimos que:

\(\lambda.xM \equiv_\alpha \lambda.y[y/x]M\)

Si un término \(P\) cambia a \(Q\) por un cambio en sus variables ligadas decimos que \(P\) se convierte en \(\alpha\) a \(Q\) o expresado de otra forma, \(P \equiv_\alpha Q\).

Se debe tener en cuenta el conflicto entre variables, decimos que un término \(M\) tiene un conflicto de variable ligada \(\iff M\) contiene un *abstractor \(\lambda x \) y otra ocurrencia de \(x\) que no está en el ámbito.

Dos reglas importantes a tener en cuenta:

  1. \(P \equiv_\alpha Q \implies \left|P\right| = \left|Q\right| \)
  2. \(P \equiv_\alpha Q \implies FV(P) = FV(Q) \)

Ejemplos:

  1. \(x(\lambda x.N)\) : Vemos que existe un abstractor \(\lambda x \) y una variable x que está fuera del ámbito.
Marco Ordonez