Affordable Access

Access to the full text

Symbolic Reasoning About Quantum Circuits in Coq

Authors
  • Shi, Wen-Jun1
  • Cao, Qin-Xiang2
  • Deng, Yu-Xin1
  • Jiang, Han-Ru3
  • Feng, Yuan4
  • 1 East China Normal University, Shanghai, 200062, China , Shanghai (China)
  • 2 Shanghai Jiao Tong University, Shanghai, 200240, China , Shanghai (China)
  • 3 Yanqi Lake Beijing Institute of Mathematical Sciences and Applications, Beijing, 101408, China , Beijing (China)
  • 4 University of Technology Sydney, Sydney, NSW, 2007, Australia , Sydney (Australia)
Type
Published Article
Journal
Journal of Computer Science and Technology
Publisher
Springer-Verlag
Publication Date
Nov 30, 2021
Volume
36
Issue
6
Pages
1291–1306
Identifiers
DOI: 10.1007/s11390-021-1637-9
Source
Springer Nature
Keywords
Disciplines
  • Regular Paper
License
Yellow

Abstract

A quantum circuit is a computational unit that transforms an input quantum state to an output state. A natural way to reason about its behavior is to compute explicitly the unitary matrix implemented by it. However, when the number of qubits increases, the matrix dimension grows exponentially and the computation becomes intractable. In this paper, we propose a symbolic approach to reasoning about quantum circuits. It is based on a small set of laws involving some basic manipulations on vectors and matrices. This symbolic reasoning scales better than the explicit one and is well suited to be automated in Coq, as demonstrated with some typical examples.

Report this publication

Statistics

Seen <100 times