Pasar al contenido principal

 Sup: Un nuevo conectivo lógico para no determinismo.

Fecha de inicio
Fecha de fin

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)