Wave-Style Token Machines and Quantum Lambda Calculi

TL;DR

This paper extends particle-style token machines to quantum lambda calculus, enabling a new operational semantics that captures quantum entanglement through multiple concurrent tokens.

Contribution

It introduces a novel multi-token machine model for quantum lambda calculus, generalizing classical token machines to incorporate quantum phenomena like entanglement.

Findings

Multi-token machines model quantum entanglement.

Operational semantics align with quantum computation principles.

Framework supports simple quantum lambda calculus interpretation.

Abstract

Particle-style token machines are a way to interpret proofs and programs, when the latter are written following the principles of linear logic. In this paper, we show that token machines also make sense when the programs at hand are those of a simple quantum lambda-calculus with implicit qubits. This, however, requires generalising the concept of a token machine to one in which more than one particle travel around the term at the same time. The presence of multiple tokens is intimately related to entanglement and allows us to give a simple operational semantics to the calculus, coherently with the principles of quantum computation.