A TypeTheoretic
Account of
Quantum
Computation
Jacques
Garrigue,
Takafumi
Saikawa
Animation
Background:
Unitary
semantics
Double power
vector spaceand naturality

A Type-Theoretic Account of Quantum
Computation
Jacques Garrigue

Takafumi Saikawa

Lens,
curry-uncurry,
focus
Proving
circuits correct

TPP2023

Conclusion

1 / 34

A TypeTheoretic
Account of
Quantum
Computation
Jacques
Garrigue,
Takafumi
SaikawaShor’s 9-qubit code
|ψ⟩
|0⟩
|0⟩
|0⟩
|0⟩
|0⟩
|0⟩
|0⟩
|0⟩

Animation
Background:
Unitary
semantics
Double power
vector spaceand naturality
Lens,
curry-uncurry,
focus
Proving
circuits correctz•encoder
}|
•
•
H


{
•

z
•

decoder
}|
•
H

•

{
•

•
•
H

•

•

•

•

H

•

•

H

•

H

•

•
•

E
•

•
•
•



Conclusion

2 / 34

A TypeTheoretic
Account of
Quantum
Computation
Jacques
Garrigue,
Takafumi
Saikawa
Animation
Background:
Unitary
semantics

Animation

Double power
vector spaceand naturality
Lens,
curry-uncurry,
focus
Proving
circuits correct
Conclusion

3 / 34

A TypeTheoretic
Account of
Quantum
Computation
Jacques
Garrigue,
Takafumi
Saikawa
Animation
Background:
Unitary
semantics

|ψ⟩
|0⟩
|0⟩
|0⟩
|0⟩
|0⟩
|0⟩
|0⟩
|0⟩

Double power
vector spaceand naturality
Lens,
curry-uncurry,
focus
Proving
circuits correct
Conclusion

=

•

•

H

•

•

•

•

•

H

•

•
•
H

•

•

•

•

H

•

H

•

H

•

•
•

Id
•

•

•
•
•

|ψ⟩
|0⟩
|0⟩
|0⟩
|0⟩
|0⟩
|0⟩
|0⟩
|0⟩

•

•

H

•

•

•

•

H

•

•

•
•
H

•

•

•

•

H

•

H

•

•
•
H

•

•

•

•
•
•

4 / 34

A TypeTheoretic
Account of
Quantum
Computation
Jacques
Garrigue,
Takafumi
Saikawa
Animation
Background:
Unitary
semantics
Double power
vector spaceand naturality
Lens,
curry-uncurry,
focus
Proving
circuits correct
Conclusion

|ψ⟩
|0⟩
|0⟩
|0⟩
|0⟩
|0⟩
|0⟩
|0⟩
|0⟩

•

•

H

•

•

•

•

•

H

•

•
•
H

•

•

•

•

H

•

H

•

•
•
H

•

•

•

•
•
•

|ψ⟩

=

•

•

H

|0⟩
|0⟩
|0⟩

H

|0⟩
|0⟩
|0⟩
|0⟩
|0⟩

H

•

•

•
•
H

•

H

•

•
•
H
•
•

5 / 34

A TypeTheoretic
Account of
Quantum
Computation
Jacques
Garrigue,
Takafumi
Saikawa
Animation
Background:
Unitary
semantics|ψ⟩

Proving
circuits correct
Conclusion

•

H

|0⟩

H

•

•

H

•

H

•

•
•

|0⟩

H

|0⟩
|0⟩

•
•
|ψ⟩

=

H
•
•

|0⟩
|0⟩

Double power
vector spaceand naturality
Lens,
curry-uncurry,
focus

•

|0⟩
|0⟩

•

•

•

•

H

H

H

H

•

H

H

•

|0⟩
|0⟩
|0⟩
|0⟩
|0⟩
|0⟩
|0⟩
|0⟩

6 / 34

A TypeTheoretic
Account of
Quantum
Computation
Jacques
Garrigue,
Takafumi
Saikawa
Animation
Background:
Unitary
semantics|ψ⟩•

Proving
circuits correct

•

•

H

H

|0⟩

H

H

•

H

H

•

|0⟩
|0⟩
|0⟩
|0⟩
|0⟩

Double power
vector spaceand naturality
Lens,
curry-uncurry,
focus

•

|0⟩
|0⟩

=

|ψ⟩
|0⟩
|0⟩
|0⟩
|0⟩
|0⟩
|0⟩
|0⟩
|0⟩

•
•

=

|ψ⟩
|0⟩
|0⟩
|0⟩
|0⟩
|0⟩
|0⟩
|0⟩
|0⟩

Conclusion

7 / 34

A TypeTheoretic
Account of
Quantum
Computation
Jacques
Garrigue,
Takafumi
Saikawa

Table of contents
1 Animation

Animation
Background:
Unitary
semantics
Double power
vector spaceand naturality

2 Background: Unitary semantics
3 Double power vector space and naturality

Lens,
curry-uncurry,focus

4 Lens, curry-uncurry, focus

Proving
circuits correct

5 Proving circuits correct

Conclusion

6 Conclusion

8 / 34

A TypeTheoretic
Account of
Quantum
Computation
Jacques
Garrigue,
Takafumi
Saikawa
Animation
Background:
Unitary
semantics

Background: Unitary semantics

Double power
vector spaceand naturality
Lens,
curry-uncurry,
focus
Proving
circuits correct
Conclusion

9 / 34

A TypeTheoretic
Account of
Quantum
Computation
Jacques
Garrigue,
Takafumi
Saikawa
Animation
Background:
Unitary
semantics

Unitary semantics of purequantum computation• An isolated qubit is a vector of norm 1 in C2|0⟩ = (1, 0), |1⟩ = (0, 1), √i2 |0⟩ + √i2 |1⟩, etc.

Double power
vector spaceand naturality
Lens,
curry-uncurry,
focus
Proving
circuits correct
Conclusion

10 / 34

A TypeTheoretic
Account of
Quantum
Computation
Jacques
Garrigue,
Takafumi
Saikawa
Animation
Background:
Unitary
semantics
Double power
vector spaceand naturality
Lens,
curry-uncurry,
focus
Proving
circuits correct

Unitary semantics of purequantum computation• An isolated qubit is a vector of norm 1 in C2|0⟩ = (1, 0), |1⟩ = (0, 1), √i2 |0⟩ + √i2 |1⟩, etc.
• States composed of n qubits are vectors of norm 1 in theHilbert space of the n-iterated tensor productn(C2 )⊗n = C2 ⊗ · · · ⊗ C2 = C2

|i1 . . . in ⟩ = |i1 ⟩ ⊗ · · · ⊗ |in ⟩, √12 |00⟩ + √12 |11⟩, etc.

Conclusion

10 / 34

A TypeTheoretic
Account of
Quantum
Computation
Jacques
Garrigue,
Takafumi
Saikawa
Animation
Background:
Unitary
semantics
Double power
vector spaceand naturality
Lens,
curry-uncurry,
focus
Proving
circuits correct

Unitary semantics of purequantum computation• An isolated qubit is a vector of norm 1 in C2|0⟩ = (1, 0), |1⟩ = (0, 1), √i2 |0⟩ + √i2 |1⟩, etc.
• States composed of n qubits are vectors of norm 1 in theHilbert space of the n-iterated tensor productn(C2 )⊗n = C2 ⊗ · · · ⊗ C2 = C2

|i1 . . . in ⟩ = |i1 ⟩ ⊗ · · · ⊗ |in ⟩, √12 |00⟩ + √12 |11⟩, etc.
• basis and entangled states

Conclusion

10 / 34

A TypeTheoretic
Account of
Quantum
Computation
Jacques
Garrigue,
Takafumi
Saikawa
Animation
Background:
Unitary
semantics
Double power
vector spaceand naturality
Lens,
curry-uncurry,
focus
Proving
circuits correct
Conclusion

Unitary semantics of purequantum computation• An isolated qubit is a vector of norm 1 in C2|0⟩ = (1, 0), |1⟩ = (0, 1), √i2 |0⟩ + √i2 |1⟩, etc.
• States composed of n qubits are vectors of norm 1 in theHilbert space of the n-iterated tensor productn(C2 )⊗n = C2 ⊗ · · · ⊗ C2 = C2

|i1 . . . in ⟩ = |i1 ⟩ ⊗ · · · ⊗ |in ⟩, √12 |00⟩ + √12 |11⟩, etc.
• basis and entangled states• Pure operations are unitary transformations (linear andnorm preserving) on that space

10 / 34

A TypeTheoretic
Account of
Quantum
Computation
Jacques
Garrigue,
Takafumi
Saikawa
Animation

Quantum gates• Basic operations are unitary transformations called gates• They can be described by their matrix representation

Hadamard gate

Background:
Unitary
semantics
Double power
vector spaceand naturality
Lens,
curry-uncurry,
focus



H



1 1 1
=√
2 1 −1


CNOT gate

Proving
circuits correct•Conclusion




1
0
=
0
0

0
1
0
0

0
0
0
1


0
0

1
0


11 / 34

A TypeTheoretic
Account of
Quantum
Computation
Jacques
Garrigue,
Takafumi
Saikawa

Example of quantum circuitShor’s 9-qubit code
|ψ⟩
|0⟩
|0⟩
|0⟩
|0⟩
|0⟩
|0⟩
|0⟩
|0⟩

Animation
Background:
Unitary
semantics
Double power
vector spaceand naturality
Lens,
curry-uncurry,
focus
Proving
circuits correct
Conclusionz••

encoder
}|
•
H


{
•

z
•

decoder
}|
•
H

•

{
•

•
•
H

•

•

•

•

H

•

•

H

•

H

•

•
•

E
•

•
•
•





• A quantum circuit applies unitary transformations to an
input state to obtain an output state• Here E denotes a possibly noisy quantum channel
12 / 34

A TypeTheoretic
Account of
Quantum
Computation
Jacques
Garrigue,
Takafumi
Saikawa
Animation
Background:
Unitary
semantics
Double power
vector spaceand naturality
Lens,
curry-uncurry,
focus
Proving
circuits correct

Semantics of composition• For pure computations, the whole circuit can also be
described by a matrix• Application of a gate to a large state uses padding,i.e. taking a tensor product with an identity matrix andreordering dimensions.
For instance the first CNOT gate becomes:


I128
0
0
0
 0 I12800 
 U ⊗9 ((24))
U2⊗9 ((42))  0
0
0 I128  2
0
0 I1280Conclusion

where U2⊗9 ((24)) is the tensor permutation matrix
exchanging 2nd and 4th component of the tensor product13 / 34

A TypeTheoretic
Account of
Quantum
Computation

Problems with this semantics

Jacques
Garrigue,
Takafumi
Saikawa
Animation

1

The size of matrices becomes huge (here 512 × 512)

Background:
Unitary
semantics

2

The reorderings are particularly cumbersome

Double power
vector spaceand naturality

3

While these problems can be fixed to some extent by using
a symbolic representation of Kronecker products, and/or
by adopting the so-called labelled Dirac notation, thiscomes at a cost in terms of compositionality

Lens,
curry-uncurry,
focus
Proving
circuits correct
Conclusion

14 / 34

A TypeTheoretic
Account of
Quantum
Computation
Jacques
Garrigue,
Takafumi
Saikawa
Animation

Compositionality

Shor’s code is actually based on the following two simpler
codes, which are able to fix respectively bit-flips and sign-flips.

Background:
Unitary
semantics

•

•

•

•
•
•

E
Double power
vector spaceand naturality
Lens,
curry-uncurry,
focus
Proving
circuits correct
Conclusion

•

•

H
H
H

H
E

•

•

H

•

H

•

|ψ⟩
|0⟩
|0⟩
|0⟩
|0⟩
|0⟩
|0⟩
|0⟩
|0⟩

z
•

•

encoder
}|
•
H

{
•

z
•

decoder
}|
•
H

•

{
•

•
•
H

•

•

•

•

H

•

•

H

•

H

•

•
•

E
•

•
•
•

We would like to be able to handle such subcircuits just likegates, but we do not want to be bothered by the permutations.

15 / 34

A TypeTheoretic
Account of
Quantum
Computation
Jacques
Garrigue,
Takafumi
Saikawa
Animation
Background:
Unitary
semantics

Double power vector space and naturality

Double power
vector spaceand naturality
Lens,
curry-uncurry,
focus
Proving
circuits correct
Conclusion

16 / 34

A TypeTheoretic
Account of
Quantum
Computation
Jacques
Garrigue,
Takafumi
Saikawa
Animation
Background:
Unitary
semantics
Double power
vector spaceand naturality
Lens,
curry-uncurry,
focus
Proving
circuits correct
Conclusion

Quantum states as functions
An alternative view of quantum states• uses the isomorphism C2 ∼= {0, 1} → C• The basis states |0⟩ = (1, 0) and |1⟩ = (0, 1) become|0⟩ = λx : 2.if x = 0 then 1 else 0|1⟩ = λx : 2.if x = 1 then 1 else 0
where 2 = {0, 1}• This extends to states composed of n qubits:n(C2 )⊗n (= C2 ) = {0, 1}n → C|i1 , . . . , in ⟩ = λx : 2n .
if x = (i1 , . . . , in ) then 1 else 0

17 / 34

A TypeTheoretic
Account of
Quantum
Computation
Jacques
Garrigue,
Takafumi
Saikawa
Animation
Background:
Unitary
semantics
Double power
vector spaceand naturality
Lens,
curry-uncurry,
focus
Proving
circuits correct
Conclusion

Generalization : Double PowerFor any vector space T , we define the double power vector
space of functions from the nth power of a finite type (e.g. 2n )to T .
We use mathematical definitions from MathComp.
double power vector spaceVariables (I : finite type) (dI : I) (K : field).
fin
Definition dpower n T := In −→ T.
Notation Tbn := (dpower n T).
Definition dpbasis m (vi : In ) : (K1 )bm :=fin(vj : In ) 7−→ if vi == vj then 1 else 0.
lin

Definition morlin m n := ∀ T : VectK , Tbm −→ Tbn .
This allows to nest quantum states without tensor product.

18 / 34

A TypeTheoretic
Account of
Quantum
Computation
Jacques
Garrigue,
Takafumi
Saikawa
Animation
Background:
Unitary
semantics
Double power
vector spaceand naturality
Lens,
curry-uncurry,
focus
Proving
circuits correct
Conclusion

Generalization : Double PowerFor any vector space T , we define the double power vector
space of functions from the nth power of a finite type (e.g. 2n )to T .
We use mathematical definitions from MathComp.
double power vector spaceVariables (I : finite type) (dI : I) (K : field).
fin
Definition dpower n T := In −→ T.
Notation Tbn := (dpower n T).
Definition dpbasis m (vi : In ) : (K1 )bm :=fin(vj : In ) 7−→ if vi == vj then 1 else 0.
lin

Definition morlin m n := ∀ T : VectK , Tbm −→ Tbn .
This allows to nest quantum states without tensor product.
Problem: how do we ensure that functions in morlin m n havea unique matrix representation, that does not depend on T ?
18 / 34

A TypeTheoretic
Account of
Quantum
Computation
Jacques
Garrigue,
Takafumi
Saikawa

Naturality
The solution is to additionally require naturality.
naturality

Animation

T1I

T1

Background:
Unitary
semanticsφDouble power
vector spaceand naturality

T2

φI

m

G T1

T1I

m

T2I

m

φI
m

G T2

T2I

m

m

Lens,
curry-uncurry,
focus



Proving
circuits correct

Definition dpmap m T1 T2 (φ : T1 → T2 ) (st : Tbm1 ) : Tbm2 :=Conclusion




fin

m
(v : Im ) 7−→ φ (st(v)).
((dpmap φ) is denoted φIabove)
Definition naturality m n (G : morlin m n) :=lin∀(T1 T2 : VectK ), ∀(φ : T1 −→ T2 ),(dpmap φ) ◦ (G T1 ) = (G T2 ) ◦ (dpmap φ).

19 / 34

A TypeTheoretic
Account of
Quantum
Computation
Jacques
Garrigue,
Takafumi
Saikawa

Linearity, naturality, unitarity(* natural morphisms *)Record mor m n := {φ : morlin m n | naturality φ}.
Notation endo n := (mor n n).

Animation
Background:
Unitary
semantics
Double power
vector spaceand naturality
Lens,
curry-uncurry,
focus
Proving
circuits correct
Conclusion(* from matrix *)bnDefinition mxmor n m : Kbm → mor m n.
(* vertical composition *)Definition comp_mor : mor m p -> mor n m -> mor n p.
Notation "F \v G" := (comp_mor F G).
(* unitarity *)Definition unitary_endo m n (F : mor m n) :=∀ s t, tinner (F K1 s) (F K1 t) = tinner s t.

(K1 is the field K seen as a vector space)
20 / 34

A TypeTheoretic
Account of
Quantum
Computation
Jacques
Garrigue,
Takafumi
Saikawa
Animation
Background:
Unitary
semantics

Lens, curry-uncurry, focus

Double power
vector spaceand naturality
Lens,
curry-uncurry,
focus
Proving
circuits correct
Conclusion

21 / 34

A TypeTheoretic
Account of
Quantum
Computation

Lens, curry-uncurry, focus

Jacques
Garrigue,
Takafumi
Saikawa
Animation
Background:
Unitary
semantics
Double power
vector spaceand naturality
Lens,
curry-uncurry,
focus
Proving
circuits correct
Conclusion

22 / 34

A TypeTheoretic
Account of
Quantum
Computation
Jacques
Garrigue,
Takafumi
Saikawa
Animation

Lens, curry-uncurry, focus• Lens = choice of wires tobe connected to gates;
basic combinatorial data

Background:
Unitary
semantics
Double power
vector spaceand naturality
Lens,
curry-uncurry,
focus
Proving
circuits correct
Conclusion

22 / 34

A TypeTheoretic
Account of
Quantum
Computation
Jacques
Garrigue,
Takafumi
Saikawa
Animation
Background:
Unitary
semantics

Lens, curry-uncurry, focus• Lens = choice of wires tobe connected to gates;
basic combinatorial data
• Currying = quotienting
unused wires away

Double power
vector spaceand naturality
Lens,
curry-uncurry,
focus
Proving
circuits correct
Conclusion

22 / 34

A TypeTheoretic
Account of
Quantum
Computation
Jacques
Garrigue,
Takafumi
Saikawa
Animation
Background:
Unitary
semantics
Double power
vector spaceand naturality
Lens,
curry-uncurry,focus

Lens, curry-uncurry, focus• Lens = choice of wires tobe connected to gates;
basic combinatorial data
• Currying = quotienting
unused wires away
• Focusing = composing
curry, gate and uncurry tobuild the diagram

Proving
circuits correct
Conclusion

22 / 34

A TypeTheoretic
Account of
Quantum
Computation
Jacques
Garrigue,
Takafumi
Saikawa

Lens

lens


injective

Animation
Background:
Unitary
semantics
Double power
vector spaceand naturality
Lens,
curry-uncurry,
focus
Proving
circuits correct
Conclusionlens n m : {1, . . . , m} −−−−−→ {1, . . . , n}

• Provides both inclusion and permutation• Basic operations:
Variables (n m p : nat) (I : Type).
Definition extract : lens n m → In → Im .
Definition merge : lens n m → Im → In−m → In .
Definition lensC : lens n m → lens n (n - m).
Definition lens_comp :lens n m -> lens m p -> lens n p.

23 / 34

A TypeTheoretic
Account of
Quantum
Computation
Jacques
Garrigue,
Takafumi
Saikawa

Currying
curry and uncurry


n

∼
=



curry : T I ←→ T I

n−m

I m

: uncurry

Animation
Background:
Unitary
semantics
Double power
vector spaceand naturality
Lens,
curry-uncurry,
focus
Proving
circuits correct
Conclusionnn−m ×I m
n−m I m
∼
TI ∼
)
= TI
= (T I

Variables (n m : nat) (ℓ : lens n m) (T : VectK ).

bm
n−m
Definition curry (st : Tbn ) : T[
:=


fin
fin
(v : Im ) 7−→ (w : In−m ) 7−→ st (merge ℓ v w) .
bm

n−m
Definition uncurry (st : T[
) : Tbn :=fin(v : In ) 7−→ st (extract ℓ v) (extract (lensC ℓ) v).
24 / 34

A TypeTheoretic
Account of
Quantum
Computation
Jacques
Garrigue,
Takafumi
Saikawa

focus

focus







Animation
Background:
Unitary
semantics
Double power
vector spaceand naturality
Lens,
curry-uncurry,
focus
Proving
circuits correct
Conclusion

Variables (n m : nat) (ℓ : lens n m).
Definition focuslin (G : endo m) : morlin n n :=λT. uncurryℓ,T ◦ GT[n−m ◦ curryℓ,T .
Definition focus (G : endo m) : endo n.

25 / 34

A TypeTheoretic
Account of
Quantum
Computation
Jacques
Garrigue,
Takafumi
Saikawa

Properties(* Distributivity wrt vertical composition *)Lemma focus_comp n m (f g : endo m) (l : lens n m) :focus l (f \v g) = focus l g \v focus l g.

Animation
Background:
Unitary
semantics
Double power
vector spaceand naturality
Lens,
curry-uncurry,
focus
Proving
circuits correct(* Composition of lenses *)Lemma focusM n m p(l : lens n m) (l' : lens m p) (f : endo p) :focus (lens_comp l l') f = focus l (focus l' f).
(* Composition of disjoint lenses commutes *)Lemma focusC n m p (l : lens n m) (l' : lens n p)
(f : endo m) (g : endo n) : [disjoint l & l'] ->focus l f \v focus l' g = focus l' g \v focus l f.

Conclusion(* Unitarity *)Lemma focusU n m (l : lens n m) (f : endo m) :unitary_endo f -> unitary_endo (focus l f).
26 / 34

A TypeTheoretic
Account of
Quantum
Computation
Jacques
Garrigue,
Takafumi
Saikawa
Animation
Background:
Unitary
semantics

Proving circuits correct

Double power
vector spaceand naturality
Lens,
curry-uncurry,
focus
Proving
circuits correct
Conclusion

27 / 34

A TypeTheoretic
Account of
Quantum
Computation
Jacques
Garrigue,
Takafumi
Saikawa
Animation
Background:
Unitary
semantics
Double power
vector spaceand naturality
Lens,
curry-uncurry,
focus
Proving
circuits correct
Conclusion

Representing Shor’s code
Notation mxapp l M := (focus l (mxmor M)).
Definition bit_flip_enc : endo 3 :=mxapp [lens 0; 2] cnot \v mxapp [lens 0; 1] cnot.
Definition bit_flip_dec : endo 3 :=mxapp [lens 1; 2; 0] toffoli \v bit_flip_enc.
Definition hadamard3 : endo 3 :=mxapp [lens 2] hadamard \v mxapp [lens 1] hadamard\v mxapp [lens 0] hadamard.
Definition sign_flip_dec := bit_flip_dec \v hadamard3.
Definition sign_flip_enc := hadamard3 \v bit_flip_enc.
Definition shor_enc : endo 9 :=focus [lens 0; 1; 2] bit_flip_enc \v
focus [lens 3; 4; 5] bit_flip_enc \v
focus [lens 6; 7; 8] bit_flip_enc \v
focus [lens 0; 3; 6] sign_flip_enc.
Definition shor_dec : endo 9 := ...

28 / 34

A TypeTheoretic
Account of
Quantum
Computation
Jacques
Garrigue,
Takafumi
Saikawa
Animation
Background:
Unitary
semantics
Double power
vector spaceand naturality
Lens,
curry-uncurry,
focus
Proving
circuits correct
Conclusion

Proving Shor’s code
We have only proved the correctness for error-free channels.
Definition flip (i : 'I_2) := rev_ord i. (* exchanges 0 and 1 *)Lemma mxmor_cnot0 i : mxmor cnot Co ¦0, i〉 = ¦0, i〉.
Lemma mxmor_cnot1 i : mxmor cnot Co ¦1, i〉 = ¦1, flip i〉.
Lemma mxmor_toffoli00 i : mxmor toffoli Co ¦0,0,i〉 = ¦0,0,i〉.
Lemma hadamardK T : involutive (mxmor hadamard T).
Lemma bit_flip_enc0 j k : bit_flip_enc Co ¦0,j,k〉 = ¦0,j,k〉.
Lemma bit_flip_enc1 j k :bit_flip_enc Co ¦1,j,k〉 = ¦1, flip j, flip k〉.
Lemma bit_flip_toffoli :(bit_flip_dec \v bit_flip_enc) = mxapp [lens 1; 2; 0] toffoli.
Lemma sign_flip_toffoli :(sign_flip_dec \v sign_flip_enc) = mxapp [lens 1; 2; 0] toffoli.
Theorem shor_code_id i :(shor_dec \v shor_enc) Co ¦i,0,0,0,0,0,0,0,0〉 = ¦i,0,0,0,0,0,0,0,0〉.

The above lemmas require about 80 lines of proof in total.
29 / 34

A TypeTheoretic
Account of
Quantum
Computation
Jacques
Garrigue,
Takafumi
Saikawa
Animation
Background:
Unitary
semantics
Double power
vector spaceand naturality
Lens,
curry-uncurry,
focus
Proving
circuits correct
Conclusion

Focusing in and out
We provide a number of functions and lemmas that allow tochange the view of the current state.
Variables (n m : nat) (l : lens n m).
lin
Definition dpmerge : (K1 )bn → (K1 )bm −→ (K1 )bn .
Lemma focus_dpbasis (f : endo n) (vi : In ) :focus l f _ (dpbasis vi) =dpmerge vi (f _ (dpbasis (extract l vi))).
Lemma dpmerge_dpbasis (vi : In ) (vj : Im ) :dpmerge vi (dpbasis vj) =dpbasis (merge l vj (extract (lensC l) vi)).
Lemma decompose_scalerk (st : (K1 )bn ) :Pst =t:Ik st t *: dpbasis t.
30 / 34

A TypeTheoretic
Account of
Quantum
Computation
Jacques
Garrigue,
Takafumi
Saikawa
Animation

Proof of bit_flip_enc1 (first half)
1
2
3
4
5

Background:
Unitary
semantics

6
7

8
Double power
vector space 9
and naturality1011
Lens,
curry-uncurry,12
focus
13
14
Proving
circuits correct15
Conclusion

16
17
18
19
20

bit_flip_enc Co ¦1,j,k〉
rewrite /=.
= mxapp [lens 0; 2] cnot Co (mxapp [lens 0; 1] cnot Co ¦ 1, j, k 〉)rewrite focus_dpbasis.
= mxapp [lens 0; 2] cnot Co(dpmerge [lens 0; 1] [tuple 1; j; k](mxmor cnot Co(dpbasis (extract [lens 0; 1] [tuple 1; j; k]))))
simpl extract.
= mxapp [lens 0; 2] cnot Co(dpmerge C [lens 0; 1] [tuple 1; j; k] (mxmor cnot Co ¦ 1, j 〉))rewrite mxmor_cnot1.
= mxapp [lens 0; 2] cnot Co(dpmerge C [lens 0; 1] [tuple 1; j; k] ¦ 1, flip j 〉)rewrite dpmerge_dpbasis.
= mxapp [lens 0; 2] cnot Co(dpbasis (merge [lens 0; 1] [tuple 1; flip j](extract (lensC [lens 0; 1]) [tuple 1; j; k])))rewrite (_ : merge _ _ _ = [tuple 1; flip j; k]); last by eq lens.
= mxapp [lens 0; 2] cnot Co ¦ 1, flip j, k 〉31 / 34

A TypeTheoretic
Account of
Quantum
Computation

Other examples formalized• GHZ state prerapation

Jacques
Garrigue,
Takafumi
Saikawa

GHZ3 :=•

H•

Animation
Background:
Unitary
semantics
Double power
vector spaceand naturality

1
GHZ3 (|000⟩) = √ (|000⟩ + |111⟩)2• Reversal circuit
|φ1 ⟩
|φ2 ⟩
|φ3 ⟩
|φ4 ⟩
|φ5 ⟩
|φ6 ⟩

Lens,
curry-uncurry,
focus
Proving
circuits correct
Conclusion

where

|φ6 ⟩
|φ5 ⟩
|φ4 ⟩
|φ3 ⟩
|φ2 ⟩
|φ1 ⟩

×
×
×
×
×
×


1
0
×

=
0
×
0

0
0
1
0

0
1
0
0


0
0

0
1
32 / 34

A TypeTheoretic
Account of
Quantum
Computation
Jacques
Garrigue,
Takafumi
Saikawa
Animation
Background:
Unitary
semantics

Conclusion

Double power
vector spaceand naturality
Lens,
curry-uncurry,
focus
Proving
circuits correct
Conclusion

33 / 34

A TypeTheoretic
Account of
Quantum
Computation
Jacques
Garrigue,
Takafumi
Saikawa
Animation
Background:
Unitary
semantics
Double power
vector spaceand naturality
Lens,
curry-uncurry,
focus

Conclusion
We have provided an alternative account of pure quantum
computation, based on• quantum state seen as function• currying of this function for focusing• parametric polymorphic definition of transformations• characterizing parametricity by naturality
This approach allowed us to prove a number of pure circuits• Shor’s 9-qubit code (on error-free channel)

Proving
circuits correct• GHZ state preparation

Conclusion• reverse circuit
The ability to manipulate state through currying really seems
to simplify proofs!
34 / 34