quantum Fourier transform · quantum computing

@Yijun He There might be a problem with the first sorry in qft_no_swap_of_unit_vec. Maybe some additional assumptions are needed. Please see the attached file with my comments.
Quantum_Fourier_Transform_draft.thy

Yijun He (Jul 04 2019 at 15:06):

Yijun He (Jul 04 2019 at 15:11):

I also have a question about induction: how can I impose a restriction to the induction variable? For example, I want to induct in the range 0 <= m <= n-1, but using "proof (induction m)" stops me from using the assumption "m<n" in case (Suc m), since m is already specified in this case

Anthony Bordg (Jul 04 2019 at 15:20):

@Yijun He The fastest method to get an answer to your question is to ask Larry before he leaves his office at 5pm! :running:

Yijun He (Jul 04 2019 at 15:24):

Anthony Bordg (Jul 04 2019 at 15:39):

@Yijun He OK, I had no luck with the documentation. For an induction on

m

with the specified range, in the case Suc m you should be able to use

m < n-1

, not

m<n

, so Isabelle is right. Can you ask the mailing list (Distribution & Support) ?

Yijun He (Jul 04 2019 at 16:17):

I found a way to use the assumption just now, but it looks a bit messy: I added "m>n or..." to the induction hypothesis of qft_no_swap_of_unit_vec, which allows me to trivially say "m > n ==> (Suc m) > n" when m is greater than n.

Anthony Bordg (Jul 05 2019 at 21:16):

@Yijun He ind_from_1 and its use in pow_tensor_dim_row by @Hanna Lachnitt in her theory Deutsch_Jozsa.thy might be a source of inspiration wrt the problem we discuss earlier.

Anthony Bordg (Jul 06 2019 at 14:33):

Anthony Bordg (Jul 08 2019 at 13:52):

@Yijun He In uniq_select_index I'm thinking about refactoring the statement ⋀a. (a∈{..<n+1} ⟹ i mod (2^a) = j mod (2^a)) under the appropriate assumptions. Do you think it might be a useful lemma on its own ?

Yijun He (Jul 08 2019 at 13:54):

Yijun He (Jul 08 2019 at 13:56):

That statement requires the assumption that ⋀a. (a∈{..<n} ⟹ select_index n a i = select_index n a j), which seems too specific

Anthony Bordg (Jul 08 2019 at 13:58):

Ok, in that case I don't see a way to shorten the proof by refactoring or changing its structure. But at least I can try to clean the proof of ⋀a. (a∈{..<n+1} ⟹ i mod (2^a) = j mod (2^a)) which seems the longest step.

Yijun He (Jul 08 2019 at 13:59):

Anthony Bordg (Jul 08 2019 at 14:02):

On the other hand, it's true that ⋀a. (a∈{..<n} ⟹ select_index n a i = select_index n a j) is specific, but refactoring may be the first step towards putting all this fancy stuff about select_index into a dedicated theory, or even into a specific section of the Basics theory.

Yijun He (Jul 08 2019 at 14:06):

That might be a better solution, as it is indeed a basic/intuitive result of number theory/modular arithmetic

Anthony Bordg (Jul 08 2019 at 14:11):

Of course, in that case we can directly put the whole proof uniq_select_index somewhere else, but I still feel the proof is too long. Also, somewhere else we might have burried some lemmas related to select_index inside proofs. In that case, refactoring and then putting that stuff in a dedicated place is the way to go.

Anthony Bordg (Jul 08 2019 at 15:01):

@Yijun He Inside the syntax case (Suc a) you can't write a + 1, but everywhere else in the proof note that you can and should write a + 1, since we do not want the code to feel alien for any ordinary mathematician.

Yijun He (Jul 08 2019 at 15:06):

I am not sure why, but sometimes auto might fail when I change Suc k to k+1 (and sometimes it works properly).

Anthony Bordg (Jul 08 2019 at 15:07):

Yijun He (Jul 08 2019 at 15:10):

Anthony Bordg (Jul 08 2019 at 15:11):

Anthony Bordg (Jul 08 2019 at 15:30):

So, keep Suc k if for whatever reason you have some trouble and write k + 1 whenever possible.

Anthony Bordg (Jul 08 2019 at 18:53):

@Yijun He I cleaned the proof of uniq_select_index (please see my PR). From that proof I factored out two lemmas mod_pow_2_eq and select_index_eq_to_mod_eq. It's unlikely that select_index_eq_to_mod_eq will be useful in the future, but I believe mod_pow_2_eq may be useful. Also, the whole thing is now much more legible than previously.

Yijun He (Jul 09 2019 at 13:45):

@Anthony Bordg I am currently struggling with the complicated expressions in quantum Fourier transform. In the book, the vectors are expressed as the tensor product of n qubits, but I am not sure about how to do that in Isabelle (product and sum require the operators to be comm_monoid, which doesn't work for tensor product and even vector addition), and my current expressions using products and select_index seems too complicated to work with. Could you give me some advice about it? Many thanks.

Anthony Bordg (Jul 09 2019 at 13:58):

@Yijun He vector addition is obviously a monoid law (for any given dimension), so I would be very surprised if it's not already proven, and if it's not then we need to prove it.

Yijun He (Jul 09 2019 at 14:05):

For example, when I try to make a statement "v = (∑k<n. unit_vec n k)" (this is incorrect, but the variable types should be correct), Isabelle gives an error message saying No type arity Matrix.vec :: comm_monoid_add

Anthony Bordg (Jul 09 2019 at 14:07):

Yijun He (Jul 09 2019 at 14:10):

Yijun He (Jul 09 2019 at 14:11):

I added a test lemma sum_of_unit_vec, which uses the exact statement above and should give an error message.

Anthony Bordg (Jul 09 2019 at 14:21):

unit_vec n k is of type complex Matrix.vec. Now, if you look at the theory Matrix.thy, you see the lemma comm_monoid_vec, where the locale comm_monoid is introduced in Group.thy. But, comm_monoid_add is a class introduced in Groups.thy.

Anthony Bordg (Jul 09 2019 at 14:24):

So, it's enough to prove comm_monoid_add of the set of complex vectors of a given dimension. I will do that.

Yijun He (Jul 09 2019 at 14:26):

Jose Manuel Rodríguez Caballero (Jul 09 2019 at 14:29):

Just to show a different approach. My solution for expressing "v = (∑k<n. unit_vec n k)" would be to go from "complex vec" to "nat ell2" using my function "vec_to_ell2". The type "nat ell2" is the complex Hilbert space of square-summable sequences of complex numbers (in particular comm_monoid). In order to return to "complex vec" from "nat ell2", I use the function "ell2_to_vec". Indeed, "unit_vec n k" goes to what I call "ket k" in "nat ell2". Finite_Dimensional_Case.thy

Anthony Bordg (Jul 09 2019 at 15:14):

@Yijun He Even better, I browsed the theory Matrix.thy and I discovered that one has the definition finsum_vec. I think this is the definition you want to use here and the corresponding lemmas they proved to handle such sums.

Yijun He (Jul 09 2019 at 15:31):

Anthony Bordg (Jul 09 2019 at 15:32):

The only thing lacking is a nice notation like

\sum

for finsum_vec, but we can introduce it as an abbreviation.

Anthony Bordg (Jul 17 2019 at 21:54):

@Yijun He About the use of Suc n vs n+1 Part 2 of the style guide (7th bullet) seems to have a point when it says that it depends on the distinction between top-level lemmas that you may want to present to people and lemmas that are used in further proofs as a convenient scaffolding in the formalization process. For the latter, normal forms are fine and may help automation.

Anthony Bordg (Jul 19 2019 at 13:33):

@Yijun He This afternoon I plan to work on the proof of qubits_tensor_prod. Is that ok with you ?

Yijun He (Jul 19 2019 at 13:37):

That would be great, thanks! Actually it still needs some assumptions on the functions f and g's. I am still working on the proof of qft_no_swap_of_unit_vec.

Anthony Bordg (Jul 20 2019 at 16:27):

@Yijun He done. But, for the proof the associativity of the tensor product of matrices is needed. So, I'm going to prove this associativity in Tensor.thy.

Anthony Bordg (Jul 20 2019 at 22:30):

@Yijun He Probably due to the changes in Binary_Nat.thy your proof of select_index_eq_bin_rep is broken. The bad thing: I don't get a proof without smt.

Anthony Bordg (Jul 20 2019 at 22:39):

@Yijun He In qubits_rep I changed select_index n j i to select_index n i j (and made the corresponding changes).
Indeed, in Quantum.thy select_index is defined as

select_index n i j ≡ (i≤n-1) ∧ (j≤2^n - 1) ∧ (j mod 2^(n-i) ≥ 2^(n-1-i)).

Anthony Bordg (Jul 21 2019 at 09:32):

Anthony Bordg (Jul 21 2019 at 10:33):

@Yijun He I made a PR in your master branch. Also, Tensor.thy is up-to-date in my master branch.

Yijun He (Jul 21 2019 at 10:37):

Anthony Bordg (Jul 22 2019 at 14:32):

Yijun He (Jul 22 2019 at 14:36):

Maybe the sorry in qft_no_swap_of_unit_vec? Now I am not even sure whether my formulation is correct. Many thanks.

Anthony Bordg (Jul 22 2019 at 14:39):

Anthony Bordg (Jul 22 2019 at 15:29):

@Yijun He In the book what is the corresponding element to qft_no_swap n m v ?

Yijun He (Jul 22 2019 at 15:32):

It should be an intermediate state of the expression (5.17), where v is the unit vector |j⟩.

Anthony Bordg (Jul 26 2019 at 14:29):

@Yijun He We have to do some reverse engineering here if we have Shor's algorithm in mind. To what extent do we need the quantum Fourier Transform to formalize Shor's algorithm ?

Yijun He (Jul 26 2019 at 14:41):

Proving correctness of Shor's algorithm seems to need the correctness of inverse Quantum Fourier Transform.

Anthony Bordg (Jul 26 2019 at 14:48):

@Yijun He Yes, but this is not what I meant.
As usual in mathematics we want to make our life easier, at least to start and generalize eventually. So, If we start with the quantum Fourier transform on 3 qubits for instance, to avoid a difficult and messy formalization at least at the beginning, then to what extent the nice applications of the quantum Fourier transform still make sense ?

Yijun He (Jul 26 2019 at 14:57):

I think quantum Fourier transform is just a faster way of computing the classical Fourier transform on qubits, so Shor's algorithm works (more slowly, but still correctly) even with the classical Fourier transform, and it doesn't depend on any nice property of the quantum one.

Anthony Bordg (Jul 26 2019 at 15:21):

Yes, you're right and actually one could say the same thing about anything in quantum computing, it's "just" a way to speed up classical algorithms. But, the fast Fourier transform is already in the AFP and we want to contribute something new. Moreover, it would be a shame to lose your nice work on the quantum Fourier transform, but to avoid to get stuck we may need, at least temporarily, to assume a fixed number of qubits, then the formalization should be more workable.

Hanna Lachnitt (Aug 12 2019 at 09:01):

Hey :) I believe that I found a way to formalize quantum Fourier tranform without things getting so complicated in the first place. My controlled R gate is just a 4x4 matrix (as in the literature) and I use swapping to get the qubit needed in front of the unit vector (this seems to be done in practice as well). I am not entirely sure if this will avoid getting in trouble (it needs some unit vector decomposition lemmas) but I am pretty confident. @Yijun He do you feel this is a way I should pursue or do you think the current formalization is fixable? I will also have a more thoroughly look at the current file once I finish with Grover.

Yijun He (Aug 12 2019 at 10:40):

I still think the current proof is fixable, but a 4x4 controlled R gate sounds much better than the current proof. It would be great if you can help with the formalization of quantum Fourier transform.

Anthony Bordg (Aug 12 2019 at 15:17):

Hanna Lachnitt (Aug 16 2019 at 10:46):

Until now everything worked out, although of course there could be troubles later. I uploaded a first tentative theory in a QFT branch in my fork where I tried out my ideas. Everything is still under construction (especially some indices might be wrong). I hope I did not just do nonsense or made a stupid mistake :fear: However, I feel with this new approach proving becomes more difficult in terms of thinking about what parameters to use before proving something but the proofs themselves are rather easy now. And I feel that its well understandable for a reader especially with some explanations

Hanna Lachnitt (Aug 16 2019 at 10:50):

The idea behind the approach is not to define a matrix R_k with takes a huge unit vector and has to select all indices of qubits i and k to extend the binary fraction as this creates complexity. Instead swap the needed qubit

|j_k\rangle

outside of unit vector

| j_l,...,j_n \rangle

(which is just a tensor product of single qubits, and

j_k

corresponds to the qubit at position k). Then, apply a 4x4 CR gate to the tensor product of this two qubits i and k. Since the second qubit is left untouched by this operation it can just be swapped back afterwards. This corresponds to an application of a

R_k

gate to qubit i.

Hanna Lachnitt (Aug 16 2019 at 10:54):

The file is still messy but I felt it was better to involve you in the process, I will make it more readable and add further proofs, so please pull from time to time if you have a look at it. Right now I am leaving proofs which are supposed to be very easy or bound to work for later to see if the overall approach is promising.

Hanna Lachnitt (Aug 30 2019 at 09:36):

Hey guys :) Just to keep you updated, I managed to prove calculation (5.4) from page 218 of Nielsen and Chuang. There are some easy proofs missing (including almost all gate proofs) but nothing that should cause any problems. The equivalence of (5.4) to the definition of quantum fourier transform is described as using only elementary algebra so I hope it will be doable :)

Hanna Lachnitt (Oct 19 2019 at 09:39):

@Anthony Bordg Regarding your comment about:
subsection ‹Transformation of j into a Tensor Product of Single Qubits›
what do you thing about:
subsection ‹Transformation of the Input into a Tensor Product of Single Qubits›

Anthony Bordg (Oct 19 2019 at 09:50):

@Hanna Lachnitt I think it's better. If I remember correctly "Mike and Ike",

|j\rangle

is any basis state. Do you define qFt directly on an arbitrary state ? In other words is your "input" here refering to an arbitrary state ? If yes, why not simply "Transformation of a State into a Tensor Product of Single Qubits"? We could even later move this part into More_Tensor.thy.

Hanna Lachnitt (Oct 19 2019 at 18:18):

Yes qFt takes an arbitrary basis state (actually just a natural number). Sound good, I will take that. Especially if its moved to some other theory input does not make sense. Also I wrote an introductory comment which might explain things a bit better.

Hanna Lachnitt (Oct 19 2019 at 18:28):

As to your comment to to_list_bound:

Also, it seems that you start counting from 1 for the position s while all the rest of the library takes the convention that we start counting from 0.

I did this to stick closely to the literature where

j_1j_2...j_n

are used for the binary representation of j. Actually I also did this for the

CR_i

gates and so on. Otherwise it would be a bit confusing. While I work through the theory I will search for cases where I started to count from 0 it might be better to change them instead of changing the cases where counting starts from 1.

Hanna Lachnitt (Oct 19 2019 at 19:57):

I have renamed the abbreviation for to_tensor_prod j⨂ with ⨂r, standing for tensor product representation since j should not appear in any names

Hanna Lachnitt (Oct 20 2019 at 09:49):

Hanna Lachnitt (Oct 20 2019 at 10:09):

I decided to rename qr to phase_shifted_qubit, in short psq. I am still not 100% happy with that but qr is unacceptable. If there is a better possibility I would be happy for suggestions.

Hanna Lachnitt (Oct 20 2019 at 10:25):

Regarding your comment about lemma transpose_of_controlled_phase_shift: (* AB: Maybe simply transpose_of_CR ? *)
Isn't this the same thing as having H in a lemma name instead of hadamard_gate? So it would mix up notation and full name of the definition. But I would be happy to change this, shorter names would be preferable here.

Hanna Lachnitt (Oct 20 2019 at 13:20):

I also tried to change the definition qr/phase_shifted_qubit into an abbreviation. But then it got so slow that I had to set everything back. Might be just my laptop though, its not very powerful.

Anthony Bordg (Oct 21 2019 at 09:58):

There are two things we should absolutely avoid. First, variables in names. Second, notations in names if those notations are not standard. However, using very standard notations, like H or cR, in names is fine.

Hanna Lachnitt (Oct 21 2019 at 10:03):

Anthony Bordg (Oct 21 2019 at 10:30):

At some point we should replace the source comments with text blocks, but it's unimportant at that stage. They are more fundamental things we need first to take care

Hanna Lachnitt (Oct 21 2019 at 10:34):

Yes of course. I just replaced some of the latex code in the comments with the built-in code for readability, e.g. $|j_1,j_2,...,j_n\rangle$ with

|j_1,j_2,...,j_n\rangle

but if they are replaced with text at some point I would not do that.

Anthony Bordg (Oct 21 2019 at 10:46):

@Hanna Lachnitt There is something still confusing in the first comment. In your example, what's the link between

j=11

and

|01011\rangle

? Do you mean

|00011\rangle

instead ?

Hanna Lachnitt (Oct 21 2019 at 11:06):

01011 is the binary representation of 11. I used the notation as it is introduced in the book of Nielsen and Chuang. To make it clearer I could add that

|j_1j_2...j_n\rangle

|01011\rangle

where

j = j_1*2^{n-1}+...+j_n*2^0

which is simply written as

j=j_1...j_n

in the book (the notation is a bit untidy).

Hanna Lachnitt (Oct 21 2019 at 11:10):

Indeed if one writes

|j\rangle

what is meant is always j in binary representation (its really untidy), never something like 000j. Otherwise how would you encode e.g. 3 if 11 is

|00011\rangle

?
I realize now that I maybe should take another number as example that does contain a digit beyond 1, e.g. 12. This might make it clearer and avoid confusion between binary and decimal representation.

Anthony Bordg (Oct 21 2019 at 11:21):

Oh I see, it's eleven, not the binary representation 11 (namely 3)! Maybe it's better to use 9 or 12 to avoid any confusion.

Anthony Bordg (Oct 21 2019 at 11:37):

lemma pow_tensor_list_one [simp]:
  assumes "xs = []"
  shows "(pr (Cons x xs) 1) = x"
  by (simp add: assms)

lemma pow_tensor_length_1:
  fixes X:: "complex Matrix.mat"
  shows "(pr [X] 1) = X"
  by simp

Anthony Bordg (Oct 21 2019 at 12:02):

Hanna Lachnitt (Oct 23 2019 at 13:04):

Thanks for your PR, there seems to be still some confusion left about the binary representation. If j is a natural number strictly smaller than 2^m then the binary representation in this setting has length m, i.e.

j=j_1j_2...j_m

and not length n.

I put m instead of n for some reasons (I used a locale in the first versions and needed another variable for inductions) but I wonder now if m should not be renamed to n since you would usually use j and n.

Hanna Lachnitt (Oct 23 2019 at 13:08):

Thanks! I only used Cons because of our talk about when to use (Suc n) instead of (n+1) and this is not a lemma that is for people to look at it. I removed the type annotation (fixes X:: "complex Matrix.mat") however, since it was done nowhere else.

Hanna Lachnitt (Oct 23 2019 at 13:10):

Anthony Bordg (Oct 23 2019 at 15:44):

Formal proofs is a tricky business. A rule has exceptions, but there is the spirit of the rule. Regarding canonical forms, sometimes they will help, in particular in involved proofs, but here the proof is trivial. So, here canonical forms only make the statement less legible.

Anthony Bordg (Oct 28 2019 at 11:13):

Yes, it would be better to use n for the number of qubits to be consistent across the library. To be consistent would help the readers and the maintainers.
Also, why use the variable k to denote a length when one can use l ?

Hanna Lachnitt (Oct 28 2019 at 20:21):

On another issue, should j also be replaced by j_dec or jd? Otherwise it is a bit cumbersome if j appears inside of a matrix, e.g.

 (Matrix.mat 2 1 (λ(i,j). if i=0 then (1::complex)/sqrt(2) else (exp (complex_of_real (2*pi)*𝗂*(bin_frac (s-1) (t-1) n jd)))*1/sqrt(2)))"

Hanna Lachnitt (Oct 28 2019 at 20:24):

I am currently working towards replacing m by n and k with l if its used for a length

Stream: quantum computing

Topic: quantum Fourier transform

Anthony Bordg (Jul 04 2019 at 13:31):

Anthony Bordg (Jul 04 2019 at 14:57):