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

Linear Quipper: 埋め込み線形型付き量子プログラミ
ング言語
菅野 翔太

松田 一孝

本研究では，埋め込み線形型付き量子プログラミング言語 Linear Quipper を提案する．Quipper は Haskell に埋め込まれた量子プログラミング言語であり，高階関数等の Haskell の機能を利用し量子回路を簡潔に記述することができる．しかし，Quipper は量子ビットと量子回路を素朴に Haskell のデータ及び関数として表現しているため，量子ビットの複製や破棄を許してしまうという問題がある．本研究では，Polakow による線形 λ 計算の埋め込み技法を応用し，Quipper に線形型を導入した Linear Quipper を実現する．具体的には，Linear Quipper は Quipperの構文を表現する型クラスを提供する．この型クラスの各メソッドは Quipper の各言語要素に対応し，メソッドの型はその言語要素が持つべき線形型を表現している．そのため，この型クラスに適切なインスタンスを与えることに
より Linear Quipper のプログラムを Quipper のプログラムに変換することができ，Quipper の実装を再利用可能という利点がある．また，GHC 拡張を活用することにより，少なくとも単純な回路については Linear Quipper では Quipper とほぼ同等の記述により量子回路を記述可能である．

This paper proposes Linear Quipper, an embedded linear quantum programming language, extending Quipper with Linear Types. Quipper is an embedded quantum programming language in Haskell that makes
use of Haskell’s functionalities including its powerful type system and higher-order functions to describe
quantum circuits. However, since Quipper naively represents quantum bits and circuits respectively by
Haskell data and functions, it allows users to define circuits that clone or discard quantum bits, which arephysically impossible. In this paper, we propose Linear Quipper, which addresses this limitation by adopting
the Polakow’s embedding method of the linear lambda calculus. Linear Quipper provides a type class that
represents the syntax of Quipper. Each method of the type class represents a languages construct in Quipper and has a type corresponding to the linear type the language construct should have. We can translate
Linear Quipper programs to Quipper programs via an appropriate instance of the type class, which enables
us to reuse the Quipper’s implementation. Furthermore, thanks to GHC extensions, Linear Quipper has
similar programmability to Quipper at least for simple circuits, allowing users to reuse Quipper programs
only with small changes.

Microsoft により開発された Q# [10] 等があり，関数

1 序論

型量子プログラミング言語には，QPL [8] や QML [1]，ゲート型量子コンピュータの実用化が期待される中，Quipper [5] といったものがある．

量子回路を記述するための様々なプログラミング言語

Quipper [5] も量子プログラミング言語の１つで（量子プログラミング言語）が提案されている．例えあり，Haskell に埋め込まれた形で実装されている．

ば，命令型量子プログラミング言語には，QCL [6] やQuipper では量子回路は Haskell の関数として表現されているため，ユーザーは高階関数や強力な型シス

Linear Quipper: An Embedded Linear Quantum Programming Language(This is an unrefereed paper. Copyrights belong to
the Authors.)
Shota Sugano Kazutaka Matsuda, 東北大学大学院情報科学研究科, Graduate School of Information Sciences, Tohoku University.

テムなど Haskell の様々な機能を利用して量子回路の記述が可能である．また，Quipper は関数型の量子プログラミングも，命令型の量子プログラミングもサポートしている．さらに，Quipper では量子回路のシミュレーションに加え，量子回路の描画出力など

様々な便利な機能も提供されている．
しかし Quippe では量子ビットや量子回路を Haskellの通常のデータや関数として素朴に表現しているた• Polakow による線形 λ 計算の埋め込み技法を応用し，Quipper に線形型を導入した Linear

Quipper を提案する．

め，量子ビットの複製や破棄といった記述を許して• Quipper には単純に線形型を与えるのが難しい

しまうという問題がある．例えば，Quipper では

関数 controlled が存在するが，Polakow による

qcirc q1 q2 = return (q1 , q1 ) といった関数を定義す

埋め込み技法の特徴を活用し，適切にその表現方ることができる．この例では量子ビット q1 は複製さ法を与える．

れ，q2 が破棄されているため量子回路として意味を• GHC 拡張を活用し，Linear Quipper においてなさない．そこで Quipper の関数に適切な線形型をも Quipper と同様に do 記法を用いた回路記述

導入し，このような操作を禁止したい．

を可能にする．

本研究では，Polakow による線型 λ 計算の埋め込

本論文は次のように構成される．2 節では Quipper

み技法 [7] を応用して，Quipper の関数型サブセッ及び Polakow の埋め込み技法について簡潔に紹介す

トに線形型を導入した Linear Quipper を提案する．

る．3 節では Linear Quipper の基本設計及び単純な

Polakow の埋め込みの基本的なアイデアは，線形 λ実現方法の問題点とその解決方法について述べる．4

計算における term-in-context を Haskell による型推

節では量子テレポーテーションの例に Quipper の記論が可能な形で型クラスとして表現することである．

述性と Linear Quipper の記述性を比較する．5 節で

我々はその型クラスを拡張し，Quipper の各関数を

は関連研究について議論し，6 節では本論文をまと「その関数が持つべき線形型」を表現する型を持つメ

める．

ソッドとして追加する．拡張された型クラスの適切なインスタンスにおいてそれらの追加されたメソッド

2 準備

を元の Quipper の関数を用いて実装することにより，

本節では，まず埋め込み量子プログラミング言語

Quipper の実装を再利用することが可能である．
この拡張は単純ではないためさらなる工夫が必要である．問題の 1 つは Quipper には素朴には線形型をQuipper [4, 5] について簡潔に述べ（2. 1 節），その後 Polakow の線形 λ 計算の Haskell への埋め込み手法 [7] について述べる（2. 2 節）．

与えるのが難しい関数が存在することである．例えば

Quipper の関数 controlled は第 2 引数を制御ビット

2. 1 Quipperとしたような第 1 引数の回路を表現するが，第 2 引数

Quipper は Haskell に埋め込まれた量子プログラに出現する量子ビットを消費しない．我々は Polakow

ミング言語である [4, 5]．Quipper では，関数的な記の埋め込み技法において変数の線形性と型が別々に述や命令的な記述の両方が可能であるが，本稿では関管理されているという特徴を利用し，controlled にも数的な記述方法に絞って述べる．

適切な表現を与える．また，それだけだと Quipper

関数的な Quipper においては，量子ビットは Qubitのプログラムと Linear Quipper のプログラムが大という型で表現されていて，n 入力 n 出力の量子回

きく異なってしまうようという問題がある．例えば，路はQuipper では do 記法を用いて量子回路をプログラム
するが，素朴に Polakow の埋め込みを応用するのでQubit → · · · → Qubit → Circ (Qubit, . . . , Qubit)
|
{z
}
|
{z
}

は do 記法が利用できなくなる．我々はこの問題点をと い う 型 の 関 数 と し て 表 現 さ れ る ．こ こ で Circ

GHC の RebindableSyntax 拡張を利用することによは 量 子 回 路 を 表 す モ ナ ド で あ る ．Quipper で は ，り解消し，Linear Quipper においても do 記法を用

qnot :: Qubit → Circ Qubit や hadamard :: Qubit →いた回路記述を可能にする．

Circ Qubit などの多数の基本的な量子ゲートが定義まとめると，本研究の貢献は以下である．

nn

されていて，それをモナドの演算（>>=，return ）で

組み合わせることにより，量子回路の記述が可能で1 であるときにゲート g を a に適用するようなゲーある．たとえば，circA, circB :: Qubit → Qubit →トを表す．ここで，制約 ControlSource c は c が制御(Qubit, Qubit) という量子回路が与えられたときに，ビットとして有効な型，具体的には古典ビットまとは

circA の二つ目の出力を，circB の一つ目の入力に繋量子ビットからなる組であることを表している．これげることで得られる 3 入力 3 出力回路を以下のようにより，以下のように複数の制御ビットを持つ関数をに記述できる．

controlled 関数一つで記述が可能となっている．

circAB :: Qubit → Qubit → Qubit

ccnot :: Qubit → Qubit → Qubit→ Circ (Qubit, Qubit, Qubit)→ Circ (Qubit, Qubit, Qubit)
circAB i1 i2 i3 = do

ccnot a b c = do

(s1 , s2 ) ← circA i1 i2

a ′ ← qnot a ‘controlled ‘ (b, c)(t1 , t2 ) ← circB s2 i3

return (a ′ , b, c)

return (s1 , t1 , t2 )2. 1. 2 問題点
Quipper は量子ビットを Haskell の通常のデータ

こうして定義された量子回路に対し，Quipper でとして表現しているため，次のような記述が可能ではシミュレーションしたり，また図として出力したりある．

することが可能である [4, 5]．

例 1 (badcirc). この例では，量子ビット a の複製，

Quipper は量子回路の記述を助けるための様々な関数を提供している．そうした関数の中で重要な量子ビット b の破棄が起きている．これは量子回路として実現不可能な操作である．

ものの一つである，本論文で主に議論の対象とする

badcirc :: Qubit → Qubit → Circ Qubit

controlled 関数について述べる．

badcirc a b = do

2. 1. 1 controlled 関数a ← hadamard a

制御付きのゲートとは，制御ビットが 1 であるときb ← hadamard bのみ特定のゲートを適用するゲートである．たとえa ← qnot a ‘controlled ‘ a

ば，制御 NOT ゲートは，二つの入力を取り，一つのreturn a

ビットが 1 であるときだけ，もう一方のビットを反転させる．制御 NOT ゲートは可逆回路を記述するための基本回路の一つであり，量子回路においても重要である．Quipper では，こうした制御付きのゲートを作るための関数，controlled を提供している．たとえば，controlled を使うことで以下のように制御 NOT
ゲートを定義することができる．

2. 2 線形 λ 計算の Polakow による Haskell への埋め込み

Polakow は線形 λ 計算を Haskell に埋め込む手法を提案した [7]．
素朴な線形 λ 計算の埋め込み手法の一つは，

Γ ⊢ e : τ という項を LLam Γ τ のような de Bruijn

cnot :: Qubit → Qubit → Circ (Qubit, Qubit)

表現で表すことである．しかしながら，この手法は埋

cnot a b = do

め込み実装において問題がある．例として，以下の線
形 λ 計算における関数適用の型付け規則を考える．†1′a ← qnot a ‘controlled ‘ breturn (a ′ , b)
ここで，qnot :: Qubit → Circ Qubit は（量子）NOT
ゲートである．

Γ = Γ1 ⊎ Γ2

Γ1 ⊢ e1 ⊢ τ ⊸ τ ′Γ ⊢ e1 e2 : τ ′Γ2 ⊢ e2 ⊢ τ

こ こ で ，Γ ⊢ e1 e2 : τ ′ で あ る こ と を 確 認 す る

具 体 的 に は ，controlled は ControlSource c ⇒Circ a → c → Circ a という型を持つ．直観的には，controlled (g a) c は制御ビット（の組）c が全て†1 本稿では説明を単純にするため，特に必要な場合を除いて非線形型環境を無視する．

に は ，Γ = Γ1 ⊎ Γ2 と い う 型 環 境 Γ1 と Γ2 で ，′Γ1 ⊢ e1 : τ ⊸ τ で Γ2 ⊢ e2 : τ であるものを発見する必要がある．しかし，このような型環境の発見
を Haskell の型推論器に行わせるのは用意ではない．
この問題点を解決するため，Polakow は IO-⊤ シ
ステムという線形 λ 計算の変種を提案している [7]．
主なアイデアは元の線形 λ 計算における型環境 Γ を，

• i は入力型環境 Γ1 を表す．しかし型情報自体は持たない．

• o は出力型環境 Γ2 を表す．しかし型情報自体は持たない．

• t は項の線形型 τ を表す．
ここで，Nat はdata Nat = Z | S Nat

その差分 Γ1 \ Γ2 が Γ を表すような入力型環境 Γ1 とで定義される kind（DataKinds 拡張により昇華）で

出力型環境 Γ2 の組により表現することである．たとある．

えば，線形 λ 計算の ⊸ に関するフラグメントに対する型付け規則は以下となる．

持つ．以下，本稿で使用するもののみに絞り説明する．

(Γ1 , x : τ, Γ′1 ) \ (Γ2 , □, Γ′2 ) ⊢ x : τ
Γ1 \ Γ2 ⊢ e1 : τ ⊸ τ ′LLC は線形 λ 計算の各構文に対応するメソッドを

Γ2 \ Γ3 ⊢ e2 : τ

Γ1 \ Γ3 ⊢ e1 e2 : τ ′(Γ1 , x : τ ) \ (Γ2 , □) ⊢ e : τ

2. 2. 1 llam および (^) メソッド
メソッド llam は，線形関数抽象 λx.e に対応する．

llam ::(VarOk b var ) ⇒′(LVar repr vid s →Γ1 \ Γ2 ⊢ λx.e : τ ⊸ τ ′repr (S vid ) b (Just vid : i) (var : o) t) →repr vid b i o (s ⊸ t)

入力の型環境が与えられたときに出力の型環境が高々一つに定まることに注意する．しかし上記の型システ

LVar repr vid a は線形 λ 計算における変数式の型でムは，線形 λ 計算の加法的直積型（&）のフラグメン

ある．

トを考えた場合には十分でなく，出力の型環境が入力の型環境から定まらなくなる．それを避けるために

type LVar repr (vid :: Nat) a =forall (v :: Nat)

IO-⊤ システムでは，型判断に ⊤（& の単位元）の導(i :: [Maybe Nat ])入則に対応する型付け規則がその導出木において使(o :: [Maybe Nat ]).

用されたかを表すフラグ b を含め，Γ1 \ Γ2 ⊢b e : τConsume vid i o ⇒ repr v False i o aという形の型判断を扱う．しかし，本稿では & およ

直観的には，LVar 型は以下の規則に対応している．

び ⊤ は扱わないため，この詳細は割愛する．

Polakow の埋め込みでは，Γ1 \ Γ2 ⊢b e : τ なるよ(Γ1 , x : τ, Γ′1 ) \ (Γ2 , □, Γ′2 ) ⊢False x : τ

うな項を型クラス LLC を用いて表す．直観的には，

ここで，Consume vid i o という制約により，i が型

LLC repr は repr vid b i o t が上記の項を表す抽象

レベル変数名 vid を含む型環境であり，o はそれを消型であることを表している．ここで，repr は費して得られるものであることが保証される．⊤ の

repr :: Nat → Bool →[Maybe Nat ] → [Maybe Nat ] →Type → Type扱い立ち入る必要があるため VarOk の定義は割愛す
るが，制約 VarOk b var は b が False ならば（つまり，⊤ の導入が行われていない），var が Nothing とという kind を持ち，vid ，b ，i ，o ，t はそれぞれ以ならなければならないことを述べておく．メソッド

下を表している．

llam は，Haskell の関数により，線形 λ 計算の束縛• vid は現在の de Brujin レベル（すなわち，束縛を表現している．そのため，llam $ λx → x のようの深さ）を表す．型レベルの変数名の表現としてに，Haskell の関数抽象を用いて線形関数を定義可能

利用される．

である．

• b は Γ1 \ Γ2 ⊢b e : τ の b を表す．

メソッド (^) は線形関数の適用を表す．

(^) :: (Or b1 b2 b) ⇒bang :: repr vid b [ ] [ ] s →repr vid b1 i h (s ⊸ t) →repr vid False i i (Bang s)

repr vid b2 h o s →ここで，repr vid b [ ] [ ] s は直観的には（線形な変repr vid b i o t

数に関して）閉じた式を表している．閉じた式は，外

ここで，Or b1 b2 b は b が b1 ∨ b2 であることを表部で導入された変数を含まないため複数回の使用がす型クラスである．

可能となる．

2. 2. 2 ulam および $$ メソッド
Polakow による埋め込み手法は，非線形な関数とその適用についても表現可能である．
メソッド ulam は，非線形関数抽象を表す．

それに対し，letBang は，線形 λ 計算における式

let !x = e1 in e2 に対応するメソッドであり，Bangを除去する．

letBang ::(Or b1 b2 b) ⇒ulam :: (UVar repr s → repr vid b i o t) →repr vid b1 i h (Bang s) →repr vid b i o (s → t)
ここで，UVar repr a は以下のように定義される型(UVar repr a → repr vid b2 h o t) →である．

repr vid b i o t

type UVar repr a =ここでも llam と同様，線形 λ 計算の束縛が Haskell

forall (vid :: Nat) (i :: [Maybe Nat ]).

の関数により表現されているが，llam と異なりここ

repr vid False i i a

では UVar が使われている．そのため，letBang e k

UVar repr vid a は線形 λ 計算における非線形な変数式を表す．つまり，以下の規則に対応する．

の k は入力を複数回使用可能である．

2. 2. 4 one ，letOne ，(⊗) および letStar メソッド
Polakow の埋め込み手法は，テンソル積型（乗法∆; Γ \ Γ ⊢False x : ∆(x)ここで，∆ は非線形型環境である．
対応して，($$) は非線形関数の適用を表す．†2($$) :: repr vid b i o (a → b) →的直積型）およびその単位元についても表現可能である．
メソッド (⊗) はテンソル積を導入する．

(⊗) :: (Or b1 b2 b) ⇒′repr vid b [ ] [ ] a →repr vid b1 i h a →repr vid b i o b

repr vid b2 h o b →repr vid b i o (a ⊗ b)

ここで，e1 $$ e2 の e2 が閉じた式であることが要求されていることに注意する．

第一引数の入力型環境が i，出力型環境境が h，第二2. 2. 3 bang および letBang メソッド

引数の入力型環境が h，出力型環境が o となっている

線形 λ 計算において，!s は複数回の使用が可能

ことに注意する．このことは，第 1 引数と第 2 引数な型を表す．Polakow の埋め込みにおいては，!s はBang s のように表現される．
メソッド bang は，Bang を導入する．

の式の間で変数の重複がないことを表している．
メ ソッド letStar は ，線 形 λ 計 算 に お け る 式

let x ⊗ y = e1 in e2 に対応する．ここでも，llam や
letBang の場合と同様に線形 λ 計算における束縛がHaskell における関数として表現されていることに注†2 Haskell では repr vid b ′ [ ] [ ] a のように書くと [ ] が（型レベルの）空リストでなくリストの型構成子として解釈されてしまうため本来は repr vid b ′ ′ [ ] ′ [ ] aのように記述する必要があるが，本稿では記述の簡便のためこれを無視する．

意する．

である．

letStar :: (VarOk b2 vid 1 ,VarOk b2 vid 2 ,Qubit ⊸ · · · ⊸ Qubit ⊸ Circ (Qubit ⊗ · · · ⊗ Qubit)
|
{z
}
|
{z
}

Or b1 b2 b) ⇒それに対応し，Quipper の提供する各関数について，

repr vid b1 i h (a ⊗ b) →元々→ を用いていた部分を ⊸ で置き換え，以下のよ(LVar repr vid a →うに型クラス LLC をそれらの関数で拡張した型クラ

LVar repr (S vid ) b →ス LinearQuipper を提供する．

nrepr (S (S vid )) b2(Just vid : Just (S vid ) : h)(vid 1 : vid 2 : o) c) →nclass LLC repr ⇒ LinearQuipper repr where...
た と え ば ，Quipper の 関 数 hadamard :: Qubit →Circ Qubit は，以下の LinearQupper のメソッドとrepr vid b i o c
メソッド one はテンソル積の単位元を表す．

one :: repr vid False i i One

して表現される．

hadamard :: UVar repr (Qubit ⊸ Circ Qubit)

メソッド letOne は，線形 λ 計算における式 let ⟨⟩ =ここで，UVar は hadamard 自体は何回も使用できる

e1 in e2 に対応するメソッドであり，One 型の値をことを表している．また，古典ビットを入力とする回除去する．

路は非線形関数に対応させ，古典ビットを出力とする

letOne :: (Or b1 b2 b) ⇒回路は Bang 型を返す関数に対応させる．たとえば，

repr vid b1 i h (One) →Quipper の関数 qinit qubit :: Bool → Circ Qubit

repr vid b2 h o a →と measure qubit :: Qubit → Circ Bit は 以 下 の

repr vid b i o a

LinearQuipper のメソッドとして表現される．

たとえば，a と a ⊗ One の間の相互変換は以下のように記述できる．

qinit qubit :: Uvar repr (Bool → Circ Qubit)
measure qubit ::UVar repr (Qubit ⊸ Circ (Bang Bit))

introOneL :: LLC repr ⇒UVar repr (a ⊸ a ⊗ One)
introOneL = llam $ λa → a ⊗ one
elimOneL :: LLC repr ⇒UVar repr (a ⊗ One → a)elimOneL = llam $ λao → letStar ao $ λa o →letOne o $ a

しかし，このアイデアを単純に適用するだけでは以下の理由により不十分である．

• Quipper では，do 記法を用いて回路を記述する
が，単純に (>>=)::m a → (a → m b) → m b を，(>>=) :: UVar expr (m a ⊸ (a ⊸ m b) ⊸ m b)に置き換えてしまうと do 記法が使用できなくなる．

• Quipper の一部の関数は単純に線形型を与える

3 Linear Quipper
本節では，Quipper に Polakow の埋め込み技法を適用することにより，埋め込み線形量子プログラミン
グ言語 Linear Quipper を実現する．

ことが難しい．たとえば，前節の cnot の例が示
すように，controlled 関数は第 2 引数の量子ビットを消費しない．

• (⊗) や Bang 型は回路の記述で頻繁に使用されるが，LLC のメソッドをそのまま利用したのでは，

3. 1 基本的なアイデアとその問題点

letBang や letStar を用いて陽に Bang や (⊗) を基本的なアイデアは，Quipper における関数を線一つ一つ分解しなければならない．これにより，形関数におきかえること，つまり n 入力 n 出力の量

ネストされたパターンを使用している Quipper

子回路を以下のような線形型を用いて表現することのプログラムに対し，対応する Linear Quipper

のプログラムは大きく形が異なったものになってしまう．

Γ1 ⊢ e : τΓ ⊢ return e : Circ τ

以下では，これらのそれぞれの問題点についての解決法を議論する．

対応して，我々は return に以下の型を与えることができる．

return :: repr vid b i o a →3. 2 モナドのメソッドの表現
前述の通り，我々は Linear Quipper においてもrepr vid b i o (Circ a)do 記法を利用したい．一つの方法は GHC 拡張のこれらのメソッドより，Linear Quipper においてRebindableSyntax 使うことであるが，そのためにはも do 記法を利用して量子回路をプログラムすること

return および (>>=) はが可能である．たとえば，入力に qnot を二度適用す(>>=) :: ??? → (??? → ???) → ???

る回路は以下のように記述可能である．

return :: ??? → ???

qnotnot ::と い う 形 の 型 を 持 た な け れ ば な ら な い ．こ の こLinearQuipper repr ⇒と は ，た と え ば do {p ← e1 ; return e2 } と い う

UVar repr (Qubit ⊸ Circ Qubit)

do 式が e1 >>= λp → return e2 といった形の式に

qnotnot = llam $ λa → do

翻 訳 さ れ る た め で あ る ．し か し ，(>>=) を 素 朴 に

a ′ ← qnot a(>>=) :: UVar expr (m a ⊸ (a ⊸ m b) ⊸ m b)

a ′′ ← qnot a ′と表現してしまうと，型が上記の形でないため Re-

return a ′′bindableSyntax を活用できない．

ここで，上記で定義した (>>=) および return がスコー

3. 2. 1 (>>=) メソッド

プ内に存在していることを仮定している．

基本的なアイデアは，(>>=) を以下の型付け規則を

Quipper では，qterm qubit :: Qubit → Bool →持つ言語要素として扱うことである．

Γ1 ⊢ e1 : Circ τ Γ2 , x : τ ⊢ e2 : Circ τΓ1 ⊎ Γ2 ⊢ e1 >>= (λx.e2 ) : Circ τ ′3. 2. 3 (>>) メソッド′

この構文要素は llam や (^) の類推から以下の型を与えることができる．

Circ () を用いて qterm qubit q b と書くことで，量子ビット q の値が b となっていることをアサートし，量子ビットを破棄することが可能である．これは，q が出
力 ancilla ビットになっていることを意味する．しかし，上記の >>= を使ったのでは do {qterm qubit e1 b; e2 }(>>=) ::(Or b1 b2 b, VarOk b2 var ) ⇒といったコードを排除してしまう．これは上記のコー

repr vid b1 i h (Circ s) →ドが qterm qubit e1 b >>= λ → e2 へと変換される(LVar repr vid a →ためである．ここで，(>>=) の第二引数は，線形関数

repr (S vid ) b2 (Just vid : h)(var : o) (Circ s)) →repr vid b i o (Circ t)

でなければならないが λ → e2 は入力を破棄しているため，型チェックが通らない．

RebindableSyntax 拡張は，スコープ内に (>>) が上記において，束縛の扱いは llam と同様であり，環定義されていれば，do {e1 ; e2 } を e1 >> e2 のように境や ⊤ フラグの扱いは (^) と同様である．

(>>) を用いて翻訳する．そのため，我々は以下のよ

3. 2. 2 return メソッド
同様のアイデアにより，return もより簡潔に表現

うに定義される (>>) を提供している．

(>
>) ::

することができる．具体的には，return を以下の型(Or b1 b2 b, VarOk b2 var ) ⇒付け規則を持つ言語要素として考える．

repr vid b1 i h (Circ One) →repr (S vid ) b2

引数の出力型環境は第二引数の入力型環境となってい(Nothing : h) (var : o) (Circ e2 ) →る．そのため，上の型により，controlled の第二引数

repr vid b i o (Circ e2 )に使われた量子ビットを消費しないことと，第一引数(>>) e1 e2 = e1 >>= λx → letOne x e2と第二引数に同一の量子ビットを使用しないことの二点が保証される．

3. 3 controlled 関数⇒

なお，ControlSource は Quipper の提供する同名のCirc a → c → Circ a 関数を提供している．こ型クラスと同一である．この型クラスが Linear Quip-

Quipper は controlled :: ControllSourcec

こで c は量子ビットか古典ビットかブール値からな

per においても再利用可能なのは，a ⊗ b が (a, b) のる組であり，第 2. 1 節の cnot や ccnot の例が示すよ型シノニムとして定義されていることによる．このうに，量子ビットを使用した場合でもそれを消費しa ⊗ b と (a, b) の同一視は安全なである．なぜなら，ない．

型 repr が抽象化されている限りにおいて a ⊗ b 型の

素 朴 に は ，controlled に は ControlSource c ⇒値は Linear Quipper のメソッドを通してしか操作でCirc a ⊸ c ⊸ Circ (a ⊗ c) と a と c の組を返きないためである．

す関数として実現可能である．しかしながら，制御つ

例 2 (cnot, ccnot). 第 2. 1 節の cnot と ccnot は Lin-きゲートは可逆回路において最も基本的な回路の一つ

ear Quipper でもほぼ同等の形で記述することがでであり，量子回路においても頻繁に利用されるため，きる．

この変換はプログラミングを煩雑にしてしまう．
関数 controlled に適切な線形型を与えることは容cnot :: LinearQuipper repr ⇒UVar repr (Qubit ⊸ Qubit ⊸易ではない．たとえば，以下の型付け規則は，e2 がCirc (Qubit ⊗ Qubit))

リソースを消費しないことを表しているはいるもの

cnot = llam $ λa → llam $ λb → doの，e2 の型検査に現在の型環境とはまったく関係のa ′ ← qnot a ‘controlled ‘ bない型環境を使用しているため正しくない．

return (a ′ ⊗ b)

Γ1 ⊢ e1 : Circ τ Γ2 ⊢ e2 : control bit の型
Γ1 ⊢ e1 ‘controlled ‘ e2 : Circ τ
幸運にも LLC では変数の使用情報と型情報が別々に管理されている（前者は入出力型環境，後者はHaskell が管理している）ため，e2 がリソースを消費しないことと，現在の型環境と同じ型として使用されることの両方を同時に表現することが可能である．
具体的には，controlled メソッドは以下の型を持つ．

ccnot :: LinearQuipper repr ⇒UVar repr (Qubit ⊸ Qubit ⊸ Qubit ⊸Circ (Qubit ⊗ Qubit ⊗ Qubit))
ccnot = llam $ λa →llam $ λb → llam $ λc → do′a ← qnot a ‘controlled ‘ (b ⊗ c)return (a ′ ⊗ b ⊗ c)controlled :: ControlSource c ⇒repr vid b i h (Circ a)→ repr vid b h o c→ repr vid b i h (Circ a)

3. 4 パターンマッチングの表現
Linear Quipper のコアなメソッドのみでは，ネストしたテンソル積を扱うのは煩雑である．たとえば，

制約 ControlSource c は c が，古典/量子ビットある

以下は Quipper で NAND 回路を記述したプログラ

いはブール値のテンソル積からなることを表していムである．可逆性のため，返り値の組の第 2 要素とる．ここで，controlled の返り値の入力型環境と出力

第 3 要素はゴミ出力となっている．

型環境と，その第一引数の型環境が一致していることに注意する．また，⊗ の型付け規則のように，第一pvar ::

nand orig a b = doc ← qinit False(Or b1 b2 b, VarOk b1 v ) ⇒-- ancilla bit(c, a, b) ← ccnot c a b

repr vid b2 h o a →c ← qnot c(LVar repr vid a →repr (S vid ) b1 (Just vid : i) (var : h) b) →return (c, a, b)
同等のプログラムを Linear Quipper で記述すると以下となる．

repr vid b i o bpvar a k = llam k ^ anand lin = llam $ λa → llam $ λb → do

たとえば，pvar e1 $ λx → e2 と書くことにより，

c ← qinit qubit $$ false

let x = e1 in e2 に対応するプログラムを表現するこcab ← ccnot ^ c ^ a ^ bとができる．ここで，pvar の型は，(>>=) の型からletStar cab $ λc ab →Circ を除いたものであることに注意する．

letStar ab $ λa b → do

テンソル積パターン p1 @* p2 は，letStar を用いてc ← qnot ^ c

入力を分解し，それを部分パターン p1 と p2 に渡し，

return (c ⊗ a ⊗ b)

その結果を組として継続に渡す．

ここで，Linear Quipper では ccnot の出力は (Qubit ⊗(@*) :: (VarOk b2 var 1 , VarOk b2 var 2 ,Qubit) ⊗ Qubit であるため，それを分解するのにOr b1 b2 b,

letStar のネストが必要となっている．一般に，複数Consume vid i1 i2 ,個の Qubit を返す関数を利用する際に，その個数だ

Consume (S vid ) i2 o2 ) ⇒け letStar のネストが必要になってしまう．

(repr v1 False i1 o1 a1 →(a2 → t1 ) →Haskell に詳しい読者は PatternSynonym を用いれば問題がないように思うかもしれないが，これもrepr (S (S vid )) b2

難しい．なぜならば，LLC では repr . . . (a ⊗ b) ⊸(Just vid : Just (S vid ) : h)(repr . . . a, repr . . . b) という関数を定義することが難(var 1 : var 2 : o3 ) c) →しいためである．テンソル積と違い組についてはその(repr v2 False i2 o2 b1 →(b2 → t2 ) → t1 ) →要素の使用に制限がないことに注意する．

repr vid b1 i3 h (a1 ⊗ b1 ) →そこで，我々は un-unparsing コンビネータ [2] に((a2 , b2 ) → t2 ) →倣い，パターンを継続渡し形式で表現することにより，合成可能なパターンを実現する．より具体的にrepr vid b i3 o3 c

は，パターンは，そのマッチングによって束縛される

p1 @* p2 = λz k → letStar z $ λa b →自由変数の値を引き数にとる継続を入力にとる関数p1 a (λx → p2 b (λy → k (x , y)))として表現される．
もっとも基本形なパターンは変数パターンである．
これは以下の関数として表される．

たとえば，(pvar @* pvar ) e1 $ λ(x , y) → e2 と書くことにより，let (x ⊗ y) = e1 in e2 に対応するプログ
ラムを表現することができる．
また，パターンと束縛する変数を近い場所に書けるようにするために，我々は以下の関数も提供している．

letQ :: t1 → (t1 → t2 → t3 ) → t2 → t3
letQ e p k = p e k
たとえば，これらの関数により nand lin を以下のように記述することが可能となる．

nand lin = llam $ λa → llam $ λb → doc ← qinit $$ false

H
1

H

meas
meas

1

X

Z

cab ← ccnot ^ c ^ a ^ b
図1

letQ cab

量子テレポーテーションを行う回路(pvar @* pvar @* pvar ) $λ((c, a), b) → doc ← qnot ^ cinstance Corr Qubit Qubit where . . .

return (c ⊗ a ⊗ b)...

ここで，pvar や (@*) を用いることによって letStar

instance Corr One () where . . .

のネストの煩雑さを抑られていることに注意する．

instance (Corr a a ′ , Corr b b ′ ) ⇒Corr (a ⊸ b) (a ′ → b ′ ) where . . .

こうした継続を用いたパターンの表現は，非線形変数を導入する letBang にも適用可能である．しかし，instance (Corr a a ′ , Corr b b ′ ) ⇒Corr (a ⊗ b) (a ′ , b ′ ) where . . .

線形な変数を導入するパターンと非線形変数を導入するパターンを組み合わせることは単純ではなく，そinstance (Corr a a ′ )⇒ Corr (Bang a) a ′ where ....

の検討は今後の課題とする．

4 評価
3. 5 Linear Quipper の項から Quipper の項への変換

本節では，量子テレポーテーションを行う回路（図1）を Quipper および Linear Quipper の両者で記述

Linear Quipper は型クラスで Quipper の構文を表することにより，Linear Quipper の記述性を評価す現しているため，適切なインスタンスを与えることにる．Quipper における，量子テレポーテーンションのよりその項を Quipper の項に変換することが可能でプログラムは [4] のものを用いた．

ある．我々は，そのアイデアに従い以下の変換関数を提供している．

図 2 および図 4 に Quipper における量子テレポー
テーションの実装を，図 3 および図 5 に Linear Quip-

convert :: Corr a r ⇒(forall repr . LinearQuipper repr ⇒repr vid b i o a) → r

per における量子テレポーテーションの実装を示す．
図 2 と図 3 を比較すると，比較的単純な補助関数については，Quipper と Linear Quipper のプログラム

ここで，Corr は以下のように定義される型クラスでの差は小さい．一方で，図 4 と図 5 を比較すると，テあり，線形型システムにおける型構成子と通常の型構

ンソル積や ! 型の分解を伴う teleport 関数について

成子との対応を表現している．

は，Quipper と Linear Quipper の差は大きいことがclass Corr a b | a → b where

わかる．これは，3. 4 節で述べたように，Haskell レ

to :: a → b

ベルのパターンマッチングを用いてテンソル積や ! 型

from :: b → aの分解を行えないことが原因である．特に teleport 関数においては，bell00 も alice についても組を返すので，その差が顕著となる．
通常の線形でないプログラムに対しては，図 5 のようなプログラムも，継続モナドを用いることで do記法を用いたプログラムとして表現することが可能な場合がある．同様のアプローチが Linear Quipperに対しても可能か否かの検討は今後の課題である．

plus minus :: Bool → Circ Qubit

alice :: Qubit → Qubit → Circ (Bit, Bit)plus minus b =alice q a = doq ← qinit ba ← qnot a ‘controlled ‘ qhadamard q

q ← hadamard q

share :: Qubit → Circ (Qubit, Qubit)(x , y) ← measure (q, a)share a = doreturn (x , y)b ← qinit False

bob :: Qubit → (Bit, Bit) → Circ Qubitb ← qnot b ‘controlled ‘ abob b (x , y) = dob ← gate X b ‘controlled ‘ yreturn (a, b)
bell00 :: Circ (Qubit, Qubit)b ← gate Z b ‘controlled ‘ x

bell00 = do

cdiscard (x , y)return ba ← plus minus False
share a
図2

Quipper における量子テレポーテーションの実装（補助関数）

plus minus :: (LLCQuipper repr ) ⇒UVar repr (Bool → Circ Qubit)
plus minus = ulam $ λb → doalice :: LLCQuipper repr ⇒UVar repr (Qubit ⊸ Qubit ⊸Circ (Bang Bit ⊗ Bang Bit))
alice = llam $ λq → llam $ λa → doq ← qinit qubit $$ ba ← qnot ^ a ‘controlled ‘ qhadamard ^ qshare :: LLCQuipper repr ⇒UVar repr (Qubit ⊸ Circ (Qubit ⊗ Qubit))share = llam $ λa → dob ← qinit qubit $$ falseb ← qnot ^ b ‘controlled ‘ aq ← hadamard ^ q
x ← measure qubit ^ qy ← measure qubit ^ areturn (x ⊗ y)bob :: LLCQuipper repr ⇒UVar repr (Qubit ⊸ Bit → Bit → Circ Qubit)

return (a ⊗ b)
bell00 :: LLCQuipper repr ⇒UVar repr (Circ (Qubit ⊗ Qubit))bob = llam $ λb →ulam $ λx → ulam $ λy → dob ← gate X ^ b ‘controlled ‘ ybell00 = doa ← plus minus $$ falseb ← gate Z ^ b ‘controlled ‘ xshare ^ a

cdiscard bit $$ x
cdiscard bit $$ y
return b
図3

Linear Quipper における量子テレポーテーションの実装（補助関数）関数として表現する方法を提案している．また，型付5 関連研究き量子 λ 計算 [9] もまた提案されている．これは線形量子プログラミング言語の基礎理論としては量子 λ論理を基にし，静的に量子ビットの複製や破棄を防い

計算 [11] がある．これは λ 計算を基に，量子回路をれる．

teleport :: Qubit → Circ Qubit

cnot :: Qubit → Qubit → Circ Qubit

teleport q = docnot a c = do(a, b) ← bell00

qnot a ‘controlled ‘ c(x , y) ← alice q areturn abob b (x , y)Linear Quipper の実装方針では，Qubit は量子ビッ

図4トそのものを表現しているため，このような命令的な

Quipper における teleport 関数記述を扱うには大きな変更が必要となる．

teleport :: LLCQuipper repr ⇒UVar repr (Qubit ⊸ Circ Qubit)
teleport = llam $ λq →letQM bell00 (pvar @* pvar ) $ λ(a, b) →letQM (alice ^ q ^ a) (pvar @* pvar ) $ λ(x , y) →letBang x $ λx →letBang y $ λy → bob ^ b $$ x $$ y
letQM m p k = m >>= λa → letQ a p k
図5Linear Quipper における teleport 関数

Haskell に線形型を取り入れる技法としては，GHCの LinearTypes 拡張 [3] の実装が行われている．Lin-

earTypes 拡張を用いると，Polakow の埋め込み技
法 [7] とは異なり，Haskell の通常の構文を用いて，線型型プログラムを記述できるようになる．例えば，(^)
や ($$) といったメソッドが不要となり，Linear Quip-

per では煩雑になってしてしまうテンソル積の分解も，パターンマッチを用いて簡潔に記述できるようになると予想される．また，関数の線形型に関する多相型を利用でき，例えば量子ビットと古典ビットに関する一部の処理を別々に定義する必要がなくなると予想されでいる．

る．しかし LinearTypes 拡張付きの Haskell を含む通実装としては，命令型と関数型それぞれに様々な量常の線型型付きプログラミング言語においては，一部子プログラミング言語が提案されている．命令型量の Quipper の関数を直接表現するのは難しい．例えば，子プログラミング言語としては QCL [6] を始め，最Quipper の関数 controlled は，Linear Quipper のよ

近では Q# [10] が提案されている．関数型プログラ

うに制御ビットを消費しないことを制約する型を与えミング言語では QPL [8] や，QML [1]，Quipper 等

るのは困難であり，controlled :: ControlSource c ⇒がある．QPL はこれらの中で最初に提案され，他のQubit ⊸ c ⊸ Circ (Qubit ⊗ c) のような型を持つ関関数型量子プログラミング言語に影響を与えている．

数として実装する必要があるだろう．また，現時点にQML は Haskell に似た文法で量子回路を記述でき，

おいては LinearTypes 拡張は GHC に取り入れられ

線形型システムを備えている．Quipper は Haskell のる予定はない．それに対して Linear Quipper は現在

埋め込み言語であり，Haskell の関数として量子回路の GHC（バージョン 8.2.2）で利用可能である．

を記述する．

Quipper の基本概念については，“Thus, the basic

6 結論

abstraction oﬀered by Quipper is that a quantum

本研究の成果は，埋め込み線形型付き量子プログラ

operation is a function that inputs some quantum

ミング言語 Linear Quipper を提案したことである．

data, performs state changes on it, and then out-

Linear Quipper では量子ビットの複製，破棄を許容

puts the changed quantum data.” [5] と述べられてしないため，より安全な量子回路を設計することがでいる．よって本研究ではそのポリシーにしたがってきる．またその中で，単純に線形型をつけることがで

Quipper の各関数に線形型を与えた．しかしながらきない Quipper のメソッドのための LLC の応用や，

Quipper では，Qubit 型は実際にはワイヤを表して記述性の向上のための RebindableSyntax 拡張を用

おり，たとえば以下のように命令的な記述も許容さいた do 構文の利用手法，継続渡し形式を用いた (⊗)

に対するパターンマッチングの提案を行った．
現時点では，Linear Quipper は Quipper の全ての関数を備えているわけではない．それらの実装が今後の課題である．

参 考 文 献[ 1 ] Altenkirch, T. and Grattage, J.: A Functional
Quantum Programming Language, 20th IEEE Symposium on Logic in Computer Science (LICS 2005),
26-29 June 2005, Chicago, IL, USA, Proceedings,
IEEE Computer Society, 2005, pp. 249–258.
[ 2 ] Asai, K., Kiselyov, O., and Shan, C.: Functional
un|unparsing, Higher-Order and Symbolic Computation, Vol. 24, No. 4(2011), pp. 311–340.
[ 3 ] Bernardy, J., Boespflug, M., Newton, R. R.,
Peyton Jones, S., and Spiwack, A.: Linear Haskell:practical linearity in a higher-order polymorphic
language, PACMPL, Vol. 2, No. POPL(2018),
pp. 5:1–5:29.
[ 4 ] Green, A. S., Lumsdaine, P. L., Ross, N. J.,
Selinger, P., and Valiron, B.: An Introduction
to Quantum Programming in Quipper, Reversible
Computation - 5th International Conference, RC
2013, Victoria, BC, Canada, July 4-5, 2013. Proceedings, Dueck, G. W. and Miller, D. M.(eds.),
Lecture Notes in Computer Science, Vol. 7948,
Springer, 2013, pp. 110–124.
[ 5 ] Green, A. S., Lumsdaine, P. L., Ross, N. J.,

Selinger, P., and Valiron, B.: Quipper: a scalable quantum programming language, 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 ] Ø̈mer, B.: A Procedural Formalism for Quantum Computing, Master’s thesis, Department ofTheoretical Physics Technical University of Vienna,
1998.
[ 7 ] Polakow, J.: Embedding a full linear Lambda
calculus in Haskell, Proceedings of the 8th ACM
SIGPLAN Symposium on Haskell, Haskell 2015,
Vancouver, BC, Canada, September 3-4, 2015,
Lippmeier, B.(ed.), ACM, 2015, pp. 177–188.
[ 8 ] Selinger, P.: Towards a quantum programming
language, Mathematical Structures in Computer
Science, Vol. 14, No. 4(2004), pp. 527–586.
[ 9 ] 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.
[10] Svore, K. M., Geller, A., Troyer, M., Azariah,J., Granade, C. E., Heim, B., Kliuchnikov, V.,
Mykhailova, M., Paz, A., and Roetteler, M.: Q#:
Enabling scalable quantum computing and development with a high-level domain-specific language,
CoRR, Vol. abs/1803.00652(2018).
[11] van Tonder, A.: A Lambda Calculus for Quantum Computation, SIAM J. Comput., Vol. 33,
No. 5(2004), pp. 1109–1135.