Baby's First Diagrammatic Calculus for Quantum Information...

39

Transcript of Baby's First Diagrammatic Calculus for Quantum Information...

Page 1: Baby's First Diagrammatic Calculus for Quantum Information ...cs.tulane.edu/~vzamdzhi/slides/quilt.pdf · Introduction Syntax Semantics Proof System Pure states ! mixed states Conclusion

Introduction Syntax Semantics Proof System Pure states → mixed states Conclusion

Baby's First Diagrammatic Calculus for Quantum Information

Processing

Vladimir Zamdzhiev

Department of Computer Science

Tulane University

30 May 2018

1 / 38

Page 2: Baby's First Diagrammatic Calculus for Quantum Information ...cs.tulane.edu/~vzamdzhi/slides/quilt.pdf · Introduction Syntax Semantics Proof System Pure states ! mixed states Conclusion

Introduction Syntax Semantics Proof System Pure states → mixed states Conclusion

Quantum computing

� Quantum computing is usually described using �nite-dimensional Hilbert spacesand linear maps (or �nite-dimensional C*-algebras and completely positive maps).

� Computing the matrix representation of quantum operations requires memoryexponential in the number of input qubits.

� This is not a scalable approach for software applications related to quantuminformation processing (QIP).

� An alternative is provided by the ZX-calculus which is a sound, complete anduniversal diagrammatic calculus for equational reasoning about �nite-dimensionalquantum computing.

2 / 38

Page 3: Baby's First Diagrammatic Calculus for Quantum Information ...cs.tulane.edu/~vzamdzhi/slides/quilt.pdf · Introduction Syntax Semantics Proof System Pure states ! mixed states Conclusion

Introduction Syntax Semantics Proof System Pure states → mixed states Conclusion

Quantum computing

� Quantum computing is usually described using �nite-dimensional Hilbert spacesand linear maps (or �nite-dimensional C*-algebras and completely positive maps).

� Computing the matrix representation of quantum operations requires memoryexponential in the number of input qubits.

� This is not a scalable approach for software applications related to quantuminformation processing (QIP).

� An alternative is provided by the ZX-calculus which is a sound, complete anduniversal diagrammatic calculus for equational reasoning about �nite-dimensionalquantum computing.

2 / 38

Page 4: Baby's First Diagrammatic Calculus for Quantum Information ...cs.tulane.edu/~vzamdzhi/slides/quilt.pdf · Introduction Syntax Semantics Proof System Pure states ! mixed states Conclusion

Introduction Syntax Semantics Proof System Pure states → mixed states Conclusion

ZX-calculus

� The calculus is diagrammatic (some similarities to quantum circuits).� Example: Preparation of a Bell state.

H7→

|0〉

|0〉

� The ZX-calculus is practical. Used to study and discover new results in:� Quantum error-correcting codes [Chancellor, Kissinger, et. al 2016].� Measurement-based quantum computing [Duncan & Perdrix 2010].� (Quantum) foundations [Backens & Duman 2014].� and others...

3 / 38

Page 5: Baby's First Diagrammatic Calculus for Quantum Information ...cs.tulane.edu/~vzamdzhi/slides/quilt.pdf · Introduction Syntax Semantics Proof System Pure states ! mixed states Conclusion

Introduction Syntax Semantics Proof System Pure states → mixed states Conclusion

ZX-calculus

� The ZX-calculus is formal.� Developed through the study of categorical quantum mechanics.� Rewrite system based on string diagrams of dagger compact closed categories.� Universal: Any linear map in FdHilb is the interpretation of some ZX-diagram D.� Sound: If ZX ` D1 = D2, then JD1K = JD2K.� Complete: If JD1K = JD2K, then ZX ` D1 = D2.

4 / 38

Page 6: Baby's First Diagrammatic Calculus for Quantum Information ...cs.tulane.edu/~vzamdzhi/slides/quilt.pdf · Introduction Syntax Semantics Proof System Pure states ! mixed states Conclusion

Introduction Syntax Semantics Proof System Pure states → mixed states Conclusion

ZX-calculus� The ZX-calculus is amenable to automation and formal reasoning.

� Implemented in the Quantomatic proof assistant.

Figure: The quantomatic proof assistant.5 / 38

Page 7: Baby's First Diagrammatic Calculus for Quantum Information ...cs.tulane.edu/~vzamdzhi/slides/quilt.pdf · Introduction Syntax Semantics Proof System Pure states ! mixed states Conclusion

Introduction Syntax Semantics Proof System Pure states → mixed states Conclusion

ZX-calculus

� The ZX-calculus provides a di�erent conceptual perspective of quantuminformation.

Example

The Bell state is the standard example of an entangled state:

H7→

|0〉

|0〉= · · · =

The diagrammatic notation clearly indicates this is not a separable state.

6 / 38

Page 8: Baby's First Diagrammatic Calculus for Quantum Information ...cs.tulane.edu/~vzamdzhi/slides/quilt.pdf · Introduction Syntax Semantics Proof System Pure states ! mixed states Conclusion

Introduction Syntax Semantics Proof System Pure states → mixed states Conclusion

SyntaxA ZX-diagram is an open undirected graph constructed from the following generators:

α , ,α ,

where α ∈ [0, 2π).

Example

π π/2

π/4

7 / 38

Page 9: Baby's First Diagrammatic Calculus for Quantum Information ...cs.tulane.edu/~vzamdzhi/slides/quilt.pdf · Introduction Syntax Semantics Proof System Pure states ! mixed states Conclusion

Introduction Syntax Semantics Proof System Pure states → mixed states Conclusion

Syntax

The ZX-calculus is an equational theory. Equality is written as D1 = D2:

Example

=

8 / 38

Page 10: Baby's First Diagrammatic Calculus for Quantum Information ...cs.tulane.edu/~vzamdzhi/slides/quilt.pdf · Introduction Syntax Semantics Proof System Pure states ! mixed states Conclusion

Introduction Syntax Semantics Proof System Pure states → mixed states Conclusion

Normalisation

Remark: I ignore scalars and normalisation throughout the rest of the talk for brevity.But that can be handled by the language.

9 / 38

Page 11: Baby's First Diagrammatic Calculus for Quantum Information ...cs.tulane.edu/~vzamdzhi/slides/quilt.pdf · Introduction Syntax Semantics Proof System Pure states ! mixed states Conclusion

Introduction Syntax Semantics Proof System Pure states → mixed states Conclusion

Semantics: wires

J K :=(1 00 1

)t |

:=

1 0 0 00 0 1 00 1 0 00 0 0 1

t |

= |00〉+ |11〉

t |

= 〈00|+ 〈11|

10 / 38

Page 12: Baby's First Diagrammatic Calculus for Quantum Information ...cs.tulane.edu/~vzamdzhi/slides/quilt.pdf · Introduction Syntax Semantics Proof System Pure states ! mixed states Conclusion

Introduction Syntax Semantics Proof System Pure states → mixed states Conclusion

Semantics: spiders and hadamard

J K =1√2

(1 11 −1

)= H

u

wwwv

α

}

���~

=

|0m〉 7→ |0n〉|1m〉 7→ e iα|1n〉others 7→ 0

u

wwwv

α

}

���~

=

|+m〉 7→ |+n〉|−m〉 7→ e iα|−n〉

others 7→ 0

11 / 38

Page 13: Baby's First Diagrammatic Calculus for Quantum Information ...cs.tulane.edu/~vzamdzhi/slides/quilt.pdf · Introduction Syntax Semantics Proof System Pure states ! mixed states Conclusion

Introduction Syntax Semantics Proof System Pure states → mixed states Conclusion

Semantics: tensors

If

u

v D1

}

~ = M1 and

u

v D2

}

~ = M2, then:

u

wwwwwwwwv

D1

D2

}

��������~

= M1 ⊗M2

12 / 38

Page 14: Baby's First Diagrammatic Calculus for Quantum Information ...cs.tulane.edu/~vzamdzhi/slides/quilt.pdf · Introduction Syntax Semantics Proof System Pure states ! mixed states Conclusion

Introduction Syntax Semantics Proof System Pure states → mixed states Conclusion

Semantics: composition

If

u

v D1

}

~ = M1 and

u

v D2

}

~ = M2, then:

u

v D1 D2

}

~ = M2 ◦M1

By following these rules we can represent any linear map f : C2m 7→ Cn as aZX-diagram (universality).

13 / 38

Page 15: Baby's First Diagrammatic Calculus for Quantum Information ...cs.tulane.edu/~vzamdzhi/slides/quilt.pdf · Introduction Syntax Semantics Proof System Pure states ! mixed states Conclusion

Introduction Syntax Semantics Proof System Pure states → mixed states Conclusion

Example: Quantum States

State ZX-diagram

|0〉|1〉 π

|+〉|−〉 π

|00〉+ |11〉

14 / 38

Page 16: Baby's First Diagrammatic Calculus for Quantum Information ...cs.tulane.edu/~vzamdzhi/slides/quilt.pdf · Introduction Syntax Semantics Proof System Pure states ! mixed states Conclusion

Introduction Syntax Semantics Proof System Pure states → mixed states Conclusion

Example: unitary operations

Unitary map ZX-diagram

Z π

X π

H

Z ◦ X ππ

15 / 38

Page 17: Baby's First Diagrammatic Calculus for Quantum Information ...cs.tulane.edu/~vzamdzhi/slides/quilt.pdf · Introduction Syntax Semantics Proof System Pure states ! mixed states Conclusion

Introduction Syntax Semantics Proof System Pure states → mixed states Conclusion

Example: 2-qubit gates

Unitary map ZX-diagram

Z ⊗ Xπ

π

∧Z

CNOT

16 / 38

Page 18: Baby's First Diagrammatic Calculus for Quantum Information ...cs.tulane.edu/~vzamdzhi/slides/quilt.pdf · Introduction Syntax Semantics Proof System Pure states ! mixed states Conclusion

Introduction Syntax Semantics Proof System Pure states → mixed states Conclusion

Proof systemThere are only 12 axioms. Five of them are:

α

β

= α+ β = =

=

; ; ;

; α α=

Remark: The color-swapped versions follow as derived rules.

Remark: This rewrite system is sound and complete, i.e. no need for linear algebra:

ZX ` D1 = D2 ⇐⇒ JD1K = JD2K.

17 / 38

Page 19: Baby's First Diagrammatic Calculus for Quantum Information ...cs.tulane.edu/~vzamdzhi/slides/quilt.pdf · Introduction Syntax Semantics Proof System Pure states ! mixed states Conclusion

Introduction Syntax Semantics Proof System Pure states → mixed states Conclusion

Example: Preparation of Bell state

H7→

|0〉

|0〉= = =

18 / 38

Page 20: Baby's First Diagrammatic Calculus for Quantum Information ...cs.tulane.edu/~vzamdzhi/slides/quilt.pdf · Introduction Syntax Semantics Proof System Pure states ! mixed states Conclusion

Introduction Syntax Semantics Proof System Pure states → mixed states Conclusion

Example: CNOT is self-adjoint

Lemma: =

Then:

= == =7→

=

19 / 38

Page 21: Baby's First Diagrammatic Calculus for Quantum Information ...cs.tulane.edu/~vzamdzhi/slides/quilt.pdf · Introduction Syntax Semantics Proof System Pure states ! mixed states Conclusion

Introduction Syntax Semantics Proof System Pure states → mixed states Conclusion

From Hilbert spaces to C*-algebras

� So far we talked about pure state quantum mechanics (FdHilb).

� Next, we show how to model mixed-states (FdCStar).

� I omit some details for simplicity (see [Coecke & Kissinger, Picturing QuantumProcesses]).

� The basic idea is to double up our diagrams and negate all angles in one of thecopies (but there are other ways as well).

Example

π/4 π π/2 7→π/4 π π/2

−π/4 π −π/2

20 / 38

Page 22: Baby's First Diagrammatic Calculus for Quantum Information ...cs.tulane.edu/~vzamdzhi/slides/quilt.pdf · Introduction Syntax Semantics Proof System Pure states ! mixed states Conclusion

Introduction Syntax Semantics Proof System Pure states → mixed states Conclusion

Example: Quantum States

State (FdHilb) ZX-diagram

|0〉|1〉 π

|+〉|−〉 π

|00〉+ |11〉

State (FdCStar) ZX-diagram

|0〉〈0|

|1〉〈1| π

π

|+〉〈+|

|−〉〈−| π

π

|00〉〈00|+ |11〉〈11|

21 / 38

Page 23: Baby's First Diagrammatic Calculus for Quantum Information ...cs.tulane.edu/~vzamdzhi/slides/quilt.pdf · Introduction Syntax Semantics Proof System Pure states ! mixed states Conclusion

Introduction Syntax Semantics Proof System Pure states → mixed states Conclusion

Example: unitary operations

Unitary map (FdHilb) ZX-diagram

Z π

X π

T π/4

H

Z ◦ X ππ

Unitary map (FdCStar) ZX-diagram

π

π

Tπ/4

−π/4

H

Z ◦ Xππ

π π

22 / 38

Page 24: Baby's First Diagrammatic Calculus for Quantum Information ...cs.tulane.edu/~vzamdzhi/slides/quilt.pdf · Introduction Syntax Semantics Proof System Pure states ! mixed states Conclusion

Introduction Syntax Semantics Proof System Pure states → mixed states Conclusion

Example: conditional unitary operations

Conditional unitary ZX-diagram

Zb

X b

23 / 38

Page 25: Baby's First Diagrammatic Calculus for Quantum Information ...cs.tulane.edu/~vzamdzhi/slides/quilt.pdf · Introduction Syntax Semantics Proof System Pure states ! mixed states Conclusion

Introduction Syntax Semantics Proof System Pure states → mixed states Conclusion

Measuremens

Measurement ZX-diagram

Measurement in Z basis

Measurement in X basis

Measurement in Bell basis

24 / 38

Page 26: Baby's First Diagrammatic Calculus for Quantum Information ...cs.tulane.edu/~vzamdzhi/slides/quilt.pdf · Introduction Syntax Semantics Proof System Pure states ! mixed states Conclusion

Introduction Syntax Semantics Proof System Pure states → mixed states Conclusion

Example: quantum teleportation

0. A qubit owned by Alice.

25 / 38

Page 27: Baby's First Diagrammatic Calculus for Quantum Information ...cs.tulane.edu/~vzamdzhi/slides/quilt.pdf · Introduction Syntax Semantics Proof System Pure states ! mixed states Conclusion

Introduction Syntax Semantics Proof System Pure states → mixed states Conclusion

Example: quantum teleportation

1. Prepare Bell state.

26 / 38

Page 28: Baby's First Diagrammatic Calculus for Quantum Information ...cs.tulane.edu/~vzamdzhi/slides/quilt.pdf · Introduction Syntax Semantics Proof System Pure states ! mixed states Conclusion

Introduction Syntax Semantics Proof System Pure states → mixed states Conclusion

Example: quantum teleportation

2. Do Bell basis measurement on both of Alice's qubits.

27 / 38

Page 29: Baby's First Diagrammatic Calculus for Quantum Information ...cs.tulane.edu/~vzamdzhi/slides/quilt.pdf · Introduction Syntax Semantics Proof System Pure states ! mixed states Conclusion

Introduction Syntax Semantics Proof System Pure states → mixed states Conclusion

Example: quantum teleportation

3. Alice sends two bits (b1, b2) to Bob to inform him of measurement outcome.

b1

b2

28 / 38

Page 30: Baby's First Diagrammatic Calculus for Quantum Information ...cs.tulane.edu/~vzamdzhi/slides/quilt.pdf · Introduction Syntax Semantics Proof System Pure states ! mixed states Conclusion

Introduction Syntax Semantics Proof System Pure states → mixed states Conclusion

Example: quantum teleportation

4. Bob performs unitary correction X b1 ◦ Zb2 .

29 / 38

Page 31: Baby's First Diagrammatic Calculus for Quantum Information ...cs.tulane.edu/~vzamdzhi/slides/quilt.pdf · Introduction Syntax Semantics Proof System Pure states ! mixed states Conclusion

Introduction Syntax Semantics Proof System Pure states → mixed states Conclusion

Example: quantum teleportation

We can now prove the correctness of the teleportation protocol in the ZX-calculus:

=

30 / 38

Page 32: Baby's First Diagrammatic Calculus for Quantum Information ...cs.tulane.edu/~vzamdzhi/slides/quilt.pdf · Introduction Syntax Semantics Proof System Pure states ! mixed states Conclusion

Introduction Syntax Semantics Proof System Pure states → mixed states Conclusion

Example: quantum teleportationInput: A qubit owned by Alice.

==

31 / 38

Page 33: Baby's First Diagrammatic Calculus for Quantum Information ...cs.tulane.edu/~vzamdzhi/slides/quilt.pdf · Introduction Syntax Semantics Proof System Pure states ! mixed states Conclusion

Introduction Syntax Semantics Proof System Pure states → mixed states Conclusion

Example: quantum teleportationInput: A qubit owned by Alice.

==

32 / 38

Page 34: Baby's First Diagrammatic Calculus for Quantum Information ...cs.tulane.edu/~vzamdzhi/slides/quilt.pdf · Introduction Syntax Semantics Proof System Pure states ! mixed states Conclusion

Introduction Syntax Semantics Proof System Pure states → mixed states Conclusion

Example: quantum teleportationInput: A qubit owned by Alice.

==

33 / 38

Page 35: Baby's First Diagrammatic Calculus for Quantum Information ...cs.tulane.edu/~vzamdzhi/slides/quilt.pdf · Introduction Syntax Semantics Proof System Pure states ! mixed states Conclusion

Introduction Syntax Semantics Proof System Pure states → mixed states Conclusion

Example: quantum teleportationInput: A qubit owned by Alice.

==

34 / 38

Page 36: Baby's First Diagrammatic Calculus for Quantum Information ...cs.tulane.edu/~vzamdzhi/slides/quilt.pdf · Introduction Syntax Semantics Proof System Pure states ! mixed states Conclusion

Introduction Syntax Semantics Proof System Pure states → mixed states Conclusion

Example: quantum teleportationInput: A qubit owned by Alice.

==

35 / 38

Page 37: Baby's First Diagrammatic Calculus for Quantum Information ...cs.tulane.edu/~vzamdzhi/slides/quilt.pdf · Introduction Syntax Semantics Proof System Pure states ! mixed states Conclusion

Introduction Syntax Semantics Proof System Pure states → mixed states Conclusion

Example: quantum teleportation

=

Therefore, teleportation works as expected.

36 / 38

Page 38: Baby's First Diagrammatic Calculus for Quantum Information ...cs.tulane.edu/~vzamdzhi/slides/quilt.pdf · Introduction Syntax Semantics Proof System Pure states ! mixed states Conclusion

Introduction Syntax Semantics Proof System Pure states → mixed states Conclusion

Conclusion

� The ZX-calculus is a sound and complete alternative to linear algebra for�nite-dimensional quantum information processing.

� Great potential for formal methods, veri�cation and computer-aided reasoning.� Useful tool for studying QIP.� If you want to learn more, check out the book (contains outdated and incompleteversion of ZX):

37 / 38

Page 39: Baby's First Diagrammatic Calculus for Quantum Information ...cs.tulane.edu/~vzamdzhi/slides/quilt.pdf · Introduction Syntax Semantics Proof System Pure states ! mixed states Conclusion

Introduction Syntax Semantics Proof System Pure states → mixed states Conclusion

Thank you for your attention!

38 / 38