# Is there a formalization of the computational model for quantum computers?

There are several equivalent computation models, each capable of simulating each other. For example, the lambda calculus or the SKI calculus which are based on rewriting, Cardelli's object calculus, Hoare's communicating sequential processes, and of course the universal Turing machine, all of them formally defined.

I do understand that though there are possibly different ways of building quantum computers, the ways we build them today are Turing-complete and equivalent to the other models of computation. My question is: have anyone formalized a mathematical computation model for a quantum computer (such as the D-Wave)? (As the other models, I assume this could be used as a programming language.)

(I do understand that a possible answer would be "the quantum mechanics", but that's not exactly what I'm looking for...)

• As with most of the models you mention, the mathematical formalism(s) for quantum computing came before anyone had any clue how to actually build one. Sep 15, 2017 at 10:11
• Also, the D-Wave is not a classical quantum computer (apologies for the pun). It solves a single class of problems apparently using quantum effects, but is not capable of general-purpose computing or running Shor's algorithm or anything. Sep 15, 2017 at 10:14
• That's what I was looking for, @Clément. As Haskell is built upon the lambda calculus, I was looking for some minimalist model that could be used as the foundation for a quantum programming language. Sep 15, 2017 at 14:23

Just as Turing machines aren't widely used to model computation, so are quantum Turning machines not wildly used to model quantum computation. Instead Quantum circuits are more popular. Quantum circuits defined in the obvious way: reversible transformations on a quantum mechanical analog of an n-bit register.

• Would you have any resources with the formalization of quantum circuits, with the primitive operations, etc? Sep 15, 2017 at 15:52
• @paulotorrens Try looking at the lecture notes for this CMU course, especially the first two: cs.cmu.edu/~odonnell/quantum15 Sep 15, 2017 at 16:09

Yes. The quantum Turing machine is a mathematical formalization of a computation model for a quantum computer.

• This answer would be better if it weren't wholly reliant on Wikipedia links (and mentioned Quantum Circuits). Sep 15, 2017 at 10:30

Peter Sellinger has been working on programming languages for quantum computing for a long time now. He is not the only one working in that field, of course, but I believe his work is accessible and largely accepted enough to fit your bill.

What he essentially developed is a "typed lambda calculus for quantum computation". I believe the best place to start is in the chapter of the textbook Semantic Techniques in Quantum Computation (written with B. Valiron), available at http://www.mscs.dal.ca/~selinger/papers/qlambdabook.pdf. I believe the list of references in that chapter is quite authoritative, too.

If you're looking for a concrete formalization, have a look at the Quipper language, which is embedded in Haskell. The introductory paper as well as the devoted webpage are probably the best places to start.

If you're looking for a more general discussion / introduction to those topics, you can have a look at the video and the article Programming the Quantum Future.