Quantum programming with inductive datatypes: causality and affine type theory

DOI10.1007/978-3-030-45231-5_29zbMATH Open1442.68034arXiv1910.09633OpenAlexW3104517613MaRDI QIDQ2200848FDOQ2200848

Authors: Romain Péchoux, Simon Perdrix, Mathys Rennela, Vladimir Zamdzhiev 

Publication date: 23 September 2020

Abstract: Inductive datatypes in programming languages allow users to define useful data structures such as natural numbers, lists, trees, and others. In this paper we show how inductive datatypes may be added to the quantum programming language QPL. We construct a sound categorical model for the language and by doing so we provide the first detailed semantic treatment of user-defined inductive datatypes in quantum programming. We also show our denotational interpretation is invariant with respect to big-step reduction, thereby establishing another novel result for quantum programming. Compared to classical programming, this property is considerably more difficult to prove and we demonstrate its usefulness by showing how it immediately implies computational adequacy at all types. To further cement our results, our semantics is entirely based on a physically natural model of von Neumann algebras, which are mathematical structures used by physicists to study quantum mechanics.

Full work available at URL: https://arxiv.org/abs/1910.09633

Recommendations

• Semantics for first-order affine inductive data types via slice categories
• Semantics for a quantum programming language by operator algebras
• Semantics for a quantum programming language by operator algebras
• A lambda calculus for quantum computation with classical control

zbMATH Keywords

adequacyquantum programminginductive types

Mathematics Subject Classification ID

Theory of programming languages (68N15) Quantum computation (81P68) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30) Semantics in the theory of computing (68Q55)

Cites Work

• A single quantum cannot be cloned
• Towards a quantum programming language
• Quantum programming languages: survey and bibliography
• Theory of operator algebras I.
• Towards a quantum domain theory: order-enrichment and fixpoints in \(W^*\)-algebras
• Polynomial-Time Algorithms for Prime Factorization and Discrete Logarithms on a Quantum Computer
• Quantum collections
• Semantics of higher-order quantum computation via geometry of interaction
• Applying quantitative semantics to higher-order quantum computing
• A categorical semantics for causal structure
• Semantics for a quantum programming language by operator algebras
• Semantics for a quantum programming language by operator algebras
• Enriching a linear/non-linear lambda calculus: a programming language for string diagrams
• Quantum Programs as Kleisli Maps
• Title not available (Why is that?)
• Quantum Entanglement Analysis Based on Abstract Interpretation
• Title not available (Why is that?)
• Concurrent quantum strategies
• The geometry of parallelism: classical, probabilistic, and quantum effects

Cited In (12)

• Semantics for first-order affine inductive data types via slice categories
• Semantics of quantum programming languages: Classical control, quantum control
• A computer scientist’s reconstruction of quantum theory*
• Semantics for a lambda calculus for string diagrams
• Title not available (Why is that?)
• Title not available (Why is that?)
• Title not available (Why is that?)
• Quantum CPOs
• Quantum expectation transformers for cost analysis
• Title not available (Why is that?)
• Type-safe quantum programming in Idris
• Complexity of Grammar Induction for Quantum Types

This page was built for publication: Quantum programming with inductive datatypes: causality and affine type theory

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