日本ソフトウェア科学会第 37 回大会 (2020 年度) 講演論文集

量子ビット連結性制約検査のための依存型システム
脇坂 遼

五十嵐 淳

量子回路モデルに基づく量子プログラムでは，量子ゲートを量子ビットに適用することで計算を行う．量子ゲートの
うち，CNOT ゲートは量子ビットペアに適用される特殊なゲートである．この特殊性から，実際の量子コンピュータ上では CNOT ゲートは特定の量子ビットペアにしか適用できない．この制約は qubit connectivity とよばれ，coupling graph という，量子ビットを頂点とし，CNOT ゲートが適用できる量子ビット対を辺とするグラフで表現される．本研究では，量子プログラムが qubit connectivity 制約を満たすかどうかを検証するために，Selinger
らの量子ラムダ計算に依存型を導入した型システムを提案する．そして，与えられた coupling graph のもとで型付け可能なプログラムが，その実行中の CNOT ゲートの適用時に制約に違反しないことを証明する．

q0

1 はじめに量子ゲートを用いた量子計算においては，量子ビッ
トに量子ゲートを作用させることで計算を行う．量子

q1

q2

q3

計算のためのプログラミング言語のモデルとして，ラムダ計算に量子ビットと量子ゲートを導入したような体系 [19] [14] [15] [1] [12] [4] [3] が研究されてきている．

q4

これらの体系では，線形型などを使って，量子複製不可能定理 (no-cloning theorem) [20] に由来する量子

図1

IBM qx2 量子コンピュータの coupling graphプログラム独特の制約を静的に検査するものが多い．
量子プログラムやアルゴリズムを設計する際には，の量子ビットペアにしか適用できないという制約であ量子ゲートを任意の量子ビットにたいして正確に適用る．この制約は，量子ビットを頂点とし，CNOT ゲー

できることを前提にすることが多いが，実際の量子トが適用できるペアを辺とする，coupling graph と呼コンピュータ上で動作させる際には量子誤りや qubit

ばれるグラフで表現される．Coupling graph の辺はconnectivity といったハードウェアに由来する制約

有向辺であり，始点を control qubit，終点を targetを考慮する必要がある．

qubit とする CNOT ゲートが実行できる．Coupling

Qubit connectivity 制約 (以下，単に連結性制約とgraph は量子コンピュータアーキテクチャ毎に固有の呼ぶ) とは，量子ゲートのうち CNOT ゲートは特定ものであり，例えば IBM の qx2 量子コンピューター[2] は図 1 に表される coupling graph をもつ． 量子∗ A Dependent Type System for Qubit Connectivity

Veriﬁcation
This is an unrefereed paper. Copyrights belong to
the Author(s).
Ryo Wakizaka, Atsushi Igarashi, 京 都 大 学 大 学 院 情報学研究科, Graduate School of Informatics, Kyoto
University.

プログラムを実機上で動かす際には，対象のアーキテ
クチャの coupling graph に対して動かしたいプログ
ラムが制約を満たしているか，すなわち，そのプログラムを実行した際に CNOT ゲートが適用されうる任意の量子ビットペアが，coupling graph 上で辺で直接隣接していることを検証する必要がある．しかしなを表す情報を付加する [18]．use κ は 0, 1, ω のいず

がら，プログラムが連結性制約に反していないことをれかの値をとり，κ = 0 ならばその値は使えないこ

静的に保証する枠組みはあまり研究されていない．

と，κ = 1 ならば高々1 回だけ用いられることを表し，以上を踏まえ，本研究では関数型量子プログラムのκ = ω なら使用回数に制限がないことを表す．例えための連結性制約を満たすことを保証するための静ば，ペア型 T1 ⊗κ T2 は，ペアから κ 回要素が取り的型システムを提案する．この型システムは，依存型出せることを示す．量子ビット型を qbit とすれば，を使うことで，coupling graph 上で隣接していない

高々1 回だけ用いられる量子ビット型は qbit1 と表

量子ビットペアへの CNOT ゲートの適用を禁止する

記される．

ものとなっている．本論文の具体的な技術的貢献は以下の通りである．

• Selinger らの量子ラムダ計算 [15] を拡張した体Π;

型環境中の変数の型につけられた use はその変数が何回使えるかを表すので，ペアや関数適用など複数の部分式を持つ式に対する型付け規則では，各部分の形式的定義を与える．

式のための型環境の use の合計を考慮する必要があ• 型付け可能なプログラムは連結性制約を満たする．例えば，ペアに対する型付け規則はだいたい以下

系 λQことを意味する型安全性定理を示す
本論文は以下のように構成される．第 2 節では，提案する体系について概要を述べる．第 3 節では，提案する体系の形式的な定義，型システムおよび操作的意味論について述べる．第 4 節では，提案する体系が備える性質について述べる．第 5 節では，型がつく
プログラムの具体例を述べる．第 6 節では関連研究について述べ，第 7 節で結論と今後の課題を述べる．

2 提案体系の概要
本論文で与える λQΠ; の型システムは，線形型，

singleton 型，依存関数型などを使って，与えられたのようになる．
Γ1 ` M : T1
Γ2 ` N : T2
Γ1 + Γ2 ` hM, N i : T1 ⊗κ T2
結論の Γ1 + Γ2 は，ふたつの型環境に現れる型の useを足しあわせる演算である．これによると，

x : unitω ` hx, xi : unitω ⊗κ unitω
は，ペアの両要素 x の use が ω であり ω + ω = ωとなるので導出できるが，

x : qbit1 ` hx, xi : qbit1 ⊗κ qbit1
は，ペアの両要素 x の use 1 を足すと 1 + 1 = ω になるので導出できない．
本節の以降の説明では，簡単のため use を省略す
ることにする．

プログラムが連結性制約を満たすことを検査する．以下では，体系の形式的定義を与える前にそれらのアイ
デアを概観する．

2. 2 Singleton type による量子ビット型の詳
細化
次に，依存型による連結性制約の検証について述

2. 1 線形型
線形型は，値が一度しか使われないことを示すための型である．第 1 節で述べたとおり，量子ビットは複製不可能であるため，量子ビットがプログラム中で複製されないことを線形型によって保証する．例えば，量子ビット q を受け取って複製し，ペアを作るような以下のプログラム M1 は線形型システムにより型
エラーとすることができる．

M1 ≡ (λx. hx, xi) q
λQ

Π;の型システムでは，各型コンストラクタにuse と呼ばれる，その型を持つ値が何回使用されるかべる．連結性制約で問題になるのは CNOT ゲートであるから，CNOT ゲートを適用できる量子ビット
ペアを型付け規則で制限できるような型システムを構築する必要がある．このために，適用できる量子ビットペアの情報，すなわち coupling graph の情報を型判断にのせ，プログラム中の量子ビット変数がcoupling graph 上のどの量子ビットに対応するのかを追跡する．
このために，λQΠ; では，coupling graph 上のノードに対応するラベル i, j を導入し，各量子ビットの型を Q(i), Q(j) と表現することにより，型レベルですることしかできず，他の量子ビットに適用すること

量子ビットの追跡を行えるようにする．この i, j をができない．

qidx と呼ぶ．型 Q(i) は qidx i に対応するひとつこの問題に対処するために，λQΠ; では qidx にの量子ビットを表すという意味で singleton 型 [6] のついての抽象化を許し量子ビットを引数に取る関数の一種と考えられる．さらに，量子ビットペア i1 , i2 が再利用性を高める．例えば前節の関数 f1 を，i, j に

coupling graph 上で i1 から i2 への辺があるというついて抽象化し

条件を i1 ; i2 と表し，型環境中に変数の型宣言とと

λi, j : qidx.λx : Q(i).λy : Q(j). hx, yi

もに i1 ; i2 を並べることにする．この時，CNOTとすることができる †1 ．この関数は，ふたつの qidx，

ゲートの型付け規則は以下のようになる (use は省略

それらの qidx に対応する量子ビット x, y を受け取している)．

り，ペアにして返す関数となり，引数として与える

i, j : qidx ∈ Γi;j∈ΓΓ ` cnot[i, j] : Q(i) ⊗ Q(j) → Q(i) ⊗ Q(j)つまり，i, j に対応する量子ビットペア (つまり，型

qidx を変えることで，様々な量子ビットに適用する

Q(i), Q(j) をもつ式) に CNOT ゲートを適用したい場合，型環境に i ; j が含まれることが要求される．
このように，qidx を使って量子ビット型を詳細化
し，連結性制約を型環境に含めることで，連結性制
約を満たしているかを検証することができるようになる．
また qidx によって，Selinger らの量子ラムダ計算[15] では区別できなかった型を区別できるようになる．その例が以下の f1 , f2 である．

f1 ≡ λx : qbit.λy : qbit. hx, yi
f2 ≡ λx : qbit.λy : qbit. hy, xi
Selinger らの量子ラムダ計算では，量子ビットはす
べて同じ型 qbit を持つため，f1 , f2 の型はどちらもqbit → qbit → qbit ⊗ qbit となる．しかし，f1 , f2
では戻り値の量子ビットの順番が入れ替わっており，個々の量子ビットを区別する今回の設定ではこれらを区別したい．qidx を用いれば，f1 , f2 の型はそれぞれ

f1 : Q(i) → Q(j) → Q(i) ⊗ Q(j)f2 : Q(i) → Q(j) → Q(j) ⊗ Q(i)と表され，区別できるようになる．

2. 3 依存関数型による再利用性の向上
qidx を使うことで，上の f1 , f2 の型の例のように，より細かくプログラムの挙動が型で表現できるが，一方でそのままだと細かすぎる場合がある．例えば，上記の f1 は，i, j に対応する量子ビットのみをペアにことができる．この関数の型は，依存関数型を使って

Πi, j : qbit.Q(i) → Q(j) → Q(i) ⊗ Q(j)と表される．
また，λQΠ; では qidx パラメータに対する連結
性制約を型で表現することができる．これは例えば以下のプログラムを考えるとわかりやすい．

λi, j : qidx.λx : Q(i).λy : Q(j).cnot hx, yi
このプログラムは 2 つの量子ビットを 1 つずつ受け取って cnot を適用する関数であるが，パラメータi, j は連結性制約をみたす必要がある．このことを表現するために，i ; j ⇒ T という形の型を導入する．
この型を持つ式は，型文脈に i ; j が存在する時にT として使うことができる．例えば，
Πi, j : qbit.i ; j ⇒ Q(i) → Q(j) → Q(i) ⊗ Q(j)という型で i, j が隣接した量子ビットであることを型で表現することができる．この型は Jones の qualiﬁedtype [9] の一種と考えられる．ただし，Jones の形式化とは異なり，i ; j ⇒ T 型のための明示的な項の構文を用意する．例えば，上の関数は，λQΠ; では
以下のように与えられる．

f3 ≡ λi, j : qidx.λ_ : i ; j.
λx : Q(i).λy : Q(j).cnot hx, yi
f3 : Πi, j : qbit.i ; j ⇒Q(i) → Q(j) → Q(i) ⊗ Q(j)λ_ の部分が型 i ; j ⇒ を導入する．制約が満たされていることの検査は，この関数を _ に適用することで行う．例えば，f3 であれば以下のようになる．(変†1 λi, j : qidx.M は λi : qidx.λj : qidx.M の略記である．以降，連続するラムダ抽象は同様に略記する．

数 q1 , q2 はそれぞれ型 Q(i), Q(j) を持つとする．)

る．例えば，f4 は α についての抽象を使って，

f3 i j _ q1 q2

f4′ ≡ λα : graph(3) .λg : (α(i1 , i2 , i3 ) ⇒ T → T ).

制約の解決時に，要求されている制約が型環境に存在する場合に限ってその適用に型がつくようにする．

λt : T.g _ (g _ t): Πα : graph(n) .((α(i1 , i2 , i3 ) ⇒ T → T ) → T → T )構文として _ を用いるのは，制約が満たされていると定義することで，後から連結性制約を具体化できるかだけが重要で，制約に名前をつける必要がないからようになる．
具体的な n 項述語は，である．

(i1 , . . . , in )i11 ; j12 , . . . im1 ; im2
2. 4 連結性制約の抽象化の形で表し，Πα 型の抽象項に渡すことで α を具体

最後に，連結性制約の抽象化に関して述べる．動化する．例えば，

f4′ ((j1 , j2 , j3 )j1 ; j2 )機付けとして，量子ビットを操作する関数を引数とするような以下の高階関数 f4 を考える．(ここでの型は α を ((j1 , j2 , j3 )j1 ; j2 ) で具体化した(i1 ; i2 ⇒ T → T ) → T → T

T ≡ Q(i1 ) ⊗ Q(i2 ) ⊗ Q(i3 ) とする．)
f4 ≡ λg : Tg .λt : T.g _ (g _ t)になり，f4′ ((j1 , j2 , j3 )j2 ; j3 )f4 の関数引数 g は，3 量子ビットの組を受け取ってその 3 量子ビットの組を返すとすると，この f4 は，の型は

量子ビットの組 t に対して同じ回路 g を繰り返し適(i2 ; i3 ⇒ T → T ) → T → T

用するようなプログラムのパターンを表しているととなる．このように，連結性制約述語についての抽象

考えることができる．しかし，g の型 Tg は，g がど化を導入することで，様々な制約を持つ関数を引数にんな連結性制約を要求するかで異なる型になってしま

取る高階関数を定義することができる．

う．例えば，g が i1 , i2 が隣接していることを要求す

3 体系 λQΠ;る関数であれば，Tg はi1 ; i2 ⇒ T → T

この節では，Selinger らの量子ラムダ計算 [15] をとすべきだし，i2 , i3 が隣接していることを要求する

元に，量子プログラムの coupling graph 解析のため

関数であれば，の型システムを備えた体系 λQΠ; の形式的定義を与i2 ; i3 ⇒ T → T

える．既に述べたように，Selinger らの体系におけるとなる．しかし，このように関数引数が課す制約に線形型では，複製可能な型は型コンストラクタ !T を

よって f4 の型が固定されてしまうのは再利用性の観使っているが，λQΠ; では Turner らの use [18] を点から問題である．

用いている．(use 0 は Igarashi ら [8] と Mogensen
Π;

に連結性

[10] によっている．) 加えて，量子ビットを動的に生制約を表す変数 α と，α についての抽象化を導入し，成するプリミティブ new を体系から取り除いている．

この問題を解決するため，我々は λQ

連結性制約についての多相性を表現できるようにす
る．具体的には，「任意の n 項連結性制約述語 α につ3. 1 構文

いて T 型」という意味の Πα : graph(n) .T という型

i, j は qidx 変数，α は連結性制約，U は 1 量子(n)は α が qidx 上の n 項述語でビットゲートを表すメタ変数であるとする．連結性制あることを表しており，α(i1 , . . . , in ) は抽象的な連

約 K ，use κ，型 T ，型環境 Γ，定数 c，項 M ，値 V

結性制約として α(i1 , . . . , in ) ⇒ T のような形で現れを以下の BNF で定義する．

を導入する．graph述語 α に関して多相的に振る舞う依存関数型である．

K ::= • | K, α(i1 , . . . , in ) | K, i ; j

α は束縛変数である．

κ ::= 0 | 1 | ω

型環境は，変数の型宣言，qidx 変数や連結性制約

T ::= Q(i) | unit | T → T | T ⊗ T | T ⊕ T |
κ

κ

κ

κ

κ

K ⇒ T | Πi : qidx.T | Πα : graph(n)性制約のときと同様，• は空列を表す記号であり，し.TΓ ::= • | Γ, x : T | Γ, i : qidx | Γ, α : graph(n)

述語変数の宣言，連結性制約の仮定の列である．連結|

ばしば省略する．
最後に，項について説明を与える．項のほとんどは

Γ, K
c ::= () | meas[i] | cnot[i, j] | U [i]Selinger らの量子ラムダ計算と同じであるため，拡M ::= c | x | λx : T.M | M M | hM, M i |張した点のみを述べる．まず λi : qidx.M は M が

let hx, yi = M in M | inl M | inr M |i について多相的に振る舞うような関数を表し (i はmatch M with (x 7→ M | y 7→ M ) |束縛変数である)，M i によって M を qidx i で具

let rec f = λx.M in M |体化して用いる．また，λα : graph(n) .M は M が n

λi : qidx.M | M i | λα : graph

(n)

.M |

項連結性制約述語を引数に取る関数であり (α は束M (i1 , . . . , in )K | λ_ : K.M | M _縛変数である)，M (i1 , . . . , in )K によって α を具体

V ::= c | x | λx : T.M | λi : qidx.M | λ_ : K.M |化する．ここで， (i1 , . . . , in )K は制約 K に現れる

λα : graph(n).M | hV, V i | inl V | inr V

qidx i1 , . . . , in を束縛した n 項連結性制約述語である．λ_ : K.M は連結性制約 K について明示的に抽

まず，連結性制約 K について説明する．連結性制象したものであり，M _ とすることでその制約を満た

約 K は直感的には qidx 上の関係 i ; j の列である

していれば解消することができる．c は定数を表す項

が，連結性制約述語 α を用いた α(i1 , . . . , in ) というであり，meas[i], cnot[i, j] および量子ゲート U であ制約が現れてもよい．また，• は空列を表し，しばしる．meas[i] は qidx i に対する測定を行い古典ビットば省略する．

を返す関数であり，cnot[i, j] は qidx i, j に対応す既に述べたように，use は 0, 1, ω のいずれかである 2 量子ビットに適用される CNOT ゲートである．

る．後述するように，use が 0 の型を持つ変数は参照

本体系では [15] にならい，古典ビットの型は直和型できないため 0 を除いて定義を与えることも可能とを使って，bit = unitω ⊕ω unitω と定義し，0 と 1思われるが，主に型環境の足し算などの定義が簡単にをそれぞれ inr () と inl () に対応させる．U は 1なるため採用している．型のうち，Q(i) は量子ビッ

量子ビットゲートを表すメタ変数であり，具体的には

ト型である．量子ビット型は qidx i に依存する依存X ゲートや H ゲートなどがある．meas と同様，ど型であり，i によって異なる量子ビットを型レベルでの量子ビットに適用するかを [i] で指定する．

区別することができる．さらに，(トップレベルに現

また，qidx の代入，連結性制約述語の代入，項変れる) 量子ビット変数の型の qidx は互いに相異なる数への項の代入をそれぞれ [j/i], [(i1 , . . . , in )K/α],

ようにすることで (定義 4.1)，異なる量子ビットに同[M/x] と書く，これらは全て束縛変数捕捉を避ける代じ型が割り当てられないようにする．また，量子ビッ入である．定義は簡単なので省略するが，図 2 に示す連ト型の use は 0 または 1 でなければならない．これ

結性制約述語の制約 K への代入 [(i1 , . . . , in )K/α]K ′は構文ではなく，規則を使って型の well-formednessの 定 義 の み 注 意 が 必 要 で あ る ．連 結 性 制 約 述 語として強制する．K ⇒ T 型を持つ項は，連結性制約(i1 , . . . , in )K が α へ代入される過程で，α が具体的

K を満たすときにのみ T として用いることができるな引数を伴う場合には K への代入が発生する．例えことを表す型である．Πi : qidx.T 型は，T 型が i にば，以下のようになる．

関して多相的に振る舞う依存関数型である．i は束縛変数である．Πα : graph(n) .T 型は，n 項連結性制約[(j1 , j2 , j3 )j1 ; j2 /α]α(i1 , i2 , i3 ) = i1 ; i2[(i1 , . . . , in )K/α]• =•()[(i1 , . . . , in )K/α](K ′ , i ; j) = [(i1 , . . . , in )K/α]K ′ , i ; j([(i1 , . . . , in )K/α]K ′ ) , [j1 /i1 , . . . , jn /in ]K[(i1 , . . . , in )K/α](K ′ , β(j1 , . . . , jm )) =([(i1 , . . . , in )K/α]K ′ ) , β(j1 , . . . , jn )
図2

ω

×

0

1

1

ω

0

0

0

0

ω

ω

1

0

1

ω

ω

ω

0

ω

ω

+

0

1

0

0

1

1

ω

ω

ω
表1

if β = α and n = m
if β 6= α

連結性制約の代入

ωuse 上の和積演算

Γ 中の型に κ を掛けて得られる型環境と定義する．
定義 3.4 型環境 Γ1 , Γ2 に対して，型環境 Γ1 + Γ2を以下で定義する．

• +• = •(Γ′1 , i : qidx) + (Γ′2 , i : qidx)= (Γ′1 + Γ′2 ), i : qidx

3. 2 型システム
まず，use に関する操作，関係，および演算をいく(Γ′1 , α : graph(n) ) + (Γ′2 , α : graph(n) )= (Γ′1 + Γ′2 ), α : graph(n)つか定義する．

(Γ′1 , K) + (Γ′2 , K) = (Γ′1 + Γ′2 ), K
定義 3.1 型 T に対し，|T | で型 T の最も外側にあ= (Γ′1 + Γ′2 ), x : (T + T ′ )る use を表す．

|Q(i)κ | = κ|unitκ | = κ|T →κ T ′ | = κ|T ⊗κ T ′ | = κ|T ⊕κ T ′ | = κ|K ⇒ T | = |T ||Πi : qidx.T | = |T |(Γ′1 , x : T ) + (Γ′2 , x : T ′ )|Πα : graph(n) .T | = |T |定義 3.2 Use 上の全順序関係を 0 ≤ 1 ≤ ω と定める．また，型 T, T ′ が，最も外側の use を除いて等
しく，かつ |T | ≤ |T ′ | であるとき，またそのときに

i : qidx, x : Q(i)1 + i : qidx, x : Q(i)1 = i :qidx, x : Q(i)ω となるが，型 Q(i)ω は well-formedではないので，実際には型導出には出現しない．
定義 3.5 型環境 Γ に含まれるすべての連結性制約の和集合 K ′ が K ⊆ K ′ を満たすとき，またそのときに限り K ⊆ Γ と書く．

限り T ≤ T ′ と書く．また，型環境 Γ, Γ′ についてのλQΠ; の型システムの判断は以下の 4 つである．

関係 Γ ≤ Γ′ を以下で定義する．

1. ` Γ は型環境 Γ の well-formedness で，直感的•≤•には，Γ で宣言される各種変数に重複がなく，各(Γ′1 , i : qidx) ≤ (Γ′2 , i : qidx) if Γ′1 ≤ Γ′2型や制約が先行する型環境のもとで well-formed(Γ′1 , α : graph(n) ) ≤ (Γ′2 , α : graph(n) ) if Γ′1 ≤ Γ′2であることを意味している．

(Γ′1 , K) ≤ (Γ′2 , K) if Γ′1 ≤ Γ′2(Γ′1 , x : T ) ≤ (Γ′2 , x : T ′ ) if Γ′1 ≤ Γ′2 and T ≤ T ′2. Γ ` K は型環境 Γ のもとでの連結性制約 K のwell-formedness についての判断である．K に現れる qidx および α が Γ に存在していれば K

定義 3.3 Use 上の和および積を表 1 で定める． 型

T, T ′ が最も外側の use を除いて型の構造および useが等しいとき，型 T + T ′ を T の最も外側の use を|T | + |T ′ | としたものと定義する．また，use κ およ
び型 T に対し κT は T の最も外側の use に κ を掛けた型と定義する．さらに，型環境 Γ に対し，κΓ はは Γ のもとで well-formed である．

3. Γ ` T は型 T が型環境 Γ のもとで well-formedであることを表す．

4. Γ ` M : T は型付け判断であり，型環境 Γ のもとで項 M に型 T が付くことを意味する．
型環境，連結性制約および型の well-formedness のであり，その全てが q1 , . . . , qn のいずれかであるとする．

規則を図 3, 4, 5 に示す．型環境と連結性制約についSelinger らの体系における quantum closure とのての各規則については先に述べたことを反映したも違いは，Selinger らの体系では coupling graph 中のκのとなっている．量子ビット型 Q(i) は i が Γ で定

L も quantum closure に含まれていたことである．

義されており κ が ω ではない時に well formed であこれは，Selinger らの体系では new の存在により評る．ペア型と直和型の use の条件は，全体が複数回価の過程で新たな量子ビットが生成され，L が更新

使える場合には，部分も複数回使えるものでなければされるためである．提案体系 λQΠ; では， new は存

ならないことを要求している．

在せず，すべての量子ビットが静的に確保された状態

型付け規則を図 6 に示す．基本的に [15] をふまを考えているため，quantum closure から L を移し，えた規則となっているので，新たに導入した型に関予め定められた coupling graph C のもとでの評価で係する規則を中心に説明する．cnot[i, j] の型付け規あることを意識した形式化を行っている．

則 T-CNOTでは，連結性制約 i ; j を要求するようこれらの定義のもとで，評価関係の導出規則 (の一にすることで，CNOT ゲートを適用する量子ビット部) を図 7 に示す．注目すべきは cnot の適用に関すペアがこの向きの辺によって直接隣接していることる規則である．cnot が量子ビットペアに適用されるを要求する．T-CONNおよび T-CONNAPPはそれぞ

際には，それらのペアが coupling graph C で直接隣れ連結性制約の抽象および解決のための規則である．

接していることを要求する．もし隣接していない量子

T-QABSおよび T-QAPPは qidx 変数に関する抽象

ビットペアに対して cnot が適用されれば行き詰まり

および適用である．T-GABSおよび T-GAPPは 連結状態となる．その他の規則については Selinger らの性制約述語の抽象および具体化を表している．

規則と同様である．

3. 3 操作的意味論

4 体系の性質

操作的意味論を定義する前に，まず，coupling graph

この節では，λQΠ; が満たす性質として型安全性，
すなわち，型付けされるプログラムは連結性制約違を定義する．

反を犯すことがないことが満たさせることを述べる．
定義 3.6 Coupling graph C を，順序付きの列 L =q1 . . . qn および接続関係 E によって C = (L, E) と定義する．各 qk (k ∈ {1, . . . , n}) は 1 つの量子ビットを表している．また，E の要素は (qk1 , qk2 ) ∈ E

型安全性は，Progress と Preservation 定理によって示される [21] [13]．
まず，準備として quantum closure についての型付けを定義する．

の形をしており，これは qk1 , qk2 が辺で直接つながっていることを表す．

Coupling graph のもとで，1 ステップの評価関係をC ` [ψ, M ] →p [ψ ′ , M ′ ]定義 4.1 Coupling graph C = (L, E) に対して，ある型環境 Γ があって以下をすべて満たすとき，またそのときに限り C ` [ψ, M ] : T と書く．

と定義する．ここで [ψ, M ] が quantum closure [15]• L = q1 · · · qn の時，ψ ∈ C2⊗nであり，ψ は量子状態を，M は項を表し，p はこ• qk ∈ L iﬀ qk : Q(ik )1 ∈ Γのステップが確率 p で起こることを表す．さらに，• ∀k1 , k2 ∈ {1, . . . , n} に対して k1 6= k2 ならば

ψ, M は C = (L, E) の L = q1 . . . qn と対応している．ψ は空間 C2⊗n 上の正規化されたベクトルであ∑り，ψ = |q1 . . . qn i = x∈{0,1}n cx |xi と書く．またM に現れる自由変数はすべて量子ビットを表す変数

ik1 6= ik2• 任意の qk1 : Q(ik1 )1 , qk2 : Q(ik2 )1 ∈ Γ に対して ik1 ; ik2 ∈ Γ iﬀ (qk1 , qk2 ) ∈ C• Γ`M :T` Γ Well-formed environments
WF-CTX-EMPTY`•`Γα 6∈ dom(G)` Γ, α : graph(n)`Γ

i 6∈ dom(Γ)Γ`K
WF-CTX-QIDX ` Γ
WF-CTX-CONN` Γ, i : qidx
` Γ, K`ΓΓ`Tx 6∈ dom(Γ)
WF-CTX-GVAR
WF-CTX-VAR` Γ, x : T
図3型環境の well-formednessΓ ` K Well-formed connectivity

Γ`•i, j : qidx ∈ Γ
WF-CONN-EDGEΓ`i;ji1 , . . . , in : qidx ∈ Γ
α : graph(n) ∈ Γ
WF-CONN-GRAPHΓ ` α(i1 , . . . , in )WF-CONN-EMPTY

図4

連結性制約の well-formednessΓ ` T Well-formed types`Γi : qidx ∈ Γκ≤1
WF-TYPE-QBITΓ ` Q(i)κΓ ` T2κ ≤ min{|T1 |, |T2 |}WF-TYPE-SUM
Γ ` T1 ⊕κ T2
Γ ` T2κ ≤ min{|T1 |, |T2 |}WF-TYPE-PAIRΓ ` T1 ⊗κ T2

Γ, i : qidx ` T`ΓWF-TYPE-PI-QIDXΓ ` Πi : qidx.TΓ ` T1`ΓWF-TYPE-UNITΓ ` unitκΓ ` T1
Γ, K ` T
WF-TYPE-CONN
Γ`K⇒T
図5

型の well-formedness

定義 4.1 は，量子状態のベクトル長が L の長さとつ ` Γ1 + Γ3 ならば (Γ1 + Γ3 ), Γ2 ` [V /x]M : T ．

対応していること，qidx および連結性制約によってcoupling graph C と対応した文脈 Γ のもとで項に型

補題 4.4 Γ, i : qidx, Γ′ ` M : T かつ j : qidx ∈ Γが付くことを表している．すなわち，C ` M : T はならば Γ, [j/i]Γ′ ` [j/i]M : [j/i]T ．

M の型付け判断において連結性制約を満たすことを意味する．
これを使って，Progress は以下のように述べられる．この文言は M が CNOT ゲートを適用しようとしている時に行き詰まらないことを含んでいる．

補題 4.5 Γ, α : graph(n) , Γ′ ` M : T か つ Γ, i1 :qidx, . . . , in : qidx ` K ならば Γ, [(i1 , . . . , in )K/α]Γ′ `[(i1 , . . . , in )K/α]M : [(i1 , . . . , in )K/α]T ．
定理 4.6 (Preservation) C ` [ψ, M ] : T かつ C `定理 4.2 (Progress) Coupling graph C に対し，量[ψ, M ] →p [ψ ′ , M ′ ] ならば C ` [ψ ′ , M ′ ] : T ．

子状態が ψ であるような項 M が C ` [ψ, M ] : T を定理 4.2 および定理 4.6 より，与えられた coupling

満たすとする．このとき M は値であるか，あるいgraph C に対応する型環境 Γ を用いて型がつくよう

′

′

′

′

はある ψ , M , p が存在して C ` [ψ, M ] →p [ψ , M ]なプログラムは，cnot の適用に際して連結性制約違となる．

反とならないことが保証される．

Preseravtion を述べる前に各種代入補題を述べる．
補題 4.3 Γ1 , x : S, Γ2 ` M : T かつ Γ3 ` V : S か

5 例
ここでは，これまで定義してきた体系で型がつく項をいくつか与える．説明を簡単にするため，適宜ラムΓ ` M : T TypingΓ ` () : unitκ`Γ

T-UNITi : qidx ∈ ΓΓ ` meas[i] : Q(i)1 →ω bit`Γ
i, j : qidx ∈ Γi;j∈ΓT-CNOT111ωΓ ` cnot[i, j] : Q(i) ⊗ Q(j) → Q(i)1 ⊗1 Q(j)1`Γx : T′ ∈ Γ
1 ≤ |T |Γ`x:TΓ1 ` M : T1 →κ T2

T ≤ T′

T-VAR

Γ2 ` N : T1
Γ1 + Γ2 ` M N : T2

Γ, x : T1 ` M : T2
κΓ = ΓT-ABS
Γ ` λx : T1 .M : T1 →κ T2` Γ1 + Γ2
κ≥1
T-APP

Γ ` M : T2
Γ ` T1 ⊕κ T2
T-SUMRΓ ` inr M : T1 ⊕κ T2

Γ ` M : T1
Γ ` T1 ⊕κ T2
T-SUMLΓ ` inl M : T1 ⊕κ T2

Γ1 ` P : T1 ⊕κ T2

T-MEASΓ2 , x : T1 ` M : T3
Γ2 , y : T2 ` N : T3
κ≥1
Γ1 + Γ2 ` match P with (x 7→ M | y 7→ N ) : T3

Γ1 ` M : T1

Γ2 ` N : T2
κ ≤ min{|T1 |, |T2 |}Γ1 + Γ2 ` hM, N i : T1 ⊗κ T2

Γ1 ` M : T1 ⊗κ T2

Γ2 , x : T1 , y : T2 ` N : T3
κ≥1
Γ1 + Γ2 ` let hx, yi = M in N : T3

` Γ1 + Γ2

T-MATCH

T-PAIRCONS` Γ1 + Γ2

ω · Γ1 , f : T1 →ω T2 ` λx : T1 .M : T1 →ω T2
Γ2 , f : T1 →ω T2 ` N : T3
ω · Γ1 + Γ2 ` let rec f = λx : T1 .M in N : T3

Γ, K ` M : T
T-CONNΓ ` λ_ : K.M : K ⇒ T
Γ, i : qidx ` M : T
T-QABSΓ ` λi : qidx.M : Πi : qidx.T` Γ1 + Γ2

T-PAIRDEST` ω · Γ1 + Γ2

T-REC

Γ`M :K⇒T
K⊆Γ
T-CONNAPPΓ ` M_ : TΓ ` M : Πi : qidx.T
j : qidx ∈ Γ
T-QAPPΓ ` M j : [j/i]TΓ, α : graph(n) ` M : TΓ ` λα : graph(n) .M : Πα : graph(n) .T

T-GABSΓ ` M : Πα : graph(n) .T
Γ, i1 : qidx, . . . , in : qidx ` K
T-GAPPΓ ` M (i1 , . . . , in )K : [(i1 , . . . , in )K/α]T
図6

型付け規則

ダ抽象の引数の型を省略し，let 式を用いる．

g の制約が α によって抽象化されていることが重要である．なぜならば，例にもある通り，g には様々な

例 5.1

制約を持つ関数が与えられうるからである．今回の例
let f = λj1 , j2 .λα.λ_.λg.λx1 , x2 . g j1 j2 _ hx1 , x2 i in では，f の 1 回目の適用時には g に恒等関数が与え

let hq1 , q2 i = f i1 i2 ((j1 , j2 )•) _ (λx.x) q1 q2 in

られているため，α(i1 , i2 ) は • として振る舞う．そf i1 i2 ((j1 , j2 )j1 ; j2 ) _ (λ_.cnot) q1 q2

れに対し，2 回目の適用時には cnot が与えられてい関数 f は，直感的には量子ビットペアを受け取ってるため，α(i1 , i2 ) は i1 ; i2 という制約として振る

量子ビットペアを返す関数 g と，2 つの量子ビット

舞う．

x, y を受け取り，g を hx, yi に適用する関数である．
この例では，f の型は次のようになる．
(2)

Πj1 , j2 : qidx.Πα : graph.α(j1 , j2 ) ⇒(Πj3 , j4 : qidx.α(j3 , j4 ) ⇒Q(j3 )1 ⊗1 Q(j4 )1 →ω Q(j3 )1 ⊗1 Q(j4 )1 )→ω Q(j1 )1 ⊗1 Q(j2 )1 →ω Q(j1 )1 ⊗1 Q(j2 )1

例 5.2 以下は，連結性制約 α が有用である 2 つ目のC ` [ψ, (λx : T.M )V ] →1 [ψ, [V /x]M ]C ` [ψ, (λi : qidx.M ) j] →1 [ψ, [j/i]M ]C ` [ψ, (λα : graph(n) .M ) (i1 , . . . , in )K] →1 [ψ, [(i1 , . . . , in )K/α]M ]C ` [ψ, (λ_ : K.M )_] →1 [ψ, M ](qi , qj ) ∈ C
C ` [ψ, cnot[_, _] hqi , qj i] →1 [ψ ′ , hqi , qj i]
C ` [ψ, M ] →p [ψ ′ , M ′ ]C ` [ψ, M ] →p [ψ ′ , M ′ ]C ` [ψ, M _] →p [ψ ′ , M ′ _]′′C ` [ψ, M i] →p [ψ ′ , M ′ i]C ` [ψ, M ] →p [ψ , M ]C ` [ψ, M (i1 , . . . , in )K] →p [ψ ′ , M ′ (i1 , . . . , in )K]
図7

評価規則 (一部抜粋)

存型によって表現され，誤り度 n を持つ量子ビット例である．

let f = λj1 , j2 , j3 , j4 .λα.λ_.λg.λx1 , x2 , x3 , x4 .

型は Qubit n と表現される．このような量子ビット

let hx1 , x2 i = g j1 j2 _ hx1 , x2 i in型を用いることで，量子ゲートの適用によって増加し

let hx3 , x4 i = g j3 j4 _ hx3 , x4 i inていく誤り度を追跡することができる．例えば量子hx1 , x2 , x3 , x4 i

ゲート U が 1 量子ビットを受け取って誤り度を k 増in加させるような量子ゲートであるとすると，U の型

f i1 i2 i3 i4 ((j1 , j2 )j1 ; j2 ) _ (λ_.cnot) q1 q2 q3 q4

は Πn : Nat.Qubit n → Qubit (n + k) のように表現

関数 f は量子ビットペアを受け取って量子ビットペすることができる．また，誤り度が t 以下である量アを返す関数 g と，4 つの量子ビット x1 , x2 , x3 , x4

子ビットに対して誤り訂正を行うゲート EC の型は，をうけとり，g を hx1 , x2 i, hx3 , x4 i に適用する関数

Πn : Nat.n ≤ t ⇒ Qubit n → Qubit 0 のように表現である．この例では，f の型は次のようになる．

することができる．型付け導出を得る過程で誤り度の(2)

Πj1 , j2 , j3 , j4 : qidx.Πα : graph.α(j1 , j2 ), α(j3 , j4 )⇒ (Πj5 , j6 : qidx.α(j5 , j6 ) ⇒最大値を求めることができるため，量子誤り訂正に
よって訂正できる許容範囲内であるかどうかを型シQ(j5 ) ⊗ Q(j6 ) → Q(j5 ) ⊗ Q(j6 ) )ステムで検証することが可能である．このように，誤→ Q(j1 ) → Q(j2 ) → Q(j3 ) → Q(j4 )り度によって量子ビットを類別するという考え方は，→ Q(j1 ) ⊗ Q(j2 ) ⊗ Q(j3 ) ⊗ Q(j4 )我々の提案体系 λQΠ; と類似したものである．

1

ω
1

1

1

1

ω

1

1

1

1

1

1

1

1

1

1

1

1

1

1

引数の g は f の内部で異なる量子ビットペアに対しCoupling graph 上の物理量子ビットを量子プログて適用されるため，g の制約はそのどちらについても

ラム上の論理量子ビットへどう割り当てるかという問必要になるが，α によって g の制約を抽象化してい題は量子ビット割り当て問題とよばれ，連結性制約をるため，型に現れているように α(j1 , j2 ), α(j3 , j4 ) と満たすようにプログラム変換が行われる．Siraichi ら

いった記述が可能である．

[17] [16] は量子ビット割り当て問題を部分グラフ同型性判定問題と Token Swapping という問題をもって

6 関連研究Hietala らは，量子ビットを誤り度によって区別す
る型システム [7] を提案し，QWIRE [12] という量子回路記述言語を用いて実装している．誤り度は依定式化した．また，これらの問題に対する厳密な解法とヒューリスティック解法のそれぞれを示し，速度計測などの評価を行っている．我々の提案体系 λQΠ;では，量子ビット割り当てがすでに行われた状態で型が付くかの判断を行っているが，今後型システムと割り付けアルゴリズムの協調を考えるさいにこれらのため，new を取り入れる際の課題の一つである．よっ

文献が参考になる．

て，そもそも new を取り入れるのか，取り入れる場

Ohori [11] は，ある種の部分構造論理に対応する
型付計算体系を考え，(直観主義論理に対応する型シ

合にどのような形式化を行い，型システムによってど
こまで保証するのかを考える必要がある．

ステムによる) 型導出をこの体系の導出への変換する型推論アルゴリズムを設計することも今後の課題

問題が，古典コンピュータにおけるレジスタ割り当て

である．型推論アルゴリズムによって，与えられたプ問題に対応することを示した．低レベルなアーキテク

ログラムを実行する際に必要な制約を抽出すること

チャ制約を型システムで表現する点は本研究と近い．

ができ，量子ビット割当問題やプログラム変換のヒン

我々の体系も上述の量子ビット割り当て問題のター

トとして用いることができるようになる．また，実装

ゲット言語として使えると考えられる．

面では，本体系の qidx の抽象や連結性制約の抽象，

Fu らは Quipper [5] を発展させ，依存型と線形型

およびそれらの解決を暗黙的にできるような実装をを両方備えた Proto-Quipper-D [4] [3] を提案してい考えている．例えば，第 5 節の例 5.2 で触れた以下

る．また線形型と依存型の統合について操作的意味論，のプログラムを考える．

表示的意味論を与えるとともに，その圏論的構造につ

let f = λj1 , j2 , j3 , j4 .λα.λ_.λg.λx1 , x2 , x3 , x4 .

いても考察がなされている．ただし，Proto-Quipper

let hx1 , x2 i = g j1 j2 _ hx1 , x2 i inは量子ビット自体を依存型で区別する体系ではなく，

let hx3 , x4 i = g j3 j4 _ hx3 , x4 i in

例えば QFT 回路といった入力の量子ビット数が可変

hx1 , x2 , x3 , x4 iである回路に与える量子ビットの数の不整合を防い

inだり，あるいは存在型によって可逆計算の文脈におけ

f i1 i2 i3 i4 ((j1 , j2 )j1 ; j2 ) _ (λ_.cnot) q1 q2 q3 q4

る garbage bit をより簡潔な記法で扱えるようにし，もし qidx や連結性制約の抽象と適用が省略できれ

uncomputation の機構を簡潔に実現するといった目ば，以下のように書け，可読性が向上する．

的で依存型が用いられている．

let f = λg.λx1 , x2 , x3 , x4 .
let hx1 , x2 i = g hx1 , x2 i in

7 結論

let hx3 , x4 i = g hx3 , x4 i in

7. 1 本研究のまとめ

hx1 , x2 , x3 , x4 i

本研究では，Selinger らの量子ラムダ計算に依存型inを導入することによって，量子プログラムが連結性制

f cnot q1 q2 q3 q4

約を満たしていることを型システムで保証するため

連結性制約の抽象と適用は，それぞれ関数の抽象と適の体系 λQΠ; を提案した．そして，型が付いたプロ用のタイミングでまとめて行うことにすれば容易にグラムが実際に連結性制約を違反せずに実行される実現できる．しかし，連結性制約述語 α に関しては，という型安全性を証明した．

束縛変数の数や順番などを考慮する必要があり，連結性制約ほど単純ではないため，今後の課題としたい．

7. 2 今後の課題

謝辞

Selinger らの量子ラムダ計算に存在した new につ

多くの助言を頂いた末永幸平氏に深く感謝いたし

いての扱いは今後の課題の 1 つである．new が関数内

ます．

部で呼ばれうることを考えると，連結性制約を考慮したまま動的に生成される量子ビットを追跡することは

参 考 文 献難しい．さらに，量子ビットが生成されるタイミング[ 1 ] Altenkirch, T. and Grattage, J.: A functional
quantum programming language, Proceedings of the20th Annual IEEE Symposium on Logic in Computer Science (LICS’ 05), June 2005, pp. 249–258.

で coupling graph 上のノードと対応付ける必要があ
るが，これは量子ビット割り当て問題をはらんでいる[ 2 ] Devitt, S. J.: Performing Quantum Computing
Experiments in the Cloud, (2016).
[ 3 ] Fu, P., Kishida, K., Ross, N. J., and Selinger,
P.: A Tutorial Introduction to Quantum Circuit Programming in Dependently Typed ProtoQuipper, Proceedings of Reversible Computation- 12th International Conference, RC 2020, Oslo,
Norway, July 9-10, 2020, Proceedings, Lanese, I.
and Rawski, M.(eds.), Lecture Notes in Computer
Science, Vol. 12227, Springer, 2020, pp. 153–168.
[ 4 ] Fu, P., Kishida, K., and Selinger, P.: Linear
Dependent Type Theory for Quantum Programming Languages: Extended Abstract, Proceedingsof LICS ’20: 35th Annual ACM/IEEE Symposiumon Logic in Computer Science, Saarbrücken, Germany, July 8-11, 2020, Hermanns, H., Zhang, L.,
Kobayashi, N., and Miller, D.(eds.), ACM, 2020,
pp. 440–453.
[ 5 ] Green, A. S., Lumsdaine, P. L., Ross, N. J.,
Selinger, P., and Valiron, B.: Quipper: a scalable quantum programming language, Proceedingsof ACM SIGPLAN Conference on Programming
Language Design and Implementation, PLDI ’13,
Seattle, WA, USA, June 16-19, 2013, Boehm, H.
and Flanagan, C.(eds.), ACM, 2013, pp. 333–342.
[ 6 ] Hayashi, S.: Singleton, Union, and Intersection
Types for Program Extraction, Information andComputation, Vol. 109, No. 1(1994), pp. 174 – 210.
[ 7 ] Hietala, K., Rand, R. S., and Hicks, M.: Tracking Errors through Types in Quantum Programs,
Presented at Workshop on Programming Languages
for Quantum Computing, January 2020.
[ 8 ] Igarashi, A. and Kobayashi, N.: Type-based
analysis of communication for concurrent programming languages, Proceedings of Static Analysis
Symposium (SAS’97), Van Hentenryck, P.(ed.),Berlin, Heidelberg, Springer Berlin Heidelberg,
1997, pp. 187–201.
[ 9 ] Jones, M. P.: A Theory of Qualiﬁed Types, Sci.
Comput. Program., Vol. 22, No. 3(1994), pp. 231–256.
[10] Mogensen, T. Æ.: Types for 0, 1 or many uses,
Proceedings of Implementation of Functional Languages (IFL’98), Clack, C., Hammond, K., andDavie, T.(eds.), Berlin, Heidelberg, Springer Berlin
Heidelberg, 1998, pp. 112–122.
[11] Ohori, A.: Register Allocation by Proof Trans-

formation, Proceedings of European Symposiumon Programming (ESOP2003), Degano, P.(ed.),Berlin, Heidelberg, Springer Berlin Heidelberg,
2003, pp. 399–413.
[12] Paykin, J., Rand, R., and Zdancewic, S.:
QWIRE: a core language for quantum circuits,
Proceedings of the 44th ACM SIGPLAN Symposium on Principles of Programming Languages,
POPL 2017, Paris, France, January 18-20, 2017,
Castagna, G. and Gordon, A. D.(eds.), ACM, 2017,
pp. 846–858.
[13] Pierce, B. C.: Types and Programming Languages, MIT Press, 2002.
[14] Selinger, P. and Valiron, B.: A lambda calculus for quantum computation with classical control, Mathematical Structures in Computer Science,Vol. 16, No. 3(2006), pp. 527–552.
[15] Selinger, P. and Valiron, B.: Quantum Lambda
Calculus, Semantic Techniques in Quantum Computation, Gay, S. and Mackie, I.(eds.), Cambridge
University Press, 2009, pp. 135–172.
[16] Siraichi, M. Y., Santos, V. F. d., Collange, C.,
and Pereira, F. M. Q. a.: Qubit Allocation As
a Combination of Subgraph Isomorphism and Token Swapping, Proc. ACM Program. Lang., Vol. 3,
No. OOPSLA(2019), pp. 120:1–120:29.
[17] Siraichi, M. Y., Santos, V. F. d., Collange, S.,
and Pereira, F. M. Q.: Qubit Allocation, Proceedings of the 2018 International Symposium on
Code Generation and Optimization, CGO 2018,
New York, NY, USA, Association for Computing
Machinery, 2018, pp. 113–125.
[18] Turner, D. N., Wadler, P., and Mossin, C.: Once
Upon a Type, Proceedings of the Seventh International Conference on Functional Programming Languages and Computer Architecture, FPCA ’95, New
York, NY, USA, ACM, 1995, pp. 1–11.
[19] van Tonder, A.: A lambda calculus for quantum computation, SIAM Journal on Computing,Vol. 33, No. 5(2004), pp. 1109–1135.
[20] Wootters, W. and Zurek, W.: A single quantum
cannot be cloned, Nature, Vol. 299(1982), pp. 802–803.
[21] Wright, A. K. and Felleisen, M.: A Syntactic Approach to Type Soundness, Information and Computation, Vol. 115, No. 1(1994), pp. 38–94.