13 de septiembre de 2017

En Praga unificando paradigmas para tratar el no clonado en lenguajes cuánticos

En este post les quiero contar de un nuevo paper que acaba de ser aceptado en el 6th International Conference on Theory and Practice of Natural Computing (TPNC 2017) que tendrá lugar en Praga (República Checa) del 18 al 20 de diciembre. Este paper lo co-autoreamos con Gilles Dowek, del Inria y la ENS Paris-Saclay (Francia). El preprint (con un extenso apéndice) lo pueden descargar desde arXiv:1601.04294, y el paper pronto va a estar disponible en LNCS. Aquí les dejo el título y resumen, y luego una explicación más amena.

Typing quantum superpositions and measurement

Alejandro Díaz-Caro & Gilles Dowek
(aceptado en TPNC, Praga, República Checa, 18-20 de diciembre de 2017)
We propose a way to unify two approaches of non-cloning in quantum lambda-calculi. The first approach is to forbid duplicating variables, while the second is to consider all lambda-terms as algebraic-linear functions. We illustrate this idea by defining a quantum extension of first-order simply-typed lambda-calculus, where the type is linear on superposition, while allows cloning base vectors. In addition, we provide an interpretation of the calculus where superposed types are interpreted as vector spaces and non-superposed types as their basis.
Explicación más amena: Hay dos maneras en la literatura de evitar el clonado de qubits (algo que prohíbe la física cuántica): Una manera es evitar que los programas utilicen sus argumentos más de una vez. De esa manera nos aseguramos de que ningún programa duplicará su argumento, y por lo tanto no podrá clonar. Para eso se utiliza lógica lineal. La otra manera es considerar que los programas distribuyen linealmente sobre las superposiciones, y así, aunque el programa clone su argumento, no clonará una superposición cuántica sino simplemente los estados de base (y eso sí es permitido). La segunda idea parece la más lógica, sin embargo, si el programa por ejemplo tienen que tomar un argumento y medirlo, esa solución no nos sirve, ya que no tomará la superposición cuántica para medirla, sino que entrará linealmente en la superposición y simplemente medirá los estados de base. La solución que proponemos acá es un híbrido de ambos: las funciones que deben tomar toda la superposición (por ejemplo para medirla), deben usar restricciones de lógica lineal (no duplicar su argumento), las otras funciones, simplemente usan álgebra lineal y distribuyen sobre el argumento.

31 de agosto de 2017

Confluencia probabilista en Brasil y cálculo de matrices densidad en China

En este post les quiero comentar dos papers muy recientes (no relacionados) que muy pronto estarán publicados, ya que ya fueron revisados y aceptados para su publicación.

El primero de ellos fue aceptado en el 12th Workshop on Logical and Semantics Frameworks with Applications (LSFA 2017) que tendrá lugar en Brasilia (Brasil) los días 23 y 24 de septiembre. Ese paper lo co-autoreamos con Guido Martínez, de la Universidad Nacional de Rosario. De hecho, este paper es el resumen de su tesis de licenciatura (en la que yo fui su director). Todo el mérito va para Guido, ya que yo sólo le propuse el tema, y él lo desarrolló con muy poca intervención de mi parte. El preprint lo pueden descargar de arXiv:1708.03536, y aquí replico el título y el resumen.

Confluence in Probabilistic Rewriting

Alejandro Díaz-Caro & Guido Martínez
(aceptado en LSFA, Brasilia, Brasil, 23-24 de Septiembre de 2017)
Driven by the interest of reasoning about probabilistic programming languages, we set out to study a notion of unicity of normal forms for them. To provide a tractable proof method for it, we define a property of distribution confluence which is shown to imply the desired unicity and further properties. We then carry over several criteria from the classical case, such as Newman’s lemma, to simplify proving confluence in concrete languages. Using these criteria, we obtain simple proofs of confluence for λ1, an affine probabilistic λ-calculus, and for Q*, a quantum programming language for which a related property has already been proven in the literature. Lastly, we show how distribution confluence implies unicity even for distributions that are only reached asymptotically.
Explicación más amena: Definimos el concepto de confluencia para sistemas de reescritura con reglas probabilistas. La confluencia en reescritura estándar dice que si un término puede reescribirse a dos términos diferentes, entonces ambos reescribirán luego al mismo término. Cuando existe reescritura probabilista (por ejemplo, porque es el sistema de reescritura de un lambda cálculo cuántico, que tiene una regla probabilista para la medición cuántica), lo que definimos es una generalización en donde nos importa la unicidad de la distribución de probabilidades.

El segundo de ellos fue aceptado en el 15th Asian Symposium on Programming Languages and Systems (APLAS 2017) que tendrá lugar en Suzhou, China del 27 al 29 de noviembre. El preprint lo pueden descargar de arXiv:1705.00097, y aquí replico el título y el resumen.

A lambda calculus for density matrices with classical and probabilistic controls

Alejandro Díaz-Caro
(aceptado en APLAS, Suzhou, China, 27-29 de Noviembre de 2017)
In this paper we present two flavors of a quantum extension to the lambda calculus. The first one, λρ, follows the approach of classical control/quantum data, where the quantum data is represented by density matrices. We provide an interpretation for programs as density matrices and functions upon them. The second one, λρ°, take advantage of the density matrices presentation in order to follow the mixed trace of programs in a kind of generalised density matrix. Such a control can be seen as a weaker form of the quantum control and data approach.
Explicación más amena: En los lenguajes para computación cuántica hay básicamente dos paradigmas: "control clásico y datos cuánticos" o "control y datos cuánticos". El primero considera que la computadora cuántica correrá en una especie de co-procesador cuántico, controlado por una computadora clásica (que le dice qué operaciones aplicar, a qué qubits, cuándo medir, etc) y toma los resultados de las mediciones para seguir el cálculo clásico. El segundo considera superposiciones de programas. La relación entre ambos paradigmas no está del todo clara. En este paper, usando matrices densidad (que es un formalismo que permite describir todos los postulados de la mecánica cuántica), introdujimos primero un cálculo con control clásico, y luego una pequeña modificación del mismo, consiguiendo un control que, si bien no es exactamente cuántico, tampoco es clásico: le llamamos control probabilista, o control cuántico débil.

26 de junio de 2017

Llamado a registro de aspirantes a beca doctoral CONICET 2017

Se llama a una preinscripción de postulantes a Beca Interna Doctoral del CONICET relacionada al proyecto PICT-PRH 2015-1208:


«Fundamentos de lenguajes de programación cuántica: hacia una lógica computacional»


en el área de los sistemas formales para computación cuántica (lambda-cálculo, pi-cálculo, teoría de tipos, realisabilidad, reescritura, etc.), bajo la dirección de Alejandro Díaz-Caro en la Universidad Nacional de Quilmes (Bernal, Buenos Aires, Argentina).

Laboratorios de pertenencia:
* LoReL
* Infinis

Principales interacciones (proyectos conjuntos) con: Université Paris-Sud. École Normal Supérieure de Paris-Saclay. Inria. LORIA. Aix-Marseille Université. Università degli Studi di Torino. Universidad de la República (Uruguay). Universidade Federal de Santa Maria (Brazil). Universidad de Buenos Aires.

Requisitos: ser menor de 30 años, graduado o próximo a recibirse (antes del 01/04/2018) con muy buen desempeño académico en Licenciatura en Ciencias de la Computación o carreras afines.