El isomorfismo de Curry-Howard

Uno de los descubrimientos más impactantes en la lógica del siglo XX es el isomorfismo de Curry-Howard. También llamado la correspondencia de Curry-Howard o, como veremos inmediatamente, tipos como predicados.

Historia

Todo empezó cuando, en 1934, Haskell Curry se fijó en lo siguiente:

Si tengo una función f que toma un valor de tipo A y devuelve un valor de tipo B, su tipo lo escribiré como A -> B. Para indicar que f tiene ese tipo usaré los dos puntos f : A -> B y leeremos "f tiene tipo función de A a B". Escribiré los tipos en mayúsculas y los términos en minúscula. Para aplicar esa función a un término t arbitrario uso la siguiente regla de inferencia:

Si sé que f : A -> B y sé que t : A entonces puedo deducir que f(A) : B.

El golpe de genialidad de Curry consistió en quitar los términos y observar que los tipos solos conforman la regla de inferencia lógica del modus ponens.

Si sé que A implica a B y sé que A es cierto, entonces puedo deducir que B es cierto.

Tras años de trabajo, en 1958, Curry concluyó que no podía expresar la lógica proposicional clásica. Sólo una parte de ella llamada lógica intuicionista. En esta lógica no tenemos el principio del tercero excluido por lo que no podemos realizar demostraciones por reducción al absurdo.

Años más tarde, William Alvin Howard descubrió que no sólo se podía expresar la lógica proposicional intuicionista, sino un gran conjunto de lógicas intuicionistas incluidas las de primer orden y orden superior. Desde entonces se ha extendido aún más la correspondencia y se ha incluido la lógica clásica mediante el uso de continuaciones. De hecho, se han inventado lógicas gracias a la correspondencia.

Explicación

¿Pero cómo es posible que un tipo sea una proposición lógica? En todo caso un tipo es un conjunto de valores o de términos, pero ¿cómo expresar conjunciones o implicaciones? Aunque no lo parezca a primera vista, es relativamente fácil.

Por ejemplo, ¿qué significa cuando decimos 3 : int ? Que tres es un entero, sí. Pero también podemos decir que los enteros tienen algún habitante: existe un valor, el 3, que es un entero y por tanto los enteros no están vacíos. En este sentido el valor 3 sería la demostración de que los enteros están habitados. La proposición int significa "los enteros están habitados". Si nuestro lenguaje de programación no tuviera enteros, int sería falso. Si los tiene, int es cierto.

Entonces, los términos son, por un lado, valores de un tipo y, por otro, demostraciones de que ese tipo no está vacío. Que un tipo no esté vacío significa que, visto como proposición, tiene una demostración y por tanto es cierto en nuestro sistema o lenguaje de programación.

Seguimos: ¿Cómo demuestra una función una implicación? Viendo la regla modus ponens de arriba, la demostración de que B está habitado es f(t) así que lo que hace una función f es, dada una demostración t,  construye otra f(t). O como siempre se ha entendido, dado un valor devuelve otro. Por esta razón demuestra la implicación: dame una demostración de A que te doy otra de B. Si A es cierto, entonces B también.

Hasta ahora tengo predicados constantes como int e implicaciones como A->B. Introduciremos la conjunción A & B. Desde el punto de vista lógico si A & B es cierto es por que A es cierto y B es cierto. Si me pongo a trabajar con las demostraciones necesito la demostración de A y la demostración de B para tener la demostración de A & B. Llamemos a estas demostraciones a : A y b : B. Entonces, un término que agrupa ambas demostraciones es un par (a, b). Por tanto, el tipo conjunción no es más que el tipo de los pares (a, b) : A & B más usualmente llamado producto cartesiano.

De esta forma se pueden obtener todas las conectivas en gran cantidad de lógicas distintas y, lo que es más importante, se estandariza la forma de demostrar las proposiciones en dichas lógicas: Los programas son esas demostraciones.

Portada de las actas del congreso LICS'90, humorísticamente titulada el homeomorfismo de Curry-Howard. Los constructores de tipos (arriba) se transforman en las conectivas lógicas (abajo) de forma continua.

  

En acción

Para finalizar vamos a demostrar, usando programas como prueba, que A -> B -> C es lógicamente equivalente a (A & B) -> C. Para esto primero demostraremos ( (A & B) -> C) -> (A -> B -> C) y luego (A -> B -> C) -> ( (A & B) -> C).

λ f. (λ x. λ y. f (x, y) ) : ( (A & B) -> C) -> (A -> B -> C)
λ f. λ x. f (primero x) (segundo x) :  (A -> B -> C) -> ( (A & B) -> C)

Sólo hay que hacer notar que hemos usado las proyecciones de un par: primero (p, q) se evalúa a p y segundo (p, q) se evalúa a q. El resto de la demostración es obvia en el sentido de que el programa que proporciono tiene ese tipo que digo. Para comprobar eso harían falta ciertas reglas de inferencia, pero eso será para otro día.

Implementando el algoritmo de la playa de agujas

Ya he hablado de cómo funcionaba el algoritmo de la playa de agujas en una entrada anterior. Hoy voy a especificar el pseudocódigo para definir completamente el algoritmo.

Antes de entrar de lleno en materia, hemos de explicar las funciones y tipos auxiliares que vamos a usar.

• RESULTADO: El tipo del resultado del algoritmo. Será una expresión parentizada como 1+(2*3).
• TOKEN: El tipo de los elementos de la entrada podrán ser o bien operandos simples como 1, 2 o 3; o bien operadores como +, * o -.
• PrioridadDelOperador(t): Si t es un TOKEN de tipo operador, devuelve su prioridad. Los operadores con más prioridad se agrupan antes que los de menos prioridad. 
• ElSiguienteTokenEsOperador(): Devuelve cierto si el siguiente TOKEN a leer es un operador.
• LeeOperandoSimple(): Lee de la entrada un operando simple y lo consume quitándolo de la entrada. Falla (y el algoritmo termina con error) si el siguiente TOKEN es un operador.
• ConsultaSiguienteToken(): Lee sin consumir el siguiente TOKEN de la entrada.
• ConsumeToken(): Consume el siguiente TOKEN de la entrada quitándolo de la misma.
• CreaExpresion(operador, operando1, operando2): Crea una expresión parentizada con los operadores y operandos dados. Así, por ejemplo, CreaExpresion(+, 3, 7-2) crea la expresión 3+(7-2).  

Visto todo esto, podemos exponer el algoritmo que llamamos LeeExpresion().

RESULTADO LeeExpresion(int pri_anterior)
{
 RESULTADO a=LeeOperandoSimple();
 if(!ElSiguienteTokenEsOperador())
  return a;

 TOKEN t=ConsultaSiguienteToken();
 int pri_siguiente=PrioridadDelOperador(t);

 if(pri_siguiente<pri_anterior)
  return a;

 ConsumeToken();
 return CreaExpresion(t.data, a, LeeExpresion(prec));
}

Esta implementación funciona muy bien cuando todos los operadores son asociativos por la derecha. Es decir, tendremos que 1+2+3+4 se agrupa como 1+(2+(3+4)). Si queremos operadores que se asocien por la izquierda, necesitamos modificar ligeramente el algoritmo. También necesitamos saber si un operador es asociativo por la derecha o no. Esto lo conoceremos usando OperadorEsAsociativoDerecha(t) donde t es un TOKEN.

Este algoritmo mejorado es el siguiente:

RESULTADO LeeExpresion(int pri_anterior)
{
 RESULTADO a=LeeOperandoSimple();

 while(ElSiguienteTokenEsOperador())
 {
  TOKEN t=ConsultaSiguienteToken();
  int pri_siguiente=PrioridadDelOperador(t);

  if(OperadorEsAsociativoDerecha(t) ? pri_siguiente<pri_anterior : pri_siguiente<=pri_anterior)
   return a;

  ConsumeToken();
  a=CreaExpresion(t.data, a, LeeExpresion(prec));
 }

 return a;
}

Usando estos algoritmos es muy sencillo añadir operadores infijos a un reconocedor descendiente recursivo.

Fallo de LaTeX

Me he dado cuenta que el renderizador de LaTeX no funciona. Leyendo en el blog del autor parece ser que tiene problemas por sobrepaso de quota en disco duro. Según dice, está trabajando en cambiar el motor de renderización de LatexRender a mimeTex. Esperemos que tarde poco.

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 $$]

La transformación de Smirnov

Recientemente me preguntaron cómo se podía generar una variable pseudoaleatoria que no fuera uniforme. Efectivamente, en la mayoría de lenguajes de programación y bibliotecas, la única función que se proporciona es una con distribución uniforme. La clásica rand() por ejemplo.


Existen varios métodos, algunos con nombres tan bellos como el algoritmo del zigurat. Nos quedaremos con el más simple y versátil, aunque no siempre el más eficiente o exacto.


El procedimiento es bien simple. Si queremos generar una variable pseudoaleatoria con una densidad de probabilidad f, lo primero que necesitamos es calcular su distribución de probabilidad F. Esto es, básicamente, calcular una integral. Muchas veces no será posible analíticamente, razón por la cual este método no se puede usar siempre o requiere un cálculo numérico que deteriora la eficiencia del mismo.


Supongamos que podemos calcular la distribución de probabilidad F. En este caso el método consiste en transformar la variable pseudoaleatoria uniforme que hemos generado, normalizada entre cero y uno, usando la inversa de la distribución de probabilidad.

A la izquierda, la distribución de probabilidad. A la derecha su inversa. Cabe notar que los intervalos uniformes en el eje de abscisas se transforman en intervalos que siguen la densidad de probabilidad deseada en el eje de ordenadas.

El resultado es otra variable pseudoaleatoria que sigue la distribución deseada.

Este método es llamado la transformación de Smirnov (nada que ver con el vodka) o, el método de la inversa de la transformada.

Estadísticas de la red

He encontrado una página con estadísticas muy interesantes. Me han sorprendido algunas cosas, como la resolución más común (1024x768). Creía que ya habíamos mejorado un poco los monitores, pero se ve que no.