Título: Agregando punto fijo a una extensión cuántica de lambda cálculo con matrices de densidad

Director: Alejandro Díaz-Caro
Codirector: Hernán Melgratti

Jurados: Pablo Barenbaum. Santiago Figueira

Fecha y hora: Viernes 28 de agosto, 10 hs

Lugar: https://www.youtube.com/watch?v=kbqSuZ2zEF8

Resumen:

El cálculo λρ presentado por Díaz-Caro en 2017 es una extensión cuántica del lambda cálculo que usa matrices de densidad. Estas matrices permiten representar estados mixtos de conjuntos de bits cuánticos. El cálculo modificado λρ⁰ generaliza las matrices de densidad a sumatorias algebraicas de términos. Ambos cálculos tienen definida una semántica denotacional compartida.

Este trabajo representa un primer paso hacia el agregado de punto fijo al cálculo λρ⁰. Definimos una extensión con punto fijo en el límite y otra intermedia, con punto fijo incremental. La semántica denotacional fue redefinida respecto a la original para dar a los dominios estructura de orden parcial completo sobre matrices positivas. La demostración de adecuación depende de dos conjeturas dejadas para trabajo futuro.

Suponiendo correcta la definición de la semántica, esto permite probar la existencia del límite del punto fijo incremental gracias a la estructura de orden parcial completo. La interpretación del punto fijo puede definirse entonces como el límite de una secuencia creciente y acotada de interpretaciones de términos en el dominio.