Concrete Categorical Model of a Quantum Circuit Description Language with Measurement

TL;DR

This paper introduces a quantum circuit description language with dynamic lifting, enabling measurement results to be transferred from quantum to classical data, supported by a formal type system, semantics, and safety properties.

Contribution

It proposes a new language with dynamic lifting, a concrete categorical semantics based on recent models, and formal safety and soundness results for quantum-classical data transfer.

Findings

Developed a type system and operational semantics for the language

Constructed a concrete categorical semantics using Kleisli categories

Proved soundness of the semantics

Abstract

In this paper, we introduce dynamic lifting to a quantum circuit-description language, following the Proto-Quipper language approach. Dynamic lifting allows programs to transfer the result of measuring quantum data -- qubits -- into classical data -- booleans -- . We propose a type system and an operational semantics for the language and we state safety properties. Next, we introduce a concrete categorical semantics for the proposed language, basing our approach on a recent model from Rios\&Selinger for Proto-Quipper-M. Our approach is to construct on top of a concrete category of circuits with measurements a Kleisli category, capturing as a side effect the action of retrieving classical content out of a quantum memory. We then show a soundness result for this semantics.