Poniendo FoQCoSS en los fundamentos de la computación cuántica

Nos acaban de aprobar el proyecto STIC-AmSud "FoQCoSS - Foundations of Quantum Computation: Syntax and Semantics" (Fundamentos de la computación cuántica: sintaxis y semántica).

Este es un proyecto conjunto donde participan 5 instituciones (dos argentinas, una brasileña y cuatro francesas) y un total de 11 investigadores y becarios.
Los miembros argentinos somos los miembros argentinos de este blog, Gabriel Senno y, quien les escribe, Alejandro Díaz-Caro.

El objetivo del proyecto, como lo dice el título, es estudiar los fundamentos de la computación cuántica, con 5 objetivos específicos claros:

1. Estudiar el fenómeno del paralelismo, utilizando las extensiones algebraicas al lambda cálculo.
2. Estudiar la semántica denotacional del lambda cálculo vectorial.
3. Estudiar sistemas modulo isomorfismos de tipos.
4. Estudiar la  semántica categórica del lambda cálculo cuántico del equipo brasileño en el proyecto.
5. Estudiar los las consecuencias de la teoría de la computabilidad en la física y las consecuencias de la física en la teoría de la computabilidad.

Es un proyecto a dos años que nos va a permitir reunirnos todos en jornadas de trabajo un par de veces al año y es financiado por MAEDI e INRIA de Francia, CAPES de Brasil y MINCYT de Argentina.

Les dejo el link a la descripción completa del proyecto en la página de STIC-AmSud.

Los integrantes somos (en orden alfabético):

1. Pablo ARRIGHI – Université Aix-Marseille, Francia
2. Alejandro DIAZ-CARO – Universidad Nacional de Quilmes, Argentina
3. Gilles DOWEK – INRIA, Francia
4. Stefano FACCHINI – Université Aix-Marseille, Francia
5. Juliana KAIZER VIZZOTTO – Universidade Federal de Santa Maria, Brasil
6. Simon MARTIEL – INRIA, Francia
7. Simon PERDRIX – CNRS/LORIA, Francia
8. José Carlos PUIATI PIRES – Universidade Federal de Santa Maria, Brasil
9. Gabriel SENNO – Universidad de Buenos Aires, Argentina
10. Benoît VALIRON – CentraleSupélec –LRI, Francia
11. Hanry (Quanlong) WANG – LORIA, Francia

Proyectos

Tenemos bastante abandonado el blog. Por mi parte mis excusas son que este semestre he estado dictando varios cursos a la vez (1 en la Tecnicatura en Programación Informática, 2 en la Licenciatura en Informática y 1 en la Maestría en Bioinformática, de la UNQ), ya que el semestre que viene no dictaré clase alguna en Quilmes porque me voy todo el semestre a Turín.

Presentadas las correspondientes excusas, les cuento en qué estoy trabajando actualmente, proyectos y demás. (Ah! Y estoy buscando buenos estudiantes que quieran engancharse en alguno de los temas para hacer su doctorado!).

En primer lugar, con Fidel (Pablo E. Martínez López) terminamos una implementación de λ⁺, la extensión a λ-cálculo que hicimos con Gilles Dowek donde tipos isomorfos son considerados iguales. Ya hablé de este trabajo en un post anterior (no dejen de leerlo). Lo que terminamos de hacer ahora es corregir todo lo que había que corregir de la versión presentada en IFL, y enviado a evaluación al post-proceedings de esa conferencia para su publicación. El lunes subiré el paper, tal como lo enviamos, a mi página web (no tengo acceso a ella desde mi casa). Update: Aquí está.

Por otro lado, con Abuzer Yakaryilmaz enviamos un paper para su revisión. Abuzer es especialista en Autómatas Cuánticos, y juntos diseñamos un autómata que dimos en llamar autómata afín, el cual es una especie de autómata probabilista... sólo que acepta probabilidades negativas. Dicho de otro modo, acepta "probabilidades" en los reales tales que la suma de ellas dé 1. Es como eliminar el axioma de que las probabilidades deben ser positivas. Lo interesante es que con dicho autómata podemos recrear la interferencia destructiva que existe en la cuántica (la cual existe justamente porque las "amplitudes" pueden ser negativas y por lo tanto pueden cancelarse con otras positivas).

También allí les debo el paper ya que aún no lo subí a mi página web. Veré de subirlo esta semana y actualizar el link aquí. Update: El paper fue aceptado. Más info y link de descarga aquí.

Finalmente, una tercera línea, es con Gilles Dowek, con quien nos basamos en las ideas desarrolladas en λ⁺ para definir un cálculo donde la medición cuántica proyectiva se interpreta como una conjunción conmutativa. Ya comenté de este trabajo hace unos meses. El paper ahora está listo (otro más que tengo que subir a mi página). Update: Lo pueden bajar de aquí -> arXiv:1601.04294.

Como adelanté al principio, les cuento que de Enero a Julio estaré en Italia, a donde iré como profesor invitado a la Università di Torino a trabajar con Mariangiola Dezani-Ciancaglini y Simona Ronchi della Rocca. El proyecto es utlizar tipos unión e intersección (de los cuales Mariangiola y Simona son expertas) para caracterizar ciertas propiedades de la computación cuántica. Aunque también trabajaremos en otros temas: con Mariangiola este año comenzamos un trabajo sobre el "preciseness" del subtipado con unión e intersección. Veremos qué surge de todo eso. Son seis meses para interactuar en temas de tipos unión e intersección, más cuántica.

Eso es todo por ahora. Les recuerdo el tema con el que comencé el post: si estás terminando tu Licenciatura en Ciencias de la Computación (o carreras afines) y te interesan estos temas, no dudes en contactarme ya que estoy buscando buenos estudiantes que quieran venir a hacer un doctorado conmigo a Quilmes. También hay posibilidades para tesinas de grado. Mi mail y teléfono lo encuentran en mi página web.

Mini-curso introductorio a la computación cuántica

En octubre voy a dar un curso introductorio a la computación cuántica de 4hs de duración en las XIII Jornadas de Ciencias de la Computación (JCC). Las JCC son un evento organizado por y para los estudiantes en la Universidad Nacional de Rosario, que cada año invitan investigadores tanto de Argentina como de otros lugares (muchas veces egresados de la Licenciatura en Ciencias de la Computación de la UNR, como es mi caso o el de Sergio Giro, que actualmente trabaja para Google en Londres). Este año ya hay confirmadas 8 charlas, que pueden ver en la página del evento:

XIII Jornadas de Ciencias de la Computación

Con respecto a mi charla: será el jueves 22 y viernes 23 de octubre de 10 a 12hs. Requerimientos mínimos: tener una base de álgebra (vectores y matrices). Les dejo el resumen oficial:

La computación cuántica es un paradigma de computación basado en la física cuántica. La idea es tomar la descripción de la evolución de sistemas físicos cuánticos como un proceso de cómputo: éstos tienen un estado inicial, un estado final, y la evolución del sistema puede ser descripta a través de "operadores". Uno de los principales intereses en computación cuántica desde las ciencias de la computación es que existen algoritmos en este modelo de cómputo que tienen ganancias en complejidad con respecto a algoritmos clásicos, en algunos casos llegando hasta ganancias exponenciales. En este mini-curso de dos días se verá una introducción a la computación cuántica, así como algunos ejemplos de algoritmos y una aplicación a criptografía.

Isomorfismos como igualdades: Proyectando funciones y mejorando la aplicación parcial a través de una implementación de λ⁺

El título de este post es el título de un paper (bueno, su traducción) que acabamos de terminar de escribir y enviar a una conferencia con Pablo E. Martínez López (o Fidel, como lo conoce todo el mundo).

En este paper proponemos una implementación de λ⁺ (un cálculo del que ya he hablado varias veces en este blog, que desarrollamos con Gilles Dowek). λ⁺ tiene la característica de que toma los isomorfismos de tipos y los considera igualdades. Por ejemplo, una función que toma dos argumentos es igual a una función que toma un par, y una función que retorna dos argumentos es igual a dos funciones, porque A⇒B⇒C es isomorfo a (A∧B)⇒C y A⇒(B∧C) es isomorfo a (A⇒B)∧(A⇒C).

El sistema de reescritura de λ⁺ utiliza reescritura modulo una relación de equivalencia, lo cual hace que implementar un lenguaje con esas características no sea trivial. Y eso es exactamente lo que proponemos en este nuevo paper. Además, extendemos λ⁺ con números naturales y recursión general, y, usando un resultado clásico para dividir recursiones mutuas (teorema de Bekić), junto a las características de λ⁺, logramos una forma interesante de transformación de programas: podemos, por ejemplo, definir una función recursiva que calcula dos valores y luego proyectar el valor que nos interesa... sólo que el programa va a hacer la proyección antes de recibir sus argumentos, proyectando la función y transformándola en una función que sólo calcula el valor que nos interesa.

Otra propiedad interesante es que la curryficación, llevada al extremo, junto a la asociatividad y conmutatividad, hacen que tengamos una forma de aplicación parcial muy potente: una función que recibe más de un argumento, puede recibir cualquiera de ellos en cualquier orden.

Bueno, les dejo el paper tal como lo acabamos de enviar (aún debe ser revisado por los reviewers):

http://diaz-caro.web.unq.edu.ar/lambdaPlusI.pdf

Workshop INFINIS

Este viernes 17 de julio se realizará un Workshop en la Universidad de Buenos Aires, organizado por el Laboratorio Internacional Asociado INFINIS, un laboratorio en cooperación entre la Universidad de Buenos Aires y el CONICET con la Université Paris 7 y el CNRS.

Les dejo el link al programa del workshop en la página del laboratorio:

http://www.infinis.org/?p=726

Yo voy a dar una charla, básicamente la misma charla que dí en Rosario en junio, sólo que en inglés :-)

Update: Dejo los slides

Charla en el Workshop on Physics and Information

El lunes pasado fui invitado a dar una charla en el Workshop on Physics and Information que se llevó acabo en el Institut Henri Poincaré de París, ciudad en la que estoy desde Mayo y hasta fin de Julio trabajando con Sophie Laplante, de LIAFA, en temas de no-localidad y quantum communication complexity.

Acá les dejo el título y resumen de la charla:

Consequences of the Physical CTT over experimental setups in quantum physics

We study the limitations that the physical Church-Turing thesis imposes when performing experimental verifications of quantum theory. First, we show that different preparations of the (theoretically) same proper mixed state are distinguishable if computable. Then, we show that using independent PRNGs to choose the inputs for a Bell tests is not enough to observe a proper Bell inequality violation. That is, we give a local model that reproduces any correlations arising from a Bell scenario in which the measurement choices were made following algorithms.

Y estas son las diapositivas:

Mudanza a Paraguay

Desde Abril de este año estoy como profesor investigador a tiempo completo en la Universidad Nacional de Asunción (UNA). Después de casi 8 años en Japón, he viajado por debajo de la línea del ecuador y espero quedarme por aquí.

Actualmente estoy en el proceso de la creación de un grupo de investigación en Teoría de la Computación junto con otro profesor del área, y espero pronto tener un sitio web del grupo. Las áreas de investigación del grupo serían complejidad computacional, algoritmos, teoría de grafos, computación cuántica, en un sentido bien amplio.

Aún no tengo muy clara la situación por aquí, pero tengo entendido que hay muchas oportunidades para estudiantes de universidades sudamericanas para hacer intercambios. Una de estas redes, a la cual pertenece la UNA, es la AUGM. Esta red permite el intercambio de profesores y estudiantes. Tenemos un muy buen programa de postgrado en Ciencias de la Computación en áreas como computación científica, optimización, inteligencia artificial, visión por computador y otros; y a partir de este año se incluye teoría de la computación. Si hay estudiantes interesados en visitarnos, pueden consultar en sus universidades si hay algún acuerdo de intercambio y vemos como hacer.

Charla sobre la medición cuántica proyectiva en lambda cálculo en Rosario

Como ya es (lamentablemente) costumbre, comienzo por disculparme por lo poco que estoy posteando en el blog.

El mes de mayo estuve en París, primero trabajando con Mariangiola Dezani, de la Universidad de Torino, y luego con Gilles Dowek, del INRIA París. Con Gilles comenzamos un trabajo nuevo, del cual voy a hablar este martes 16 de junio a las 12hs en la Universidad Nacional de Rosario (más específicamente en la Facultad de Ciencias Exactas, Ingeniería y Agrimensura).

Les dejo el título y resúmen de la charla:

Sobre la medición cuántica proyectiva en lambda cálculo

Si se considera la superposición cuántica como una conjunción no-idempotente, la medición proyectiva corresponde a una proyección no-determinística sobre los pares. En este trabajo proponemos una extensión al lambda cálculo con pares simplemente tipado que tiene en cuenta mediciones , superposición equiprobable con interferencia destructiva y la propiedad cuántica del no-clonado. En esta charla daré una descripción del sistema y sus decisiones de diseño, así como un ejemplo del algoritmo de Deutsch en este cálculo.

 Update: Les dejo el link al preprint de este trabajo en arXiv: arXiv:1601.04294

Video de mi charla en las Jornadas de Ciencias de la Computación

Los organizadores de las JCC acaban de subir el video de mi charla (acá abajo). También están los videos de las demás charlas, que pueden ver aquí.

Las Jornadas de Ciencias de la Computación es un evento que se hace año a año en Rosario, organizada por y para los estudiantes de la Licenciatura en Ciencias de la Computación.

Abstract de la charla: Proponemos un sistema de pruebas para lógica proposicional en el cual proposiciones isomorfas son consideradas como iguales (en el sentido de que sus respectivas pruebas son intercambiables).
Por ejemplo, A implica (B y C) es isomorfo a A implica B y A implica C. Si consideramos un sistema de pruebas módulo este tipo de isomorfismos, desde el punto de vista del cálculo (o del sistema de pruebas), una función que toma un argumento y devuelve un par, es equivalente (o "igual" si se quiere, para algún concepto de igualdad) a un par de funciones, cada una tomando el mismo argumento, y devolviendo sólo un elemento del par. Por lo tanto, también se podría, por ejemplo, proyectar un elemento de un par que será resultado de la aplicación de una función... antes de aplicar la función, proyectando sólo una parte de la misma. Esto puede trae aparejado una simplificación importante del cómputo.
En una lógica proposicional que sólo cuente con conjunción (no-idempotente) e implicación, existen sólo cuatro isomorfismos básicos, a partir de los cuales pueden derivarse los demás. Estos cuatro isomorfismos, al considerarlos igualdades, generan un cálculo interesante, no-determinista, relacionado con otros cálculos en la literatura.

El paper completo lo pueden bajar de acá. Aún no está publicado, está en proceso de publicación en la revista Theoretical Computer Science.

Material de mi curso en la Escuela de Verano de Río Cuarto

Terminó la Escuela de Verano de Ciencias Informáticas de Río Cuarto. Esta es una escuela que se hace cada año, destinada principalmente a estudiantes de grado de todo el país. Allí dí un curso sobre fundamentos de lenguajes de programación para computación cuántica (2 días de introducción a computación cuántica, 1 de introducción a lambda-cálculo y 1 sobre lenguajes en el paradigma "control clásico / datos cuánticos" y 1 en el paradigma "control y datos cuánticos").

Pueden bajar los apuntes y las transparencias en la página de la escuela.

Por supuesto es un curso introductorio, si quieren profundizar, allí mismo tienen bibliografía que les servirá para ir más a fondo.

---

Update: Al parecer la página de la RIO está caída, así que dejo el material acá:

curso-rio-2015.tar.gz

(es un paquete comprimido que incluye los apuntes de los 2 primeros días, los slides de los 5 días, una página con ejercicios introductorios de lambda cálculo y el examen).

Temas de tesis de licenciatura y doctorado

Buenas,

Como muchos de los lectores habituales del blog sabrán, estoy de vuelta en Argentina. Soy Profesor Adjunto en la Universidad Nacional de Quilmes (en Bernal, a unos 20kms de Buenos Aires). Y ahora que estoy instalado, estoy buscando estudiantes para dirigir tesis de Licenciatura y de Doctorado. Acá les detallo algunos trabajos que se me ocurren (un pequeño resúmen, para discutir, ampliar y debatir). Por supuesto siempre se pueden modificar, incluso pueden surgir trabajos que vengan del tesista, no hace falta que sea uno de la lista. Pero tiro un par de propuestas para ejemplificar mis intereses.

Doy dos para licenciatura (LIC) y uno para tesis de doctorado (DOC). La idea es que un trabajo de licenciatura debe poder realizarse en unos 6 meses, por lo tanto son cosas que tengo certeza de que se pueden hacer (lo cual no significa que hacerlo sea sencillo, pero sí que vamos a arribar a buen puerto y tendremos algo para publicar), mientras que la propuesta para tesis de doctorado es para desarrollar en 5 años, por lo cual sólo doy una idea de la dirección a seguir, con lo cual arrancar, y que puede ir tomando nuevos rumbos de acuerdo a lo que vayamos descubriendo.

Si les interesa algún tema de los detallados abajo, o algún otro que se les ocurra a ustedes, los datos de contacto están en mi página personal. Escríbanme o llamenmé y me envían un CV y me dicen qué tema les interesa, cuándo podrían arrancar y comenzamos a ver la parte administrativa formal de sus respectivas universidades.

Aclaro que el candidato ideal no es quien sepa todos los temas de los que habla la descripción de la propuesta de tesis, sino quien más demuestre interés y ganas de trabajar. Los temas se aprenden (para eso es la tesis).

---

(LIC) Confluencia en reescritura probabilista
Descripción:
Los sistemas de reescritura abstractos probabilistas (PARS por sus siglas en inglés) asocian a cada objeto diversos objetos y una probabilidad para cada uno. Así, un objeto A puede reescribir a B con probabilidad 1/4 y a C con probabilidad 3/4. La propiedad de confluencia dice que si A reescribe en uno o más pasos a A1 y también, siguiendo otro camino, a A2, entonces A1 y A2 reescriben a un nuevo objeto A'. Por lo tanto, un PARS no es necesariamente confluente (si A reescribe a B y C con ciertas probabilidades, B y C pueden ser objetos diferentes sin un reducto en común).

Este proyecto se trata de estudiar los PARS conocidos y proponer un resultado de confluencia para el ARS asociado al PARS, en el cual en lugar de reescribir A a B con probabilidad 1/4 y a C con probabilidad 3/4, reescribe {(A,1)} a {(B,1/4), (C, 3/4)} determinísticamente.

Un resultado preliminar en este sentido fue publicado en el workshop internacional Quantum Phisics and Logic [1]. La idea de esta tesina es completar dicho trabajo, para el caso genérico de los PARS. El plan es poder obtener un resultado publicable en alguna una revista internacional.

[1] Measurements and confluence in quantum lambda calculi with explicit qubits. Pablo Arrighi, Alejandro Díaz-Caro, Manuel Gadella y Jonathan J. Grattage. ENTCS 270(1):59-74, 2011

---

(LIC) Operador de punto fijo para el lambda cálculo vectorial
Descripción:
El lambda cálculo vectorial [2] es una extensión a lambda cálculo donde combinaciones lineales de términos, son también términos. Dicho cálculo fue pensado para computación cuántica: así un valor no es sólo una variable o una abstracción, sino también las combinaciones lineales de ellos, es decir: vectores dentro de un espacio vectorial de dimensión infinita. Limitando los valores posibles (los elementos de la base), se puede codificar espacios vectoriales de dimensión finita (como el espacio de n-qubits, por ejemplo).

El sistema de tipos del lambda cálculo vectorial es polimórfico, y tiene la propiedad de normalización fuerte, es decir: todo término tipado termina. Ello evita que aparezcan sumas infinitas (y por lo tanto, formas indeterminadas como infinito menos infinito). En este proyecto se busca agregarle un operador de punto fijo al cálculo vectorial, de manera de recuperar la recursión, pero teniendo en cuenta no introducir sumas infinitas (o al menos formas indeterminadas que incluyan infinito).

[2] The vectorial lambda-calculus. Pablo Arrighi, Alejandro Díaz-Caro y Benoît Valiron. arXiv:1308.1138, 2013

---

(DOC) Realisabilidad en computación cuántica con control y datos cuánticos
Descripción:
La realisabilidad es una rama de la teoría de la demostración que define una relación lógica entre las fórmulas de un sistema y los programas de un modelo de cálculo. Fue introducida por Kleene en los años 40 y luego extendida, hasta llegar a convertirse en una generalización de la correspondencia de Curry-Howard.

El proyecto se trata de usar realisabilidad para determinar una lógica cuántica, en el sentido de que las pruebas de las fórmulas lógicas, sean programas cuánticos.