Stream: quantum computing

Topic: work in progress

Anthony Bordg (Jul 03 2019 at 16:58):

@Hanna Lachnitt is working on the Deutsch-Jozsa algorithm.

Hanna Lachnitt (Aug 23 2019 at 17:17):

@Yijun He I now its a long shot but have you have you already proven anything about the parity of a number in relation to bin_rep? In particular, I want to show that if the kth position in the binary representation is 0, then the result of the division I of this number by 2^(m-k) is even where m is the total number of bits. (Intuitively this is clear, if we cut off the bit after k digits and the last one is 0 then the resulting number is even)

Yijun He (Aug 24 2019 at 00:47):

Not yet, but I have proved something similar: `select_index_div_2` in my `Quantum_Fourier_Transform.thy` shows that only the last bit of `select_index` is cut off when we divide a number by 2, and `select_index_eq_bin_rep` in the same file shows that `select_index` is exactly the same as `bin_rep` (except one gives booleans, and the other give 1 and 0s). Therefore the method in `select_index_div_2` might also help prove parity results about `bin_rep`.

Anthony Bordg (Aug 24 2019 at 09:16):

Not yet, but I have proved something similar: `select_index_div_2` in my `Quantum_Fourier_Transform.thy` shows that only the last bit of `select_index` is cut off when we divide a number by 2, and `select_index_eq_bin_rep` in the same file shows that `select_index` is exactly the same as `bin_rep` (except one gives booleans, and the other give 1 and 0s). Therefore the method in `select_index_div_2` might also help prove parity results about `bin_rep`.

`select_index_div_2` is in Measurement.thy

Hanna Lachnitt (Aug 24 2019 at 09:26):

Great thanks a lot. I guess with a little induction this should help me a lot. Also that `select_index` `bin_rep` thing is something I was thinking of proving at some point :D

Anthony Bordg (Oct 14 2019 at 16:13):

@Yijun He @Hanna Lachnitt
PR #19 and #20 have been merged.
The master branch has been tidied up.
Next is Hanna's Qft.

Last updated: Dec 07 2023 at 16:21 UTC