1. Concrete Categorical Model of a Quantum Circuit Description Language with Measurement
- Author
-
Lee, Dongho, Perrelle, Valentin, Valiron, Benoît, Xu, Zhaowei, Laboratoire Méthodes Formelles (LMF), Institut National de Recherche en Informatique et en Automatique (Inria)-CentraleSupélec-Université Paris-Saclay-Centre National de la Recherche Scientifique (CNRS)-Ecole Normale Supérieure Paris-Saclay (ENS Paris Saclay), Laboratoire Sûreté des Logiciels (LSL), Département Ingénierie Logiciels et Systèmes (DILS), Laboratoire d'Intégration des Systèmes et des Technologies (LIST (CEA)), Direction de Recherche Technologique (CEA) (DRT (CEA)), Commissariat à l'énergie atomique et aux énergies alternatives (CEA)-Commissariat à l'énergie atomique et aux énergies alternatives (CEA)-Direction de Recherche Technologique (CEA) (DRT (CEA)), Commissariat à l'énergie atomique et aux énergies alternatives (CEA)-Commissariat à l'énergie atomique et aux énergies alternatives (CEA)-Université Paris-Saclay-Laboratoire d'Intégration des Systèmes et des Technologies (LIST (CEA)), Commissariat à l'énergie atomique et aux énergies alternatives (CEA)-Commissariat à l'énergie atomique et aux énergies alternatives (CEA)-Université Paris-Saclay, and CentraleSupélec
- Subjects
FOS: Computer and information sciences ,Theory of computation ��� Categorical semantics ,Computer Science - Logic in Computer Science ,Quantum Physics ,Quantum circuit description language ,[INFO.INFO-LO]Computer Science [cs]/Logic in Computer Science [cs.LO] ,FOS: Physical sciences ,[INFO.INFO-CL]Computer Science [cs]/Computation and Language [cs.CL] ,Logic in Computer Science (cs.LO) ,Computer Science::Emerging Technologies ,[PHYS.QPHY]Physics [physics]/Quantum Physics [quant-ph] ,Mathematics::Category Theory ,Categorical semantics ,Operational semantics ,Computer Science::Programming Languages ,Quantum Physics (quant-ph) - Abstract
In this paper, we introduce dynamic lifting to a quantum circuit-description language, following the Proto-Quipper language approach. Dynamic lifting allows programs to transfer the result of measuring quantum data -- qubits -- into classical data -- booleans -- . We propose a type system and an operational semantics for the language and we state safety properties. Next, we introduce a concrete categorical semantics for the proposed language, basing our approach on a recent model from Rios\&Selinger for Proto-Quipper-M. Our approach is to construct on top of a concrete category of circuits with measurements a Kleisli category, capturing as a side effect the action of retrieving classical content out of a quantum memory. We then show a soundness result for this semantics., accepted for publication in FSTTCS 2021
- Published
- 2021
- Full Text
- View/download PDF