Two linearities for quantum computing in the lambda calculus

TL;DR

This paper introduces a unified framework for quantum lambda-calculi that combines logical and algebraic linearities, enabling a more flexible approach to non-cloning in quantum computation.

Contribution

It proposes a quantum lambda-calculus that unifies two non-cloning approaches and interprets superpositions as vector spaces, advancing the theoretical understanding of quantum programming languages.

Findings

Defines a quantum extension of simply-typed lambda-calculus with linear types

Provides an interpretation of superpositions as vector spaces

Illustrates the unification of logical and algebraic linearities

Abstract

We propose a way to unify two approaches of non-cloning in quantum lambda-calculi: logical and algebraic linearities. The first approach is to forbid duplicating variables, while the second is to consider all lambda-terms as algebraic-linear functions. We illustrate this idea by defining a quantum extension of first-order simply-typed lambda-calculus, where the type is linear on superposition, while allows cloning base vectors. In addition, we provide an interpretation of the calculus where superposed types are interpreted as vector spaces and non-superposed types as their basis.