Dick y Ken entrevistan a Kurt Gödel

Muy buen entrada en el blog Gödel's Lost Letter and P=NP. Vale la pena leerlo.

QIP 2012

Los papers de QIP 2012 y el programa ya están listos! Pueden ver en este link. Siempre QIP tiene papers de muy alta calidad. Por algo es la mejor conferencia en nuestra área. Quiero destacar algunos papers:

1. Merkle Puzzles in a Quantum World. Gilles Brassard, Peter Hoyer, Kassem Kalach, Marc Kaplan, Sophie Laplante, Louis Salvail.
   
   Está como featured talk, y es un paper escrito por mi gran amigo Kassem. Un excelente trabajo con una gran aplicación en un problem natural del método del adversario negativo. Este trabajo también lo presentaron en CRYPTO'11.
   
2. Local quantum circuits are appoximate polynomial-designs. Fernando Brandao, Aram Harrow, Michal Horodecki.
   
   Fernando es de Brasil, y es profesor asistente en la Universidad de Minas Gerais. Aún no tuve el placer de conocerlo, espero poder hacerlo y charlar un poco sobre el interés que hay en Brasil y latino-américa en computación cuántica.
   
3. Improved Output-Sensitive Quantum Algorithms for Boolean Matrix Multiplication. Francois Le Gall.
   
   Francois es un colega de la Universidad de Tokyo. Su paper es fabuloso, mejorando el paper de Harry Buhrman y Robert Spalek basado en quantum walks. Francois utiliza una reducción a triangle finding, que al mismo tiempo está basado nuevamente en quantum walks. Este paper también lo va a estar presentando en SODA'12 que será en Kyoto.

Quantum Information and Foundations StackExchange Proposal

[Este post es en inglés, ya que se trata de crear un sitio en inglés]

I just copy and paste an email from the quantum-foundations mailing list.

Dear fellow researchers:

We hope you can all join us in building a new web-based research community for quantum computing, information and foundations on StackExchange, and possibly earn some social media reputation points while they're at it (good for bragging rights, at least).

StackExchange is a collection of web sites where users can ask questions of a technical nature and receive high-quality answers from their communities. We hope to use StackExchange to coordinate expertise and facilitate research in the quantum information and quantum foundations communities, and so we have created a proposal for a new site dedicated to doing just that. StackExchange has already been found to be highly useful in pure mathematics [1], theoretical computer science [2], and applied [3] and theoretical physics [4], but our proposal addresses that quantum information and foundations lie frustratingly between these fields, and thus each of these existing sites excludes many excellent contributors.

If you're new to the idea of a StackExchange site, here's some examples of StackExchange sites being used in practice to help make it more clear what we're trying to build up: 

      - http://mathoverflow.net/questions/77985 
      - http://cstheory.stackexchange.com/questions/6085/shors-factoring-algorithm-help
(Peter Shor himself answered this one!) 
      - http://cstheory.stackexchange.com/questions/990/can-we-quantify-the-degree-of-quantumness-in-a-quantum-algorithm 
      - http://physics.stackexchange.com/questions/3777/informational-capacity-of-qubits-and-photons 
(Shor answered this one, too.) 
      - http://physics.stackexchange.com/questions/15482/how-do-i-calculate-the-position-on-the-bloch-sphere-of-a-quantum-gate-with-a-giv 
(even fairly basic questions are OK) 
      - http://physics.stackexchange.com/questions/11702/how-could-a-particle-be-isolated-to-avoid-decoherence 
(Yep, Shor.) 
      - http://theoreticalphysics.stackexchange.com/questions/370/rigorous-security-proof-for-wiesners-quantum-money 
(Asked by Scott Aaronson and answered by Daniel Gottesman.) 
      - http://theoreticalphysics.stackexchange.com/questions/93/models-of-neutrinos-consistent-with-operas-results

If you are interested in helping make this proposal happen, you can help by submitting example questions to the proposal site [5], and later joining in the private beta once it goes live. Remember, the more people that join in, the more useful the site will become! Currently, we need 15 new users for the proposal to go live, so your help is definitely appreciated. Thanks for reading! We hope to see you on StackExchange soon!

Sincerely,

Chris Ferrie
Chris Granade

Links:
  [1] http://mathoverflow.net/ (Not actually an SE site, but very similar!)
  [2] http://cstheory.stackexchange.com/
  [3] http://physics.stackexchange.com/
  [4] http://theoreticalphysics.stackexchange.com/
  [5] http://area51.stackexchange.com/proposals/36039/quantum-information-and-foundations

Otro pionero de la computación nos deja

Primero Steve Jobs, depués Dennis Ritchie, y ahora John McCarthy. El fue uno de los iniciadores de la inteligencia artificial. De hecho, él fue la persona quien acuñó ese término. Además fue el creador del primer lenguaje funcional LISP. También fué ganador del premio Turing 1971.

Recuerdo que una vez cuando estaba comenzando en la universidad, le había enviado un email a John McCarthy con algunas preguntas. Ya ni recuerdo sobre que le escribí, pero no recibí ninguna respuesta.

Poster: Foro Digiteo

En octubre comencé un postdoc financiado por el consorcio Digiteo. 
Hoy se realizó el Foro Anual de Digiteo, donde se muestran los proyectos en los cuales han invertido. Por lo tanto, tuve que presentar un poster allí explicando mi proyecto. Aquí les dejo el poster en PDF para descargar.

Mayoritariamente, los proyectos financiados por Digiteo son de aplicación inmediata (mucho de robótica, visión, ciudades inteligentes, etc), pero todos los años financian algún que otro proyecto teórico, como el mío. Grata fue la sorpresa de encontrarme con un trabajo de "Practical" Quantum Coin Flipping!

Video de la defensa de mi tesis

Como mencioné en un post anterior, el viernes 23/09/11 defendí mi tesis. La universidad puso el video de la defensa (sólo la parte de presentación, sin las preguntas del jurado). Así que aquí les dejo el video y otra vez los slides y el manuscrito:

Du typage vectoriel

Slides - Manuscript - Video

Terminando una etapa

El viernes pasado defendí mi tesis titulada "Du typage vectoriel" (sobre el tipage vectorial). El abstract ya lo puse en otro post. Aquí les dejo los slides que usé para defender la tesis y la tesis en sí.

Hoy fui a la oficina a sacar todas mis cosas, ya que en este momento estoy en plena mudanza a París, porque el martes que viene empiezo un contrato de investigación de un año en la Université de Paris-Nord, de lo cual cuento más en este post.

Y bueno, como toda etapa que termina, viene la nostalgia... y quería recordar en este blog cuando vine a Grenoble por primera vez, cuando me dieron la beca, y cuando comencé esta aventura... simplemente: Gracias a tantos lectores que mantienen vivo este blog! Espero poder seguir comentando sobre mis investigaciones en lambda cálculo, teoría de tipos y un poquito de cuántica... y para los amantes de la cuántica por suerte tenemos ahora un verdadero "cuántico" que espero los mantendrá actualizando :)

Hasta la próxima!

Update: El video de la defensa está disponible aquí.

Alán Aspuru-Guzik en "La oveja eléctrica"

Les dejo un programa mexicano de divulgación científica llamado "La oveja eléctrica", con un reportaje a Alán Aspuru-Guzik,

Soutenance / Defence / Defensa + QuAND

(English) (Español)


J'ai le plaisir de annoncer ma soutenance de thèse, accompagné d'un rencontre QuAND, qui aura lieu le 23 septembre à Grenoble. Voici le programme, les infos pratiques et les détails de la thèse.

PROGRAMME :

10h - 11h :
  Réunion stratégique du projet QuAND (privé)
11h15 - 12h :
  Exposé de Michele Pagani « Working for a theory of algebraic abstract reduction systems »
12h - 14h :
  Pause repas
14h30 - 16h :
  Soutenance de thèse d'Alejandro Díaz-Caro : « Du typage vectoriel »
16h :
  Pot de thèse

INFOS PRATIQUES :

Voilà un petit carte http://g.co/maps/rc8dc et quelques renseignements :
Depuis la gare vous pouvez prendre le Tram B direction « Plaine des sports » et descendre à l'arrêt « Bibliothèques universitaires ».
Le rencontre QuAND aura lieu à la Salle Aquarium, et la soutenance dans l'Amphi du MJK ( Maison Jean Kuntzmann ) même que le pot de thèse.


DÉTAILS DE LA THÈSE :

Titre :

Du typage vectoriel
Par :

Alejandro DÍAZ-CARO
Directeur :

Pablo ARRIGHI
Co-directeur :

Frédéric PROST

Cette soutenance aura lieu Vendredi 23 Septembre 2011 à 14h30 devant le jury composé de :

Rapporteurs :
Gilles DOWEK
Directeur de recherche - INRIA Centre Paris-Rocquencourt 
Thomas EHRHARD
Directeur de recherche CNRS - Laboratoire Preuves, Programmes et Systèmes 
Eduardo BONELLI
Profesor Asociado et Investigador Adjunto - Universidad Nacional de Quilmes et CONICET

Examinateurs :
Philippe JORRAND
Directeur de Recherche Émérite - CNRS
Laurent REGNIER
Professeur - Université de la Méditerranée
Lionel VAUX
Maitre de Conférences - Université de la Méditerranée
Michele PAGANI
Maitre de Conférences - Université de Paris Nord

Directeur de thèse :
Pablo ARRIGHI
Maitre de Conférences - Université de Grenoble

Résumé de la thèse : 
L'objectif de cette thèse est de développer une théorie de types pour le λ-calcul linéaire-algébrique, une extension du λ-calcul motivé par l'informatique quantique. Cette extension algébrique comprend tous les termes du λ-calcul plus leurs combinaisons linéaires, donc si t et r sont des termes, α.t+β.r est aussi un terme, avec α et β des scalaires pris dans un anneau. L'idée principale et le défi de cette thèse était d'introduire un système de types où les types, de la même façon que les termes, constituent un espace vectoriel, permettant la mise en évidence de la structure de la forme normale d'un terme. Cette thèse présente le système Lineal , ainsi que trois systèmes intermédiaires, également intéressants en eux-même : Scalar, Additive et λCA, chacun avec leurs preuves de préservation de type et de normalisation forte.

---

I am happy to announce that my thesis defence, accompanied of a QuAND meeting, will be held on September 23 at Grenoble. Here you are the programme, the venue and the thesis details.

PROGRAMME:
10h - 11h:
  Business meeting of the QuAND project (private)
11h15 - 12h:
  Seminar by Michele Pagani "Working for a theory of algebraic abstract reduction systems"
12h - 14h:
  Lunch
14h30 - 16h:
  Alejandro Díaz-Caro's thesis defence: "On vectorial typing"
16h:
  Drinks

VENUE:


Here is a map http://g.co/maps/rc8dc and some details:
From the train station, you can take the Tram B in direction "Plaine des sports", and take off at the stop "Bibliothèques universitaires".
The QuAND meeting will be held at the Aquarium room, and the defence at the lecture hall of the MJK building (Maison Jean Kuntzmann), same as the drinks afterwards.


DETAILS OF THE THESIS:

Title :

On vectorial typing
By:

Alejandro DÍAZ-CARO
Adviser:

Pablo ARRIGHI
Co-adviser:

Frédéric PROST

The defence will take place on Friday, September 23, 2011 at 2:30 pm in front of the following jury:

Rapporteurs:
Gilles DOWEK
Directeur de recherche - INRIA Centre Paris-Rocquencourt 
Thomas EHRHARD
Directeur de recherche CNRS - Laboratoire Preuves, Programmes et Systèmes 
Eduardo BONELLI
Profesor Asociado and Investigador Adjunto - Universidad Nacional de Quilmes et CONICET

Examinateurs:
Philippe JORRAND
Directeur de Recherche Émérite - CNRS
Laurent REGNIER
Professeur - Université de la Méditerranée
Lionel VAUX
Maitre de Conférences - Université de la Méditerranée
Michele PAGANI
Maitre de Conférences - Université de Paris Nord

Thesis adviser:
Pablo ARRIGHI
Maitre de Conférences - Université de Grenoble

Thesis abstract: 
The objective of this thesis is to develop a type theory for the linear-algebraic λ-calculus, an extension of λ-calculus motivated by quantum computing. This algebraic extension encompass all the terms of λ-calculus together with their linear combinations, so if t and r are two terms, so is α.t + β.r, with α and β being scalars from a given ring. The key idea and challenge of this thesis was to introduce a type system where the types, in the same way as the terms, form a vectorial space, providing the information about the structure of the normal form of the terms. This thesis presents the system Lineal, and also three intermediate systems, however interesting by themselves: Scalar, Additive and λCA, all of them with their subject reduction and strong normalisation proofs.

---

Me es un placer anunciarles que mi defensa de tesis, acompañada de un encuentro QuAND, será el 23 de Setiembre en Grenoble. Aquí tienen el programa, las informaciones prácticas y los detalles de la tesis.

PROGRAMA:

10h - 11h:
  Encuentro de trabajo del proyecto QuAND (privado)
11h15 - 12h:
  Charla de Michele Pagani "Working for a theory of algebraic abstract reduction systems"
12h - 14h:
  Almuerzo
14h30 - 16h:
  Defensa de tesis de Alejandro Díaz-Caro: "Sobre el tipage vectorial"
16h:
  Brindis

INFORMACIÓN PRÁCTICA:

Aquí hay un mapa http://g.co/maps/rc8dc y algunos detalles:
Desde la estación de trenes, pueden tomar el Tram B en dirección "Plaine des sports", y bajarse en la parada "Bibliothèques universitaires".
El encuentro QuAND será en la sala Aquarium, y la defensa en el anfiteatro del edificio MJK (Maison Jean Kuntzmann), al igual que el brindis.

DETALLES DE LA TESIS:

Título:

Sobre el tipage vectorial
Por:

Alejandro DÍAZ-CARO
Director:

Pablo ARRIGHI
Co-director:

Frédéric PROST

La defensa se llevará a cabo el viernes 23 de Setiembre de 2011 a las 14:30hs delante del jurado compuesto por:

Rapporteurs:
Gilles DOWEK
Directeur de recherche - INRIA Centre Paris-Rocquencourt 
Thomas EHRHARD
Directeur de recherche CNRS - Laboratoire Preuves, Programmes et Systèmes 
Eduardo BONELLI
Profesor Asociado e Investigador Adjunto - Universidad Nacional de Quilmes et CONICET

Examinateurs:
Philippe JORRAND
Directeur de Recherche Émérite - CNRS
Laurent REGNIER
Professeur - Université de la Méditerranée
Lionel VAUX
Maitre de Conférences - Université de la Méditerranée
Michele PAGANI
Maitre de Conférences - Université de Paris Nord

Director de tesis:
Pablo ARRIGHI
Maitre de Conférences - Université de Grenoble

Resumen de la tesis: 
El objetivo de esta tesis es desarrollar una teoría de tipos para el λ-cálculo algebraico-lineal, una extensión de λ-cálculo motivada por la computación cuántica. Esta extensión algebraica comprende todos los términos del λ-cálculo y sus combinaciones lineales, de manera que si t y r son dos términos, α.t + β.r, con α y β escalares de un anillo dado, también lo es. La idea principal y el desafío de esta tesis ha sido introducir un sistema de tipos donde los tipos, de la misma manera que los términos, formen un espacio vectorial, proveyendo información acerca de la estructura de la forma normal de los términos. Esta tesis presenta el sistema Lineal, y también tres sistemas intermedios, aunque interesantes por ellos mismos: Scalar, Additive y λCA, todos ellos con sus pruebas de preservación de tipo y normalización fuerte.

Los nuevos pontífices

El pontífice cuántico Dave Bacon se ha retirado para dar lugar a un grupo nuevo de pontífices: Steve Flammia, Charles Bennett, y Aram Harrow. Les deseo mucha suerte a sus santidades.

Comparto una imagen muy interesante de uno de sus recientes posts.

Video de Introducción a la Computación Cuántica

Este es simplemente una de las mejores explicaciones de como funciona la computación cuántica. Video de Charlie Marcus.

Escuelas, conferencias, y otras cosas

Hace mucho que debería haber escrito esta entrada, pero simplemente luego de mi viaje a Canadá se me acumuló un montón de trabajo.

Primero, la escuela canadiense en computación cuántica: 11th Summer School on Quantum Information. En general, estuvo  genial! Los profesores eran todos investigadores reconocidos en su especialidad. En el área de ciencias de la computación cuántica tengo que destacar a Michele Mosca, Andrew Childs, Gilles Brassard, Renato Renner, y Daniel Gottesman. Todas sus clases estuvieron fabulosas. Las otras clases eran en teoría de la información, las cuales entendí regularmente bien, y en física, esto último más o menos. Fueron 2 semanas muy buenas en donde pude conocer gente de todo el mundo, y con quien pude hablar sobre computación cuántica con libertad, sin tener que explicar los porques ni dar razones de su estudio. Simplemente directo al asunto. En este enlace se pueden encontrar las notas de curso de todas las clases. El próximo año va a ser en IQC, uno de los mejores lugares del mundo para estudiar la materia.

Segundo, en agosto 23-27 se realiza AQIS 2011 en Busan, Korea. Voy a estar dando una presentación allí sobre el mismo tema que presenté en la escuela. El título del trabajo es: Quantum Query Complexity of Hamming Distance Estimation. Ya estaré subiendo una versión del paper en mi página web personal y arXiv.

Por último, estuve colaborando con Stasys Jukna en la correción (proofread) de su último libro que estará publicándose muy pronto. Solo leí 4 capítulos, pero está increíble! Sin duda será un éxito. Stasys tiene otro libro que es una joya en combinatorica: Extremal Combinatorics with Applications in Computer Science. Lo tengo aquí mismo, y siempre lo estoy consultando para cualquier problema que tenga. Recomiendo ese libro a cualquiera que esté interesado en cotas inferiores para algoritmos.

Mi interés está principalmente en técnicas de cotas inferiores para dos modelos de computación cuántica: árboles de decisión y protocolos de comunicación. Mis últimos trabajos estuvieron básicamente en la aplicación de técnicas conocidas a problemas específicos. Pero ahora quisiera realmente intentar desarrollar una técnica nueva en communication complexity. Para ello, estoy estudiando tensor rank. Quiesiera hacer mención de un muy lindo paper sobre esto que aparareció en el último CCC 2011: Tensor Rank Some Lower and Upper Bounds (arXiv:1102.0072). Además tiene un apéndice que explica muy bien varias propiedades de los tensores.

Postdoc: Proyecto ALAL

Como anuncié en un post anterior, se aproxima mi defensa de tesis: el 23 de Setiembre. A partir de Octubre comenzaré un postdoc en la Université de Paris-Nord (Paris XIII), un proyecto financiado por DIGITEO y la región Île-de-France. El responsable del proyecto de Michele Pagani, del Laboratoire d'Informatique de Paris Nord y el socio Gilles Dowek, director de uno de los 5 dominios de investigación del INRIA.

Título del proyecto: 

ALAL: Algebraic approaches to lambda calculi

(Métodos algebraicos para cálculos lambda)

No voy a poner el proyecto entero acá, pero dejo el resumen corto (abajo la traducción al español)

The project focuses on formal foundations for language-based (especially static) techniques guaranteeing resource-related runtime properties of programs. The project belongs to the research area whose aim is to associate to a program a certification assuring some specific properties. We will derive the tools and techniques for our investigation from the field of logical proof-theory and semantics, with special interest in linear logic and λ-calculus. In particular, we will explore the new interactions between linear algebra and the formal methods approach to computation, recently arisen from the differential extension of linear logic and the algebraic λ-calculi. The expected result is a robust theoretical framework in which to develop static analysis and verification tools for non-deterministic paradigms, such as stochastic systems, concurrent computation, quantum programming, etc.

Y aquí una traducción:

El proyecto se centra en los fundamentos formales de las técnicas basadas en lenguaje (sobre todo estáticas) que garantizan propiedades de ejecución de los programas relacionadas con recursos. Este proyecto pertenece al área de investigación cuyo objetivo es asociar a un programa una certificación que garantice ciertas propiedades. Vamos a derivar las herramientas y técnicas de nuestra investigación del campo de la teoría de la demostración lógica y de la semántica, con especial interés en lógica lineal y cálculo lambda. En particular, vamos a explorar las nuevas interacciones entre álgebra lineal y enfoques de métodos formales recientemente surgidos a partir de la extensión diferencial de lógica lineal y de los cálculos lambda algebraicos. El resultado esperado es un framework sólido en el cual desarrollar herramientas de análisis estático y verificación para paradigmas no-determinísticos como sistemas estocásticos, computación concurrente, computación cuántica, etc.

LSFA (y QuAND!)

Con Pablo Buiras, a quien estoy dirigiendo en su tesis de licenciatura (el equivalente a la tesis de master en el sistema de la Unión Europea) y Mauro Jaskelioff, su codirector, hemos escrito un paper basado en la tesis de Pablo, que fue aceptado en LSFA 2011. Será Pablo quien lo presente allí.

El paper aborda el problema de la confluencia del lambda cálculo algebraico lineal por medio de un sistema de tipos (el cual permite sólo términos fuertemente normalizables, lo que en conjunto con la confluencia local, nos da la confluencia del lenguaje). Este sistema de tipos puede verse como una extensión de Additive al cálculo completo o como una simplificación de Vectorial. Tiene la ventaja de que, al igual que Additive, sólo introduce sumas en los tipos, y no escalares como lo hace Vectorial, lo cual lo haría mucho más complejo y difícil de interpretar en otros sistemas conocidos. Además, da información aproximada de qué es lo que está pasando en el término: por ejemplo, si tenemos un término 2.1 M + 1.5 N donde M tiene tipo T y N tipo R, el tipo de esta combinación lineal de términos será T+T+R, dicho de otro modo, el tipo "aproxima las cantidades" de términos de cada tipo que están presentes en la combinación, tomando su parte entera.

El paper completo (el borrador, claro, aún tenemos tiempo para enviar la versión definitiva) lo pueden bajar de acá. Y el lunes pasado presenté el trabajo (con un cambio, ya que en mi presentación la normalización fuerte la derivo a partir de la normalización fuerte de Vectorial) en el encuentro del proyecto QuAND. Los slides de esa presentación están acá.

La versión definitiva del paper será publicada en el Electronic Proceedings in Theoretical Computer Science, una revista científica electrónica que suele publicar los anales de workshops y conferencias, y que tiene la particularidad de ser abierta: cualquiera puede descargarse sus artículos, no hace falta pagar por ello.

Update 25/03/12: Los proceedings del workshop han aparecido. Pueden bajar la versión publicada del paper desde aquí.

Habemus date definito : XXIII Septembris

(English below)

Mi tesis titulada "Du typage vectoriel" (Del tipage vectorial) ha sido aceptada para ser defendida. Hemos fijado la fecha de la defensa para el 23 de septiembre. Aquí la traducción del resumen oficial.

El objetivo de esta tesis es desarrollar una teoría de tipos para el λ-cálculo algebraico-lineal, una extensión de λ-cálculo motivada por la computación cuántica. Esta extensión algebraica comprende todos los términos del λ-cálculo y sus combinaciones lineales, de manera que si t y r son dos términos, α.t + β.r, con α y β escalares de un anillo dado, también lo es. La idea principal y el desafío de esta tesis ha sido introducir un sistema de tipos donde los tipos, de la misma manera que los términos, formen un espacio vectorial, proveyendo información acerca de la estructura de la forma normal de los términos. Esta tesis presenta el sistema Lineal, y también tres sistemas intermedios, aunque interesantes por ellos mismos: Scalar, Additive y λCA, todos ellos con sus pruebas de preservación de tipo y normalización fuerte.

Aquí les dejo el anuncio oficial. El manuscrito no lo voy a hacer público hasta que no corrija la enorme cantidad de errores de tipeo que tiene.

---

My thesis entitled "Du typage vectoriel" (On vectorial typing) has been accepted to be defended. The Viva has been fixed for the 23th September. Here you are the official abstract:

The objective of this thesis is to develop a type theory for the linear-algebraic λ-calculus, an extension of λ-calculus motivated by quantum computing. This algebraic extension encompass all the terms of λ-calculus together with their linear combinations, so if t and r are two terms, so is α.t + β.r, with α and β being scalars from a given ring. The key idea and challenge of this thesis was to introduce a type system where the types, in the same way as the terms, form a vectorial space, providing the information about the structure of the normal form of the terms. This thesis presents the system Lineal, and also three intermediate systems, however interesting by themselves: Scalar, Additive and λCA, all of them with their subject reduction and strong normalisation proofs.

Here it is the official announcement. I won't make the manuscript public until I do not correct the huge amount of typos it has.

DCM 2011

Luego de un período de larga ausencia del blog (me excuso con que estaba terminando de redactar mi tesis (la cual se encuentra en revisión por el jurado ahora)) vuelvo para comentarles que este domingo estaré presentando un paper en el 7th International Workshop on Developments of Computational Models (el 3 de Julio, en Zúrich). El paper es un trabajo en conjunto con Pablo Arrighi y Benoît Valiron, el cual presenté antes en algunos encuentros informales y ahora fue aceptado para ser publicado en los proceedings de este workshop.

Les dejo los detalles originales en inglés y debajo la traducción.

A type system for the vectorial aspects of the linear-algebraic lambda-calculus

(joint work with Pablo Arrighi and Benoît Valiron)

We describe a type system for the linear-algebraic lambda-calculus. The type system accounts for the part of the language emulating linear operators and vectors, i.e. it is able to statically describe the linear combinations of terms resulting from the reduction of programs. This gives rise to an original type theory where types, in the same way as terms, can be superposed into linear combinations. We show that the resulting typed lambda-calculus is strongly normalizing and features a weak subject-reduction.

Un sistema de tipos para los aspectos vectoriales del lambda cálculo algebraico lineal

(trabajo en conjunto con Pablo Arrighi y Benoît Valiron)

Describimos un sistema de tipos para el lambda cálculo algebraico lineal. El sistema de tipos tiene en cuenta la parte del lenguaje que emula operadores lineales y vectores, o sea, es capaz de describir estáticamente las combinaciones lineales de términos resultantes de la reducción de los programas. Esto conduce a una teoría de tipos original donde los tipos, de la misma manera que los términos, pueden ser superpuestos en combinaciones lineales. Mostramos que el cálculo tipado resultante tiene normalización fuerte y una versión débil de la propiedad de conservación de tipo.

Hasta que esté publicado (en EPTCS, de libre acceso), les dejo aquí los links: (ver más abajo)

• Versión oficial de 12 páginas (preprint)
• Versión completa con todas las pruebas en apéndice

Luego del workshop subiré aquí los slides de la presentación también.

Update (05/07/11): Aquí están los slides que presenté durante el workshop.

Update (31/07/12): Finalmente el paper está online (y es de libre acceso): EPTCS.

Poster para la escuela

Este domingo me pongo en camino al 11th Summer School on Quantum Information & 8th Canadian Student Conference on Quantum Information, como lo mencioné en el post anterior.

Por lo tanto, aquí está el poster que voy a presentar allí (enlace). No es perfecto, siempre mi punto débil fue el diseño de posters y presentaciones. Pero, es lo suficientemente bueno para transmitir la idea, lo cual es lo más importante.

No creo que vaya a escribir durante mi estadía allá, pero si seguramente estaré dando algunos avisos por el twitter. Al regresar voy a escribir sobre mis impresiones. Después de más de 3 años por Asia, voy a volver a un uso horario Americano.

Ahh, si a alguien le interesa el tema de investigación del poster, dejen un comentario, y puedo explicar sobre que es. Básicamente, son dos cotas superiores en una generalización de la distancia de Hamming. Como aún es un trabajo en progreso, sigo buscando las cotas inferiores para el problema. A ver si puedo conseguir un poco de feedback en la escuela.

Ultimos eventos

Hace mucho tiempo que ya no escribía nada en el blog. No tengo excusas, aunque si he estado muy ocupado (reductio ad absurdum). Escribir papers, tesis y otras cosas endiabladas hizo que me olvide un poco del blog. Pero voy a volver a tomar el ritmo de antes, más o menos 2 posteos al mes.

La última entrada que escribí es el CFP de AQIS 2011. Muy linda conferencia, yo fuí el año pasado y me encantó. Este año me gustaría ir, pero creo que no. Tengo otros planes. Uno de ellos es que voy a Canadá por 2 semanas al 11th Summer School on Quantum Information & 8th Canadian Student Conference on Quantum Information. Echenle un vistazo al programa y verán que muchos expertos en el área estarán dictando clases. Estoy muy ansioso por participar de esta escuela desde hace mucho tiempo. Alejandro ya fué y le gusto mucho. También voy a estar presentando un poster, y apenas lo tenga listo lo pondré aquí en el blog. Es sobre un problema que me tiene enganchado desde hace mucho tiempo, sobre estimación de edit distance pero utilizando quantum queries. Ya más adelante daré más detalles.

Otra cosa, ya están los papers de ICALP 2011. Muy buen nivel este año aparentemente y promete mucho. También no se olviden de ISAAC 2011. Todavía hay tiempo para enviar, va a ser en Yokohama. Y por último SODA 2012 aquí en Kyoto. Con o sin paper, definitivamente voy a ir!!

AQIS 2011 CFP

You are cordially invited to submit your precious research papers to AQIS11,
which will be held in Busan, Korea.

http://newton.kias.re.kr/aqis11

is a tentative homepage for AQIS11 still under construction.
Busan is the second largest city of Korea and was the capital city of Korea during the Korean war. It is now one of the most favorite Korean places for the tourists with beautiful beach and movie business.

Important dates of AQIS11 are
Submission dead line: June 13, 2011
Acceptance notification: July 10, 2011
Final draft: July 31, 2011
Tutorials: August 23, 2011
Main conference: August 24-27, 2011
Workshops: August 29-30, 2011

λvec en QAPL 2011: los slides

Hace un par de horas dí la charla sobre el sistema de tipos vectorial que había anunciado aquí, aquí (explicación del paper) y aquí (updated (λvec)) en el QAPL 2011.

Dejo los slides aquí (más adelante los subiré a mi página web y cambiaré el link).

@compucuantica

Acabo de crear una cuenta twitter exclusiva para el blog: @compucuantica

Por ahora allí aparecerán actualizaciones de los posts cada vez que haya nuevos contenidos en el blog. Más adelante se verá si puede servir para algo más.

Para entretenerse

Dejo dos videos muy interesentes. El primero es sobre el gran resultado del año pasado en complejidad computacional cuántica QIP=PSPACE, explicado por uno de los mejores, John Watrous.

El segundo es para mirar con una coca cola y papas fritas. Es sobre la mecánica cuántica de los viajes en el tiempo, explicado por uno de los grandes también en computacion cuántica, Seth Lloyd.

Talk @ École Polytechnique

Mañana daré una charla en la École Polytechnique de Paris, invitado por el grupo COMÈTE del laboratorio LIX.

Aquí les dejo los detalles: http://www.lix.polytechnique.fr/comete/seminar/abs2011.php#DiazCaro11

.

Curso introductorio a topología

En el marco del grupo de estudio SELEN (SEmántica de LENguages), el cual es coordinado por Mauro Jaskelioff, de la Universidad Nacional de Rosario (UNR), Raúl Kantor ha comenzado a dictar un curso introductorio a topología, y lo han grabado y subido. Aquí les dejo el video, el cual no tiene desperdicio.

Curso Topología 1 from Mauro Jaskelioff on Vimeo.
Dr. Raúl Kantor

para SELEN 2011

24/2/2011

Raúl Kantor, doctor en matemática y más tarde abogado, fue el director de la carrera de Ciencias de la Computación en la UNR cuando yo la cursé, de hecho, él es uno de los fundadores de la carrera.

Update:
Dejo los siguientes videos de la serie.

Curso Topología 2 from Mauro Jaskelioff on Vimeo.

Curso de Topología 3 from Mauro Jaskelioff on Vimeo.

TEDxCaltech: Quantum Computing

An interesting intervention of Scott Aaronson at the TED^x organized at Caltech



via La Consigna

Cotas inferiores para funciones booleanas simétricas

Últimamente he estado estudiando una técnica para encontrar cotas inferiores para árboles de decisión basadas en polinomios. Básicamente, la función booleana se escribe como si fuera un polinomio, e.g. x1∧x2 se puede escribir como un polinomio en dos variables p(x1,x2)=x1⋅x2. Entonces el número de consultas al oráculo es exactamente el grado del polinomio. Para el ejemplo del and tenemos que este número es 2.

Bueno, hay un resultado en computación cuántica que dice que el número de consultas que hace un algoritmo a un oráculo cuántico está acotado por abajo por el grado de un polinomio de bajo grado que aproxima la función booleana. Este es el link al paper original que desarrolló la técnica.

Ahora consideremos la función threshold, donde Thrt(x)=1 si y solo si el número de 1s en x es mayor o igual a t, i.e. |x|≥t. La cota inferior reportada en muchos papers es de . Existe un teorema (Paturi 1992) basado en el método de los polinomios. Este teorema nos permite calcular la cota inferior para cualquier función booleana simétrica. Una función booleana f es simétrica, si dado cualquier entrada x, permutar el orden de los bits no cambia el valor de f(x). Claramente Thrt es simétrica.

Tengo una pregunta en Theoretical Computer Science Stack Exchange que está sin respuesta ya por unos días. Básicamente el problema es que la cota inferior para threshold indicada arriba no sigue en forma directa desde el teorema de Paturi.

Creo que voy a esperar unos días más, y si sigue sin respuesta voy a  poner una recompensa. Pero si algún lector de este blog conoce la respuesta, le voy a estar muy agradecido :-)

QPL 08 y 09 en Electronic Notes in Theoretical Computer Science

El primer paper internacional que publiqué, en el QPL 2008, finalmente apareció en Electronic Notes in Theoretical Computer Science. Los editores se demoraron un poco (bastante), pero finalmente publicaron los proceedings de este workshop.

Este paper fue la culminación de mi tesis de licenciatura, y lo escribimos con Pablo Arrighi (mi director de doctorado), Manuel Gadella (uno de mis directores de tesis de licenciatura) y Jonathan Grattage.

Y acá les dejo la cronología en el blog de este paper :)

• Acá está el post de cuando lo enviamos.
• Acá cuando nos avisaron que fue aceptado
• Acá cuando mandamos la versión final.
• Y finalmente, este post para la versión publicada :)

-

Y la cosa no queda allí, también los mismos editores enviaron los papers del QPL 2009! Allí encontrarán la primera versión de Scalar, en el siguiente número de ENTCS (esta es una versión de sólo 10 páginas, la versión de arXiv está mucho más completa). Este fue el primer paper durante mi doctorado, y como no podía ser de otra manera, la cronología también está reflejada en nuestro blog:

• Aquí cuando fue aceptado,
• y luego los slides de mi presentación y la versión arXiv.

2 nuevos: λFA y λvec

El miércoles envié dos nuevos papers:

El primero está basado en la tesis de licenciatura, en progreso, de Pablo Buiras. El paper lo escribimos entre Pablo, Mauro Jaskelioff, y yo (sus directores). Pueden bajar el paper libremente del arXiv: arXiv:1102.0749.

El título del paper es

Lower bounds for scalars in a typed algebraic λ-calculus

(Cotas inferiores para escalares en un λ-cálculo algebraico tipado)

Acá copio el abstract y explico un poquito de qué se trata "en criollo".

The linear-algebraic λ-calculus is an untyped λ-calculus extended with arbitrary linear combinations of terms. As shown by previous works, building a type system on top of it is a delicate matter. A straightforward extension of a classic type system, like System F, would impose an undesirable restriction: it would only allow superpositions of terms of the same type. Adding sums of types lifts this restriction but raises the question of how to deal with the interaction between scalars and additions. We propose a type system with sums of types for the linear-algebraic λ-calculus which provides an answer to this question by allowing types to have some degree of imprecision. The proposed type system has a subject reduction property and is strongly normalising. Furthermore, we show that the additive fragment of the calculus can be seen as an abstract interpretation of the full calculus.

En lugar de traducir el abstract, explico un poquito la idea: En [DCP10] Barbara Petit y yo creamos un sistema de tipos, λadd, para el fragmento aditivo del linear-algebraic lambda-calculus [AD08] (λlin para abreviar). Luego mostramos que ese cálculo podía traducirse a System F con pares.

En el nuevo trabajo, extendemos ese resultado para el cálculo λlin completo: Primero creamos un sistema de tipos muy similar a λadd, pero para todo el cálculo: o sea, no sólo para lambda términos que se pueden sumar, como t+r, con t y r lambda términos, sino que también se pueden escalar: α.t+β.r, con α, β reales positivos. El sistema se llama λFA (por Full-Additive). La sintaxis de los tipos sigue siendo la misma que la de λadd : básicamente es Sistem F donde además se pueden sumar tipos. Y los escalares? Bueno, lo que hacemos es aproximarlos tomando su parte entera: si un término t tiene tipo T, el término α.t:⌊α⌋.T (nótese que ⌊α⌋ es un número natural y por tanto ⌊α⌋.T no es más que T+T+····+T, ⌊α⌋-veces). Como alguno ya inferirá, mezclar escalares y sumas no es nada sencillo, por ejemplo: 1/2.t+1/2.t tendría tipo ⌊1/2⌋.T+⌊1/2⌋.T = 0.T+0.T = 0, sin embargo si tomamos números mayores (por ejemplo, multipliquemos todo por 100), pues la precisión será muy buena... bueno, depende de lo que queramos decir por "muy buena", pero si no nos parece buena, pues agregamos más 0s al 100 :)

Probamos una especie de subject reduction para este sistema: básicamente lo que dice que se pierde precisión en los escalares al reducir el término, pero no en los tipos. O sea, si un término tiene tipo T+R+S+S, pues sabemos que al reducirlo (al "ejecutar el programa"), obtendremos un término con al menos los tipos T, R y dos veces S.

Además hicimos una prueba de strong normalisation: algo no sencillo ya que la prueba de Scalar [ADC09] no nos sirve porque en Scalar sólo se puede tipar t+r si t y r tienen el mismo tipo (módulo un escalar), por lo tanto el conjunto de términos no es el mismo. Tampoco se puede re-usar la de λadd, porque allí los escalares en los términos no existen (por lo tanto también tenemos otro conjunto de términos), así que hubo que hacer una prueba desde cero.

Por último, mostramos que λadd se comporta como una interpretación abstracta de λFA, y luego conjeturamos (con muchas pistas de que la conjetura es cierta), que System F con pares por extensión también es una interpretación abstracta de λFA.

-

El segundo paper es un trabajo con Pablo Arrighi y Benoît Valiron y es una extensión (o digamos, la continuación) de este. El título es:

A type system for the vectorial aspects of the linear-algebraic lambda-calculus

(Un sistema de tipos para los aspectos vectoriales del linear-algebraic lambda-calculus)

Abstract:

In this paper we describe a type system for the linear-algebraic lambda-calculus. The type system accounts for the part of the language emulating linear operators and vectors. The type system is able to statically describe the linear combinations of terms resulting from the reduction of programs. This gives rise to an original type theory where types, in the same way as terms, can be superposed into linear combinations. We show that the resulting typed lambda-calculus is strongly normalizing and features a weak subject-reduction.

Básicamente los cambios con respecto al viejo son: volvimos a agregar una regla de reescritura que habíamos quitado previamente (usando un truco para que ahora sí funcione), haciendo que el sistema sirva para todo el cálculo λlin, y lo más importante: λlin originalmente (el cálculo no tipado) podía encodear programas cuánticos. Ninguno de los sistemas de tipos en los que trabajé hasta ahora podía hacerlo, Scalar puede tipar programas con distribuciones baricéntricas, λadd podría pensarse como no determinista y λFA podrían ser usado para tipar programas probabilísticos, pero este es el primero que permite tipar los programas cuánticos propuestos en el paper original.

El cálculo se llama λvec (bueno, el nombre correcto sería ).

Aún no lo subimos al arXiv, pero lo que vamos a hacer es actualizar el anterior, ya que es su versión final (ah, por cierto, el anterior, que sería la versión "work-in-progress" de este, fue aceptado y lo vamos a presentar en QAPL 2011 (sólo como presentación, sin aparecer en los proceedings ya que es un work-in-progress)). Cuando aparezca la versión nueva en arXiv pondré el link aquí. Lo pueden bajar de aquí: arXiv:1012.4032.

Novedad en el blog: Barra wibiya

Buenas, este post es para comentarles que hemos agregado la barra wibiya al blog (la barrita que ven abajo). Aquí les describo las funcionalidades que tiene (por ahora, ya que se le pueden agregar cosas a gusto):

Aquí se muestra cuánta gente está viendo el sitio en este momento. Haciendo click muestra algunas estadísticas del sitio (de dónde vienen los últimos visitantes del sitio, por ejemplo).

Este botón sirve para lo que imaginan: traducir los posts a diferentes idiomas. Creo que puede ser útil sobre todo para post escritos sólo en inglés.

Pues eso: acceso directo y cómodo a los últimos posts.


Esta es mi funcionalidad favorita: Haciendo click aquí los lleva a un post cualquiera.


También tienen los botones típicos de las distintas redes sociales y un "+ compartir" para incluso más redes.

Acceso al RSS del blog. Para seguir el blog con algún lector de RSS (como por ejemplo el online Google Reader).


Para ver las últimas actividades en la "Fan Page" del sitio en Facebook. Lo interesante es que pueden verla sin necesidad de irse del blog.

Esta utilidad (obviamente: un chat) aún no estoy seguro de qué tan útil será, ya que 1) por lo general no hay mucha gente online al mismo momento en el blog y 2) hay que autorizar la aplicación en alguna red social para poder acceder al chat. Veremos si gusta o no.

Por último: un link a wibiya, por si a alguien le interesa para su propio blog, y una flechita para ocultar la barra por si a alguien le molesta.

Bueno, espero les guste la nueva funcionalidad.
Happy reading!

Videos from QIP 2011

QIP2011 videos are online!! You can find them on this link.

I only watched one: Bo'az Klartag and Oded Regev, Quantum one-way communication can be exponentially stronger than classical communication. It presents a classical lower bound for a promise problem from linear algebra which the authors call Vector in Subspace Problem. Their lower bound is based on a very interesting geometric argument on the n-dimensional sphere. This result implies an exponential gap between one-way quantum and classical communication complexity.

Others that I would like to watch (which are related to my own interests) are:

1. Tsuyoshi Ito, Hirotada Kobayashi and John Watrous, Quantum interactive proofs with weak error bounds.
   
2. Loïck Magnin, Martin Roetteler and Jérémie Roland, On the additive and multiplicative adversary methods.
   
3. Jianxin Chen, Xie Chen, Runyao Duan, Zhengfeng Ji, Zhaohui Wei and Bei Zeng, On the solution space of quantum 2-SAT problems.
   
4. Andrew Childs and Robin Kothari, Quantum query complexity of minor-closed graph properties.
   

Enjoy the videos!!

Debate: Sobre-calificación?

Este post no es técnico, sino más bien referido a la preparación que tenemos en Argentina (y a quien le quepa, hablo de Argentina porque es lo que conozco) y algunas ideas discutibles sobre qué tan necesarias son algunas cosas.

Lo primero que me sorprendió al llegar a Francia, no fue tanto la preparación de los investigadores de acá (la cual a modo general es muy buena), sino la edad de la gente: Mi director tiene prácticamente mi edad. Los estudiantes de doctorado comienzan a los 23 y a los 25 ya son doctores. Luego hacen un par de años de post-doc y pum, un cargo permanente... a los 28, 29 años.

En Argentina tendemos a querer hacer muchísimas cosas antes de recibirnos, lo cual está perfecto, pero lo hacemos en perjuicio de demorarnos varios años más para obtener el título (hablo del primer título, la licenciatura de 5 años en nuestro caso). Conozco casos de chicos que se han ido a hacer hasta 3 pasantías al extranjero, de al menos 6 meses cada una. Otros casos de tesis de licenciatura que llevan años. Otros que se ponen a dar clases y terminan dando tantas clases que no se reciben nunca.

Creo que lo ideal sería tratar de recibirse jóvenes, con la mayor experiencia posible... o sea: balancear la cosa. Por ejemplo: una pasantía de 6 meses puede ser muy valorada a la hora de buscar una beca doctoral. 3 pasantías es aceptar ser explotado con trabajo precarizado que nos demora el título. Una buena tesis de licenciatura nos ayudará también con el CV. Si incluye una publicación, pues tanto mejor (y puede ser una publicación post-tesis, no hay ningún problema con ello). 3 publicaciones antes de recibirse sería una exageración (y tomaría demasiado tiempo). Dar clases como ayudante de cátedra colabora con el CV. Dar 200 horas de clases al año es una exageración que nos demorará el título.

El modelo europeo es totalmente distinto al nuestro, acá se supone que uno comienza su carrera a los 18 años y para los 23 se recibió y comenzó el doctorado. Las carreras tienen mucho menos contenidos en general, ya que son mucho más especializadas, lo cual se puede hacer porque cuentan con muchísimos más cargos docentes. Por ejemplo, si queremos hacer una carrera orientada a la teoría de lenguajes, metemos muchas materias sobre el tema, quitamos otras no relacionadas al tema y dividimos la carrera en "Cs. de la Computación" y "Cs. de la Computación con orientación a la teoría de lenguajes". Eso implica que cada una tendrá menos alumnos y se necesitarán más cargos docentes. Algo difícilmente permisible en Argentina. Por lo tanto, es normal que nuestras carreras tengan tantos temas juntos, lo cual nos da una preparación mayor (más amplia) pero también nos lleva más tiempo terminarla. La cuestión está en no agregarle a eso, cosas innecesarias. Y que no se mal entienda, tampoco digo meterle pata a rendir todas las materias y exclusivamente eso y terminar sin haber hecho nada extra. Eso nunca es bueno tampoco. Lo que digo es tener un sano balance.

Bueno, este post pretende arrancar una discusión, no cerrar el tema, así que sientanse libres de comentar! Mi opinión no está cerrada sobre el tema, es algo que estoy reflexionando y quise compartir para reflexionar en grupo (de ser posible, comenten en el post y no en facebook, ya que en facebook la discusión se termina perdiendo).

Talk @ Paris 13

(English version below)

El próximo 17 de enero daré una charla sobre los sistemas de tipos algebraicos en Paris 13 (Lab LIPN) en las series "Sémiraires LCR". Aquí está la información y aquí reproduzco el resumen:

En esta charla voy a presentar varias extensiones a System F, para tipar el lambda-cálculo lineal-algebraico, un lambda-cálculo enriquecido con una estructura vectorial. El primer sistema de tipos es una extensión directa de System F, el cual sólo tipa el cálculo sin más adorno. El segundo es un sistema de tipos que tiene en cuenta escalares, el cual puede servir como una garantía de que la forma normal de un término tiene forma con . El siguiente sistema incluye "suma de tipos" reflejando los de los términos -- mostrando que las sumas en el cálculo algebraico se comportan como una clase particular de pares. Finalmente el último sistema de tipos combina los dos anteriores. Damos contraejemplos de porqué este tipo de sistema de tipos vectorial no se puede hacer en estilo Curry y mostramos algunas pistas de un futuro sistema de tipos vectorial en estilo Church, adecuado para especializarlo en un cálculo cuántico.

Edit: Aquí dejo los slides.

---

Next January 17th I will give a talk about the algebraic type systems at Paris 13 (LIPN Lab) in the series "Sémiraires LCR". Here it is the information and I reproduce here the abstract:

In this talk I will present several extensions to the System F, for the sake of type the linear-algebraic lambda-calculus, a lambda-calculus enriched with a vectorial structure. The first type system is a straightforward extension of System F, which just types the calculus without any further adornment. The second one is a type system accounting for scalars, which can serve as a guarantee that the normal form of a term is of the form with . The following system includes "sums of types" reflecting that of the terms--showing that sums in the algebraic calculus behaves as a special kind of pairs. Eventually the last type system combines the previous two. We give counterexamples of why this kind of vectorial type system cannot be made in Curry style and show the clues of a future vectorial type system in Church style suitable to specialize the calculus into a quantum calculus.

Edit: Here are the slides.