Formal Verification of Robertson-Type Uncertainty Relation

Takaaki Masuhara; Toru Kuriyama; Masakazu Yoshida; Jun Cheng

doi:10.4236/jqis.2015.52008

Home > Journals > Physics & Mathematics > JQIS

Journal of Quantum Information Science > Vol.5 No.2, June 2015

Formal Verification of Robertson-Type Uncertainty Relation ()

Takaaki Masuhara, Toru Kuriyama, Masakazu Yoshida^*, Jun Cheng

Department of Intelligent Information Engineering and Sciences, Doshisha University, Kyoto, Japan.

DOI: 10.4236/jqis.2015.52008 PDF HTML XML 3,036 Downloads 3,569 Views

Abstract

Formal verification using interactive theorem provers have been noticed as a method of verification of proofs that are too big for humans to check the validity of them. The purpose of this work is to verify the validity of Robertson-type uncertainty relation toward verifying unconditional security of quantum key distributions. We verify the validity of the relation by using proof assistant Coq and it is turned out that the theorem regarding the relation formally holds. The source code for Coq which represents the validity of the theorem is printed in Appendix.

Keywords

Formal Verification, Proof Assistant Coq, Uncertainty Relation

Share and Cite:

Masuhara, T. , Kuriyama, T. , Yoshida, M. and Cheng, J. (2015) Formal Verification of Robertson-Type Uncertainty Relation. Journal of Quantum Information Science, 5, 58-70. doi: 10.4236/jqis.2015.52008.

Conflicts of Interest

The authors declare no conflicts of interest.

References

[1]	Gordon, M.J.C. (1986) Why Higher-Order Logic Is a Good Formalism for Specifying and Verifying Hardware. In: Milne, G.J. and Subrahmanyam, P.A., Eds., Proceedings of the 1985 Edinburgh Workshop on VLSI, North-Holland, 153-177.
[2]	Boyer, R.S., Moore, J.S. and Kaufmann, M. (1996) ACL2 Version 7.0. http://www.cs.utexas.edu/users/moore/acl2/
[3]	University of Cambridge Computer Laboratory (1989) Isabelle. http://isabelle.in.tum.de/
[4]	INRIA (1985) The Coq Proof Assistant. http://coq.inria.fr/
[5]	Heine, M., Sørensen, B. and Urzyczyn, P. (2006) Lectures on the Curry-Howard Isomorphism. Warsaw University, Poland.
[6]	Feit, W. and Thompson, J.G. (1963) Solvability of Groups of Odd Order. Pacific Journal of Mathematics, 13, 775-1029. http://dx.doi.org/10.2140/pjm.1963.13.775
[7]	Bender, H. and Glaubernan, G. (1995) Local Analysis for the Odd Order Theorem. Cambridge University Press, Cambridge. http://dx.doi.org/10.1017/CBO9780511665592
[8]	Gonthier, G., Asperti, A., Avigad, J., Bertot, Y., Cohen, C., Garillot, F., Roux, S.L., Mahboubi, A., O’Connor, R., Biha, S.O., et al. (2013) A Machine-Checked Proof of the Odd Order Theorem. Lecture Notes in Computer Science, 7998, 163-179. http://dx.doi.org/10.1007/978-3-642-39634-2_14
[9]	Affeldt, R., Hagiwara, M. and Sénizergues, J. (2014) Formalization of Shannon’s Theorems. Journal of Automated Reasoning, 53, 63-103. http://dx.doi.org/10.1007/s10817-013-9298-1
[10]	Shannon, C.E. (1948) A mathematical Theory of Communication. Bell System Technical Journal, 27, 379-423. http://dx.doi.org/10.1002/j.1538-7305.1948.tb01338.x
[11]	Hayashi, M., Ishizaka, S., Kawachi, A., Kimura, G. and Ogawa, T. (2014) Introduction to Quantum Information Science. Springer.
[12]	Robertson, H.P. (1929) The Uncertanty Principle. Physical Review, 34, 163-164. http://dx.doi.org/10.1103/PhysRev.34.163
[13]	Bennett, C.H. and Brassard, G. (1984) Quantum Cryptography: Public Key Distribution and Coin Tossing. Proceedings of IEEE International Conference on Computers Systems and Signal Processing, Bangalore, 175-179.
[14]	Biham, E., Boyer, M., Boykin, P.O., Mor, T. and Roychowdhury, V. (2000) A Proof of the Security of Quantum Key Distribution. Proceedings of 32nd Annual ACM Symposium on the Theory of Computing, New York, 715-724.
[15]	Miyadera, T. and Imai, H. (2006) Information-Disturbance Theorem for Mutually Unbiased Observables. Physical Review A, 73, Article ID: 042317. http://dx.doi.org/10.1103/PhysRevA.73.042317
[16]	Miyadera, T. and Imai, H. (2007) Information-Disturbance Theorem and Uncertainty Relation. http://arxiv.org/abs/0707.4559
[17]	Maassen, H. and Uffink, J.B.M. (1988) Generalized Entropic Uncertainty Relations. Physical Review Letters, 60, 1103. http://dx.doi.org/10.1103/PhysRevLett.60.1103
[18]	Krishna, M. and Parthasarathy, K.R. (2002) An Entropic Uncertainty Principle for Quantum Measurements. Sankhya: The Indian Journal of Statistics, Series A, 64, 842-852.