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.
