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.

Escuela: "Foundational Structures in Quantum Computation and Information" en Oxford

Como mencioné en un post anterior, justo antes del QPL de este año se realizará una escuela sobre estructuras fundamentales en información y computación cuántica. Habrá cursos en los siguientes temas:

• modelo de computación cuántica basado en medición (MBQC: measurement-based quantum computation); propiedades de grafos de estados; MBQC y física de materia condensada; computación cuántica ciega (blind quantum computing); determinismo en MBQC; modelo de computación clásica basado en medición y no-localidad;
• categorías monoidales, álgebras de Frobenius y su cálculo gráfico; (co)algebra de observables complementarios y enredo cuántico multipartito, y aplicaciones en MBQC; grupos de fase y no-localidad;
• simulación clásica de circuitos cuánticos; topología categórica de computación cuántica; cálculo gráfico para medición y canales de información; teorías probabilísticas generalizadas; modelos operacionales convexos y no-localidad;
• autómatas celulares cuánticos (QCA); QCAs y causalidad; typos de alto orden en computación cuántica; lógicas cuánticas y máquinas cuánticas; métodos coalgebraicos.

De la mayoría de los temas, conozco poco y nada; y por eso planeo asistir a la escuela :)

La escuela dura cinco días, del 24 al 28 de Mayo, en Oxford y es organizada por Bob Coecke y Ross Duncan.

Trataré de ir haciendo resúmenes diarios sobre lo que vaya viendo.

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.

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!

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

Teoría de Categorías

El viernes aparecieron en arXiv tres nuevos artículos de Bob Coecke. Son introducciones a Categorías Cuánticas. Acá les dejo los links para quienes les interese:

• Categorical quantum mechanics (con Samson Abramsky) arXiv:0808.1023

• Introducing categories to the practicing physicist arxiv:0808.1032

• Toy quantum categories (con Bill Edwards) arXiv:0808.1037
  

Además de esos tres, apareció este otro, también de él, actualizado:

• Quantum measurements without sums (con Dusko Pavlovic) arXiv:quant-ph/0608035

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.

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.