量⼦プログラミング⾔語の研究
静的解析から量⼦プログラム統合開発環境へ
国⽴情報学研究所
総合研究⼤学院⼤学
ERATO 蓮尾メタ数理システムデザインプロジェクト

蓮尾 ⼀郎

in Collaboration with
崇城⼤学

星野 直彦
京都⼤学 情報学研究科

脇坂 遼 ・ 五⼗嵐 淳
情報処理学会 連続セミナー2020「⼈間中⼼社会を⽀える情報技術の新潮流」
2020/12/14 「量⼦コンピュータとソフトウェア」

Outline• Introduction• Hoare logic as a showcase of static analysis• QPL Work (1): Ying's quantum Hoare logic• QPL Work (2): Quantum GoI for semantics of quantum λ-calculus[H. & Hoshino]• "Static analysis for hardware-specific, low-level concerns in NISQ"• QPL Work (3): Quantum Hoare logic for bounding errors [Hung+, POPL'19]• QPL Work (4): Language-Based Automated Uncomputation [Bichsel+, PLDI'20]• QPL Work (5): Type System for Qubit Connectivity[Wakizaka & Igarashi, JSSST Congress '20]

• Towards Quantum IDE
Hasuo (NII)

2

⾃⼰紹介
Ichiro Hasuo (NII & SOKENDAI)PhD (Computer Science, Radboud U. Nijmegen, 2008)• 研究テーマ： ソフトウェアの安全性• 形式検証（ソフトウェアが安全であることを定理として証明）• プログラミング⾔語理論（ソフトウェア記述のための形式体系）• ソフトウェア意味論（ソフトウェアの振舞いの数学的定義．形式検証に必要）• 論理学，代数学，圏論（ソフトウェア意味論の数学的道具）• 物理情報システム，⾃動運転，機械学習システム（最近の応⽤，ERATO プロジェクト）

Lopez-Pindato+, CAiSE’19• このトークは，「量⼦ソフトウェア」の中でも特に量⼦プログラミング⾔語に注⼒しますHasuo (NII)

3

Disclaimer:“Informed Outsider” です• 量⼦ソフトウェアとの関わりはしばらく前• H. & Naohiko Hoshino,
Semantics of Higher-Order Quantum
Computation via Geometry of Interaction.
LICSʼ11 & Ann. Pure Appl. Logic ʼ17• 蓮尾，星野： 「量⼦プログラミング⾔語」
情報処理 Vol. 55, No. 7 (2014年6⽉)• Organizing Chair, 11th workshop on
Quantum Physics and Logic (QPL 2014),
Kyoto, Japan• 当時の動機：
数学的⼀般論のわかりやすい応⽤例として
Hasuo (NII)

4

Not at allcomprehensive!

Trends in
Quantum Programming Language (QPL) Research
D-Wave’s Quantum
Annealing Machine[2011]IBM Quantum
Experience [2016]

2015

2010
Quantum Hoare Logic[Ying, ACM TOPLAS 2012]
Program logic for correctness ofimperative quantum programs

Quantum lambda
calculus [Selinger &Valiron, 2008, 2009]
Functional,
categorical semantics

QCL[Ömer 2000]
First QPL,
imperative
quantum λ-calculus[van Tonder,
SIAM J. Comp. 2004]
Functional, linear
types for no-cloning,

Quantum I/O monad[Green & Altenkirch, 2009]
Making Haskell a QPL

Quantum flowchart language[Selinger, MSCS 2004]
Formal semantics bysuperoperators

Quantum lambda
calculus [Hasuo &Hoshino, LICS 2011]
Categorical GoI
semantics for “quantum
data, classical control”

Quipper[Green, Lumsdaine, Ross,
Selinger, Valion, PLDI 2013]
A functional language thatgenerates quantum circuits
Quantum lambda calculus[Pagani, Selinger, Valion,
POPL 2014]
Anothercategorical
Hasuo
(NII)
semantics

Google claimed
quantumsupremacy [2019]

QWIRE[Paykin, Rand, Zdancewic,
POPL 2017]
Functional, generates
circuits, Coq-integrated
Q#[Svore et al., RWDSL 2018]by Microsoft,
functional/imperative

Logic for qubit error analysis[Hung, Hietala, Zhu, Ying, Hicks,
Wu, POPL 2019]
Quantum Hoare logic adapted
for bounding errors

2020
Silq
[Bichsel, Baader, Gehr, Vechev,
PLDI 2020]
Functional, automatic
uncomputation & a type system
for itType system for qubit connectivity[Wakizaka & Igarashi, JSSST
Congress 2020]
Type system for Selinger’s quantum
λ-calculus that ensures qubit
connectivity

5Physical
Not at all realization
emerging
comprehensive!
➜ let’s take “details”
seriously

Theoretically,
there is nothing
fundamentallychallenging…

Chance to exercise
advanced PL &semanticaltechniques…

Trends in
Quantum Programming Language (QPL) Research
D-Wave’s Quantum
Annealing Machine[2011]

No physicalrealization➜ no bothering
details J

IBM Quantum
Experience [2016]

2015

2010
Quantum Hoare Logic[Ying, ACM TOPLAS 2012]
Program logic for correctness ofimperative quantum programs

Quantum lambda
calculus [Selinger &Valiron, 2008, 2009]
Functional,
categorical semantics

QCL[Ömer 2000]
First QPL,
imperative
quantum λ-calculus[van Tonder,
SIAM J. Comp. 2004]
Functional, linear
types for no-cloning,

Quantum I/O monad[Green & Altenkirch, 2009]
Making Haskell a QPL

Quantum flowchart language[Selinger, MSCS 2004]
Formal semantics bysuperoperators

Quantum lambda
calculus [Hasuo &Hoshino, LICS 2011]
Categorical GoI
semantics for “quantum
data, classical control”

Quipper[Green, Lumsdaine, Ross,
Selinger, Valion, PLDI 2013]
A functional language thatgenerates quantum circuits
Quantum lambda calculus[Pagani, Selinger, Valion,
POPL 2014]
Anothercategorical
Hasuo
(NII)
semantics

Google claimed
quantumsupremacy [2019]

QWIRE[Paykin, Rand, Zdancewic,
POPL 2017]
Functional, generates
circuits, Coq-integrated
Q#[Svore et al., RWDSL 2018]by Microsoft,
functional/imperative

Logic for qubit error analysis[Hung, Hietala, Zhu, Ying, Hicks,
Wu, POPL 2019]
Quantum Hoare logic adapted
for bounding errors

2020
Silq
[Bichsel, Baader, Gehr, Vechev,
PLDI 2020]
Functional, automatic
uncomputation & a type system
for itType system for qubit connectivity[Wakizaka & Igarashi, JSSST
Congress 2020]
Type system for Selinger’s quantum
λ-calculus that ensures qubit
connectivity

6Outline• Introduction• Hoare logic as a showcase of static analysis• QPL Work (1): Ying's quantum Hoare logic• QPL Work (2): Quantum GoI for semantics of quantum λ-calculus[H. & Hoshino]• "Static analysis for hardware-specific, low-level concerns in NISQ"• QPL Work (3): Quantum Hoare logic for bounding errors [Hung+, POPL'19]• QPL Work (4): Language-Based Automated Uncomputation [Bichsel+, PLDI'20]• QPL Work (5): Type System for Qubit Connectivity[Wakizaka & Igarashi, JSSST Congress '20]

• Towards Quantum IDE
Hasuo (NII)7

Hoare Logic

静的解析 static analysis の代表例としてComputes thefactorial N! …

• A logical system for program correctness• Derives Hoare triples

Really? Can
we prove it?

• Such as

Hasuo (NII)8

Hoare Logic• A derivation (“proof”) is repeated application of syntactic derivation
rules è automated proof check & proof search
From top tobottom…
Validity of rule application ischecked (mostly) syntactically,
symbolically, mechanicallyHasuo (NII)

Desiredconclusion

9Outline• Introduction• Hoare logic as a showcase of static analysis• Program correctness, semantically• Syntactic derivation rules (proof system) in Hoare logic• Soundness (meta-)theorem, summary• QPL Work (1): Ying's quantum Hoare logic•…

Hasuo (NII)

10

Program Correctness, SemanticallyHasuo (NII)

11

Program Correctness, SemanticallyHasuo (NII)

12

Program Correctness,
SemanticallyHasuo (NII)

13

Program Correctness,
SemanticallyHasuo (NII)

14

Program Correctness,
SemanticallyHasuo (NII)

15

Outline• Introduction• Hoare logic as a showcase of static analysis• Program correctness, semantically• Syntactic derivation rules (proof system) in Hoare logic• Soundness (meta-)theorem, summary• QPL Work (1): Ying's quantum Hoare logic•…

Hasuo (NII)

16

Hoare Logic

Computes thefactorial N! …

• A logical system for program correctness• Derives Hoare triples

Really? Can
we prove it?

• Such as

Hasuo (NII)

17

Hoare Logic: (Syntactic) Derivation Rules

Hasuo (NII)18

Hoare Logic• A derivation (“proof”) is repeated application of syntactic derivation
rules è automated proof check & proof search
From top tobottom…
Validity of rule application ischecked (mostly) syntactically,
symbolically, mechanicallyHasuo (NII)

Desiredconclusion

19

Outline• Introduction• Hoare logic as a showcase of static analysis• Program correctness, semantically• Syntactic derivation rules (proof system) in Hoare logic• Soundness (meta-)theorem, summary• QPL Work (1): Ying's quantum Hoare logic•…

Hasuo (NII)

20

Are These Rules “Correct”?
• For example:• “To have A after x:=a, we need to have A[a/x] before”• Examples:

Hasuo (NII)

21

Semantics (Meaning) and Correctness• Def. A memory state is a function: Var
Z• Def. Program semantics JP K : MSt ! MSt [ {?}is a transformation of memory states, defined inductively on theconstruction of a program P<latexit sha1_base64="ndqH5UeFLzJoKVKM+rVVfF6hHNo=">AAACVXicbZHLSgMxFIbT8V4vrbp0EyyCCykzIuhSdONGqGhVaEpJMpk2mEmG5IxShj6XjyIu3OrKRxDM1Fl4OxD4859zkpMvLFPSQRg+14KZ2bn5hcWl+vLK6lqjub5x7Uxuuehyo4y9ZdQJJbXoggQlbjMraMqUuGF3p2X+5l5YJ42+gnEm+ikdaplITsFbg+YFUYpZyu8E4A4m1lYbUh6tMUkpjFhSnF/ChHhjaOVwBNRa8/AjxfOMFIQZIJNBsxW2w2ngvyKqRAtV0Rk030lseJ4KDVxR53pRmEG/oBYkV2JSJ7kTmR+KDkXPS01T4frF9OkTvOOdGCfG+qUBT93vHQVNnRunzFeW87rfudLcc5BSO7bxf0W9HJKjfiF1loPQ/OvGJFcYDC6B4lhawUGNvaDcSj805iPqKYLHXp9Sqj6gYEbFJZ/oN42/4nq/HYXt6OKgdXxSkVpEW2gb7aIIHaJjdIY6qIs4ekQv6BW91Z5qH8FsMP9VGtSqnk30I4LGJ+juuRI=</latexit>• Def. A Hoare triple {A}P{B} is true if,
for any memory state σ that satisfies A,
JP K satisfies B<latexit sha1_base64="4Qpu8Vxftwu5Vinxphey2LFnCnc=">AAACIXicbZBNS8MwGMfT+TbnW9WjCMEheJDRiqDHoRePE9wcrGWkabqFJW1Jngqj7ORH8eRVP4U38SZ+Br+D6daDbj4Q+Of/vCW/IBVcg+N8WpWl5ZXVtep6bWNza3vH3t3r6CRTlLVpIhLVDYhmgsesDRwE66aKERkIdh+Mrov8/QNTmifxHYxT5ksyiHnEKQFj9e1DT4hAETpigFvYU6q8eJoPJOnbdafhTAMvCrcUdVRGq29/e2FCM8lioIJo3XOdFPycKOBUsEnNyzRLzQIyYD0jYyKZ9vPpNyb42DghjhJlTgx46v7uyInUeiwDUykJDPV8rjBPNUiixir8r6iXQXTp5zxOM2AxnW2MMoEhwQUcHHLFKIixEYQqbh6N6ZAYImAQ1rxiYAkzDxIRTgwfd57GouicNVyn4d6e15tXJakqOkBH6AS56AI10Q1qoTai6BE9oxf0aj1Zb9a79TErrVhlzz76E9bXD+h+pN8=</latexit>

Hasuo (NII)

22

Soundness (Meta-)Theorem• Thm. In each rule applicationof Hoare logic, if the premises
are true, then the conclusion
is true• Cor. (Soundness)
Every Hoare triple that isderived in Hoare logic is true

Hasuo (NII)23

Hoare Logic: Summary• As an example ofstatic analysis techniques…
• Points• Static (⇔ dynamic):reasoning about programs without executing them
• Reasoning about infinitely many input values all at once
(N can be any integer)• Syntactic, mechanizable. Potential automation• The goal can be other than correctness (as we’ll see)• Symbol manipulation➜ need meta-theory (soundness etc.) to make sense of it
Hasuo (NII)24

Outline• Introduction• Hoare logic as a showcase of static analysis• QPL Work (1): Ying's quantum Hoare logic• QPL Work (2): Quantum GoI for semantics of quantum λ-calculus[H. & Hoshino]• "Static analysis for hardware-specific, low-level concerns in NISQ"• QPL Work (3): Quantum Hoare logic for bounding errors [Hung+, POPL'19]• QPL Work (4): Language-Based Automated Uncomputation [Bichsel+, PLDI'20]• QPL Work (5): Type System for Qubit Connectivity[Wakizaka & Igarashi, JSSST Congress '20]

• Towards Quantum IDE
Hasuo (NII)25

Quantum Hoare Logic [Ying, ACM TOPLAS 2012]• Natural extension of Hoare logic• Target language: imperative

Target programming language• Variables ➜ quantum variables• Assignment➜ application of unitary gate
• If-branch ➜ branching by measurement• Assertions: use projections• Classical: x = y + 1, ∃y. (x = 2y), x > y, …
• Quantum: a self-adjoint operator P such that 0 v P v I<latexit sha1_base64="C2cONOPAvkArJjhMYwXQ0sVixKg=">AAACIXicbZC7SgNBFIZnvcZ4W7XUYjAIFhJ2RdAyaKNdBHOBJITZ2ZNkyOwlM2eFsKTxVWxs9S3sxE58B5/BSbJFTDww8M9/zj+Xz4ul0Og4X9bS8srq2npuI7+5tb2za+/tV3WUKA4VHslI1T2mQYoQKihQQj1WwAJPQs3r34z7tUdQWkThAw5jaAWsG4qO4AyN1baPnKYe6MTTgDCgZTq7u2vbBafoTIouCjcTBZJVuW3/NP2IJwGEyCXTuuE6MbZSplBwCaN8M9EQM95nXWgYGbIAdCud/GJET4zj006kzAqRTtzZRMoCrYeBd6YxYGqofBMJGPb0/NDY/K/XSLBz1UpFGCcIIZ/e2EkkxYiO2VBfKOAoh0YwroR5NOU9phhHQzDfHB+YsUy9SPqjvAHkzuNYFNXzousU3fuLQuk6Q5Ujh+SYnBKXXJISuSVlUiGcPJEX8krerGfr3fqwPqejS1aWOSB/yvr+BUYkpD0=</latexit>
sha1_base64="AEqs4xbFyalbumKvzHK32uSZIwU=">AAAB9XicbZC7TsMwFIZPuJZQoMwsFhUSA6oSFhiRWBiLRC9SG1WO47RWfYlsBymKujGx8hZsiKfhJXgGnDYDtPySpV//8Tk+/uKMM2OD4Mvb2t7Z3dtvHPiHTf/o+KTV7BuVa0J7RHGlhzE2lDNJe5ZZToeZpljEnA7i+X1VHzxTbZiST7bIaCTwVLKUEWxd1J202kEnWAptmrA2bag1aX2PE0VyQaUlHBszCoPMRiXWlhFOF/44NzTDZI6ndOSsxIKaqFyuuUAXLklQqrQ70qJl+rujxMKYQsRXxgqsC524FoHtzKxfqsL/aqPcprdRyWSWWyrJ6sU058gqVH0eJUxTYnnhDCaauaURmWGNiXWI/HE1sIZVxoonC9/xCddpbJr+dScMOuFjAA04g3O4hBBu4A4eoAs9IJDAK7x5L96797HiuOXVQE/hj7zPH6JvlhU=</latexit>
sha1_base64="qvfSzgMp/Z7mEScNWsULKS9qdnA=">AAACFnicbZDLSgMxFIbPeK21anWri2ARXEiZcaNLwY3uKtgLtKVkMqdtaObS5IxQhm58FTdu9S3ciTtfwmcwvSxq6w+BP//JOUk+P1HSkOt+O2vrG5tb27md/G5hb/+geFiomTjVAqsiVrFu+NygkhFWSZLCRqKRh77Cuj+4ndTrT6iNjKNHGiXYDnkvkl0pONmoUzxxW2ZoUt8g4ZBV2OLuvlMsuWV3KrZqvLkpwVyVTvGnFcQiDTEiobgxTc9NqJ1xTVIoHOdbqcGEiwHvYdPaiIdo2tn0F2N2ZpOAdWNtV0Rsmi52ZDw0ZhT6F4ZCrkc6sC0hp75ZPjQJ/6s1U+petzMZJSlhJGY3dlPFKGYTNiyQGgWpkTVcaGkfzUSfay7IEsy3JgPnLDM/VsE4bwF5yzhWTe2y7Lll78GFHBzDKZyDB1dwA3dQgSoIeIZXeIN358X5cD5nKNecOdMj+CPn6xc38qKx</latexit>
sha1_base64="CNVFnYN9H/31S8cxeKBX4j/WAwU=">AAACIXicbZC7TgJBFIZn8YZ4Qy21mEhMLAzZtdGSaKMdJnJJgJDZ2QNMmL0wc9aEbGh8FRtbfQs7Y2d8B5/BWdgCwZNM8s9/zj+Xz42k0GjbX1ZuZXVtfSO/Wdja3tndK+4f1HUYKw41HspQNV2mQYoAaihQQjNSwHxXQsMd3qT9xiMoLcLgAccRdHzWD0RPcIbG6haP7bYe6djVgDCiVTq/u+sWS3bZnhZdFk4mSiSrarf40/ZCHvsQIJdM65ZjR9hJmELBJUwK7VhDxPiQ9aFlZMB80J1k+osJPTWOR3uhMitAOnXnEwnztR777rlGn6mx8kzEZzjQi0Op+V+vFWPvqpOIIIoRAj67sRdLiiFN2VBPKOAox0YwroR5NOUDphhHQ7DQTg/MWCZuKL1JwQByFnEsi/pF2bHLzr1dqlxnqPLkiJyQM+KQS1Iht6RKaoSTJ/JCXsmb9Wy9Wx/W52w0Z2WZQ/KnrO9fROSkOQ==</latexit>• Semantics: (as expected)

Hasuo (NII)

26

Quantum Hoare Logic [Ying, ACM TOPLAS 2012]• Derivation rules mirror classical ones

• Case study: correctness of the Grover search algorithm“after execution, a solution is found with at least this much probability”
Hasuo (NII)27

Outline• Introduction• Hoare logic as a showcase of static analysis• QPL Work (1): Ying's quantum Hoare logic• QPL Work (2): Quantum GoI for semantics of quantum λ-calculus[H. & Hoshino]• "Static analysis for hardware-specific, low-level concerns in NISQ"• QPL Work (3): Quantum Hoare logic for bounding errors [Hung+, POPL'19]• QPL Work (4): Language-Based Automated Uncomputation [Bichsel+, PLDI'20]• QPL Work (5): Type System for Qubit Connectivity[Wakizaka & Igarashi, JSSST Congress '20]

• Towards Quantum IDE
Hasuo (NII)28

Quantum Geometry of Interaction[H. & Hoshino, LICS’11 & Ann. Pure Appl. Logic ’17]
• Semantics of higher-order functional QPL
Quantum teleportation:
where

Types from linear logic forenhanced resource analysis(qubits cannot be used twice➜ no-cloning)• ”Quantum data, classical control”—much like other QPLs
• Semantics of higher-order functional languages is challenging already inclassical settings (λ-calculus, domain theory, categorical semantics, …)

Quantum Geometry of Interaction[H. & Hoshino, LICS’11 & Ann. Pure Appl. Logic ’17]
• Tool: geometry of interaction (GoI) [Girard 1987]• Higher-order computation interpreted
by first-order interaction• Categorical axiomatization bytraced monoidal categories

MN
What’s the value of x?

What’s the value of f2?

Then f2 is (2 + 1)

x is 2[Abramsky, Haghverdi, Scott 2002]

M ⌘<latexit sha1_base64="0rXjaoMNhDnWjeLnW0xaZBjEcCI=">AAACH3icbZDLSsNAFIYn9VbjLepON4NFcFFCUgQFN0U3boQKthWaUCaTSTt0cnFmUgih4Ku4catv4U7c9iV8BidtFtp6YJif/5x/Lp+XMCqkZU21ysrq2vpGdVPf2t7Z3TP2DzoiTjkmbRyzmD96SBBGI9KWVDLymHCCQo+Rrje6KfrdMeGCxtGDzBLihmgQ0YBiJJXVN47unCuHPKV0rHamcj6CgQmdetDoGzXLtGYFl4Vdihooq9U3vh0/xmlIIokZEqJnW4l0c8QlxYxMdCcVJEF4hAakp2SEQiLcfPaHCTxVjg+DmKsVSThzfydyFAqRhV5dyBDxjPsqEiI5FItDhflfr5fK4NLNaZSkkkR4fmOQMihjWJCBPuUES5YpgTCn6tEQDxFHWCp+ulMcWJLMvZj5E10BshdxLItOw7Qt074/rzWvS1RVcAxOwBmwwQVoglvQAm2AwTN4BW/gXXvRPrRP7Ws+WtHKzCH4U9r0B+9qolo=</latexit>f. f 2N ⌘x. (x + 1)

<latexit sha1_base64="Q6NA26lYW/78g7/VAGQxoirAO9o=">AAACInicbZDLSsNAFIYn9VbjLepShMEiVCwlEUHBTdGNK6lgL9CUMplM2qEzSZyZlJbQla/ixq2+hTtxJfgMPoPTNgutHhjm5z/nn8vnxYxKZdsfRm5hcWl5Jb9qrq1vbG5Z2zt1GSUCkxqOWCSaHpKE0ZDUFFWMNGNBEPcYaXj9q0m/MSBC0ii8U6OYtDnqhjSgGCltdaz9G/fCJfcJHeid6ZyP4LAM3VJxeOwcdayCXbanBf8KJxMFkFW1Y325foQTTkKFGZKy5dixaqdIKIoZGZtuIkmMcB91SUvLEHEi2+n0G2N4qB0fBpHQK1Rw6v5MpIhLOeJeSSqOxEj4OsKR6sn5oYn5X6+VqOC8ndIwThQJ8ezGIGFQRXACB/pUEKzYSAuEBdWPhriHBMJKIzTdyYEZzNSLmD82NSBnHsdfUT8pO3bZuT0tVC4zVHmwBw5AETjgDFTANaiCGsDgATyBZ/BiPBqvxpvxPhvNGVlmF/wq4/MbfrajGA==</latexit>
sha1_base64="AEqs4xbFyalbumKvzHK32uSZIwU=">AAAB9XicbZC7TsMwFIZPuJZQoMwsFhUSA6oSFhiRWBiLRC9SG1WO47RWfYlsBymKujGx8hZsiKfhJXgGnDYDtPySpV//8Tk+/uKMM2OD4Mvb2t7Z3dtvHPiHTf/o+KTV7BuVa0J7RHGlhzE2lDNJe5ZZToeZpljEnA7i+X1VHzxTbZiST7bIaCTwVLKUEWxd1J202kEnWAptmrA2bag1aX2PE0VyQaUlHBszCoPMRiXWlhFOF/44NzTDZI6ndOSsxIKaqFyuuUAXLklQqrQ70qJl+rujxMKYQsRXxgqsC524FoHtzKxfqsL/aqPcprdRyWSWWyrJ6sU058gqVH0eJUxTYnnhDCaauaURmWGNiXWI/HE1sIZVxoonC9/xCddpbJr+dScMOuFjAA04g3O4hBBu4A4eoAs9IJDAK7x5L96797HiuOXVQE/hj7zPH6JvlhU=</latexit>
sha1_base64="sCpVztIFuQl8b//Ghe6wu0ZiyTQ=">AAACF3icbZDLSgMxFIbPeK216uhWhGARKpZhxo2CG8GNK6lgL9ApJZPJtKGZi0mmtAxd+Spu3OpbuBNXvoTPYNrOQlsPhPz8J/9J8nkJZ1LZ9pexsrq2vrFZ2Cpul3Z298z9UkPGqSC0TmIei5aHJeUsonXFFKetRFAcepw2vcHNtN8cUiFZHD2ocUI7Ie5FLGAEK211zaM798qljykb6p3rnI/RyEJutTI6c067Ztm27FmhZeHkogx51brmt+vHJA1ppAjHUrYdO1GdDAvFCKeToptKmmAywD3a1jLCIZWdbPaNCTrRjo+CWOgVKTRzfycyHEo5Dr2qVCEWY+HrSIhVXy4empr/9dqpCi47GYuSVNGIzG8MUo5UjKZwkM8EJYqPtcBEMP1oRPpYYKI0wqI7HZjDzLyY+5OiBuQs4lgWjXPLsS3n3oYCHMIxVMCBC7iGW6hBHQg8wQu8wpvxbLwbH3OUK0bO9AD+lPH5A31JoYs=</latexit>
sha1_base64="KgZgQgyysxQ7d1zMJIQg8vhDGsk=">AAACInicbZDLSsNAFIYn9VbrLepShMEiVCwhcaPgpujGlVSwF2hKmUym7dBJJs5MSkPoyldx41bfwp24EnwGn8Fpm4W2Hhjm5z/nn8vnRYxKZdufRm5peWV1Lb9e2Njc2t4xd/fqkscCkxrmjIumhyRhNCQ1RRUjzUgQFHiMNLzB9aTfGBIhKQ/vVRKRdoB6Ie1SjJS2OubhrXvpkoeYDvXOdM5HcGRBt1wanTonHbNoW/a04KJwMlEEWVU75rfrcxwHJFSYISlbjh2pdoqEopiRccGNJYkQHqAeaWkZooDIdjr9xhgea8eHXS70ChWcur8TKQqkTAKvLFWARCJ8HQmQ6sv5oYn5X68Vq+5FO6VhFCsS4tmN3ZhBxeEEDvSpIFixRAuEBdWPhriPBMJKIyy4kwMzmKnHmT8uaEDOPI5FUT+zHNty7uxi5SpDlQcH4AiUgAPOQQXcgCqoAQwewTN4Aa/Gk/FmvBsfs9GckWX2wZ8yvn4AfXajFA==</latexit>• Different base categories for different effects(nondeterminism, probability, quantum). The essence is the same
Hasuo (NII)30

Outline• Introduction• Hoare logic as a showcase of static analysis• QPL Work (1): Ying's quantum Hoare logic• QPL Work (2): Quantum GoI for semantics of quantum λ-calculus[H. & Hoshino]• "Static analysis for hardware-specific, low-level concerns in NISQ"• QPL Work (3): Quantum Hoare logic for bounding errors [Hung+, POPL'19]• QPL Work (4): Language-Based Automated Uncomputation [Bichsel+, PLDI'20]• QPL Work (5): Type System for Qubit Connectivity[Wakizaka & Igarashi, JSSST Congress '20]

• Towards Quantum IDE
Hasuo (NII)31

Static Analysis:
Towards Low-Level Concerns• Static analysis: reasoning about programs without execution• Goals: correctness (in Hoare logic, …),security (non-interference [Sabelfeld & Myers ‘03], differential privacy [Barthe+ ‘14], …),complexity analysis [Hofmann’00], …

• For quantum programs?
• Execution is costly ➜ static analysis makes even bigger sense• Can be seen as generalization of classical simulation• Hardware constraints (such as in NISQ)➜ a number of new goals of static analysis(error estimate, uncomputation, qubit connectivity, …)• “Static analysis for hardware-specific, low-level concerns in NISQ”
Hasuo (NII)32

Physical
Not at all realization
emerging
comprehensive!
➜ let’s take “details”
seriously

Theoretically,
there is nothing
fundamentallychallenging…

Chance to exercise
advanced PL &semanticaltechniques…

Trends in
Quantum Programming Language (QPL) Research
D-Wave’s Quantum
Annealing Machine[2011]

No physicalrealization➜ no bothering
details J

IBM Quantum
Experience [2016]

2015

2010
Quantum Hoare Logic[Ying, ACM TOPLAS 2012]
Program logic for correctness ofimperative quantum programs

Quantum lambda
calculus [Selinger &Valiron, 2008, 2009]
Functional,
categorical semantics

QCL[Ömer 2000]
First QPL,
imperative
quantum λ-calculus[van Tonder,
SIAM J. Comp. 2004]
Functional, linear
types for no-cloning,

Quantum I/O monad[Green & Altenkirch, 2009]
Making Haskell a QPL

Quantum flowchart language[Selinger, MSCS 2004]
Formal semantics bysuperoperators

Quantum lambda
calculus [Hasuo &Hoshino, LICS 2011]
Categorical GoI
semantics for “quantum
data, classical control”

Quipper[Green, Lumsdaine, Ross,
Selinger, Valion, PLDI 2013]
A functional language thatgenerates quantum circuits
Quantum lambda calculus[Pagani, Selinger, Valion,
POPL 2014]
Anothercategorical
Hasuo
(NII)
semantics

Google claimed
quantumsupremacy [2019]

QWIRE[Paykin, Rand, Zdancewic,
POPL 2017]
Functional, generates
circuits, Coq-integrated
Q#[Svore et al., RWDSL 2018]by Microsoft,
functional/imperative

Logic for qubit error analysis[Hung, Hietala, Zhu, Ying, Hicks,
Wu, POPL 2019]
Quantum Hoare logic adapted
for bounding errors

2020
Silq
[Bichsel, Baader, Gehr, Vechev,
PLDI 2020]
Functional, automatic
uncomputation & a type system
for itType system for qubit connectivity[Wakizaka & Igarashi, JSSST
Congress 2020]
Type system for Selinger’s quantum
λ-calculus that ensures qubit
connectivity

33

Outline• Introduction• Hoare logic as a showcase of static analysis• QPL Work (1): Ying's quantum Hoare logic• QPL Work (2): Quantum GoI for semantics of quantum λ-calculus[H. & Hoshino]• "Static analysis for hardware-specific, low-level concerns in NISQ"• QPL Work (3): Quantum Hoare logic for bounding errors [Hung+, POPL'19]• QPL Work (4): Language-Based Automated Uncomputation [Bichsel+, PLDI'20]• QPL Work (5): Type System for Qubit Connectivity[Wakizaka & Igarashi, JSSST Congress '20]

• Towards Quantum IDE
Hasuo (NII)34

Quantum Hoare Logic for Bounding Errors[Hung, Hietala, Zhu, Ying, Hicks, Wu, POPL’19]• Target language:
Ying’s imperative quantum QPL + noisy unitary gates
Applies U with prob. 1-p;

Hasuo (NII)

applies Φ with prob. p (error)

35

Quantum Hoare Logic for Bounding Errors[Hung, Hietala, Zhu, Ying, Hicks, Wu, POPL’19]• The logic extends Ying’s quantum Hoare logic with“error bounding judgments”

If the current quantum state ρ satisfies tr(Qρ) ≧ λ,then the trace distance between• the result of the noisy program P and• that of the ideal program P
is at most ε (the actual def. involves ancillas)• Derivation rules are introduced,
such as

Hasuo (NII)36

Quantum Hoare Logic for Bounding Errors[Hung, Hietala, Zhu, Ying, Hicks, Wu, POPL’19]• They also show that, for the base case (noisy unitary gate),
error bounds can be computed by solving suitable SDP

Hasuo (NII)37

Quantum Hoare Logic for Bounding Errors[Hung, Hietala, Zhu, Ying, Hicks, Wu, POPL’19]• Examples:
quantum Bernoulli factory (QBF)

Fault-tolerant QBF

ENCODE, CORRECT:
3-qubit repetition code

Classical computation(symbolic reasoning + SDP)O(p)if p = pV = pU
“For ρ s.t. tr(Iρ) ≧ 0”
➜ no constraint

whereClassical computation(symbolic reasoning + SDP)

O(p2)
Hasuo (NII)

if p = pV = pU
38

Outline• Introduction• Hoare logic as a showcase of static analysis• QPL Work (1): Ying's quantum Hoare logic• QPL Work (2): Quantum GoI for semantics of quantum λ-calculus[H. & Hoshino]• "Static analysis for hardware-specific, low-level concerns in NISQ"• QPL Work (3): Quantum Hoare logic for bounding errors [Hung+, POPL'19]• QPL Work (4): Language-Based Automated Uncomputation [Bichsel+, PLDI'20]• QPL Work (5): Type System for Qubit Connectivity[Wakizaka & Igarashi, JSSST Congress '20]

• Towards Quantum IDE
Hasuo (NII)39

Language-Based Automated Uncomputation[Bichsel, Baader, Gehr, Vechev, PLDI’20]• Physical qubits are scarce ➜ ancilla qubits should be reused
ancilla |0⟩

c1

|0⟩

c2

Reuse?

• But old ancilla shouldn’t be projected out(affects other qubits in entanglement)• ➜ Uncomputation!
• Make operations on ancilla qubits reversible, and• Apply their inverse to recover |0⟩
Hasuo (NII)40

Language-Based Automated Uncomputation[Bichsel, Baader, Gehr, Vechev, PLDI’20]• Goal: free (quantum) programmers
from tedious task of writing
uncomputation code…
• by automatic uncomputation• Detect reversible operations
on ancilla qubits, and• Insert uncomputation code

Code in Silq [Bichsel+ ‘20].
Uncomputation is implicit and automatic

Hasuo (NII)

Explicit uncomputation in Quipper 41

Outline• Introduction• Hoare logic as a showcase of static analysis• QPL Work (1): Ying's quantum Hoare logic• QPL Work (2): Quantum GoI for semantics of quantum λ-calculus[H. & Hoshino]• "Static analysis for hardware-specific, low-level concerns in NISQ"• QPL Work (3): Quantum Hoare logic for bounding errors [Hung+, POPL'19]• QPL Work (4): Language-Based Automated Uncomputation [Bichsel+, PLDI'20]• QPL Work (5): Type System for Qubit Connectivity[Wakizaka & Igarashi, JSSST Congress '20]

• Towards Quantum IDE
Hasuo (NII)

42

Type System for Qubit Connectivity[Wakizaka & Igarashi, 日本ソフトウェア科学会 2020]• Approaches to physical qubits

Superconducting
Trapped ion

Scalability

Qubit
connectivity

Qubit
lifetime

Gate operation
time

Players

✓

✘

✘

✓

(c. 50 qubits)(adjacent only)(c. 50-100 µs)(c. 10-50 ns)

Google, IBM,
…

??

✓

✓

✘

(fully connected)(> 1000 s)(c. 3-50 µs)

Honeywell,
IonQ, …

• Some issues are physical, but others are logical➜ QPL research can help the latter
Hasuo (NII)

43

Type System for Qubit Connectivity[Wakizaka & Igarashi, 日本ソフトウェア科学会 2020]• Qubit connectivity:
binary gates (such as CNOT) can beapplied only to connected qubits• Different hardware has different coupling graphs• An issue quantum programmers shouldtake care of• Or better: automated qubit connectivity analysis• “Does the given program adhere to qubit connectivity
constraints?” (this work)• Automatic qubit allocation and swapping

Hasuo (NII)

Coupling graph for
IBM qx2

44

Type System for Qubit Connectivity[Wakizaka & Igarashi, 日本ソフトウェア科学会 2020]• Approach: a type system“if a program is typable then it doesn’t go wrong”• The user annotates types, including the qubit allocation information• CNOT is typable only if there is suitable qubit connectivity
i and j must be connected in
the connectivity graph Γ

i-th quantum register

Hasuo (NII)45

Type System for Qubit Connectivity[Wakizaka & Igarashi, 日本ソフトウェア科学会 2020]• Typing rules. Features:• Target language:
functional, higher-order. E.g.

• Based on linear logic• CNOT requires connectivity• Dependent product Π𝑖. 𝑇 𝑖
for qidx abstraction(“for any qidx i”)• Qubit connectivity constraints K
as types(which can further be abstracted)

Hasuo (NII)

46

Type System for Qubit Connectivity[Wakizaka & Igarashi, 日本ソフトウェア科学会 2020]• Correctness theorems “if a program is typable then it doesn’t go wrong”• Thm. (Progress) If a program M is typable (), then

M is either a value, or M has a reduction
Special programs for output ofcomputation (constants, functions, …)• Thm. (Preservation)
andA computation step in λ-calculus

Types are preserved along reduction

imply

Hasuo (NII)47

Cf. proof tree in Hoare logic

Type System for Qubit Connectivity[Wakizaka & Igarashi, 日本ソフトウェア科学会 2020]• Usage(note that this is static)• A programmer writes a program M with type annotation(amounts to writing a type derivation tree)• Type checker returns no type error(i.e. all derivation steps adhere to rules)➜ the programmer is sure that there will be
no runtime error that is due to qubit connectivity

Type derivationtree• Future work
• Type checking (“does the user-specified qubit allocation respect connectivity?”)➜ type inference(automatic search for type derivation trees,i.e. automated qubit allocation)• Accommodating qubit reallocation (costly but sometimes inevitable)
Hasuo (NII)48

Outline• Introduction• Hoare logic as a showcase of static analysis• QPL Work (1): Ying's quantum Hoare logic• QPL Work (2): Quantum GoI for semantics of quantum λ-calculus[H. & Hoshino]• "Static analysis for hardware-specific, low-level concerns in NISQ"• QPL Work (3): Quantum Hoare logic for bounding errors [Hung+, POPL'19]• QPL Work (4): Language-Based Automated Uncomputation [Bichsel+, PLDI'20]• QPL Work (5): Type System for Qubit Connectivity[Wakizaka & Igarashi, JSSST Congress '20]

• Towards Quantum IDE
Hasuo (NII)

49

Not at allcomprehensive!

repeatTrends in
Quantum Programming Language (QPL) Research
D-Wave’s Quantum
Annealing Machine[2011]IBM Quantum
Experience [2016]

2015

2010
Quantum Hoare Logic[Ying, ACM TOPLAS 2012]
Program logic for correctness ofimperative quantum programs

Quantum lambda
calculus [Selinger &Valiron, 2008, 2009]
Functional,
categorical semantics

QCL[Ömer 2000]
First QPL,
imperative
quantum λ-calculus[van Tonder,
SIAM J. Comp. 2004]
Functional, linear
types for no-cloning,

Quantum I/O monad[Green & Altenkirch, 2009]
Making Haskell a QPL

Quantum flowchart language[Selinger, MSCS 2004]
Formal semantics bysuperoperators

Quantum lambda
calculus [Hasuo &Hoshino, LICS 2011]
Categorical GoI
semantics for “quantum
data, classical control”

Quipper[Green, Lumsdaine, Ross,
Selinger, Valion, PLDI 2013]
A functional language thatgenerates quantum circuits
Quantum lambda calculus[Pagani, Selinger, Valion,
POPL 2014]
Anothercategorical
Hasuo
(NII)
semantics

Google claimed
quantumsupremacy [2019]

QWIRE[Paykin, Rand, Zdancewic,
POPL 2017]
Functional, generates
circuits, Coq-integrated
Q#[Svore et al., RWDSL 2018]by Microsoft,
functional/imperative

Logic for qubit error analysis[Hung, Hietala, Zhu, Ying, Hicks,
Wu, POPL 2019]
Quantum Hoare logic adapted
for bounding errors

2020
Silq
[Bichsel, Baader, Gehr, Vechev,
PLDI 2020]
Functional, automatic
uncomputation & a type system
for itType system for qubit connectivity[Wakizaka & Igarashi, JSSST
Congress 2020]
Type system for Selinger’s quantum
λ-calculus that ensures qubit
connectivity

50Physical
Not at all realization
emerging
comprehensive!
➜ let’s take “details”
seriously

Theoretically,
there is nothing
fundamentallychallenging…

Chance to exercise
advanced PL &semanticaltechniques…

Trends in
Quantum Programming Language (QPL) Research
D-Wave’s Quantum
Annealing Machine[2011]

No physicalrealization➜ no bothering
details J

IBM Quantum
Experience [2016]

2015

2010
Quantum Hoare Logic[Ying, ACM TOPLAS 2012]
Program logic for correctness ofimperative quantum programs

Quantum lambda
calculus [Selinger &Valiron, 2008, 2009]
Functional,
categorical semantics

QCL[Ömer 2000]
First QPL,
imperative
quantum λ-calculus[van Tonder,
SIAM J. Comp. 2004]
Functional, linear
types for no-cloning,

Quantum I/O monad[Green & Altenkirch, 2009]
Making Haskell a QPL

Quantum flowchart language[Selinger, MSCS 2004]
Formal semantics bysuperoperators

Quantum lambda
calculus [Hasuo &Hoshino, LICS 2011]
Categorical GoI
semantics for “quantum
data, classical control”

Quipper[Green, Lumsdaine, Ross,
Selinger, Valion, PLDI 2013]
A functional language thatgenerates quantum circuits
Quantum lambda calculus[Pagani, Selinger, Valion,
POPL 2014]
Anothercategorical
Hasuo
(NII)
semantics

Google claimed
quantumsupremacy [2019]

QWIRE[Paykin, Rand, Zdancewic,
POPL 2017]
Functional, generates
circuits, Coq-integrated
Q#[Svore et al., RWDSL 2018]by Microsoft,
functional/imperative

Logic for qubit error analysis[Hung, Hietala, Zhu, Ying, Hicks,
Wu, POPL 2019]
Quantum Hoare logic adapted
for bounding errors

2020
Silq
[Bichsel, Baader, Gehr, Vechev,
PLDI 2020]
Functional, automatic
uncomputation & a type system
for itType system for qubit connectivity[Wakizaka & Igarashi, JSSST
Congress 2020]
Type system for Selinger’s quantum
λ-calculus that ensures qubit
connectivity

51

Static Analysis in the Quantum Age• Static analysis: reasoning about programs without execution• Goals, conventionally:correctness (in Hoare logic, …),security (non-interference [Sabelfeld & Myers ‘03], differential privacy [Barthe+ ‘14], …),complexity analysis [Hofmann’00], …

• For quantum programs?
• Execution is costly and probabilistic➜ static analysis makes even bigger sense• Can be seen as generalization of classical simulation• “Static analysis for hardware-specific, low-level concerns in NISQ”• Error estimate [Hung+, POPL’19]• Automated uncomputation [Bichsel+, PLDI’20]• Qubit connectivity [Wakizaka & Igarashi, JSSST Congress ‘20]
Hasuo (NII)52

Static Analysis and Quantum Software

Information
obtained

Respecting connectivity,
using types to generategraph-theoretic constraints
Syntactic type-checking andrule-based code insertion[Bichsel+ PLDI’20]

Automated qubit
allocation

Automateduncomputation

Type-based qubit
connectivity check
Syntactic type-checking[Wakizaka & Igarashi ‘20]

Logical error
estimate

Actualexecution

Quantum
computation

Classical
simultation

Classical
computation

Precise result,but for single input

For an infinite familyof input. The boundmay not be sharp, andit’s rather costly (SDP)[Hung+, POPL’19]… and much more!
Hasuo (NII)

Computational
cost

53

Towards Quantum IDE(Integrated Development Environment)• Support quantum programmers to write correct and efficient code
• Conventional IDE functionalities:
syntax highlighting, code completion, refactoring, version control,
debugging support, code search, …
For managing a big codebase…
• Not relevant to quantum programs (yet)• Works for quantum programs as well

wikipedia• + quantum-specific functionalities:
error estimate, automated uncomputation, automated qubit allocation, …

• More semantical consideration is needed➜ static analysis, logical and type-theoretic techniques from the PL community• Spare quantum trials & errors by classical static reasoning• Choice/design of a QPL is important(structured programming [Dijkstra] ➜ better logical support)

Hasuo (NII)54

Towards Quantum IDE(Integrated Development Environment)• To the PL community:
it’s time to “get our hands dirty”• Researchers prefer fundamental challenges(logical correctness, soundness and completeness meta-theorems, …)• In comparison, low-level concerns in NISQ may seem to be minor
Dynamic analysis(testing) is costly!
• but they can really benefit from static analysis techniques• Theoreticians diving into applications• Need to dive in— nobody formulates a clean theoretical problem for you• Matching practical needs and theoretical seeds— fun and rewarding• (in our ERATO project:
category theorists in automated driving safety)
Hasuo (NII)55

ご清聴ありがとうございました
蓮尾 ⼀郎（NII, i.hasuo@acm.org）

Summary

In collaboration with
星野 直彦（崇城⼤），脇坂 遼・五⼗嵐 淳 （京⼤）• Static analysis: reasoning about programs without executing it• “Static analysis for hardware-specific, low-level concerns in NISQ”• Execution is costly and probabilistic ➜ dynamic analysis (testing) is hard
• Hardware limitation (NISQ) ➜ a lot of low-level concerns

Actualexecution• Examples:
logical error bounds [Hung+ ’19],
automatic uncomputation [Bichsel+ ’20],
connectivity check [Wakizaka & Igarashi ‘20], …
• Quantum IDE for correct and efficient code, with the help of static analysis• To PL people: QPL is a gold mine. Let’s dive in!
To others: involve (open-minded) PL people in your quantum software project!
Information
obtained

Respecting connectivity,
using types to generategraph-theoretic constraints

Syntactic type-checking andrule-based code insertion[Bichsel+ PLDI’20]

Automated qubit
allocation

Automateduncomputation

Type-based qubit
connectivity check

Syntactic type-checking[Wakizaka & Igarashi ‘20]

Logical error
estimate

Classical
simultation
Precise result,but for single input

For an infinite familyof input. The boundmay not be sharp, andit’s rather costly (SDP)[Hung+, POPL’19]… and much more!

Computational
cost

Hasuo (NII)

56

Quantum
computation
Classical
computation