Es un placer anunciarles que mañana miércoles *6 de setiembre* a las
18:00, el Prof. Alejandro Díaz-Caro (Universidad de Buenos Aires &
Universidad de Quilmes) nos dará una charla sobre el siguiente tema:
Sup: Un nuevo conectivo lógico para no determinismo.
En esta charla, voy a resumir los resultados de los papers [1] a [4]. En
[1] introdujimos el conectivo lógico ⊙ ("sup") en Deducción Natural, el
cual coincide con la conjunción, pero agrega además la regla de eliminación
de la disyunción, con un cut-elimination no-determinista. Además, se
agregan dos términos de prueba, una suma y un producto por escalar, lo cual
permite codificar directamente algoritmos cuánticos, usando el conectivo
sup para codificar la medición cuántica. En [2] mostramos que, para el
fragmento sin "sup" pero con la suma y el producto por escalar, empleando
tipos lineales, la linealidad se puede expresar directamente en el los
términos de prueba: la prueba t(u+v) se demuestra equivalente a la prueba
t(u)+t(v), y la prueba t(a∙u) se muestra equivalente a a∙t(u). Además,
mostramos que el conectivo "sup" corresponde a la conjunción aditiva, con
una regla de eliminación que corresponde a la disyunción aditiva. En [3]
damos un modelo categórico para el cálculo lineal sin "sup", en la
categoría SM de semimódulos sobre un semianillo conmutativo fijo.
Finalmente, en [4] mostramos que la misma categoría permite modelar el
conectivo "sup", dando una alternativa para lenguajes no deterministas a la
Powerset Monad de Moggi, en contextos como la categoría SM, en donde dicha
mónada no se puede utilizar.
Referencias:
[1] A. Díaz-Caro y G. Dowek. A new connective in Natural Deduction and its
application to quantum computing. Theoretical Computer Science 957:113840,
2023.
[2] A. Díaz-Caro y G. Dowek. Linear Lambda-Calculus is Linear. (FSCD 2022)
- LIPIcs 228:21, 2022. Version journal en revisión: arXiv:2201.11221, 2023.
[3] A. Díaz-Caro y O. Malherbe. Semimodules and the (syntactically-)linear
lambda calculus. En revisión. arXiv:2205.02142, 2022.
[4] A. Díaz-Caro y O. Malherbe. Non-determinisn in a Linear Logic type
discipline: A concrete categorical perspective. En progreso avanzado (por
subir a arXiv muy próximamente).
La charla tendrá lugar en el salón C11 (Aulario, primer piso)