Presheaf models of quantum computation: an outline

TL;DR

This paper develops categorical presheaf models for higher-order quantum computation, providing a concrete denotational semantics for quantum lambda calculus using advanced category theory techniques.

Contribution

It constructs the first concrete presheaf-based denotational semantics for quantum lambda calculus, addressing an open problem in quantum computation modeling.

Findings

Successfully modeled quantum lambda calculus using presheaves

Identified specific base categories satisfying model requirements

Applied Day's convolution and Kelly-Freyd's continuity in the construction

Abstract

This paper outlines the construction of categorical models of higher-order quantum computation. We construct a concrete denotational semantics of Selinger and Valiron's quantum lambda calculus, which was previously an open problem. We do this by considering presheaves over appropriate base categories arising from first-order quantum computation. The main technical ingredients are Day's convolution theory and Kelly and Freyd's notion of continuity of functors. We first give an abstract description of the properties required of the base categories for the model construction to work. We then exhibit a specific example of base categories satisfying these properties.