The dagger lambda calculus

MaRDI QIDQ4997293zbMATH OpenFDO

Authors Philip Atzemoglou

Publication date 29 June 2021

Full work available at URL https://arxiv.org/abs/1406.1633, http://eptcs.web.cse.unsw.edu.au/paper.cgi?QPL2014.15

Mathematics Subject Classification ID

Quantum computation (81P68) Combinatory logic and lambda calculus (03B40) Closed categories (closed monoidal and Cartesian closed categories, etc.) (18D15) Dagger categories, categorical quantum mechanics (18M40)

Abstract: We present a novel lambda calculus that casts the categorical approach to the study of quantum protocols into the rich and well established tradition of type theory. Our construction extends the linear typed lambda calculus with a linear negation of "trivialised" De Morgan duality. Reduction is realised through explicit substitution, based on a symmetric notion of binding of global scope, with rules acting on the entire typing judgement instead of on a specific subterm. Proofs of subject reduction, confluence, strong normalisation and consistency are provided, and the language is shown to be an internal language for dagger compact categories.

Recommendations

• Dagger compact closed categories and completely positive maps (extended abstract)
• A categorical quantum logic
• Strong normalization theorems for quantized \(\lambda \)-calculi
• On a measurement-free quantum lambda calculus with classical control
• A double effect \(\lambda \)-calculus for quantum computation

Cited in

(4)

• The differential lambda-calculus
• Dagger compact closed categories and completely positive maps (extended abstract)
• Taming Non-compositionality Using New Binders
• Quantum Control in the Unitary Sphere: Lambda-S1 and its Categorical Model

This page was built for publication: The dagger lambda calculus

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q4997293)