Marco Ordoñez

Sustitución en el cálculo lambda (type free)

En posts anteriores hemos visto sobre la historia y los términos del calculo lambda, en esta ocasión veremos con un poco más de detalle la estructura de los términos y la sustitución de los mismos.

Definimos \([N/x]M\) como el resultado de sustituir N en cada ocurrencia libre de x en M haciendo los cambios necesarios en las variables ligadas para prevenir que las variables libres se vuelvan ligadas en la sustitución.

  1. \([N/x]x \equiv N\)

  2. \([N/x]y \equiv y\)

  3. \([N/x](P,Q) \equiv (([N/x]P)([N/x]Q)) \)

  4. \([N/x](\lambda x.P) \equiv \lambda x.P \)

  5. \([N/x](\lambda y.P) \equiv \lambda y.P \) si x \(\notin FV(P)\)

  6. \([N/x](\lambda y.P) \equiv \lambda y.[N/x]P \) si x \(\in FV(P)\) y \(y \notin FV(N)\)

  7. \([N/x](\lambda y.P) \equiv \lambda z.[N/x][z/y]P \) si x \(\in FV(P)\) y \(y \in FV(N)\)

\(FV(P)\) significa que las variables libres de \(P\)

Ahora veamos algunos ejemplos.

Ejemplo 1:

Se nos pide sustituir \(\color{red}{(uv)}\) por cada \(\color{blue}{x}\) en la expresión \((\lambda y.x(\lambda w.vwx))\).

Utilizando la regla 6 tenemos:

\((\lambda y.\color{blue}{x}(\lambda w.vw\color{blue}{x}))\) \(\rightarrow\) \((\lambda y.\color{red}{uv}(\lambda w.vw\color{red}{(uv)}))\)

Ejemplo 2:

Se nos pide sustituir \(\color{red}{(λy.xy)}\) por cada \(\color{blue}{x}\) en la expresión \((\lambda y.x(\lambda x.x))\).

Utilizando la regla 6 tenemos:

\((\lambda y.\color{blue}{x}(\lambda x.x)) \rightarrow (\lambda y.\color{red}{(λy.xy)}(\lambda x.x))\)

Espero que sea esta información les sea útil.

Marco Ordonez