Título: Una Extensión Composicional de λρ° mediante Descomposición de Pauli
Director: Alejandro Díaz-Caro
Jurados: Rafael Romero

                Romain Péchoux

Resumen:

Extendemos el cálculo lambda cuántico λρ°, un cálculo que manipula matrices de densidad con control probabilístico, con un operador let. El cálculo original, propuesto por Díaz-Caro, permite la expresión de algoritmos cuánticos donde los datos se representan mediante matrices de densidad en lugar de vectores de estado, sin necesidad de llevar un registro separado de dichos datos. Sin embargo, carece de un mecanismo para descomponer un estado cuántico de múltiples qubits en sus componentes individuales. Nuestra extensión introduce un constructor let x⊗ⁿ = ρⁿ in t que, mediante la descomposición de Pauli y la descomposición espectral de las matrices de Pauli, expresa cualquier estado de n qubits como combinación lineal de productos tensoriales de estados de un único qubit. Esto permite a los programas operar sobre qubits individuales de un sistema compuesto de manera algebraicamente coherente. Adicionalmente, presentamos una interpretación semántica simplificada de λρ° que elimina el seguimiento de los resultados de medición. Presentamos la gramática extendida, el sistema de reescritura, el sistema de tipos y la interpretación semántica del cálculo resultante, y demostramos las propiedades fundamentales de Subject Reduction, Progress, Strong Normalisation, Soundness y Adequacy. Además, mostramos que cuando una variable ligada por el let no aparece libre en el cuerpo, el constructor computa correctamente la traza parcial sobre los qubits descartados, respetando así el teorema de no-borrado cuántico.

Idioma de la defensa: Inglés