Measurements and confluence in quantum lambda calculi with explicit qubits

International audience This paper demonstrates how to add a measurement operator to quantum lambda-calculi. A proof of the consistency of the semantics is given through a proof of confluence presented in a sufficiently general way to allow this technique to be used for other languages. The method de...

Full description

Bibliographic Details
Published in:Electronic Notes in Theoretical Computer Science
Main Authors: Díaz-Caro, Alejandro, Arrighi, Pablo, Gadella, Manuel, Grattage, Jonathan
Other Authors: Departamento de Ciencias de la Computación, Departamento de Ciencias de la Computación Rosario (DCC), Facultad de Ciencias Exactas, Ingenieria y Agrimensura Rosario (FCEIA), Universidad Nacional de Rosario Santa Fe -Universidad Nacional de Rosario Santa Fe -Facultad de Ciencias Exactas, Ingenieria y Agrimensura Rosario (FCEIA), Universidad Nacional de Rosario Santa Fe -Universidad Nacional de Rosario Santa Fe, Calculs algorithmes programmes et preuves (CAPP), Laboratoire d'Informatique de Grenoble (LIG), Université Pierre Mendès France - Grenoble 2 (UPMF)-Université Joseph Fourier - Grenoble 1 (UJF)-Institut polytechnique de Grenoble - Grenoble Institute of Technology (Grenoble INP )-Institut National Polytechnique de Grenoble (INPG)-Centre National de la Recherche Scientifique (CNRS)-Université Pierre Mendès France - Grenoble 2 (UPMF)-Université Joseph Fourier - Grenoble 1 (UJF)-Institut polytechnique de Grenoble - Grenoble Institute of Technology (Grenoble INP )-Institut National Polytechnique de Grenoble (INPG)-Centre National de la Recherche Scientifique (CNRS), Departamento de Física Teórica, Atómica y Óptica, Universidad de Valladolid Valladolid (UVa), Université Pierre Mendès France - Grenoble 2 (UPMF)-Université Joseph Fourier - Grenoble 1 (UJF)-Institut polytechnique de Grenoble - Grenoble Institute of Technology (Grenoble INP )-Institut National Polytechnique de Grenoble (INPG)-Centre National de la Recherche Scientifique (CNRS), Bob Coecke and Ian Mackie and Prakash Panangaden and Peter Selinger
Format: Conference Object
Language:English
Published: HAL CCSD 2008
Subjects:
Online Access:https://hal.inria.fr/hal-00924875
https://doi.org/10.1016/j.entcs.2011.01.006
Description
Summary:International audience This paper demonstrates how to add a measurement operator to quantum lambda-calculi. A proof of the consistency of the semantics is given through a proof of confluence presented in a sufficiently general way to allow this technique to be used for other languages. The method described here may be applied to probabilistic rewrite systems in general, and to add measurement to more complex languages such as QML or Lineal, which is the subject of further research.