Measurements and confluence in quantum lambda calculi with explicit qubits

TL;DR

This paper introduces a measurement operator into quantum lambda-calculi, providing a general confluence proof for the semantics, which can be applied to other probabilistic rewrite systems and complex quantum languages.

Contribution

It presents a novel method to incorporate measurement into quantum lambda-calculi with a general confluence proof for the semantics.

Findings

Proof of confluence for the extended calculus

Method applicable to probabilistic rewrite systems

Potential extension to complex quantum languages

Abstract

This paper demonstrates how to add a measurement operator to quantum lambda-calculi. A proof of the consistency of the semantics is given through a proof of confluence presented in a sufficiently general way to allow this technique to be used for other languages. The method described here may be applied to probabilistic rewrite systems in general, and to add measurement to more complex languages such as QML or Lineal, which is the subject of further research.