Interview à Pablo Arrighi par France Info

(este post está en Francés, porque el audio es en Francés)

Pablo Arrighi ( mon ancien directeur de thèse ), a donné un petit interview à France Info. Vous pouvez l'écouter ici.

mp3

Quick Report

Esta entrada es un status report. Terminé de escribir un paper y lo envié para una conferencia. Actualmente estoy escribiendo mi tesis y al mismo tiempo trabajando en un proyecto de teoría de automatas y sistema de pruebas interactivos con un colaborador. También estoy buscando otro problema interesante sobre el cual trabajar. Pienso seguir en computación nondeterminística y tengo dos opciones allí: Exponential Time Algorithms y Fixed Parameter Complexity o sigo con quantum/classical proofs. Hasta ahora he comprobado que puedo hacer dos proyectos al mismo tiempo, o inclusive tres si tengo más colaboradores.

La elección de un problema o tema de investigación es por supuesto muy importante, y al mismo tiempo, tan difícil como la solución. En palabras de Emil Artin:

"Our difficulty is not in the proofs, but in learning what to prove".

Revista ensemble + Encuentro en París

Hace mucho (demasiado) tiempo que no publico nada en el blog. La razón: en octubre comencé a dictar clase, con lo cual mis tiempos se han acortado considerablemente. Mis tiempos están divididos entre la Université Paris Ouest donde doy clase, y al centro INRIA donde me dedico a la investigación dentro del grupo DEDUCTEAM... la verdad que eso deja poco tiempo para nada más, y lamentablemente el blog a sufrido esa falta.

Lo primero que quería comentarles es que salió el número 9 (del 4to año) de la Revista Ensemble (revista de la Casa Argentina en París). En este número, se incluye el "Dossier temático: Vidas y proyectos de jóvenes científicos argentinos", con textos de 9 investigadores argentinos en Francia (entre ellos, yo :)), contando su tema de investigación, sus experiencias, etc. No se pierdan la nota de apertura del dossier por Federico Ariel y Alfonso Soler.

Lo segundo, es que este jueves se realizará el primer encuentro "Intercambiando inquietudes en la comunidad científica argentina en Francia", donde se espera establecer un espacio de participación a partir del cual proponer y llevar a la realidad acciones concretas para fortalecer y multiplicar lazos entre la comunidad científica de nuestro país y la de investigadores argentinos radicados en Francia.

El encuentro es en la Casa Argentina en la Ciudad Universitaria de París, este jueves 18 de octubre a las 18. La participación es por supuesto gratuita, pero es obligatorio inscribirse online (en esa página también encontrarán el cronograma, los organizadores, etc). Yo estoy entre los organizadores, aunque a decir verdad, lo mío es más un apoyo moral (por lo que comenté al inicio de este post), todo el mérito va al resto de los organizadores, quienes están trabajando muy fuertemente para que el encuentro no sólo sea interesante a nivel de debates, sino que además se llegue a propuestas de acciones concretas.

Argentina

Fin de las vacaciones (mechadas con congresos). Estuve un mes y medio en Argentina, del cual una semana estuve en el CLAM en Córdoba (post al respecto) y otra en el WoLLIC en Buenos Aires (post al respecto). Como se imaginarán, disfruté muchísimo la vuelta, después de casi 4 años, a mi país.

En total visité 4 universidades: UNC, UNR, UNQ, UBA. En Córdoba (UNC) me encontré con gente conocida y gente a quien conocí ahora. Hay mucha gente investigando allí, en el famoso FaMAF y siempre es un placer visitarlos. El CLAM salió muy bien, conocí diversos investigadores latinoamericanos (aunque es un congreso de matemática, por lo que había un poco de distancia temática con mi área). En Rosario (UNR) visité mi universidad, con viejos conocidos y montón de gente nueva. El progreso de la Licenciatura en Ciencias de la Computación allí es evidente, mucha gente nueva, ex-alumnos que han retornado luego de doctorarse, y ahora son la planta docente de la universidad, etc. A Quilmes (UNQ) fui invitado por Fidel (Pablo E. Martínez López), director de la carrera de programación, y un gran amigo. La verdad que me impresionó las instalaciones de esa universidad, nada que envidiar a las universidades francesas: las oficinas de los investigadores, el comedor universitario, las aulas... me dejó impresionado. A nivel de la carrera, fue un gusto ver cómo Fidel está llevando adelante una carrera con toda la pedagogía que siempre supo mostrar en sus clases, y con un nivel de los más altos, incluso tratándose de una carrera terciaria. Finalmente en Buenos Aires (UBA), estuve en el WoLLIC, donde encontré a alguna gente de exactas (el congreso se hizo en un salón de la facultad de económicas, por lo que no vi a más gente de exactas que la que estaba participando del mismo). El WoLLIC estuvo organizado impecablemente, y tuvimos 4 días de presentación de papers, tutoriales y charlas invitadas que valió mucho la pena. La publicación del WoLLIC la pueden encontrar aquí.

En unos días voy al LSFA en Río de Janeiro (post al respecto), a la PUC. Luego cuento mis impresiones.

De Vacaciones y papers

Bueno, hace mucho que ya no escribía nada en el blog. No era porque estaba ocupado, porque honestamente, siempre se está ocupado. Simplemente no sabía que escribir. Pero ahora me propuse escribir algo, cualquier cosa.

Ultimamente he estado mucho de vacaciones. Por ejemplo, me tomé 3 días en Julio, más otros 3 días en agosto, y varios fines de semana saliendo. Sumado ha eso, he estado trabajando en un nuevo paper que espero terminar de escribirlo muy pronto y estoy comenzando un nuevo tema de investigación sobre el cuál estoy muy emocionado.

El paper es sobre comunicación, y es la continuación de mi paper de TAMC'12. En este caso, en lugar de estudiar NQP-communication, nos concentramos en QCMA-communication. Todavía no voy a hablar sobre el resultado. Aún sigo escribiendo el paper y voy a esperar hasta tener todos los detalles.

El nuevo tema de investigación tiene que ver con computación clásica y los interactive proof systems. Estoy empezando con esto, y todo aún es muy nuevo por lo que no tengo nada que reportar. El tema es muy popular, con muchas aplicaciones a criptografía. Más adelante voy a hacer también la parte cuántica.

Respecto a los interactive proof systems, hay un nuevo resultado de Tsuyoshi Ito y Thomas Vidick que pueden descargarlo desde aquí arXiv:1207.0550. El resultado, que será presentado en FOCS este año, básicamente es que la clase NEXP está incluída en MIP*. En términos simples y bien generales esto significa que experimentos que utilicen entanglement serán muy difíciles de verificar eficientemente. Por suerte, sí tenemos propuesta de experimentos para probar violaciones de inigualdades de Bell que nos dan alguna esperanza. Por ejemplo este paper presenta los últimos avances arXiv:0907.3584.

Oxford Quantum Talks Archive

El archivo de charlas sobre computación cuántica del departamento de ciencias de la computación de Oxford ha sido subido a YouTube. Que lo disfruten!

---

The quantum talks archive from the department of computer science of Oxford has been YouTubed. Enjoy!

Slides + nuevo puesto

Para comenzar, pido disculpas por el abandono del blog, he andado bastante ocupado y no tuve tiempo de comentar nada por aquí.

Como posteé anteriormente, el paper que escribimos con Barbara Petit (arXiv:1011.3542) fue aceptado en WoLLIC. Como preparación para la presentación, hice una pre-presentación en un seminario de mi grupo. Les dejo los slides (ver abajo el link a los slides definitivos). Fue bueno haberlo practicado, ya que en WoLLIC tengo unos 30 minutos, y el seminario me llevó alrededor de una hora veinte :-) ...así que deberé recortarlo un poco (bastante), pero quería dejar aquí esta versión larga, ya que creo que ayuda bastante a entender el paper, con muchos ejemplos.

Les comento de paso que a partir de octubre, cuando se termina el postdoc actual, tendré un cargo de ATER (Attaché Temporaire d'Enseignement et de Recherche), lo que en Argentina se llama "cargo con dedicación exclusiva", por un año, en la Université Paris Ouest Nanterre La Défense, y tendré también una oficina en la "antena parisina" del INRIA-Rocquencourt, para seguir colaborando con Gilles Dowek e integrar el equipo Deducteam. Así que por lo pronto me quedo un año más en París.

Update: aquí les dejo los slides de WoLLIC. Además, el link a la publicación (aunque más arriba está el link al arXiv, de libre acceso).

Visitando mi tierra

El paper que enviamos con Barbara Petit (anunciado aquí, donde pueden leer más detalles) fue aceptado en WoLLIC 2012, un workshop internacional que este año se realiza en Buenos Aires del 3 al 6 de Setiembre.

Además, me aceptaron también una exposición en la sesión de Lógica y Computabilidad del CLAM 2012, que este año se hace en Córdoba (Argentina) del 6 al 10 de Agosto. Allí estaré dando una charla sobre mi tesis (básicamente presentando mi sistema de tipos Vectorial, el cual mencioné innumerables veces en este blog), y algunos desarrollos más actuales que estoy llevando a cabo con diversos autores. Pueden ver el resumen que fue aceptado (en español!) aquí.

Entre los dos eventos, estaremos disfrutando junto a mi mujer de nuestra querida tierra, familiares, amigos y muchos asados :)

Update 07/Ago/12: Aquí dejo los slides de la charla que di en el CLAM.

Escuela en Lenguajes Formales

Hay una escuela en teoría de la computación que se va a llevar a cabo en Tarragona, España. Se llama International Fall School in Formal Languages and Applications.  Aunque en el nombre dice "Lenguajes Formales", en el programa se pueden ver cursos bastantes variados como circuitos booleanos y máquinas de Turing. Estoy considerando muy seriamente asistir. Este año, exactamente en ese mismo lugar, se llevó a cabo la conferencia LATA'12. Un amigo fue a presentar un paper este año allí y quedó encantado con Tarragona.

Aprovecho también para avisar que por fin colgaron algunos videos de las presentaciones de QIP'12 en este link. Ya estuve mirando un par de videos y tienen muy buena calidad.

Bueno, espero que algunas personas puedan aprovechar la escuela que promete mucho. Ya me pensaré muy bien si asistir o no.

Mini-reporte de TAMC'12

Ya estoy de vuelta de TAMC'12. La conferencia estuvo muy buena, y tengo que destacar los Turing Lectures que se llevaron a cabo. Abajo pongo algunas fotos. No pude estar en todas porque sole estuve hasta el viernes 18.

Abajo pueden ver un poco del lugar de la conferencia, la cual se llevó a cabo en el Institute of Software, Chinese Academy of Science.

John Hopcrof: Su presentación se tituló On the Impact of Turing Machines. Fué sobre la historia de las máquinas de Turing y evolución hasta nuestros días. Hizo principal énfasis en la robustez del modelo para el estudio de la computación. Recalcó también que sin ese modelo, probablemente el descubrimiento de la complejidad computacional se hubiera atrasado en uno 10 a 20 años.

Richard Karp: Su presentación se tituló Theory of Computation as an Enabling Tool for the Sciences. Un recuento histórico del departamente de ciencias de la computación de UC Berkeley y la evolución de las ciencias de la computación como una ciencia interdisciplinaria.

S. Barry Cooper: Su presentación se tituló From Turing Machine to Morphogenesis -- Forming and Informing Computation. Tengo que admitir que entre las presentaciones en las que participé, esta fue mi favorita. Un recuento histórico sobre la historia de Turing y su impacto actual en las ciencias.

Deyi Li: Su presentación se tituló Interaction and Collective Intelligence on the Internet. Así como el título lo indica, fué sobre inteligencia colectiva, en particular en redes sociales. Destacó como el estudio de las redes sociales da cuenta de nuevos fenómenos sociales en la actualidad.

Por último, este es un recuerdo que me llevo de la conferencia.

De vuelta a Beijing

Estoy de vuelta viajando a Beijing para TAMC'12. Es para presentar este paper. Los slides se pueden descargar de aquí. Esta conferencia promete mucho, ya que varios científicos muy importantes estarán haciendo presentaciones en ocasión del año de Turing.

Espero que algunos hayan tenido la oportunidad de participar en LATIN'12 que fue en Arequipa, Perú. Tuvieron también una muy linda escuela en teoría de la computación. También hay WoLLIC'12 en Buenos Aires. Yo fuí a esa conferencia en el 2007 en Río de Janeiro. Muy buena conferencia, con temas muy interesentes, más enfocado en lógica y computabilidad. Y no se olviden de LATINCYPT este año en Santiago.

Muy buen año para latinoamérica en ciencias de la computación (teoría). Tres excelentes conferencias. Espero que muchos puedan aprovecharlas, porque LATIN es cada 2 años, y WoLLIC suele cambiar cada año. LATINCRYPT no sé.

Linearidad en Lineal vs Linearidad en Lógica Lineal

Barbara Petit y yo hemos enviado un paper para revisión. En este trabajo, hacemos un análisis de la linealidad en el lambda cálculo algebraico lineal (Lineal), y la comparamos con la linealidad de lógica lineal.

En lógica lineal, una función es lineal, si utiliza una sola vez su argumento. Así, f(x)=x² no es lineal (ya que utiliza su argumento x dos veces), mientras f(x)=x+1 sí. En Lineal una función f(x+y) se toma como f(x)+f(y), imitando la definición de las funciones lineales en álgebra (o, tal es el objetivo, la multiplicación de matrices por vectores, como en computación cuántica).

En este nuevo paper definimos un sistema de tipos para Lineal (o para ser más precisos, para el fragmento de Lineal que sólo tiene sumas, ya que es la parte que nos interesa, y que además coincide con varios lenguajes no-deterministas). Este sistema de tipos caracteriza las superposiciones y la linealidad del lenguaje. Luego mostramos que este sistema se puede traducir en Sistema F con pares, el cual se corresponde con el fragmento no-lineal de IMELL (el fragmento intuisionista, multiplicativo, exponencial de la lógica lineal). Esto plantea la primera sorpresa: el cálculo Lineal se traduce en un fragmento no-lineal de la Lógica Lineal.

En realidad lo que sucede, es que Lineal se mantiene fiel a la computación cuántica, donde x+y representa una superposición de x e y, los cuales son atómicos, y una función que duplique su argumento, por ejemplo, es perfectamente válido, siempre y cuando sólo pueda duplicar elementos atómicos. Por tanto, f(x+y) se toma como f(x) + f(y) y no habrá problema en que f duplique su argumento. O sea, Lineal considera que todas sus funciones son lineales, no las fuerza a ser lineales, sólo las trata como tales, lo cual es necesario para evitar el clonado, operación prohibida en computación cuántica, y es suficiente ya que lo interesante en Lineal es que puede encodear operadores cuánticos, que son siempre lineales.

Update: el paper fue acceptado en WoLLIC 2012. Acá dejo un post sobre eso.

Pueden bajar el paper libremente desde arXiv o desde su sitio final de publicación (si tienen acceso) en Springer.

Update 2: slides de un seminario pre-conferencia.

Non determinism through type isomorphism

(English below)

Con Gilles Dowek hemos enviado un nuevo artículo para revisión. Una versión muy preliminar de este artículo es lo que presentamos en la semana Enfoques Cuantitativos del LI2012.

Aquí dejo una traducción del título y resumen:

No determinismo por medio de isomorfismo de tipos 

Definimos una relación de equivalencia sobre proposiciones y un sistema de pruebas donde proposiciones equivalentes tienen la misma prueba. El sistema obtenido es similar a varios lambda-cálculo no determinísticos y algebraicos. Este sistema tiene preservación de tipos y normalización fuerte.

En las conclusiones del artículo se pueden ver varios problemas para trabajos futuros, y la posible conexión con los lenguajes cuánticos.

Actualización: El paper ha sido aceptado en LSFA 2012. La versión corregida se encuentra disponible en mi página web (próximamente en EPTCS) en EPTCS 113:137-144, 2013.

---

Gilles Dowek and I have just sent a paper for review. A very preliminary version of this paper is what we presented in the Quantitative Approaches week of LI2012.

Here is the abstract:

Non determinism through type isomorphism 

We define an equivalence relation on propositions and a proof system where equivalent propositions have the same proofs. The system obtained this way resembles several known non-deterministic and algebraic lambda-calculi. This system enjoys subject reduction and strong normalisation.

Update: The paper has been accepted in LSFA 2012. The corrected version is available for download from my web page. (soon at EPTCS) EPTCS 113:137-144, 2013.

WECIQ 2012

(English below)

Del 8 al 12 de Octubre, en la ciudad de Fortaleza, Brasil, se llevará a cabo el IV Workshop-Escuela en Computación e Información Cuántica - WECIQ 2012. Tuve la grata experiencia de asistir al primero de estos workshops, en 2006 (cuando aún era estudiante de la licenciatura), y hasta blogueé sobre ello!

La opinión que me generó por ese entonces, es la misma que tengo ahora: los brasileños son los punteros sudamericanos en computación cuántica, por lo cual un workshop nacional sobre estos temas, es sin lugar a dudas un buen lugar para asistir y conocer qué se está haciendo a nivel sudamericano en el área.

---

From 8 to 12 October, in Fortaleza, Brazil will be held the IV Worksop-School in Quantum Computation and Information - WECIQ 2012. I had the pleasure of attending the first of this series, in 2006 (while still an undergraduate), and I have even blogued about it!

My view at that time is the same that I have today: Brazil is the leading country in South America in quantum computation and information, so a Brazilian national workshop on these topics is, without doubt, a great place to go and see what  it is being done in South America in this field.

No-determinismo en llamada por valor, en una disciplina de tipos à la lógica lineal

La semana pasada hemos enviado un nuevo paper para revisión con Giulio Manzonetto y Michele Pagani. El título en inglés "Call-by-value non-determinism in a linear logic type discipline" (perdón por mi mala traducción al español). En este paper presentamos un sistema de tipos intersección, basado en lógica lineal, para un cálculo no determinista, donde si M y N son términos del cálculo, la elección no determinista entre ellos se expresa como M+N o M||N, dependiendo el tipo de convergencia que queramos: cada vez que hay una elección no determinista M+N, el sistema puede elegir entre uno o el otro. Con que uno de ambos converja, diremos que el término es convergente. En cambio, una elección no determinista M||N demandará que ambos términos converjan, por lo cual se continuará el cálculo hasta el final con ambas opciones en paralelo. Esto hace que, por ejemplo, si M y N son máquinas que toman un argumento R, la máquina no determinista M||N aplicada al argumento R se expresará mediante la reducción (M||N)R → MR||NR. En cambio, (M+N)R→MR o NR, ya que no nos interesan ambas opciones.

En la literatura estas dos opciones se conocen como may-convergence (+) y must-convergence (||). En este trabajo presentamos un sistema de tipos tal un término es convergente si y sólo si es tipable. A modo de ejemplo, si M es convergente: M+Y, donde Y→Y (o sea, Y no es convergente), tiene tipo en nuestro sistema, ya que el término M+Y puede converger ("may converge").

Más aún, el sistema de tipos cuenta con una medida, la cual nos da una cota de la cantidad de pasos necesarios para la convergencia (la cual es exacta si ciertas condiciones de minimalidad en el tipado se cumplen).

Estos modelos no deterministas se pueden considerar como una versión simplificada de un modelo cuántico, donde sólo interesa estudiar la superposición, sin tener en cuenta las amplitudes.

El borrador del paper estará disponible en mi página (mientras siga siendo sólo un borrador): dmp12.pdf.

Desde Beijing

(Post por Marcos Villagra)

Actualmente me encuentro en Beijing, llegué el 2 de marzo, y voy a estar hasta el 31 de marzo. Como no tengo acceso a Blogger desde aquí (eso incluye también a Facebook, Twitter, inclusive Wordpress!), estoy probando un nuevo sistema para escribir entradas vía e-mail. Asi que esta entrada la estoy escribiendo desde mi cliente de correo. Espero que cuando se publique salga todo bien formateado. Muchas gracias a Alejandro por indicarme como hacer esto.

Bueno, vine aquí porque mi universidad tiene un convenio de intercambio de estudiantes con la Universidad de Tsinghua. Muchos estudiantes de Tsinghua ya fueron a mi universidad, pero yo soy el primero que va a Tsinghua. Me encuentro actualmente continuando con mi estudios en communication complexity con Xiaoming Sun. De hecho ya tenemos un lindo teorema que vamos a seguir puliendo. La Universidad de Tsinghua es tal vez uno de los mejores lugares para estudiar este tema en el mundo, ya que aquí se encuentra trabajando como director del instituto el mismísimo, ganador del premio Turing, Andrew Chi-Chih Yao. También hay muchos otros expertos en comunicación. Yao fue el inventor del modelo de comunicación allá por finales de los años 70. Aunque ya lo vi caminando por ahí, no tuve la oportunidad de charlar con él.

También me encuentro visitando el Institute of Computing Technology de la Academia de Ciencias de China. La Academia de Ciencias es un conjunto de institutos de exclusivamente estudios graduados. Tienen varios institutos en prácticamente todas las áreas de las ciencias, biología, tienen como 10 institutos diferentes de física, matemáticas, ciencias de la computación, etc. La Academia de Ciencias de China también posee uno de los supercomputadores más grandes en el mundo. Actualmente están en el puesto 21 de la lista de Top500 Supercomputers. En el 2004, ellos estaban segundos. El primer día que llegué, me llevaron a un paseo por la sala donde está el supercomputador. Al ingresar, no solo me impresionó el tamaño de todas las máquinas, sino también el ruido que hacían. Apenas podía escuchar mi propia voz. Primera vez que entro en un lugar así, y la primera impresión que tuve fue que el lugar olía exactamente igual a cuando compras algún hardware nuevo, y al abrir la caja, sale ese olor a circuitos integrados nuevos.

Más abajo incluyo una fotografía que tomé de la entrada a la Ciudad Prohibida, el principal lugar turístico de todo Beijing.

Nature explicado (por NeoFronteras)

Este post cortito es para recomendar dos posts interesantes en NeoFronteras:

• Demuestran experimentalmente el límite de Landauer

El post explica el contexto del reciente artículo aparecido en Nature "Experimental verification of Landauer’s principle linking information and thermodynamics" (Verificación experimental del principio de Landauer relacionando información y termodinámica).
Es muy ameno para leer, como todo lo que publica NeoFronteras, y yo agregaría al final del artículo "Pero no tendría la posibilidad de olvidar... y ahí entra la computación reversible, con la computación cuántica como uno de sus exponentes más prometedores" (y así se entiende porqué lo linkeo en este blog) :-)

El segundo artículo, también en ese excelente blog, es:

• Sobre la interpretación del principio de Heisenberg

Otra muy amena explicación de otro reciente artículo de Nature "Experimental demonstration of a universally valid error–disturbance uncertainty relation in spin measurements" (Demostración experimental de una relación de incertidumbre de error-perturbación universalmente válida en las mediciones de espín).
Este está un poco menos relacionado con computación cuántica en sí, y más la interpretación de la mecánica cuántica.

Enjoy!

LI2012: los slides

(English below)
Los slides de mi presentación Equivalence on propositions and proofs en la semana Quantitative Approaches del evento Logic and Interactions 2012, están en línea.

Han subido prácticamente todos los slides, así que les recomiendo darse una vuelta por aquí. Hubo charlas muy interesantes en dos temas principales: computación cuántica (y modelos de la misma), y modelos semánticos de lógica lineal, con especial énfasis en los modelos de Thomas Ehrhard y el lambda-cálculo diferencial. En especial recomiendo ver los slides de Benoît Valiron (cuando los suban), que propone una extensión del modelo de Completely Positive Maps (CPM) que definió en su tesis doctoral, usando los modelos de Ehrhard.

---

The slides of my talk Equivalence on propositions and proofs in the Quantitative Approaches week of Logic and Interactions 2012, are online.

They have uploaded almost all the slides, so I recommend to take a look here. There has been very interesting talks, specially in two main topics: quantum computing (and its models), and semantical models of linear logic, with emphasis in Thomas Ehrhard's models and the differential lambda-calculus. In particular I recommend to see Benoît Valiron's slides (when they upload them), who propose an extension to the Completely Positive Maps (CPM) model, as he defined in his PhD thesis, using some machinery from Ehrhard's models.

A System F accounting for scalars @ LMCS

(Abajo en Español)

My first journal paper has been finally published. It is entitled A System F accounting for scalars and co-authored with Pablo Arrighi.

Before commenting about the paper itself, I want to highlight that it has been published by the journal Logical Methods in Computer Science, a high-class, peer-reviewed, open-access, free journal, published under the Creative Commons licence. This journal is managed by leader researchers in theoretical computer science (in particular, in logic), without any private editorial intervening. Why I want to point out these details? Because it is a living proof that researchers can do a pretty good job, without the need of enterprises such as Elsevier. And more importantly, it is a proof that science can be open!

Regarding to the paper, I have commented about it in this blog several times. The journal version of it, means that it has been extended to all its details, improved the motivations of it, and the reviewers have carefully read and made suggestions of how to improve the proofs and the text in general. This paper presents a type system for the linear-algebraic lambda-calculus, an extension of lambda-calculus that considers linear combination of terms, as terms. Such type system keep track of the amplitudes of the linear combination, to the point that it can be used to define a probabilistic type system.

---

Mi primer artículo en revista ha sido finalmente publicado. Se titula A System F accounting for scalars (Un Sistema F que considera escalares) y lo escribimos en conjunto con Pablo Arrighi.

Antes de comentar sobre el paper en sí, quiero resaltar que ha sido publicado por la revista Logical Methods in Computer Science (Métodos Lógicos en Ciencias de la Computación), una revista de alta calidad, con revisión por pares, la cual es gratis y de acceso libre, publicada bajo licencia Creative Commons. Esta revista es llevada a cabo por investigadores líderes en ciencias de la computación (en particular, en lógica), sin la intervención de ninguna editorial privada. Porqué quiero resaltar esos detalles? Porque es una prueba viviente de que los investigadores pueden hacer un muy buen trabajo, sin necesidad de empresas como Elsevier. Y más importante, es una prueba de que la ciencia puede ser abierta!

Con respecto al paper, he comentado sobre él en este blog varias veces. La versión para revista del mismo, significa que ha sido extendido a todos sus detalles, justificado mejor, y los revisores de la revista lo han leído cuidadosamente y marcado sugerencias de cómo mejorar las pruebas y el texto en general. El paper presenta un sistema de tipos para el cálculo lambda algebraico lineal, una extensión al cálculo lambda que considera la combinación lineal de términos, como términos. Tal sistema de tipos lleva un seguimiento de las amplitudes de las combinaciones lineal, al punto de poder ser usado para definir un sistema de tipos probabilístico.

TAMC 2012

La conferencia Theory and Applications of Models of Computation (TAMC'12) de este año ya publicó su lista de papers aceptados. Solo hay un paper en algo cuántico, y resulta que es mi paper que ya había explicado aquí.

Esta es una conferencia general de teoría, y abarca todas las áreas de ciencias de la computación (teórica). La conferencia va estar muy interesante, ya que forma parte de los festejos por los 100 años de Alan Turing. La lista de conferencistas para esta celebración incluye a Andrew Yao, John Hopcroft, Richard Karp, Jon Kleinberg, Butler Lampson, y otros. Todos son respetados científicos del área y varios de ellos poseedores del premio Turing. Así que, la conferencia va a estar muy linda. Y Beijing será un lugar muy interesante para visitar.

Sin embargo, primero tengo que ir a Beijing en marzo. Voy a darme un paseo por la Universidad de Tsinghua (la universidad más grande e importante de China), y la Academia de Ciencias de China.

12th Canadian Summer School on Quantum Information

De vuelta este año se hace la escuela canadiense en información cuántica. Quienes estén interesados, tienen tiempo hasta el 14 de mayo para registrarse. También hay apoyo financiero para participantes.

Alejandro y yo ya estuvimos en otras ediciones como lo pueden ver aquí y aquí.

Carta de John Nash

John Nash es uno de los matemáticos más importantes en nuestros días. Su principal contribución fue el descubrimiento del teorema del equilibrio para juegos de suma-cero allá por los años 50. Ese trabajo le valió el premio Nobel en economía en 1994.

Sus trabajos tienen mucha influencia hoy en día en ciencias de la computación por sus aplicaciones en un área relativamente nueva, Teoría de Juegos Computacional. En esta área Noam Nisan es uno de los principales científicos. En realidad Nisan hizo contribuciones seminales en varias áreas de ciencias de la computación.

Sucede que Noam Nisan tiene un blog, y allí hizo un anuncio bastante sorprendente. John Nash había enviado una carta a la NSA (National Security Agency) de USA en 1955 con la intención de que se interesen en una máquina de encriptación que había diseñado. En esa carta, Nash, escribió sobre sus trabajos en teoría de juegos, y mencionó también sus ideas sobre como construir protocolos criptográficos basados en la dificultad de problemas computacionales. Nash había anticipado, en 1955, ideas que recién se realizarían más o menos 20 años después, en lo que conocemos como criptografía moderna. También había anticipado en 1 año la pregunta que hizo Gödel a Von Neumman en otra famosa carta.

Nash básicamente ya estuvo pensando en preguntas que hoy corresponden a la teoría de complejidad computacional antes de su establecimiento, más o menos unos 10 años antes. Simplemente me parece increíble. Nash siempre fue considerado un matemático extraordinario, pero esto es realmente sorprendente. Cuando uno lee un libro de complejidad computacional, siempre los autores hacen referencia a la carta de Gödel. Pero ahora creo que vamos a tener que agregar a otro personaje en esta historia.

Quantum Programming Languages in South Brazil

The main focus of our work is the development of high-level quantum programming languages. More specifically, we work with the design and semantics of functional quantum programming languages. Basically, we start with simple-typed lambda calculus. Then, on top of that we add a non-deterministic monad for quantum parallelism, and finally we add arrows for quantum measurements. The work has a more theoretical flavour in the investigation of the categorical models and also has a more practical flavour in the use of the language for the investigation of quantum algorithms. We have a prototype implementation of the language in Haskell. Our first motivation is to try to understand quantum computing using well known models and tools normally used in the design and semantics of traditional (not quantum) functional programming languages. Second, we hope our work can approximate the computer science (and informatics in general) community to quantum computing. We hope that for a cs student would be easier to understand quantum computing and to develop quantum algorithms using a high-level quantum programming language than to use quantum circuits or linear algebra. Of course this is a under development work and there are many things to be done still, as higher-order, high-level quantum data structures, quantum algorithms, etc.
Nowadays, we work at Federal University of Santa Maria (UFSM) in the South of Brazil, where we have undergraduate courses and also a cs master course.
Here one can find some of our publications.

Banear Elsevier

Les recomiendo este artículo en el blog de Tim Gowers (un medalla Fields y blogger), donde expresa su preocupación sobre las revistas de Elsevier y el apoyo de esta editorial a los proyectos de ley estadounidenses SOPA, PIPA y Research Works Act (esta última es un proyecto para prohibir las publicaciones científicas estadounidenses en revistas de libre acceso).

Hay una declaración de intención donde, hasta ahora, 460 científicos han (hemos!) dado su apoyo diciendo que o bien no van a publicar, o no van a hacer reviews, o no van a participar en la edición de revistas de esa editorial (o ninguna de las 3), hasta que cambie sus políticas. Se pueden ver algunas personalidades muy reconocidas entre los firmantes, como por ejemplo Jean-Louis Krivine, entre muchos otros.

Update: Agrego más cosas al post.

En el post de Tim Gowers menciona otros 3 puntos en contra de Elsevier, que resumidamente son:

1. Precios extremadamente elevados

2. La justificación de esos precios con que te tenés que suscribir a todas sus revistas en algún tema, o a ninguna (no podés elegir a qué revistas suscribirte)

3. Cuando una biblioteca trata de negociar el precio, Elsevier directamente les corta el acceso a todas sus publicaciones.

Y lo más importante: los papers los escriben científicos (no pagados por Elsevier), los referean los mismos científicos (tampoco se recibe retribución por eso) y en la mayoría de los casos, los editan los mismos científicos, también gratuitamente. Porqué Elsevier luego les vende las publicaciones a las mismas instituciones que pagan a esos científicos? Pues no tiene sentido alguno. Hace mucho tiempo, el trabajo de Elsevier era distribuir las publicaciones, así llegaba a las distintas universidades y centros de investigación. Hoy en día, con Internet, no sólo es innecesario su trabajo, es contraproducente, ya que quien no haya pagado el acceso, no puede acceder a la publicación (y Elsevier en particular tiene reglas muy duras en cuanto a no permitir a los autores poner una copia gratuitamente en la web).

Por eso están proliferando cada vez más las publicaciones de libre acceso, como por ejemplo Logical Methods in Computer Science (hay muchas más, sólo menciono el ejemplo más relevante a mi trabajo), que cuenta con un cuerpo editorial del más alto nivel en el área, tiene un proceso de review muy riguroso, y la publicación se hace online, de libre acceso y con licencia Creative Commons. Hay muchísimas revistas, en casi cualquier área de la ciencia, de acceso gratuito. Aquí dejo un sitio que se encarga de listarlas.

Y la pregunta obligada es: Realmente necesitamos a Elsevier?

Logic and interactions 2012

Desde el 30 de Enero al 2 de Marzo, se llevará a cabo en la ciudad de Marsella (Francia) el evento Lógica e interacciones. Se trata de un evento de 5 semanas que reunirá investigadores en muchas áreas de lógica computacional.

En particular la cuarta semana, del 20 al 24 de Febrero, estará dedicada a "Enfoques Cuantitativos". Los organizadores de dicha semana son Michele Pagani, Simon Perdrix, Peter Selinger y Christine Tasson. Habrá cursos dictados por Thomas Ehrhard, Elham Kashefi, Prakash Panangaden y Christine Tasson. Además se contará con numerosos oradores invitados de renombre, y algunas contribuciones. Yo envié una contribución, la cual fue aceptada y la presentaré el jueves 23 a las 11:20. Aquí dejo los datos de mi presentación (la versión en inglés la pueden consultar en la página):

Título: 
Equivalencia entre proposiciones y pruebas
(trabajo conjunto con Gilles Dowek)

Resumen (traducción):

Sabemos que las proposiciones A∧B y B∧A son equiprobables: si una es probable, la otra también lo es, sin embargo no tienen la misma prueba. Aquí diseñamos un sistema de prueba tal que tengan la misma prueba, o sea, tomamos el cociente del conjunto de proposiciones por la relación generada por la conmutatividad de la conjunción, y definimos pruebas para elementos en este cociente. El cálculo obtenido es similar al fragmento aditivo de los cálculos algebraicos, más un proyector no determinístico.

Update: Los slides.

Update: Una versión mucho más desarrollada y terminada de este trabajo, fue aceptado en LSFA 2012. Aquí dejo el respectivo post.

Preparación para SODA 2012

El martes 17 de enero comienza SODA'12 en Kyoto. El hotel tiene muy linda pinta. Queda más o menos a 1 hora de camino desde donde vivo, asi que pienso ir y venir durante los 3 días que dure. Voy a intentar hacer un mini-reporte sobre los 3 días más adelante. Además voy a llevar mi super cámara Nikkon.

Voy a estar principalmente enfocado en las presentaciones sobre comunicación. Hay algunas muy interesantes también relacionadas a streaming. Sobre computación cuántica solo va a haber una presentación de Francois Le Gall sobre multiplicación de matrices.

Para el viaje en tren de 1 hora (2 horas ída y vuelta), me estoy llevando el libro Algebraic Complexity Theory.

Back Online!

Bueno, ya era hora de escribir algo de vuelta. Mucho pasó desde la última entrada. En particular, el fantástico anuncio de CERN sobre sus últimos experimentos en búsqueda del bosson de Higgs. Alguno siempre me pregunta por qué es tan importante descubrir esa partícula. Yo trato de explicar en los términos que yo entiendo, porque no soy físico. Este vídeo es fabuloso. Mejor que esto ya no se puede explicar. Es un poco largo.

Después también la conferencia QIP 2012 que se llevó a cabo en Montreal en diciembre. Lástima que este año no colgaron los videos en la página web como en años anteriores. Aún así, hay un excelente resumen en The Quantum Pontiff.

También, los últimos avances después de más de 20 años en multiplicación de matrices bien reportado en Shtetl Optimized.

Lo que me mantuvo ocupado, en especial los últimos 2 meses, es el nuevo paper en el que estaba trabajando. De hecho, ya había dado un pista en este post anterior. Es sobre una nueva técnica para encontrar cotas inferiores para protocolos de comunicación cuántica. En este post había explicado el modelo de comunicación. Bueno, después de mucho, mucho (y mucho) trabajo, por fin pude hacer lo que me propuse.

Uno de los problemas principales en esta área era demostrar un gap en la complejidad para modelos de comunicación con 3 o más jugadores. Un gap quiere decir, encontrar alguna función que clásicamente requiera ≥ X recursos computacionales (tiempo, espacio, etc), y quánticamente requiera a lo más estrictamente menor que X recursos computacionales. Por ejemplo, en búsqueda no-estructurada sabemos que clásicamente requerimos Ω(n) accesos a un oráculo, pero O(√n) accesos a un oráculo cuántico. Entonces acá hay un gap cuadrático.

En el caso de comunicación entre 2 jugadores, ya tenemos varios gaps exponenciales y cuadráticos. Para 3 o más jugadores no teníamos nada. Y de hecho este es un problema bastante difícil, principalmente porque las ténicas para cotas inferiores en modelos clásicos de multiparty communication son generalmente muy débiles, i.e., las cotas inferiores no son óptimas, y muchas veces están lejos de ser óptimas. Entonces ¿cómo hacer para demostrar un gap en comunicación multiparty? El truco está primero en relajar el modelo, por ejemplo, en lugar de considerar modelos de comunicación con bounded-error, considerar un modelo no-determinístico. Segundo, tener una nueva técnica.

Eso fue lo que hice en este trabajo. Primero consideramos un modelo de comunicación no-determinístico, y acotamos por arriba y por abajo utilizando el concepto de tensor rank. Esto luego lo aplicamos al problema de multiplicación de matrices y pudimos sacar un gap super-polinomial, el primero en multiparty communication.

Generalmente estos modelos no-determinísticos no son realistas, pero muchas veces se usan para hacer predicciones en modelos reales. Por ejemplo, P vs NP, i.e., tiempo determinístico vs tiempo no-determinístico. En este trabajo también hicimos algunas aplicaciones a comunicaciones cuánticas exactas, i.e., donde la respuesta se obtiene con probabilidad 1.

Al final lo mandé a una conferencia, y ahora estoy preparando la versión full para subir a arXiv y a ECCC y preparar la versión journal. Apenas lo tengo lo pondré aquí.

Actualización(14/Ene/2012): Aquí está la versión en ECCC.