4 de diciembre de 2017

Slides y Poster en APLAS

Los slides de mi presentación en APLAS los pueden ver aquí: SlideShare.
Presenté el paper "A lambda calculus for density matrices with classical and probabilistic controls", del cual les comenté en este post. El paper ya fue publicado en Lecture Notes in Computer Science (y pueden bajar una versión gratuita, corregida y con todas las pruebas, desde arXiv).

Además, aproveché y llevé un poster del paper, en colaboración con Gilles Dowek, que voy a presentar en TPNC dentro de dos semanas y comenté en este post: "Typing quantum superpositions and measurement". Acá les dejo el poster, y el paper por ahora sólo lo pueden bajar de arXiv (actualizaré el post cuando aparezca en Lecture Notes in Computer Science, lo que debería ser muy pronto, y luego de la conferencia con los slides que use para presentarlo).

Les dejo una pequeña postal de Suzhou, China, donde de llevó a cabo APLAS.

7 de noviembre de 2017

Visita de Marcos Villagra a Buenos Aires

Mañana, luego de casi 8 años, finamente nos vamos a conocer personalmente dos de los autores de este blog: Marcos Villagra, de la Universidad Nacional de Asunción (Paraguay) me visita en la Universidad Nacional de Quilmes (Argentina).

Marcos comenzó a colaborar en el blog en 2009, cuando era estudiante de doctorado en Japón y yo estudiante de doctorado en Francia. Luego de estos años compartiendo el blog, y con ambos haciendo ciencia desde nuestros países de origen, se nos da esta oportunidad de juntarnos a buscar cómo colaborar científicamente y no sólo con la divulgación desde este blog.

Después les contaremos qué sale del encuentro.

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.

23 de junio de 2017

2a Jornada de Lógica, Computación e Información Cuántica

2a Jornada de Lógica, Computación e Información Cuántica 
Jueves 13 de julio de 2017 
Universidad Nacional Arturo Jauretche
Av. Calchaquí 6200, Florencio Varela
-- Salón Auditorio --

El 13 de julio se realizará la 2a jornada de lógica, computación e información cuántica. El objetivo de las jornadas es proveer un espacio de encuentro para quienes trabajamos en fundamentos lógicos de la computación cuántica desde una perspectiva interdisciplinaria. Contaremos con charlas del Dr. Guido Bellomo (postdoctorando en el Dpto. Computación de Ciencias Exactas-UBA), el Dr. Simon Perdrix (investigador CNRS en el laboratorio LORIA de Nancy, Francia) y el Dr. Christian de Ronde (Investigador CONICET, Profesor UNAJ y FFyL-UBA). El encuentro se realizará en la Sede de la Universidad Nacional Arturo Jauretche desde las 10:30 hasta las 16:30 horas. 

Esta convocatoria que surge de jóvenes investigadores del área busca ser amplia e inclusiva. Están todos invitados a sumarse al encuentro. Se agradece la difusión.

==============================================================

Programa:

10:30 Café 
11:00 Christian de RondeOn the physical foundation of quantum superpositions (beyond measurement outcomes and mathematical structures)
12:00 Almuerzo 
14:00 Simon PerdrixDiagrammatic Quantum Reasoning: Completeness and Incompleteness
15:00 Café 
15:30 Guido BellomoQuantum entropies and lossless quantum data compression

==============================================================

Resúmenes:

Christian de Ronde (Universidad Nacional Arturo Jauretche & CONICET) - On the physical foundation of quantum superpositions (beyond measurement outcomes and mathematical structures).
Quantum superpositions are being used today in laboratories all around the world in order to create the most outstanding technological and experimental developments of the last centuries. However, while many experimentalists are showing that Schrödinger's cats are growing fat, while it becomes more and more clear that quantum superpositions are telling us something about quantum physical reality even at the macroscopic scale, philosophers of QM in charge of analyzing and interpreting these mathematical expressions (through the many interpretations of QM that can be found in the literature) have not been capable of providing a coherent physical representation of them. In this paper we attempt to discuss the importance of providing a physical representation of quantum superpositions that goes beyond the mere reference to mathematical structures and measurement outcomes.

Simon Perdrix (CNRS / LORIA, Francia) - Diagrammatic Quantum Reasoning: Completeness and Incompleteness.
The ZX-calculus introduced by Coecke and Duncan is a graphical formal language for quantum reasoning based on the complementarity of observables. I'll introduce this category-based diagrammatic calculus, give some examples, and focus on the question of completeness of the language for quantum mechanics. The language is complete if for any two diagrams representing the same quantum evolution, one can be transformed into the other using the rules of the ZX-calculus. The language was known  to be complete for non universal fragments of quantum mechanics, and incomplete in general. I will present the first complete axiomatisation of the ZX-calculus for a universal fragment of quantum mechanics.

Guido Bellomo (Universidad de Buenos Aires) - Quantum entropies and lossless quantum data compression.
One of the main concerns in classical and quantum information theories is the problem of encoding information by using fewest resources as possible. This task is known as data compression and it can be carried out either in a lossy or a lossless way, depending on whether the original data can be recovered with or without errors, respectively. Based on the problem of quantum data compression in a lossless way, we present here an operational interpretation for the family of quantum Rényi entropies. In order to do this, we appeal to a very general quantum encoding scheme that satisfies a quantum version of the Kraft-McMillan inequality. Then, in the standard situation, where one is intended to minimize the usual average length of the quantum codewords, we recover the known results, namely that the von Neumann entropy of the source bounds the average length of the optimal codes. Otherwise, we show that by invoking an exponential average length, related to an exponential penalization over large codewords, the quantum Rényi entropies arise as the natural quantities relating the optimal encoding schemes with the source description, playing an analogous role to that of von Neumann entropy.

28 de marzo de 2017

Próximos seminarios: París y La Plata

Del 3 al 12 de abril estaré en París, visitando el grupo de Gilles Dowek. El jueves 6 a las 14hs daré el siguiente seminario en el grupo Deducteam (Librería del laboratorio LSV, Cachan):

A lambda calculus for density matrices
Density matrices describe quantum systems in mixed state, that is, a statistical set of several quantum states. All the postulates of quantum mechanics can be described in such a formalism, and hence, also quantum computing can be done using density matrices. One advantage of this formalism is that it gives a natural way to reason about the probabilistic outputs of an algorithm.  In this talk we present an extension to lambda calculus for density matrices with a linear type system. Its denotational semantics is the set of density matrices and functions upon them, and so, it is possible to equate programs producing the same density matrices. For example the process of tossing a coin, and according to its result, apply Z or not to a balanced superposition, and the process of tossing a coin and not looking at its result, may look quite different in most quantum programming languages. Yet both processes output the same density matrices thus have the same denotation in our calculus.
A la vuelta, el martes 25 de abril a las 10:30hs, daré el siguiente seminario en el departamento de Física de la Universidad Nacional de La Plata (esquina de calles 115 y 49):

Cálculo lambda y computación cuántica
En esta charla vamos a dar una rápida introducción al cálculo lambda, un modelo de computación equivalente a las Máquinas de Turing, y su relación con la lógica intuicionista. Luego presentaremos diferentes extensiones al cálculo lambda para computación cuántica, en sus dos paradigmas: el paradigma de control clásico y datos cuánticos, orientado principalmente a estudiar propiedades en los lenguajes de programación para la computadora cuántica, y el paradigma de control y datos cuánticos, orientado a estudiar las consecuencias lógicas de la computación cuántica desde un punto de vista computacional.

3 de marzo de 2017

Jornada de lógica, computación e información cuántica @ UNQ

Jornada de lógica, computación e información cuántica
23 de marzo de 2017
Universidad Nacional de Quilmes
Roque Sáenz Peña 352, Bernal
-- Aula CyT-2 --

El 23 de marzo se realizará una jornada de lógica, computación e información cuántica. El objetivo es juntar a quienes trabajamos en temas afines a la computación cuántica desde las ciencias de la computación en la región. Contaremos con charlas de Gabriel Senno (Universidad de Buenos Aires), Octavio Malherbe (Universidad de la República) y Federico Holik (Universidad Nacional de La Plata), y se realizará en la Universidad Nacional de Quilmes de 10:30 a 16:30 horas.

Esta convocatoria nace de jóvenes investigadores del área, y queremos que sea lo más amplia posible. Se agradece la difusión. Por motivos de organización, se ruega confirmar participación escribiendo a alejandro.diaz-caro@unq.edu.ar.

==============================================================

Programa:

10:30 Café
11:00 Gabriel Senno: Yendo desde una ventaja cuántica en complejidad comunicacional a una gran violación de Bell resistente al loophole de la detección
12:00 Almuerzo
14:00 Octavio Malherbe: Modelos de la computación cuántica y realizabilidad
15:00 Café
15:30 Federico Holik: Probabilidades cuánticas y modelos probabilísticos generalizados

==============================================================

Resúmenes:

Gabriel Senno (Universidad de Buenos Aires) - Yendo desde una ventaja cuántica en complejidad comunicacional a una gran violación de Bell resistente al loophole de la detección
La teoría de la complejidad comunicacional estudia la cantidad de comunicación que tiene que haber entre dos jugadores Alice y Bob para que puedan computar de manera distribuida una función bipartita dada. Se conocen numerosas funciones para las cuales hay una ventaja cuántica, es decir: la cantidad de comunicación cuántica (medida en qbits) es menor que la clásica (medida en bits); para algunas funciones, la ventaja es incluso exponencial. Dada su evidente similitud con el escenario de no-localidad, una de las preguntas abiertas en el área es: ̣¿qué relación hay entre ventaja cuántica en complejidad comunicacional y violación de desigualdades de Bell? Voy a mostrar como, para una gran familia de funciones para las cuales hay ventaja cuántica, se pueden construir desigualdades de Bell y distribuciones cuánticas que las violan en una magnitud exponencial en la ventaja. Estas violaciones son, además, resistentes al loophole de la detección.

Octavio Malherbe (Universidad de la República) - Modelos de la computación cuántica y realizabilidad
En esta charla hablaremos sobre los modelos categóricos de la computación cuántica para el cálculo lambda cuántico de Valiron-Selinger. Intentaremos luego movernos al contexto de la realizabilidad para hablar sobre algunas líneas de investigación que venimos desarrollando con el equipo de lógica de Montevideo en el marco del proyecto realizabilidad y computación cuántica.

Federico Holik (Universidad Nacional de La Plata) - Probabilidades cuánticas y modelos probabilísticos generalizados
En esta charla discutimos las probabilidades cuánticas desde el punto de vista de una generalización no conmutativa de la teoría de la medida. Nos enfocamos en distintos aspectos geométricos, tales como la invariancia ante la acción de grupos. Describimos cómo extender este abordaje a otras teorías probabilisticas, y estudiamos la relación con la teoría de la información cuántica.

14 de febrero de 2017

Curso en la Escuela de Ciencias Informáticas 2017

Del 24 al 29 de Julio de 2017 voy a dictar un curso de Fundamentos de Lenguajes para Computación Cuántica en la 31a ECI, la Escuela de Ciencias Informáticas del Departamento de Computación de la Facultad de Ciencias Exactas y Naturales de la Universidad de Buenos Aires.

El curso tendrá 15 horas (5 clases de 3hs cada una), y tratará los mismos temas del curso semestral que dicté en la Universidad Nacional de Rosario, (aunque forzosamente con menos profundidad debido a la menor cantidad de horas). El material del curso que dicté en la UNR lo pueden ver aquí.

Para más información de la ECI no dejen de visitar la página oficial:

https://www.dc.uba.ar/events/eci/2017