本文へジャンプ

  • HOME
  • 講演会情報

講演会情報

量子計算のための形式手法と圏論的意味論
講演者:角谷良彦(東京大学情報理工学系研究科)
平成26年10月27日(月)16時30分〜 東京大学理学部七号館007講義室
昨今何かと話題の量子コンピュータであるが、量子コンピュータの実現可能性はさておき、この講演では、量子コンピュータが普及した場合に利用可能な技術について議論する。通常の計算の世界では、プログラム検証のための様々な形式手法が研究されている。今回は、いくつかの形式手法を量子計算に応用することを考える。

量子計算のためのプログラミング言語がいくつか提案されているが、それらで書かれたプログラムの性質を検証するための枠組みとして量子ホーア論理を導入する。ここでは、確率の入った古典計算で有効であると知られているホーア論理を量子計算にまで拡張する。

量子コンピュータだけではなく、量子プロトコルもまた量子計算の重要なテーマの一つである。中でも盛んに研究が行われているのが、量子暗号プロトコルである。通常、古典暗号プロトコルの安全性では、計算量的仮説に基づいて攻撃者の能力に制限が設けられている。それに対して、量子暗号プロトコルの安全性は無条件安全性と呼ばれ、攻撃者の能力に関する仮定なしに成立する。この講演では、量子暗号プロトコルの安全性証明を量子プロセス計算を用いて形式化する。

また、時間が許せば、より抽象的な枠組みで量子計算を捉える手法として、圏論によるアプローチを紹介する。圏論はプログラミング言語の意味論として有効なことが知られているが、量子計算にも応用可能かどうか議論する。