The Coq mailing list

[Timothy Carstens <intoverflow AT gmail.com>]

A rough answer:

Much of the work in quantum algorithms concerns problems in group theory more than problems in logic (hidden subgroups, for instance).

This is to be expected as quantum computing is all about linear operators, which (in systems with finite degrees of freedom, as we’d have in a quantum computer) are just matrices. This gives a direct link to the representation theory of groups over the complex numbers.

This (representation theory) is also the technical origin of certain exotic operators, such as quantum Fourier transform (which arises from representation theoretic notions of character).

Other popular applications concern algorithms for simulating quantum systems. Here again, the symmetries of the system under simulation give a direct link to the computational operations via representation theory.

Regarding problems in logic, here there’s potential for certain minor improvements (faster lookups due to Grover’s algorithm, for instance, maybe). I don’t know that these speed ups are needed for the problem sizes one encounters in type-checking Coq, though.

As for bigger ambitions, the jury is still out on where NP lands in the quantum realm, but it’s a popular belief that quantum machines have no serious advantage in that class. This would mean that we wouldn’t expect these machines to excel beyond classical machines at constructing proofs.

Perhaps for quantum machines the better question is, do they offer advantages for probabilistic proofs? Yes, and indeed this is an area of work in quantum cryptography. But it’s not a Coq thing so this list might not be the place for it :)

Sent from my iPhone

On Dec 12, 2019, at 3:22 PM, Alex Meyer <alex153 AT outlook.lv> wrote:



Are there some thoughts, efforts and ideas about implementing Coq (or part of it) on quantum computer? I am novice in quantum computing, but I can not find any guidance about quantum algorithms that are designed especially for the type theory of any kind or first-order/higher-order logic. Does quantum community call those algorithms somehow differently or have different perspective? Or maybe quantum speedup is not available for the type of reasoning that is done by Coq?

Alex