11 de agosto de 2015

Isomorfismos como igualdades: Proyectando funciones y mejorando la aplicación parcial a través de una implementación de λ⁺

El título de este post es el título de un paper (bueno, su traducción) que acabamos de terminar de escribir y enviar a una conferencia con Pablo E. Martínez López (o Fidel, como lo conoce todo el mundo).

En este paper proponemos una implementación de λ⁺ (un cálculo del que ya he hablado varias veces en este blog, que desarrollamos con Gilles Dowek). λ⁺ tiene la característica de que toma los isomorfismos de tipos y los considera igualdades. Por ejemplo, una función que toma dos argumentos es igual a una función que toma un par, y una función que retorna dos argumentos es igual a dos funciones, porque A⇒B⇒C es isomorfo a (A∧B)⇒C y A⇒(B∧C) es isomorfo a (A⇒B)∧(A⇒C).

El sistema de reescritura de λ⁺ utiliza reescritura modulo una relación de equivalencia, lo cual hace que implementar un lenguaje con esas características no sea trivial. Y eso es exactamente lo que proponemos en este nuevo paper. Además, extendemos λ⁺ con números naturales y recursión general, y, usando un resultado clásico para dividir recursiones mutuas (teorema de Bekić), junto a las características de λ⁺, logramos una forma interesante de transformación de programas: podemos, por ejemplo, definir una función recursiva que calcula dos valores y luego proyectar el valor que nos interesa... sólo que el programa va a hacer la proyección antes de recibir sus argumentos, proyectando la función y transformándola en una función que sólo calcula el valor que nos interesa.

Otra propiedad interesante es que la curryficación, llevada al extremo, junto a la asociatividad y conmutatividad, hacen que tengamos una forma de aplicación parcial muy potente: una función que recibe más de un argumento, puede recibir cualquiera de ellos en cualquier orden.

Bueno, les dejo el paper tal como lo acabamos de enviar (aún debe ser revisado por los reviewers):

14 de julio de 2015

Workshop INFINIS

Este viernes 17 de julio se realizará un Workshop en la Universidad de Buenos Aires, organizado por el Laboratorio Internacional Asociado INFINIS, un laboratorio en cooperación entre la Universidad de Buenos Aires y el CONICET con la Université Paris 7 y el CNRS.

Les dejo el link al programa del workshop en la página del laboratorio:

Yo voy a dar una charla, básicamente la misma charla que dí en Rosario en junio, sólo que en inglés :-)

Update: Dejo los slides

2 de julio de 2015

Charla en el Workshop on Physics and Information

El lunes pasado fui invitado a dar una charla en el Workshop on Physics and Information que se llevó acabo en el Institut Henri Poincaré de París, ciudad en la que estoy desde Mayo y hasta fin de Julio trabajando con Sophie Laplante, de LIAFA, en temas de no-localidad y quantum communication complexity.

Acá les dejo el título y resumen de la charla:

Consequences of the Physical CTT over experimental setups in quantum physics
We study the limitations that the physical Church-Turing thesis imposes when performing experimental verifications of quantum theory. First, we show that different preparations of the (theoretically) same proper mixed state are distinguishable if computable. Then, we show that using independent PRNGs to choose the inputs for a Bell tests is not enough to observe a proper Bell inequality violation. That is, we give a local model that reproduces any correlations arising from a Bell scenario in which the measurement choices were made following algorithms.

Y estas son las diapositivas: