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.

Charla de Julia Kempe en la UBA

Dia y hora:

MIERCOLES 13/8, 14hs

Lugar:

AULA FEDERMAN, PRIMER PISO, PABELLON 1
Facultad de Ciencias Exactas y Naturales, UBA

Titulo:

From Bell's inequalities to computational complexity

por Julia Kempe
Department of Computer Science, University of Tel Aviv, Israel

Resumen: Since the seminal work of John Bell it has been known that quantum entanglement between two parties can produce correlations that are not possible in a classical world, even with hidden variables. This has been one of the most remarkable discoveries and a formidable tool to prove the validity of quantum mechanics in the lab.

Computer scientists have long since appropriated Bell's inequalities. Perhaps the most prominent "application" is in unconditionally secure quantum cryptography. But among the most important challenges in the field currently is to understand the computational complexity of computing the violation of Bell's inequalities, or, in computer science lingo, the hardness of entangled multi-prover interactive proofs. Surprisingly, one of the most important approaches currently in this area builds on the work of Tsirelson who gave upper bounds on the maximal violation of Bell inequalities using semidefinite programming. I will explain the connection and the questions in this area and give an overview of some recent results, which, surprisingly, also give rise to new Bell inequalities.

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

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.

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.

Nuevo blog sobre computación cuántica... desde Guatemala

Desde Guatemala apareció un nuevo blog: "La Consigna", de Gerberth Adín Ramírez Rivera que, como tema central, trata sobre Computación Cuántica. Desde aquí les deseo suerte con el sitio!

A todos los interesados en saber de qué se trata ésto de computación cuántica, les recomiendo los primeros posts de ese blog, donde hace una didáctica introducción al tema.

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

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!