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.

Séptimo QPL

Los días 29 y 30 de Mayo se realizará el séptimo workshop QPL en Oxford, organizado como todos los años por Bob Coecke, Parkash Panagaden y Peter Selinger. Este es el 7mo workshop con estas siglas, sin embargo las siglas han cambiado de significado: en los primeros cuatro las siglas significaban "Quantum Programming Languages" (lenguajes de programación cuánticos) y ahora significa "Quantum Physics and Logics" (física cuántica y lógica) queriendo abarcar un área mucho mayor.

Justo antes del workshop hay una escuela, del 24 al 28.

He presentado trabajos en el 5to QPL y el 6to QPL, veremos si llego a enviar algo para éste (espero que si)... aunque de todas maneras supongo que iré incluso si no presento nada.

Work-in-progress en el QNET y Bisimilaridad

Como adelanté en un post anterior, el 10 y 11 de Diciembre estuve en Oxford, en el último Workshop QNET donde presenté un "work-in-progress" de mi trabajo. Aquí dejo los slides y pueden encontrar los slides de muchas de las otras charlas en la página del workshop.

En particular me interesó mucho el trabajo de Tim Davidson: "Equivalence Relations for Communicating Quantum Processes". Es un trabajo sobre "bisimilaridad"... la definición dice (más o menos) que dos procesos cuánticos son bisimilares si actúan igual. Ejemplo, una compuerta identidad es bisimilar a dos Hadamards una detrás de otra. Además, existe una propiedad llamada "congruencia", que dice que si dos procesos son bisimilares, ellos son congruentes si, dado un contexto cualquiera, poner cualquiera de los dos procesos, da como resultado lo mismo.

Tim mostró que los procesos bisimilares a la identidad son congruentes entre sí.

Aunque parezca poco intuitivo, esto no es trivial. No siempre los procesos bisimilares serán congruentes. Por ejemplo, medir un qubit es bisimilar a medir un qubit luego de aplicarle una compuerta Hadamard (en términos de matriz densidad, ambos procesos son indistinguibles), sin embargo, si el qbit a la salida de la medición es utilizado para algo más, pues ya no serán bisimilares (las probabilidades serán diferentes).

Bueno, hubo muchos trabajos interesantes, en particular me gustó este porque hace algunos años hubo gente en mi grupo que trabajó en el tema y es un problema que me parece interesante para intentar abordar... veremos.

Primer Post

Muchas gracias Alejandro por la cordial invitación. Esta es una entrada breve como para introducción y primer post.

Para conocer un poco sobre mí, pueden encontrar detalles en mi perfil de usuario de blogger.

Actualmente me encuentro muy ocupado con reportes, examenes, y otras tareas que me dificultan escribir algo bien hecho. Esta entrada la escribo en modo automático, sin pensar mucho, y salga lo que salga. A ver también si al mismo tiempo mejoro un poco la gramática y ortografía del español a medida que va pasando el tiempo :-)

Solo quiero mencionar los tipos de temas sobre los cuales me gustaría escribir.

1-Reportes de conferencias: Conferencias a la que vaya asistiendo dentro de Japón y fuera. Tengo planeado ir este miércoles a esta conferencia International Conference on Quantum Information Science and Technology que se estará desarrollando en Tokyo. Voy a preparar un reporte con fotos.

2-Investigación: Los trabajos de investigación que estoy realizando sobre Query Complexity y Automátas Cuánticos.

3-Papers: Resúmenes de artículos científicos que me gustaron y me parecen muy interesantes para compartir, dentro y fuera de mi área de especialización. Esto espero me ayudará al mismo tiempo a medir que tan bien entendí el paper.

4-Fundamentos de Computación Cuántica: Tal vez de cuando en cuando, escribir sobre las bases matemáticas requeridas para estudiar computación cuántica, Espacios de Hilbert, Complejidad Computacional, Análisis Complejo, etc. Los que venimos de ciencias de la computación estamos muy acostumbrados a matemáticas discretas, y muchas veces pasar a estudiar análisis puede resultar difícil ya que durante el pre-grado no hay tanto énfasis en esas áreas.

Bueno, esa es la idea, a ver que tal va.

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

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)

Categories, Logic and Foundations of Physics: Los videos

Copio (y traduzco) un post de Bob Coecke en el blog The n-Category Café:

Los videos del 2do workshop Categories, Logic and the Foundations of Physics que se realizó en Londres están disponibles aquí. También hay allí algunas charlas del workshop Logic, Physics and Quantum Information Theory organizado por Prakash Panagaden en Barbados. Desafortunadamente algunas de las charlas no salieron muy bien, por ejemplo la de Peter Selinger "completeness result for dagger compact categories". Esperamos poder compensar esto en el workshop Quantum Physics and Logic que se hará en julio en Islandia. Todos los créditos para Ben Jackson y Jamie Vicary por realizar esta filmación y ponerla online.

La fecha para el próximo workshop "Categories, Logic and the Foundations of Physics", el cual será en Oxford, es el 23 y 24 de agosto - dos días esta vez.

Ese congreso en Islandia es donde presentamos y nos fue aceptado el paper sobre medición y confluencia en lambdas cálculos cuánticos. Lamentablemente por razones económicas no podré ir, así que al menos espero poder ver los videos.

Publicada la lista de papers aceptados para el QPL

El paper que enviamos al QPL fue aceptado para una exposición completa de 30 minutos (en contraposición con una exposición corta de 15 minutos). La lista completa de los papers aceptados está publicada en la página del evento.

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).

WECIQ 2007

Del 29 al 31 de Octubre se desarrollará en la ciudad de Campina Grande, Brasil, el 2do Workshop-Escuela de Computación e Información Cuántica. El primero se hizo el año pasado en la ciudad de Pelotas, y estuvo realmente muy bueno!
Aún se pueden enviar resúmenes de trabajos hasta el 31 de Mayo. Le recomiendo a todo el que tenga la posibilidad de ir, que no se lo pierda.

Video de David DiVincenzo

Acá dejo un video de una charla de David DiVincenzo en el "International Workshop on Measurement-Based Quantum Computing" que se realizó en Oxford entre el 18 y 21 de Marzo pasados. La Charla se titula "The Pioneers of Quantum Computing" (Los Pioneros de la Computación Cuántica) y acá dejo el abstract.

Que lo disfruten.

Brasil: Punteros sudamericanos

Ayer volví del WECIQ, un Workshop y Escuela Brasileña sobre computación cuántica. Realmente me impresionó la cantidad de grupos y los temas variados que trabajan en nuestra hermana Brasil. El evento tuvo un nivel muy bueno y, por supuesto, un nivel de cordialidad y cooperación muy agradables.
Para todos aquellos a quienes les interese ver los trabajos y mini-cursos presentados, en la página del evento se pueden encontrar los anales digitalizados.

QIP 2007

Del 30 de Enero al 3 de Febrero de 2007 se desarrollará en Brisbane, Australia el 10º QIP (Quantum Information Processing). Este workshop es el más importante en Información Cuántica teórica y este año está a cargo de nada menos que Michael Nielsen.
El deadline para enviar abstract de charlas es el 4 de Noviembre de 2006.
El deadline para registrarse es el 24 de Noviembre de 2006.
La página del evento se puede ver aquí: http://qipworkshop.org.
Bueno, veamos si consigo alguna beca para ir allí (cualquier propuesta sobre a quién pedir una beca es bienvenida) ;)

WECIQ 2006

Del 9 al 11 de Octubre se desarrollará en la ciudad de Pelotas, Brasil, un evento que pinta ser interesante, el 1er Workshop-Escuela de Computación e Información Cuántica.
El evento contará con importantes investigadores de la región, y, además de los trabajos (que aún se pueden presentar hasta el 20 de Julio), tendrá la sección "Escuela" con charlas de 2hs en los siguientes temas:

• Conceptos e interpretaciones de la Mecánica Cuántica
• Circuitos cuánticos
• Información cuántica
• Algoritmos cuánticos
• Lenguajes de programación cuánticos
• Tecnologías para las computadoras cuánticas.

La inscripción estará abierta a partir del 20 de Agosto.