Intensión y extensión

Ya hemos hablado de la regla eta anteriormente, pero ahora vamos a relacionarla sintácticamente con el concepto de igualdad por extensión. El procedimiento de extensionalidad es siempre el mismo: si todos los casos particulares cumplen una propiedad, el caso general también. Por ejemplo, en la teoría de conjuntos la el axioma de extensionalidad dice algo así como

Todo par de conjuntos que contengan elementos iguales son conjuntos iguales.

En el caso de la computación, lo que tendríamos sería

Toda par de funciones cuyos resultados para cualquier entrada sean los mismos son funciones iguales.

Algo más matemáticamente sería decir que para todo
[$$ x $$]
si
[$$ f x =_\beta g x $$]
entonces
[$$ f =_{\beta\eta} b $$]
Lo interesante es que en el primer igual, con subíndice beta, estamos únicamente usando las definiciones y no la extensionalidad. Cuando usamos sólo las definiciones decimos que trabajamos intensionalmente. El segundo igual es distinto porque hemos usado la extensionalidad.

Lo más interesante de todo esto es que basta añadir la regla eta para que la igualdad intensional se convierta en extensional en el lambda cálculo. El problema es que esa simple regla introduce muchos quebraderos de cabeza a la hora de demostrar las propiedades de los sistemas que la usan.

La idea es bien sencilla. Como
[$$ f x $$]
se puede obtener mediante una beta-conversión desde
[$$ (\lambda y.f y) x $$]
y puedo decir que
[$$ f x =_\beta (\lambda y.f y) x $$]
Al aplicar extensión obtengo que
[$$ f =_{\beta\eta} \lambda y. f y $$]
Tomando la dirección que simplifica la expresión obtengo la eta-regla (como la variable que introduzco es fresca, no debe aparecer en f para poder aplicar la regla).

[$$ \lambda x. f x  \rightarrow f $$]

Basta añadir esta regla para comprobar si dos funciones son iguales (aunque se hayan definido de forma distinta). Esto no es inmediato ya que existen teoremas bien profundos para este tipo de igualdades extensivas. Afortunadamente la simplicidad del lambda cálculo permite automatizarlo (aunque recordemos que el lambda cálculo sin tipos puede no acabar la computación).

Resumiendo: tenemos tres tipos de igualdades.

• Igualdad sintáctica. Dos términos son iguales si son el mismo. En el lambda cálculo hay cierto detalle y es que las variables se pueden renombrar. Esto es a lo que se llama la alfa-conversión. Llamamos entonces a los términos iguales sintácticamente alfa-equivalentes.
• Igualdad intensional. Dos términos son iguales si, sustituyendo sus definiciones, son el mismo. En el lambda cálculo esto se consigue aplicando la regla beta. Por esta razón se llaman términos beta-equivalentes (aunque también son alfa-equivalentes y deberían llamarse alfa-beta-equivalentes).
• Igualdad extensional. Dos términos son iguales si hagamos lo que hagamos con ellos obtenemos el mismo resultado siempre.  Se obtienen usando las reglas beta y eta. Por esta razón se llaman beta-eta-equivalentes (aunque también se use la alfa-conversión).

Como final, planteo un breve ejercicio: ¿cuáles de estos términos son iguales sintácticamente, intensionalmente o extensionalmente?

[$$ (\lambda x.\lambda y. x) 3 = \lambda y. 3 $$]
[$$ \lambda x.x = \lambda y.y $$]
[$$ \lambda x. 5*(x+2) = \lambda x. 5*x+10 $$]