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.

Escalares y sumas, al arXiv // Scalars and sums, to arXiv

(English version below)
Ya está disponible el paper que escribimos con Barbara Petit sobre el análisis de las sumas en los cálculos algebraicos que presentamos en Types 2010. La semana pasada lo subimos al arXiv: http://arxiv.org/abs/1011.3542.

También la semana pasada con Pablo Arrighi actualizamos en el arXiv el paper sobre los escalares en los cálculos algebraicos. En este caso es un sistema de tipos que nos permite llevar de cierta manera una cuenta de 'la cantidad de un tipo' que participa en cada término. Acá dejo el link: http://arxiv.org/abs/0903.3741v4.

Ambos casos son análisis del lambda cálculo algebraico-lineal de Pablo Arrighi y Gilles Dowek, el cual fue pensado originalmente como un lambda cálculo cuántico, en el sentido de que permite encodear algoritmos cuánticos y está diseñado de tal manera de no permitir cloneo.

---

It is now available the paper we wrote with Barbara Petit about the analysis of sums in algebraic calculi, presented in Types 2010. Last week we uploaded it to arXiv: http://arxiv.org/abs/1011.3542.

Also last week with Pablo Arrighi we updated in the arXiv our paper about scalars in algebraic calculi. In this case it is a type system which allows us to take care of the 'amount of a type' that participates in each term. Here it is the link: http://arxiv.org/abs/0903.3741v4.

Both papers are analyses of the linear-algebraic lambda-calculus developed by Pablo Arrighi and Gilles Dowek, which was originally thought as a quantum lambda calculus, in the sense that it allows to encode quantum algorithms and it is designed to not allow clonning.

Slides Types 2010

Como ya había adelantado, la semana pasada estuve en Varsovia participando del workshop Types 2010. Los slides de mis presentaciones están disponibles a través de mi página web: Sums in algebraic lambda-calculi y A vectorial type system (work-in-progress).

Hubo en general muy buenas charlas. En particular, les recomiendo ver los slides de la excelente charla de Henk Barendregt: Lambda calculus with types.

Viajes y novedades en el blog

Viajes pasados y planificados:

• La semana pasada estuve en el PPS en París, donde mi director y co-autor del paper del sistema de tipos "Scalar" dio una charla sobre nuestro paper. Los slides los subiré pronto a mi página (y linkearé aquí) aquí están. La idea es que para los seminarios PPS no aceptan estudiantes de doctorado para dar las charlas, así que por eso la dió Pablo.
• El 10 y 11 de Diciembre estaré en Oxford, donde iré al último Workshop QNET a presentar un "work-in-progress" de mi trabajo. QNET es una red británica de investigación en semántica de la computación cuántica (más info en su página).
• El 7 y 8 de Enero voy al LDP en Marseille, donde daré la misma charla que dió Pablo en el PPS sobre scalar.

Cambios en el blog:

Dado que ya se está tornando aburrido mi blog, porque está demasiado centrado en mi tema de investigación y no tanto en computación cuántica en general, he invitado a Marcos Daniel Villagra, a quien ya conocen porque publicó un post recientemente en este blog, a que sea co-autor del blog, así le damos un poco más de dinámica. Él también anda bastante ocupado, así que no es que por ser dos ahora habrá post mucho más seguidos, pero al menos los habrá más variados.

Bienvenido Danny!

Vectorial, Lógica Lineal y Ortogonalidad

El miércoles y jueves pasados estuve en Lyon, invitado por Barbara Petit del grupo PLUME de la École Normale Supérieure de Lyon. Allí di un seminario sobre los sistemas de tipos que he desarrollado: Scalar, Additive y Vectorial, y algunos de los problemas sobre cómo chequear ortogonalidad entre términos y algunas pistas para resolverlo.

Olivier Laurent se dio cuenta de simplemente ver la presentación, la conexión entre Additive y Intuitionistic Multiplicative Exponential Linear Logic.

Pronto estaré publicando un nuevo paper sobre Additive (con esa conexión a la lógica lineal) y Vectorial. Además, hemos empezado a trabajar juntos con Barbara en el problema de la ortogonalidad, usando subtyping.

Próximos viajes:
Los días 4 y 5 de Mayo voy a París a visitar a Benoît Valiron y Gilles Dowek del proyecto TypiCal, en la École Polytechnique de París, donde daré otro seminario. Luego, el 18 de Mayo estaré en Chambery, donde iremos con mi director, Pablo Arrighi, a participar de una serie de seminarios organizados por Lionel Vaux del grupo LAMA.

System F à la Curry y Grupo de trabajo

Buenas!

Les cuento que ya estoy instaladísimo en Grenoble. Lo que he hecho en estos días es adaptar un sistema de tipos polomórficos (System F à la Curry, ver [1], [3] o [4] para más detalles) al Linear-Algebraic Lambda-Calculus de Arrighi y Dowek [2], además hice una prueba de strong normalization (ver [1] o [3]) para este «Linear-Algebraic System F» y algunos comentarios respecto a que este sistema se corresponde de acuerdo al Isomorfismo de Curry-Howard (ver [4]) con la misma lógica (Lógica Proposicional de Segundo Orden) que el System F original. La idea ahora es empezar a jugar con reglas de tipos más complejas, hacer alguna clase de álgebra de tipos, para obtener alguna lógica un poco más loca. Ya les comentaré cuando tenga algo más armado :)

Este próximo jueves nos juntamos con el grupo de trabajo que estamos más o menos en los mismos temas, en lo que le hemos dado a llamar WHOCAS: «(informal) Workshop on Higer-Order Calculi and Algebraic Structures», seremos sólo 5 personas, ya que es un grupo de trabajo más que un workshop: Lionel Vaux, Benoît Valiron, Gilles Dowek, Pablo Arrighi y yo. La idea es que cada uno dará una pequeña charla de 40 minutos contando en qué está trabajando, así vemos qué colaboraciones pueden salir de allí. Luego del WHOCAS publicaré aquí las transparencias que use.

Referencias
[1] Jean-Yves Girard, Yves Lafont, Paul Taylor. Proofs and types. Cambridge University Press, 1989.
[2] Pablo Arrighi, Gilles Dowek. Linear-algebraic lambda-calculus: higher-order, encodings, and confluence. Lecture Notes in Computer Science: (RTA'08), 5117:17-31, 2008. (preprint en arXiv:quant-ph/0612199)
[3] Henk Barendregt. Lambda calculi with types, volume 2 of Handbook of Logic in Computer Science. Clarendon Press, Oxford, 1992.
[4] Morten Sørensen, Pawel Urzyczyn. Lectures on the Curry-Howard Isomorphism, volume 149 of Studies in Logic and the Foundations of Mathematics. Elsevier, 2006. (disponible para bajar en CiteSeer)

Preparando las valijas

Los últimos posts de este blog han sido demasiado personales para mi gusto (comentando en qué ando). Pero bueno, lo voy a cambiar dentro de poco cuando empieze el doctorado.

Por ahora les comento, el Jueves 9 de Octubre llego a Grenoble, al grupo Quantum Computation in Grenoble, donde iniciaré mi doctorado bajo la dirección de Pablo Arrighi. La idea es que el doctorado dure tres años, espero terminarlo a tiempo :)

El trabajo será en lógica cuántica y teoría de tipos para la computación cuántica, e iré contando detalles a medida que vayamos obteniendo resultados. Mi idea es continuar este blog como un "diario de doctorado", donde iré contando los avances que vayamos teniendo.

Beca francesa

Bonjour!
Les comento que en Setiembre, si todo sale bien, iniciaré mis estudios de doctorado en el Laboratoire d'Informatiqué de Grenoble, Francia, más precisamente en el QCG bajo de dirección de Pablo Arrighi.
La semana pasada me llegó el mail donde me confirman que me han dado la beca! (ahora estoy esperando que me den todos los detalles de cómo tramitar la visa, todo el papelerío necesario, los detalles del monto de la beca, posible alojamiento, etc).
El tema de mi tesis de doctorado es "Models of quantum computation" y aquí pueden ver una descripción del proyecto (en Inglés).
Cómo decirlo.... ESTOY EUFORICO!!!! :)
Au revoir!

Paper sobre medición y confluencia enviado al QPL/DCM y subido al arXiv

El domingo pasado mandamos la versión extendida del paper que se presentará en el próximo QPL/DCM 2008 que se llevará a cabo en Reykjavik, Islandia los próximos 12 y 13 de Julio. Además, subimos esta versión preliminar al arXiv y hoy apareció como arXiv:0806.2447v1 (se puede acceder y descargar gratuitamente desde allí).

Trataré de hacer un muy breve resumen sobre el paper, dejando links a Wikipedia donde sea conveniente (claro que si les interesa enserio, nada mejor que uno o dos buenos libros (mis recomendaciones: "Quantum Computation and Quantum Information" de Michael Nielsen e Isaac Chuang y algún libro de Semántica y sistemas de Reescritura).

Primero, el título: "Measurements and confluence in quantum lambda calculi with explicit qubits", en castellano sería algo así como "Medición y confluencia en Lambda Calculos Cuánticos con qubits explícitos". Trataré de hacer una breve reseña de cada uno de los conceptos que figuran en éste título:

Medición: En Computación Cuántica, la medición es un proceso intrínsecamente probabilístico. O sea, cuando uno mide en qué estado está el sistema, cambia el estado, pero a qué cambia no se sabe con anterioridad, sólo las probabilidades de que cambie a uno u otro estado. Enlace a la Wikipedia (en Inglés).

Confluencia: Es una propiedad deseable de los sistemas de reescritura. La idea básica es: si puedo reescribir un término de mi lenguaje de dos maneras posibles, es necesario que exista otro término al cual ambos puedan "confluir". Enlace a la Wikipedia (en Inglés).

Lambda Cálculo: Es un sistema formal que abstrae el concepto de función. Es la base de los lenguajes de programación funcionales. Enlace a la Wikipedia (en Español).

Lambda Cálculos Cuánticos: Se han realizado muchas extensiones al Lambda Cálculo. Entre ellas, podemos encontrar las extensiones que se hicieron para representar las propiedades cuánticas (como paralelismo, enredo, etc). En el paper pueden encontrar muchas citas sobre estos desarrollos. También pueden ver los excelentes surveys ([1][2]) que han hecho Simon Gay y Peter Selinger.

Con qubits explícitos: Hay algunas extensiones cuánticas al lambda cálculo que manipulan qubits de manera explícita (los símbolos que representan qubits, realmente representan qubits) y hay otros que los manipulan a través de una especie de "punteros", o "memoria" (los símbolos que representan qubits, en realidad son punteros a los mismos).

Ahora sí, habiendo dejando los conceptos en claro: nuestro trabajo presenta un método de cómo agregar medición a aquellas extensiones cuánticas del lambda cálculo que manejan qubits de manera explícita. Y presenta una prueba de confluencia, la cual está hecha de una manera lo suficientemente general como para permitir utilizar el método para sistemas de reescritura probabilísticos en general. En lo particular, el paper está escrito siguiendo las extensiones cuánticas introducidas por André van Tonder, por ser uno de los mas simples.

Hemos trabajado en esto con Pablo Arrighi, Manuel Gadella y Jonathan Grattage, de quienes he aprendido muchísimo.

Medición y confluencia en lambda cálculos cuánticos con qubits explícitos

Ayer llegué de Francia. Estuve 2 semanas en Grenoble y 2 semanas en Orsay.

En Grenoble estuvimos trabajando con Pablo Arrighi y Jonathan Grattage en extender mi tesis de grado de agregado de medición al Lambda Cálculo cuántico de van Tonder[1]. La idea fue extenderlo para probar confluencia y dejar el método lo suficientemente general para que pueda ser fácilmente usado para extender otros lambda cálculos (en particular, ahora estamos trabajando en extender el lambda cálculo de Pablo[3,4], que es quien me invitó a Grenoble, y el QML de Jon[5,6], también investigador en Grenoble).

Hoy enviamos el extended abstract al QPL08 que se realizará en Reykjavík, Islandia los próximos 12 y 13 de Julio. Update: (16/6/08) En un post reciente pueden encontrar la versión extendida, la cual tiene varios cambios sustanciales

El 21 de Abril nos avisarán si el paper ha sido aceptado.

Esas dos semanas y el tiempo que le siguió, he aprendido muchísimo! Ahora Pablo está tramitando una beca para ver si puedo empezar mi doctorado allí en Setiembre.

En Orsay también fueron muy amables, y también aprendí mucho. Ellos están trabajando en algoritmos y complejidad (cuánticos), un tema que no conocía en profundidad.

Tanto en Grenoble como en Orsay, dí una charla sobre mi tesis de grado, los slides los pueden obtener de aquí. (Igualmente si les interesa el tema, les recomiendo leer el extended abstract, ya que tiene algunos cambios bastante importantes).

Referencias.

[1] A. van Tonder. A lambda calculus for quantum computation. SIAM Journal on Computing, 33(5):1109-1135, 2004. (también en arXiv:quant-ph/0307150).

[2] P. Arrighi y G. Dowek. A computational definition of the notion of vectorial space. Electronic Notes in Theoretical Computer Science, 117:249-261, 2005. (también disponible en la página de Gilles Dowek).

[3] P. Arrighi y G. Dowek. Linear-algebraic lambda-calculus: higher-order, encodings and confluence. Enviado a RTA'08 (también en arXiv:quant-ph/0612199).

[4] T. Altenkirch y J. J. Grattage. A functional quantum programming language. En Proceedings of the 20th Annual IEEE Symposium on Logic in Computer Science (LICS). IEEE Computer Society, 2005. (también en arXiv:quant-ph/0409065).

[5] T. Altenkirch, J. J. Grattage, J. K. Vizzotto, y A. Sabry. An algebra of pure quantum programming. Electronic Notes in Theoretical Computer Science, 170:23-47, 2007. (también en arXiv:quant-ph/0506012).

Volviendo a Francia

La semana que viene, más precisamente el 2 de Marzo, me voy a pasar un mes a Francia, estaré del 3 al 15 con el grupo de Pablo Arrighi en Grenoble y del 16 al 29 con el grupo de Miklos Santha en Orsay, quienes me han invitado.

Ambos grupos trabajan con Funcional Cuántico (entre otras cosas), un tema que cada día me apasiona más (y que cada día me doy más cuenta de lo poco que sé). Espero aprender mucho de ellos!