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.

Pruebas cuánticas para teoremas clásicos

Interesante preprint de Andrew Drucker (MIT) y Ronald de Wolf (CWI Amsterdam): "Pruebas cuánticas para teoremas clásicos" (Quantum Proofs for Classical Theorems, arXiv:0910.3376).

El paper es un interesante review autocontenido de distintos algoritmos cuánticos, pruebas y métodos y plantea el "framework" de la computación cuántica como un método más para probar teoremas clásicos... por lo tanto, más allá de si la computación cuántica se puede lograr físicamente en realidad o no (o peor aún, si la física cuántica es o no un modelo certero de la realidad), ésta igual sirve como una manera de pensar los problemas.

El paper en sí me pareció muy interesante y lo recomiendo, pero además lo recomiendo como un buen review sobre computación cuántica teórica en general.

A System F accounting for scalars

Hoy hemos enviado la versión extendida del paper del Scalar Type System a un journal internacional. El preprint se puede descargar del arXiv (arXiv:0903.3741).
Esta versión incluye:

• La prueba completa de subject reduction
• La prueba completa de strong normalisation
• La definición formal y prueba del probabilistic type system
• La prueba completa del teorema de no-cloning
  

Algunas novedades

Bueno, hace mucho que no escribo nada por acá, así que comentaré un poco en qué ando.

• El paper del Scalar Type System lo ampliamos bastante con todas las demostraciones y detalles y estamos a punto de enviarlo a la revista Theoretical Computer Science. Pronto subiré la versión extendida. Aquí está.
• Estuve trabajando en agregar subtyping al Vectorial Type System con Barbara Petit a quién visité hace unos meses y también haciendo muchos cambios a ese sistema de tipos.
• El 18 de Mayo fui a visitar al grupo LAMA en Chambéry, donde dí una charla acerca de este sistema de tipos.
• En agosto voy a Toronto, Canadá a una escuela de verano: Canadian Quantum Information Summer School, lo cual me genera muchas expectativas ya que espero poder ampliar un poco el panorama y tomar algún otro tema en paralelo con el que estoy desarrollando (para no quedarme estancado sólo con esto).

Bueno, esto es un resumen de los últimos meses, ya que he tenido bastante abandonado el blog. Dentro de poco estaré subiendo la versión extendida de Scalar al arXiv (ni bien la enviemos al journal) y pondré un link por aquí (arxiv:0903.3741), y a mi vuelta de Canadá, comentaré un poco de la escuela.

Vectorial, Lógica Lineal y Ortogonalidad

El miércoles y jueves pasados estuve en Lyon, invitado por Barbara Petit del grupo PLUME de la École Normale Supérieure de Lyon. Allí di un seminario sobre los sistemas de tipos que he desarrollado: Scalar, Additive y Vectorial, y algunos de los problemas sobre cómo chequear ortogonalidad entre términos y algunas pistas para resolverlo.

Olivier Laurent se dio cuenta de simplemente ver la presentación, la conexión entre Additive y Intuitionistic Multiplicative Exponential Linear Logic.

Pronto estaré publicando un nuevo paper sobre Additive (con esa conexión a la lógica lineal) y Vectorial. Además, hemos empezado a trabajar juntos con Barbara en el problema de la ortogonalidad, usando subtyping.

Próximos viajes:
Los días 4 y 5 de Mayo voy a París a visitar a Benoît Valiron y Gilles Dowek del proyecto TypiCal, en la École Polytechnique de París, donde daré otro seminario. Luego, el 18 de Mayo estaré en Chambery, donde iremos con mi director, Pablo Arrighi, a participar de una serie de seminarios organizados por Lionel Vaux del grupo LAMA.

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

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.

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

Foco en el Procesamiento de Información Cuántica basada en Medición

La primeras contribuciones a una publicación sobre "Measurement-Based Quantum Information Processing", editada por Jian-Wei Pan y Terry Rudolph, ha sido publicada en el New Journal of Physics (NJP).

Todos los artículos están disponibles para su descarga gratuita en http://herald.iop.org/njp/m52/nad/249739/link/846

QRBGS

El Instituto Ruđer Bošković de Croacia a lanzado un servicio online de generación de números aleatorios "reales" logrado por mecanismos cuánticos. El servicio se llama "Quantum Random Bit Generator Service" (QRBGS).

Los detalles técnicos se pueden ver en dos papers que han publicado[1][2] sobre el tema.

Ref.
[1] Radomir Stevanović, Goran Topić y Karolj Skala, Quantum Random Bit Generator Service for Monte Carlo and Other Stochastic Simulations, Lecture Notes in Computer Science, Springer, 2007 (Online aquí).
[2] Mario Stipčcević y Branka Medved Rogina, Quantum random number generator, arXiv:quant-ph/0609043.

Lenguajes de Programación Cuánticos

A todo aquel que le interesen los lenguajes de programación que se están desarrollando para la computación cuántica, les recomiendo el -bastante exhaustivo- review de Simon J. Gay: Quantum Programming Languages: Survey and Bibliography[1]
Además, en su página pueden encontrar un buscador de papers sobre el tema.

Ref:
[1] Mathematical Structures in Computer Science 16(4), 2006

Rankeando papers

Dave Bacon tuvo la genial idea de darle una vuelta de tuerca más al arXiv (por ahora sólo al quant-ph que es el que más nos interesa) al crear la página SciRate.com.

La idea es simple, todos los días se copiará (y enlazará) a la sección new del archivo quant-ph del arXiv desde SciRate, y los usuarios registrados podrán "puntuar" cada uno de los papers, así, se tendrá un orden de mejor puntuado a peor puntuado (por los propios lectores) para poner alguna especie de "filtro".

¿Porqué surge ésta iniciativa?: Diariamente hay más de 20 papers nuevos sólo en la sección de Cuántica en el arXiv, eso hace que haya más ruido que ciencia. La idea es lograr un pequeño filtro (al menos para lograr ordenar de "causó más impresión" a "causó menos impresión").

Además, Dave habilitó un blog para poner sugerencias y comentarios sobre ésta iniciativa.

Si quieren ver la explicación de Dave sobre cómo funciona y el porqué de este sitio, click aquí.

Lenguajes Cuánticos de "Alto nivel"

Recientemente, Nacho publicó un comentario en mi blog en el que me mostraba un lenguaje de Computación Cuántica de alto nivel. Después, Mauro (desde su "nueva" ubicación), me pasó el dato de alguien de allí (Nottingham) que está trabajando con lenguajes de Alto Nivel para computación cuántica: Thorsten Altenkirch.

En su página pueden encontrarse varios artículos sobre sus trabajos. La verdad que me ha parecido un tema más que interesante, sobre todo por lo que planteé hace unos meses en el post Niveles de abstracción, pensando ingenuamente que aún no se estaba trabajando en ello. ¡¡Y hasta me encontré con un congreso sobre Lenguajes de Computación Cuánticos!!!

Debo decirlo: esto avanza muy rápido...

Circuito para distinguir estados de Bell desconocidos.

Recorriendo la Base de Datos de Los Alamos me he topado con un paper[1] más que interesante. Se trata de un circuito que logra distinguir entre los 4 estados de Bell, sin medirlos y sin destruirlos. El circuito planteado es el que muestro a continuación:

Es un circuito ingenioso que logra dejar en los dos qubits ancillares los valores de los qubits que generan el susodicho estado de Bell.
Me pareció un circuito muy "atractivo" hasta que noté que el mismo resultado puede conseguirse sin mucho esfuerzo "desentangleando" el estado de Bell y volviendo a entanglearlo, de esta manera:

por lo que el circuito anterior pierde todo sentido. En otro paper[2] hablan de cómo utilizar este algoritmo para clonar estados de Bell y el autor termina comparando su método con la Universal Cloning Machine[3] (UCM) diciendo que el suyo es extremadamente mejor ya que puede clonar con fidelidad 1, mientras que la UCM sólo lo hace con una fidelidad de 5/6. En realidad la cuestión es que la UCM clona cualquier estado desconocido, en comparación con éste algoritmo que copia sólo estados de Bell, los cuales pueden ser copiados por más de un método, ya que el Teorema de No-Clonning lo que dice es que no se pueden clonar estados no-ortogonales, y los estados de Bell son ortogonales entre si.

Referencias

[1] M. Gupta, P. K. Panigrahi, "Deterministic Bell State Discrimination", arXiv:quant-ph/0504183 (2005).
[2] J. O. Grabbe, "Deterministic cloning of an unknown Bell state", arXiv:quant-ph/0507016 (2005).
[3] D. Bruss, D. P. DiVincenzo, A. Ekert, C. A. Fuchs, C. Macchiavello, J. A. Smolin, "Optimal Universal and State-Dependent Quantum Cloning", Phys. Rev. A 57 2368 (e-print arXiv:quant-ph/9705038) (1998)

Algoritmo de Shor y Algoritmo de "de Vries"

En un nuevo paper de Andreas de Vries[1], parece ser que el algoritmo que plantea es capaz de realizar una búsqueda en una base de datos desordenada en un órden O(log n). Esto implica que NP está dentro de BQP, o sea: los problemas NP completos son resolubles en tiempo polinomial en una computadora cuántica.

Si esto es correcto, este nuevo algoritmo hace obsoleto el algoritmo de Grover y es, junto al algoritmo de Shor, uno de los más importantes algoritmos cuánticos.

Aún debo leerlo más "sesudamente", luego comentaré mis impresiones.

Update: Estaba leyendo el paper y encontré hasta ahora un error en la ecuación (9) donde dice que C²=C-I, esto no es cierto, pero igualmente, antes de terminar de leerlo encontré este post en el Weblog de Dave Bacon que ya lo estudió a fondo y encontró otros errores más. El paper fue enviado a la Physical Review D, así que será cuestión de tiempo de esperar a que lo refereen y de Vries corrija los errores, asimismo creo que la afirmación de que NP C BQP no se podrá demostrar a partir de este algoritmo.

Update++: En palabras del mismo Andreas, el problema más severo en su paper está en el Ejemplo 5, en el cual dice que su algoritmo es más rápido que el de Grover, y esto no es cierto, ya que para el caso especial de N=4 (el que él analiza) el algoritmo de Grover requiere una sóla consulta al oráculo, no 2 como dice él, y en ese caso su algoritmo se comporta exactamente igual, por lo tanto el algoritmo de Grover sigue siendo "óptimo".

[1] A. de Vries, Fast quantum search algorithms by qubit comparisons exploiting global phase interference, arXiv:quant-ph/0506137.

Mi primer Paper

Aún no está publicado, pero ya lo he enviado a la International Journal of Quantum Information (IJQI), se puede ver el preprint desde la base de datos de Los Alamos[1].

En este paper, titulado "On the Teleportation of N-qubit States", lo que hago es una generalización del algoritmo cuántico de teleportación creado por Brassard[2] (basado en la teleportación descripta por Bennett et al.[3]) y además hago una generalización de los dos protocolos de teleportación que planteó Kak[4] (los cuales con tan sólo n bits de información clásica completan la teleportación, en contraste de los 2n bits necesitados en el protocolo de Bennett).
El único problema con los protocolos de Kak es que se necesita preparar el estado que se llevará "Bob" junto con el estado que se va a teleportar (por lo tanto no tiene mucho sentido, ya que en ese caso, sería más lógico que Bob se llevase directamente el estado que quiere obtener), igualmente a nivel teórico los protocolos de Kak, son interesantes.

Referencias
[1] A. Díaz-Caro, arXiv:quant-ph/0505009 (2005)
[2] G. Brassard, Physica D 120, 43 (1998)
[3] C. Bennett, G. Brassard, C. Crepeau, R. Jozsa, A. Peres y W. Wootters, Phys. Rev. Lett. 70, 1895 (1993).
[4] S. Kak, arXiv:quant-ph/0305085 (2003)