Stream: quantum computing

Topic: work in progress


view this post on Zulip Anthony Bordg (Jul 03 2019 at 16:58):

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

view this post on Zulip 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)

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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: Aug 15 2022 at 02:13 UTC