Encoding High-level Quantum Programs as SZX-diagrams

TL;DR

This paper introduces a method to encode quantum programs from a specific language into SZX-diagrams, enabling scalable and systematic reasoning about quantum algorithms.

Contribution

It presents a novel encoding technique for translating a fragment of Proto-Quipper-D into SZX-diagrams, facilitating scalable diagram construction.

Findings

Diagrams grow linearly with program size

The method encodes non-trivial quantum algorithms

Enables systematic reasoning with SZX-diagrams

Abstract

The Scalable ZX-calculus is a compact graphical language used to reason about linear maps between quantum states. These diagrams have multiple applications, but they frequently have to be constructed in a case-by-case basis. In this work we present a method to encode quantum programs implemented in a fragment of the linear dependently typed Proto-Quipper-D language as families of SZX-diagrams. We define a subset of translatable Proto-Quipper-D programs and show that our procedure is able to encode non-trivial algorithms as diagrams that grow linearly on the size of the program.