Extensión de Lambda-S para diferentes bases de medición

Abstract

El enfoque de control cuántico para los lenguajes de programación comenzó a ganar popularidad debido al Quantum Switch (Procopio et al., 2015; Rubino et al., 2017). Sin embargo, los primeros desarrollos en el diseño de lenguajes de programación lo incluyeron como una construcción condicional (Altenkirch et al., 2005), o como combinaciones lineales de programas cuánticos en el cálculo lambda (Arrighi y Dowek, 2017; Arrighi; Díaz-Caro et al., 2017). La idea es que el flujo de control del programa no sea sólo una descripción de puertas cuánticas aplicadas a qubits, y por tanto, una mera manipulación clásica de circuitos cuánticos, sino que los programas describan la aplicación o no de circuitos según una partícula cuántica. Lineal (Arrighi y Dowek, 2017) fue uno de los primeros lenguajes que tuvo como objetivo desarrollar un cálculo lambda de control cuántico. Es un cálculo lambda sin tipos extendido con superposiciones lineales arbitrarias. Las reglas de reescritura garantizan la confluencia y se toma una forma canónica como forma normal de los términos. Para evitar la clonación, se considera una estrategia call-by-base: se puede aplicar una abstracción λx.t a una superposición de valores (α.v +β.w) que producen α.(λx.t)v +β.(λx.t)w. De esta manera, no sólo se evita la clonación, sino que además todas las abstracciones son lineales por construcción. Esto permite expresar matrices y vectores y, por tanto, programas cuánticos, pero también mapas no unitarios y, por supuesto, vectores no normalizados. Cuando se trata de medición, la estrategia call-by-base no funciona. De hecho, si λx.πx es una abstracción que mide su argumento, entonces (λx.πx)(α.v +β.w) se reduce a α.(λx.πx)v + β.(λx.πx)w y no funcionaría como se esperaba, sino como una identidad. Así, se ha propuesto una solución guiada por tipos en el lenguaje Lambda-S (Díaz-Caro; Dowek et al., 2019). La idea es que una superposición de tipo A se marca como S(A) y, por lo tanto, la beta-reducción puede guiarse por el tipo de argumento. Si B es el tipo de qubits básicos ⋃︀0̃︀ y ⋃︀1̃︀, S(B) es el tipo de todos los qubits. Entonces, (λxB.t)(α.v + β.w) reducirá con call-by-base, mientras que (λxSB.t)(α.v +β.w) utilizará call-by-name. Sin embargo, en el último se debe realizar una verificación de linealidad: t no puede usar su variable más de una vez. En cierto sentido, la modalidad S se ve como lo opuesto a la modalidad ! en lógica lineal: los tipos !A en lógica lineal son aquellos que se pueden duplicar, mientras que los tipos S(A) en Lambda-S son aquellos que no se pueden duplicar. La utilidad de este lenguaje para la computación cuántica puede ser cuestionada, ya que se puede escribir cualquier superposición, incluso si la norma no es 1, y se puede expresar cualquier abstracción lineal, incluso si no es un mapa unitario válido. Sin embargo, se ha demostrado el refinamiento de Lambda-S, utilizando técnicas de realizabilidad, en (Díaz-Caro; Guillermo et al., 2019; Díaz-Caro y Malherbe, 2022). Se puede agregar una restricción al sistema de tipos para garantizar la unitaridad. Por lo tanto, podemos centrarnos en Lambda-S ya que sabemos que existe tal refinamiento. La principal particularidad de Lambda-S es el hecho de que permite duplicar términos base. De hecho, la duplicación de ⋃︀0̃︀ o ⋃︀1̃︀ puede lograrse mediante un CNOT. Más aún, cualquier qubit es duplicable, tan pronto como sabemos a qué base pertenece. Por lo tanto, en este trabajo, se presenta Lambda-SX como una extensión de Lambda-S para rastrear no solo la base computacional, con el tipo B, sino también una base de Hadamard representada con X. Tener más bases como tipos implica un lenguaje de programación donde tengamos más datos clásicos, ya que son copiables, medibles, etc.