24 de febrero de 2015

Video de mi charla en las Jornadas de Ciencias de la Computación

Los organizadores de las JCC acaban de subir el video de mi charla (acá abajo). También están los videos de las demás charlas, que pueden ver aquí.

Las Jornadas de Ciencias de la Computación es un evento que se hace año a año en Rosario, organizada por y para los estudiantes de la Licenciatura en Ciencias de la Computación.



Abstract de la charla: Proponemos un sistema de pruebas para lógica proposicional en el cual proposiciones isomorfas son consideradas como iguales (en el sentido de que sus respectivas pruebas son intercambiables).
Por ejemplo, A implica (B y C) es isomorfo a A implica B y A implica C. Si consideramos un sistema de pruebas módulo este tipo de isomorfismos, desde el punto de vista del cálculo (o del sistema de pruebas), una función que toma un argumento y devuelve un par, es equivalente (o "igual" si se quiere, para algún concepto de igualdad) a un par de funciones, cada una tomando el mismo argumento, y devolviendo sólo un elemento del par. Por lo tanto, también se podría, por ejemplo, proyectar un elemento de un par que será resultado de la aplicación de una función... antes de aplicar la función, proyectando sólo una parte de la misma. Esto puede trae aparejado una simplificación importante del cómputo.
En una lógica proposicional que sólo cuente con conjunción (no-idempotente) e implicación, existen sólo cuatro isomorfismos básicos, a partir de los cuales pueden derivarse los demás. Estos cuatro isomorfismos, al considerarlos igualdades, generan un cálculo interesante, no-determinista, relacionado con otros cálculos en la literatura.
El paper completo lo pueden bajar de acá. Aún no está publicado, está en proceso de publicación en la revista Theoretical Computer Science.

18 de febrero de 2015

Material de mi curso en la Escuela de Verano de Río Cuarto

Terminó la Escuela de Verano de Ciencias Informáticas de Río Cuarto. Esta es una escuela que se hace cada año, destinada principalmente a estudiantes de grado de todo el país. Allí dí un curso sobre fundamentos de lenguajes de programación para computación cuántica (2 días de introducción a computación cuántica, 1 de introducción a lambda-cálculo y 1 sobre lenguajes en el paradigma "control clásico / datos cuánticos" y 1 en el paradigma "control y datos cuánticos").


Por supuesto es un curso introductorio, si quieren profundizar, allí mismo tienen bibliografía que les servirá para ir más a fondo.



Update: Al parecer la página de la RIO está caída, así que dejo el material acá:
(es un paquete comprimido que incluye los apuntes de los 2 primeros días, los slides de los 5 días, una página con ejercicios introductorios de lambda cálculo y el examen).

17 de febrero de 2015

Temas de tesis de licenciatura y doctorado

Buenas,

Como muchos de los lectores habituales del blog sabrán, estoy de vuelta en Argentina. Soy Profesor Adjunto en la Universidad Nacional de Quilmes (en Bernal, a unos 20kms de Buenos Aires). Y ahora que estoy instalado, estoy buscando estudiantes para dirigir tesis de Licenciatura y de Doctorado. Acá les detallo algunos trabajos que se me ocurren (un pequeño resúmen, para discutir, ampliar y debatir). Por supuesto siempre se pueden modificar, incluso pueden surgir trabajos que vengan del tesista, no hace falta que sea uno de la lista. Pero tiro un par de propuestas para ejemplificar mis intereses.

Doy dos para licenciatura (LIC) y uno para tesis de doctorado (DOC). La idea es que un trabajo de licenciatura debe poder realizarse en unos 6 meses, por lo tanto son cosas que tengo certeza de que se pueden hacer (lo cual no significa que hacerlo sea sencillo, pero sí que vamos a arribar a buen puerto y tendremos algo para publicar), mientras que la propuesta para tesis de doctorado es para desarrollar en 5 años, por lo cual sólo doy una idea de la dirección a seguir, con lo cual arrancar, y que puede ir tomando nuevos rumbos de acuerdo a lo que vayamos descubriendo.

Si les interesa algún tema de los detallados abajo, o algún otro que se les ocurra a ustedes, los datos de contacto están en mi página personal. Escríbanme o llamenmé y me envían un CV y me dicen qué tema les interesa, cuándo podrían arrancar y comenzamos a ver la parte administrativa formal de sus respectivas universidades.

Aclaro que el candidato ideal no es quien sepa todos los temas de los que habla la descripción de la propuesta de tesis, sino quien más demuestre interés y ganas de trabajar. Los temas se aprenden (para eso es la tesis).



(LIC) Confluencia en reescritura probabilista
Descripción:
Los sistemas de reescritura abstractos probabilistas (PARS por sus siglas en inglés) asocian a cada objeto diversos objetos y una probabilidad para cada uno. Así, un objeto A puede reescribir a B con probabilidad 1/4 y a C con probabilidad 3/4. La propiedad de confluencia dice que si A reescribe en uno o más pasos a A1 y también, siguiendo otro camino, a A2, entonces A1 y A2 reescriben a un nuevo objeto A'. Por lo tanto, un PARS no es necesariamente confluente (si A reescribe a B y C con ciertas probabilidades, B y C pueden ser objetos diferentes sin un reducto en común).

Este proyecto se trata de estudiar los PARS conocidos y proponer un resultado de confluencia para el ARS asociado al PARS, en el cual en lugar de reescribir A a B con probabilidad 1/4 y a C con probabilidad 3/4, reescribe {(A,1)} a {(B,1/4), (C, 3/4)} determinísticamente.

Un resultado preliminar en este sentido fue publicado en el workshop internacional Quantum Phisics and Logic [1]. La idea de esta tesina es completar dicho trabajo, para el caso genérico de los PARS. El plan es poder obtener un resultado publicable en alguna una revista internacional.

[1] Measurements and confluence in quantum lambda calculi with explicit qubits. Pablo Arrighi, Alejandro Díaz-Caro, Manuel Gadella y Jonathan J. Grattage. ENTCS 270(1):59-74, 2011



(LIC) Operador de punto fijo para el lambda cálculo vectorial
Descripción:
El lambda cálculo vectorial [2] es una extensión a lambda cálculo donde combinaciones lineales de términos, son también términos. Dicho cálculo fue pensado para computación cuántica: así un valor no es sólo una variable o una abstracción, sino también las combinaciones lineales de ellos, es decir: vectores dentro de un espacio vectorial de dimensión infinita. Limitando los valores posibles (los elementos de la base), se puede codificar espacios vectoriales de dimensión finita (como el espacio de n-qubits, por ejemplo).

El sistema de tipos del lambda cálculo vectorial es polimórfico, y tiene la propiedad de normalización fuerte, es decir: todo término tipado termina. Ello evita que aparezcan sumas infinitas (y por lo tanto, formas indeterminadas como infinito menos infinito). En este proyecto se busca agregarle un operador de punto fijo al cálculo vectorial, de manera de recuperar la recursión, pero teniendo en cuenta no introducir sumas infinitas (o al menos formas indeterminadas que incluyan infinito).

[2] The vectorial lambda-calculus. Pablo Arrighi, Alejandro Díaz-Caro y Benoît Valiron. arXiv:1308.1138, 2013



(DOC) Realisabilidad en computación cuántica con control y datos cuánticos
Descripción:
La realisabilidad es una rama de la teoría de la demostración que define una relación lógica entre las fórmulas de un sistema y los programas de un modelo de cálculo. Fue introducida por Kleene en los años 40 y luego extendida, hasta llegar a convertirse en una generalización de la correspondencia de Curry-Howard.

El proyecto se trata de usar realisabilidad para determinar una lógica cuántica, en el sentido de que las pruebas de las fórmulas lógicas, sean programas cuánticos.