21 de diciembre de 2010

Explicación del paper, legible por humanos.

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.

17 de diciembre de 2010

New paper: Subject reduction in a Curry-style polymorphic type system with a vectorial structure

(Versión en español más abajo)

New paper submitted, with Pablo Arrighi and Benoît Valiron.
Title: Subject reduction in a Curry-style polymorphic type system with a vectorial structure.
Abstract: The algebraic lambda-calculus [Vau09] and the linear-algebraic lambda-calculus [AD08] extend the lambda-calculus with the possibility of making arbitrary linear combinations of lambda-terms. The two foundational works of [ADC09] and [DCP10] describe type systems for this calculus respectively accounting for scalars and sums. Building on these approaches, we devise a typed algebraic lambda-calculus merging the two approaches while keeping a language featuring local confluence and a weak subject reduction. This gives rise to an original and general type theory where types, in the same way as terms, have a vector space-like structure. The main contribution of this paper is a subject reduction result, a problem renowned to be a delicate matter under the presence of union-like type constructs.
Basically the idea of the paper is to present the several-times announced "vectorial type system": we present here a type system with a non-standard subject reduction. We conclude that, in general, to have subject reduction in a vectorial type system we would need to move to Church-style.

I uploaded the paper to arXiv today, so it will appear next Tuesday. I will put the link here. arXiv:1012.4032.

Nuevo paper enviado, con Pablo Arrighi y Benoît Valiron.
Título: Subject reduction (ni idea cómo se dice eso en español) en un sistema de tipos polimórfico à la Curry con una estructura vectorial.
Resumen: El lambda-cálculo algebraico [Vau09] y el lambda-cálculo algebraico-lineal [AD08] extienden el lambda-cálculo con la posibilidad de hacer combinaciones lineales arbitrarias de lambda-términos. Los dos trabajos fundacionales de [ADC09] y [DCP10] describen sistemas de tipos para este cálculo respectivamente teniendo en cuenta escalares y sumas. Construido sobre estos enfoques, elaboramos un lambda-cálculo algebraico fusionando ambos, logrando un lenguaje con confluencia local y una subject reducción débil. Esto da lugar a una teoría de tipos original y general donde los tipos, de la misma manera que los términos, tienen una estructura al estilo de un espacio vectorial. La principal contribución de este paper es el resultado de subject reduction, un problema reconocido como complicado en presencia de construcciones de tipo unión.
Básicamente la idea del paper es presentar el muchas veces anunciado "sistema de tipos vectorial": lo que presentamos aquí es un sistema de tipos con un subject reduction no estándar. Concluímos que, en general, para tener subject reduction in sistemas de tipos vectoriales deberíamos pasarnos a Church-style.

Hoy subí el paper a arXiv, así que aparecerá el próximo martes. Pondré el link aquí. arXiv:1012.4032. Y aquí una explicación más amena del paper.

9 de diciembre de 2010

Quantum Foundations Mailing List | Lista de correo "fundamentos cuánticos"

(Versión en español más abajo)

Bob Coecke and Jamie Vicary have started a mailing list on "quantum foundations".

The announcement is the following:

It was agreed by many that the existence of a quantum foundations mailing list, with a wide scope and involving the broad international community, was long overdue. This moderated list (to avoid spam or abuse) will mainly distribute announcements of conferences and other international events in the area, as well as other relevant adverts such as jobs in the area. It is set up at Oxford University, which should provide a guarantee of stability and sustainability. The scope ranges from the mathematical end of quantum foundations research to the purely philosophical issues.

To subscribe to the list, send a blank email to:
quantum-foundations-subscribe@maillist.ox.ac.uk

To unsubscribe, a blank email to:
quantum-foundations-unsubscribe@maillist.ox.ac.uk


Bob Coecke y Jamie Vicary comenzaron una lista de correo en "fundamentos cuánticos".

El anuncio es el siguiente:

Se ha llegado al acuerdo entre muchos que la existencia de una lista de correo en fundamentos cuánticos, con un amplio alcance y gran participación de la comunidad internacional, es una deuda desde hace mucho. Esta lista moderada (para evitar el spam o abuso), principalmente distribuirá anuncios de conferencias y otros eventos internacionales en el área, así como otros anuncios pertinentes tales como puestos de trabajo en el área. Se instaló en la Universidad de Oxford, lo que debería ofrecer una garantía de estabilidad y sostenibilidad. El ámbito de la lista abarca desde el fin matemático de la investigación en fundamentos cuánticos hasta las cuestiones puramente filosóficas.

Para suscribirse a la lista, envíe un mail en blanco a:
quantum-foundations-subscribe@maillist.ox.ac.uk

Para desuscribirse, un mail en blanco a:
quantum-foundations-unsubscribe@maillist.ox.ac.uk