Ya apareció en arXiv el último paper que enviamos, y aprovecho para hacer una introducción más sencilla a él.
Para entender un poco más el contexto, les recomiendo este post donde doy una explicación no-técnica sobre el área. El presente post va a ser (obligatoriamente) un poquito más técnica, pero trataré de que lo sea lo menos posible. Voy a continuar con los ejemplos de ese post anterior, así que aún si ya lo leyeron, les recomiendo mirarlo de nuevo por arriba para refrescarlo.
Habíamos dicho que la idea era encontrar tipos para un lenguaje en particular para obtener de allí una lógica cuántica. El lenguaje con el que estoy trabajando es el "Linear-Algebraic Lambda-Calculus" (lambda-cálculo algebraico-lineal).
¿Porqué este lenguaje y no otro? Lambda-cálculo es el lenguaje más pequeño y universal que existe (pequeño == simple). Este cálculo algebraico-lineal lo que hace es permitir combinaciones lineales de términos, esto es, si M y N son dos términos de mi lenguaje, a.M+b.N con a y b escalares cualquiera, también es un término. Si lo pensamos desde lo más básico de la computación cuántica tenemos que 0 y 1 son bits y a.|0>+b.|1> es un qubit (aunque en este caso se pide cierta propiedad que a y b deben cumplir, a saber a y b son números complejos y |a|²+|b|²=1).
Así que este lenguaje se puede pensar como "cuántico" en el sentido de que se puede codificar programas cuánticos en él y que se puede "superponer" programas. Sin embargo, si consideramos a.M+b.N como superposición, entonces también podemos hacer superposiciones que no corresponden a programas cuánticos (cuando a y b no cumplan con las propiedades necesarias).
Ahora vamos a los tipos. Como decía en el post anterior, a cada programa (lambda-término en este caso, un término de nuestro lenguaje) le podemos hacer corresponder un tipo. Podemos considerar que si el término tiene un tipo que le corresponde, es un término válido, y sino, no lo es. Así que los tipos nos sirven en este caso para limitar el lenguaje como nosotros queramos.
¿Porqué querríamos limitar el lenguaje? Como dije anteriormente, el lambda-cálculo algebraico lineal es demasiado general y admite términos que no tienen interpretación cuántica, así que la idea es darle tipos para limitarlo y que sólo admita términos con una interpretación cuántica.
Entre todas las lógicas que mencioné en el post anterior, me interesan en particular las que tienen polimorfismo. Un ejemplo para entender qué es polimorfismo es la función identidad: Supongamos que tenemos un término lógico A, es fácil deducir que A implica A, en símbolos A=>A. Si tenemos otro término B, también podemos deducir B=>B. En general, si tenemos un término X podemos deducir que X=>X. Usando polimorfismo esto se escribe como ∀X.X=>X y se lee "para todo X, X implica X".
Desde el punto de vista del lenguaje estamos diciendo que si tenemos un término, digamos I, que se comporta como una función identidad, esto es: si recibe el término M devuelve el término M, entonces le vamos a dar el tipo ∀X.X=>X, o usando la notación del post anterior, I:∀X.X=>X. O sea: I es una función tal que si le damos un término de cualquier tipo, nos devuelve un término del mismo tipo. Entonces decimos que I es una prueba de que la fórmula lógica ∀X.X=>X (esto es "para todo X, X implica X") es correcta.
Entonces lo que queremos es un sistema de tipos tal que las únicas pruebas válidas, sean programas cuánticos.
Por lo tanto, tenemos que limitar, como dije anteriormente, los escalares que se usan para las combinaciones lineales de términos. Y eso lo queremos hacer con los tipos... ¡Entonces tenemos que incluir los escalares en los tipos! Pero con escalares sólos no nos basta, necesitamos también poder sumarlos, así que lo que necesitamos es básicamente que si un término M tiene tipo T y otro término N tiene tipo R, que el término a.M+b.N tenga tipo a.T+b.R. Y eso es lo que llamamos un sistema de tipos vectorial: un sistema en el cual dados tipos básicos, la combinación lineal de ellos es un nuevo tipo.
Para poder considerar un sistema lógico y programas como sus pruebas, necesitamos tener una propiedad llamada Subject Reduction (si alguien conoce el término que se usa en español, lo agradeceré). Esta propiedad es simple, dice que si un programa M tiene tipo T, el término N que se obtiene de ejecutar el programa, también tendrá tipo T. En este formalismo, ejecutar el programa M y obtener N se anota como "M→*N" y se lee "M reduce a N". Entonces Subject Reduction dice
Si M→*N y M:T, entonces N:T
Hay otras maneras de escribir los términos y los tipos. Hasta ahora estábamos escribiendo los términos en lo que se conoce como estilo Curry, en contraposición con el estilo Church. Un ejemplo: En el estilo Curry simplemente decimos que la función f aplicada a x tiene tipo A=>B de la siguiente manera, f(x):A=>B. En estilo Church el tipo es parte del término y diríamos algo como f^B(x:A):A=>B. Viendo el término ya tenemos el tipo, el tipo es parte del término.
Y ahora si, después de toda esta introducción puedo decir en forma relativamente corta qué es lo que probamos en este paper: El paper muestra que un sistema de tipos vectorial que incluya polimorfismo y esté expresado en estilo Curry, no tiene Subject Reduction. Y además, mostramos qué es lo más cercano a Subject Reduction que podemos tener, que es esto:
Si M→*N y M:T, entonces N:T' donde T' tiene una relación con T y si la forma de ejecutar el programa M para arribar a N no incluye una reducción en particular, entonces T' es simplemente T.El preprint del paper está disponible aquí: arXiv:1012.4032.
