Challenges
Datasets
Workspaces
Papers
Discussions
Leaderboard
Log inSign up
Challenges
Datasets
Workspaces
Papers
Discussions
Leaderboard
Blog
Job Board
Q3AS

© 2026 Aqora Quantum S.A.S.

TermsPrivacyLegal Notice

arXiv:quant-ph/9810066 · ACM Transactions on Programming Languages and Systems

Reasoning about Grover's quantum search algorithm using probabilistic wp

Michael J. Butler, Pieter Hartel

Published May 1, 1999• 17 citations
arXivHTMLPDF

Abstract

Grover's search algorithm is designed to be executed on a quantum-mechanical computer. In this article, the probabilistic wp -calculus is used to model and reason about Grover's algorithm. It is demonstrated that the calculus provides a rigorous programming notation for modeling this and other quantum algorithms and that it also provides a systematic framework of analyzing such algorithms.

DOI
10.1145/319301.319303

Related papers

A Formal Derivation of Grover's Quantum Search Algorithm

Paolo Zuliani

In this paper we aim at applying established formal methods techniques to a recent software area: quantum programming. In particular, we aim at providing a stepwise derivation of Grover's quantum search algorithm. Our work shows that, in principle, traditional software engineering techniques such as specification and refinement can be applied to quantum programs. We have chosen Grover's algorithm as an example because it is one of the two main quantum algorithms. The algorithm can find with high probability an element in an unordered array of length L in just O(radicL) steps (while any classical probabilistic algorithm needs Omega(L) steps). The derivation starts from a rigorous probabilistic specification of the search problem, then we stepwise refine that specification via standard refinement laws and quantum laws, until we arrive at a quantum program. The final program will thus be correct by construction.

International Symposium on Theoretical Aspects of Software Engineering (TASE)•Jan 1, 2007•10 citations

How to utilize a Grover search in general programming

Shigeru Yamashita

It is widely believed that quantum computers (if realized) will be more powerful than today’s computers from the viewpoint of computational complexity . However, it is not obvious how to utilize quantum computers in practical situations. For practical purposes, a Grover search may be one of the most promising quantum algorithms known so far. Thus, in this paper, we propose an efficient framework where we can use Grover search for general programming. Our framework has the following steps. (1) A programmer writes a program by using standard C++ programming language. (2) Some if expressions within for loops in the C++ source code are chosen as candidates to be performed as a Grover search on a quantum computer. (3) The framework automatically generates a corresponding quantum circuit for each Grover search chosen in (2). Unlike the existing quantum circuit design methods, we can treat large problems in our quantum circuit design. (4) By evaluating the number of primitive quantum gates in the quantum circuit generated in (3), the framework determines whether the processing time of the quantum circuit is faster than the processing time of the corresponding if expression on a classical computer. If the framework determines that the quantum circuit is faster, it generates some interface source codes for a classical computer. Thus, in our framework, a programmer can use a Grover search with almost no effort.

Laser Physics•Apr 1, 2006•1 citation

Quantum Algorithmic Gate-Based Computing: Grover Quantum Search Algorithm Design in Quantum Software Engineering

Sergey Victorovich Ulyanov, V.S. Ulyanov

The difference between classical and quantum algorithms (QA) is following: problem solved by QA is coded in the structure of the quantum operators. Input to QA in this case is always the same. Output of QA says which problem coded. In some sense, give a function to QA to analyze and QA returns its property as an answer without quantitative computing. QA studies qualitative properties of the functions. The core of any QA is a set of unitary quantum operators or quantum gates. In practical representation, quantum gate is a unitary matrix with particular structure. The size of this matrix grows exponentially with an increase in the number of inputs, which significantly limits the QA simulation on a classical computer with von Neumann architecture. Quantum search algorithm (QSA) - models apply for the solution of computer science problems as searching in unstructured data base, quantum cryptography, engineering tasks, control system design, robotics, smart controllers, etc. Grovers algorithm is explained in details along with implementations on a local computer simulator. The presented article describes a practical approach to modeling one of the most famous QA on classical computers, the Grover algorithm.

arXiv:2304.13703•Apr 20, 2023•2 citations

Analysis and Simulation of Grover’s Search Algorithm

Jiayu Zhuang, Junsuo Zhao, Fanjiang Xu +2 more

A quantum computation problem of quantum search is discussed in this paper.Grover's search algorithm, the most commonly used quantum search algorithm, is introduced in details.The flow of quantum search algorithm and the quantum circuit model are shown.And the error of the search value, as well as the probability of measurement, is analyzed.For further research we simulated the Grover's search algorithm in classical computer.By quantum simulator the probability distribution of the measuring result of search value is presented and the computational efficiency is discussed.The simulation result demonstrates the effectiveness of the proposed algorithm.

International Journal of Machine Learning and Computing•Feb 1, 2014•5 citations

Grover's search algorithm and the quantum measurement problem

Manoj K. Samal, Partha Ghose

It is suggested that the individual outcomes of a measurement process can be understood within standard quantum mechanics in terms of the measuring apparatus, treated as a quantum computer, executing Grover's search algorithm.

arXiv:quant-ph/0202176•Feb 28, 2002•0 citations

Quantum Algorithms for Searching Manifolds

Hooman Sherkat-Massoom

Quantum computing is a system of computation that exploits the quantum-mechanical nature of reality at nano-scales in order to perform certain operations in a way that can scale better than is possible with classical computing. While the hardware sideof quantum computing is still in its infancy, many quantum algorithms - sets of instructions to run on a quantum computer in order to complete particular tasks - have been designed and analyzed. One of the most famous of these is Grover’s algorithm, an algorithm for searching a database. Two types of generalizations of Grover’s algorithm have been studied: spatial search algorithms (algorithms for searching discrete spaces) and “analog” search algorithms (algorithms performed by the evolution of physical systems). We develop and analyze algorithms that are generalizations of both those generalizations – an analog search algorithm for searching continuous, rather than discrete, spaces.

•Jan 1, 2018•0 citations
Grover's search algorithm is designed to be executed on a quantum-mechanical computer. In this article, the probabilistic wp -calculus is used to model and reason about Grover's algorithm. It is demonstrated that the calculus provides a rigorous programming notation for modeling this and other quantum algorithms and that it also provides a systematic framework of analyzing such algorithms.
In this paper we aim at applying established formal methods techniques to a recent software area: quantum programming. In particular, we aim at providing a stepwise derivation of Grover's quantum search algorithm. Our work shows that, in principle, traditional software engineering techniques such as specification and refinement can be applied to quantum programs. We have chosen Grover's algorithm as an example because it is one of the two main quantum algorithms. The algorithm can find with high probability an element in an unordered array of length L in just O(radicL) steps (while any classical probabilistic algorithm needs Omega(L) steps). The derivation starts from a rigorous probabilistic specification of the search problem, then we stepwise refine that specification via standard refinement laws and quantum laws, until we arrive at a quantum program. The final program will thus be correct by construction.
It is widely believed that quantum computers (if realized) will be more powerful than today’s computers from the viewpoint of computational complexity . However, it is not obvious how to utilize quantum computers in practical situations. For practical purposes, a Grover search may be one of the most promising quantum algorithms known so far. Thus, in this paper, we propose an efficient framework where we can use Grover search for general programming. Our framework has the following steps. (1) A programmer writes a program by using standard C++ programming language. (2) Some if expressions within for loops in the C++ source code are chosen as candidates to be performed as a Grover search on a quantum computer. (3) The framework automatically generates a corresponding quantum circuit for each Grover search chosen in (2). Unlike the existing quantum circuit design methods, we can treat large problems in our quantum circuit design. (4) By evaluating the number of primitive quantum gates in the quantum circuit generated in (3), the framework determines whether the processing time of the quantum circuit is faster than the processing time of the corresponding if expression on a classical computer. If the framework determines that the quantum circuit is faster, it generates some interface source codes for a classical computer. Thus, in our framework, a programmer can use a Grover search with almost no effort.
The difference between classical and quantum algorithms (QA) is following: problem solved by QA is coded in the structure of the quantum operators. Input to QA in this case is always the same. Output of QA says which problem coded. In some sense, give a function to QA to analyze and QA returns its property as an answer without quantitative computing. QA studies qualitative properties of the functions. The core of any QA is a set of unitary quantum operators or quantum gates. In practical representation, quantum gate is a unitary matrix with particular structure. The size of this matrix grows exponentially with an increase in the number of inputs, which significantly limits the QA simulation on a classical computer with von Neumann architecture. Quantum search algorithm (QSA) - models apply for the solution of computer science problems as searching in unstructured data base, quantum cryptography, engineering tasks, control system design, robotics, smart controllers, etc. Grovers algorithm is explained in details along with implementations on a local computer simulator. The presented article describes a practical approach to modeling one of the most famous QA on classical computers, the Grover algorithm.
A quantum computation problem of quantum search is discussed in this paper.Grover's search algorithm, the most commonly used quantum search algorithm, is introduced in details.The flow of quantum search algorithm and the quantum circuit model are shown.And the error of the search value, as well as the probability of measurement, is analyzed.For further research we simulated the Grover's search algorithm in classical computer.By quantum simulator the probability distribution of the measuring result of search value is presented and the computational efficiency is discussed.The simulation result demonstrates the effectiveness of the proposed algorithm.
Quantum computing is a system of computation that exploits the quantum-mechanical nature of reality at nano-scales in order to perform certain operations in a way that can scale better than is possible with classical computing. While the hardware sideof quantum computing is still in its infancy, many quantum algorithms - sets of instructions to run on a quantum computer in order to complete particular tasks - have been designed and analyzed. One of the most famous of these is Grover’s algorithm, an algorithm for searching a database. Two types of generalizations of Grover’s algorithm have been studied: spatial search algorithms (algorithms for searching discrete spaces) and “analog” search algorithms (algorithms performed by the evolution of physical systems). We develop and analyze algorithms that are generalizations of both those generalizations – an analog search algorithm for searching continuous, rather than discrete, spaces.