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.

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.

Types 2010

Ya está publicada la lista de charlas y cronograma de Types 2010. Yo presentaré dos charlas allí:

• Sumas en cálculos lambda algebraicos. Un trabajo conjunto con Barbara Petit. En este trabajo definimos el fragmento (confluente) "aditivo" del Linear-Algebraic Lambda-Calculus. Le definimos un sistema de tipos que incluye sumas de tipos como reflejo de las sumas en los términos. Luego de probar subject reduction y strong normalisation, estudiamos el rol de las sumas en el cálculo interpretando nuestro sistema en System F con pares. Mostramos que este cálculo se puede interpretar como System F con un constructor de pares asociativo y conmutativo, el cual es distributivo con respecto a la aplicación.
• Un sistema de tipos vectorial. Un trabajo en colaboración con Pablo Arrighi y Benoît Valiron. El objetivo de este trabajo es combinar Scalar con Additive (el de más arriba) para crear un sistema de tipos al estilo System F para el Linear-Algebraic Lambda-Calculus el cual nos de una teoría de tipos general y original donde los tipos, de la misma manera que los términos, tengan una estructura de espacio vectorial. Mencionamos las conexiones con computación cuántica.

Luego de las charlas subiré aquí los slides. Aquí están.

Oxford → Marsella → Turín

Las últimas semanas he estado viajando un poco:

• Del 24 al 30 de Mayo fui a Oxford donde se llevó a cabo la spring school foundational structures in quantum computation and information (escuela de primavera estructuras fundamentales en computación e información cuántica), seguida del workshop quantum physics and logic (Física y Lógica Cuánticas). Los videos de todas las charlas de la escuela están acá y del workshop acá. Allí mismo tienen videos de eventos anteriores ordenados por evento o por speaker.
• El 8 de Junio fui a Marsella al primer encuentro del proyecto QuAND a presentar el "additive type system" (próximamente en arXiv), trabajo realizado con Barbara Petit, y la traducción del Linear-Algebraic Lambda-Calculus al Algebraic Lambda-Calculus (y viceversa), trabajo realizado con Simon Perdrix, Christine Tasson y Benoît Valiron que ya fue aceptado para el workshop higher-order rewriting que se realizará en Edimburgo el 14 de Julio próximo.
• Finalmente, del 9 al 11 de Junio estuve en Turin en el encuentro CONCERTO-PICS donde presenté el mismo trabajo con Barbara. Proximamente van a poner los slides de todas las charlas en esa página.

Equivalencia de λ-cálculos algebraicos

Como ya adelanté anteriormente, con Simon Perdrix, Christine Tasson y Benoît Valiron tenemos un paper aceptado en el workshop Higer-Order Rewriting que se llevará a cabo en Edimburgo el 14 de Julio.

Ayer enviamos la versión final (extended abstract de 5 páginas + referencias) y subimos la versión completa (con todas las pruebas, 19 páginas) al arXiv.

En este paper lo que hacemos es probar que el Algebraic λ-Calculus de Lionel Vaux (λalg), el cual es un fragmento del differential λ-Calculus, puede simular el Linear-Algebraic λ-Calculus de Pablo Arrighi y Gilles Dowek (λlin), el cual es un candidato a λ-Calculus para computación cuántica, y también probamos la simulación inversa. Ambos cálculos permiten la combinación lineal de términos, sin embargo presentan diferencias a la hora de realizar las reducciones. Por ejemplo en λalg el término


reduce a


en cambio en λlin, ese mismo término reduce a


Las pruebas de simulación se basan en la observación de que esencialmente λlin es call-by-value mientras que λalg es call-by-name. La simulación en un sentido usa la idea de "thunks" y en el otro es una extensión del continuation passing style.

Este paper es un paso hacia probar la dualidad entre ambos cálculos.

Trabajos en progreso

• Scalar. Con Pablo Arrighi estamos preparando la versión completa del Scalar Type System para un journal. Ya recibimos algunas críticas y estamos enviando una versión corregida. El 11 de abril es el deadline, así que se supone que la terminemos antes. En cuanto esté lista subiré la actualización al arXiv y avisaré aquí. Update: Aquí está arXiv:0903.3741
• Vectorial. También con Pablo estamos terminando el Vectorial Type System para enviar a una conferencia (aquí dejo los slides que presenté en las Jornadas GEOCAL-LAC a las que fui la semana pasada). El deadline es el viernes 2 y aún falta bastante por hacer, así que no sé si llegaremos... ya comentaré. Update: No llegamos, aún quedan por retocar algunas cosas, así que apuntaremos a algún otro congreso
• Lineal → Alg. Con Simon Perdrix, Benoît Valiron y Christine Tasson estamos trabajando en una traducción del linear-algebraic lambda-calculus de Pablo Arrighi y Giles Dowek al algebraic lambda-calculus de Lionel Vaux. Tenemos un deadline este miércoles, lo cual es complicado ya que es muy poco tiempo y todos estamos ocupados con otras cosas, pero si llegamos con esto les comento. Esto es un work-in-progress para un Workshop. Update: Extended abstract enviado, ahora estamos preparando una versión un poquito mas larga (con más detalles) para subir al arXiv, avisaré cuando aparezca. Update 20/04/10: Paper aceptado en el HOR2010. Ahora tenemos hasta el 17 de mayo para enviar la versión extendida, así que no creo que ponga otra versión online antes de esa fecha. Update 18/05/10: Extended abstract (5 páginas + ref) | arXiv:1005.2897 (con todas las pruebas). Post en el blog.
• Additive → IMELL. Con Barbara Petit estamos trabajando en una traducción de Additive (vendría a ser un Vectorial sin escalares, o sea, sólo sumas) en Linear Logic (más precisamente: Intuisionistic Multiplicative Exponential Linear Logic, o sea, La parte de Linear Logic que tiene sólo multiplicaciones y bangs (!) y no "tercero excluído").
• FullAdditive. Pablo Buiras, de Rosario, está trabajando en una extensión del Additive, ya que el additive que tenemos ahora sólo sirve para el cálculo sin escalares (o sea, el linear-algebraic lambda-calculus que tiene sumas, pero no escalares ni 0), la idea es hacer un sistema de tipos con sumas y no escalares, para el cálculo completo, lo cual presenta problemas no triviales sobre cómo hacer la interpretación (abtracta?) de los términos en los tipos. Esa es una tesis de Licenciatura (lo que acá en Francia sería una tesis de Master), la cual voy a dirigir junto a Mauro Jaskelioff.
• Lineal diferencial. Esta es una inquietud que surgió a partir de una visita de Emmanuel Beffara a nuestro laboratorio, en la que estamos trabajando con Emmanuel, Simon y Benoît: Cómo agregar un operador diferencial al linear-algenbraic lambda-calculus.

A medida que vaya teniendo resultados / papers completos los iré posteando aquí.

System F escalar: los slides

Subí a mi home page los slides que usé para la presentación del System F escalar. Aquí pueden bajar la versión para ver en pantalla (qpl09-talk.pdf) y aquí una versión print friendly (qpl09-talk-to-print.pdf).

La presentación era de 15 minutos, así que los slides están muy resumidos, lo que puede ser útil para un primer pantallazo sobre de qué se trata. Si les interesa, el paper completo está aquí: arXiv:0903.3741v1.

El workshop en general estuvo muy bueno. Filmaron todas las presentaciones, así que supongo que pronto estarán online (avisaré cuando estén y dónde).

System F escalar: hacia una lógica cuántica.

Primer paper desde que empecé con este proyecto de doctorado. Fue aceptado en el VI Workshop Quantum Physics and Logic que se va a llevar a cabo en Oxford el 8 y 9 de Abril próximos. Está disponible para descargar libremente aquí: arXiv:0903.3741.

Título:

Scalar System F for Linear-Algebraic λ-Calculus: Towards a Quantum Physical Logic

(System F escalar para el λ-Cálculo Algebraico Lineal: Hacia una Lógica Física Cuántica)

Y acá dejo el abstract en español:

El λ-cálculo algebraico lineal [1] extiende el λ-cálculo con la posibilidad de crear combinaciones lineales arbitrarias de términos α.t+β.u. Dado que se pueden expresar operadores de punto fijo sobre sumas en este cálculo, surge la noción de infinito, y por lo tanto, la noción de formas indefinidas. Como consecuencia, a fin de garantizar confluencia, t-t no siempre reduce a 0, sólo si t es cerrado y en forma normal. En este paper proveemos un sistema de tipos estilo System F para el λ-cálculo algebraico lineal, el cual garantiza normalización y por lo tanto no hay necesidad de esas restricciones: t-t siempre reduce a 0. Además este sistema de tipos lleva la cuenta de "la cantidad de un tipo". Por lo tanto puede verse como un sistema de tipos probabilístico, garantizando que los términos definen funciones probabilísticas correctas. Por último, se puede ver este sistema de tipos como un paso en la búsqueda de una lógica física cuántica a través del isomorfismo de Curry-Howard [2].

Bueno, tal como se expresa en el abstract, lo que hicimos fue darle tipos al λ-cálculo algebraico lineal. Usamos System F, o sea un sistema de tipos polimórfico, expresado à la Curry. Los tres resultados que se podrían destacar son:

• Con System F tenemos strong normalization, o sea, todo término que tiene un tipo normaliza, siguiendo cualquier vía de reducción. Por lo tanto, no tenemos más el problema de los infinitos del λ-cálculo algebraico lineal.
• El sistema de tipos hace que cualquier función probabilística expresada en el lenguaje, esté bien definida, o sea, que, por ejemplo, en una función que devuelve una cosa u otra dependiendo de su argumento, ambos branches suman lo mismo.
• La idea de darle tipos a este cálculo, no es por el lenguaje en sí, sino para extraer una lógica utilizando el isomorfismo de Curry-Howard, lo cual, a diferencia de la lógica cuántica definida en 1936 por Barkhoff y von Neumann [3] (la cual no se sabe cómo relacionar con la computación cuántica), esta lógica no está definida ad hoc sino extraída de un sistema de tipos de un cálculo que permite expresar la computación cuántica. Por supuesto, este es el primer paso, aún falta trabajo por hacer hasta tener un sistema de tipos que sólo admita programas representables por la computadora cuántica (i.e. que sus términos estén normalizados y que sus compuertas sean unitarias), pero aquí, con este primer sistema de tipos, hacemos un intento de interpretación de la lógica: como ya dije, esta lógica no está inventada ad hoc, sino extraída automáticamente del sistema de tipos, entonces ¿qué significa esta lógica? ¿qué interpretación le podemos dar? A modo de discusión dejamos algunas ideas en la última sección del paper.

Referencias:

[1] Pablo Arrighi y Gilles Dowek. Linear-algebraic λ-calculus: higher-order, encodings and confluence. Lecture Notes in Computer Science (RTA'08), 5117:17-31, 2008. (arXiv:quant-ph/0612199).

[2] Morten H. Sørensen y Pawel Urzyczyn.Lectures on the Curry-Howard Isomorphism, Volume 149 (Studies in Logic and the Foundations of Mathematics). Elsevier Science Inc., New York, NY, USA, 2006. (PDF).

[3] George D. Birkhoff y John von Neumann. The logic of quantum mechanics. Annals of Mathematics, 37:823-843, 1936. (JSTOR).

Update 11/04/09: Slides disponibles
Update 31/07/09: Versión extendida disponible

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.