nLab quantum programming language

Contents

Context

Quantum systems

quantum logic


quantum physics


quantum probability theoryobservables and states


quantum information


quantum computation

qbit

quantum algorithms:


quantum sensing


quantum communication

Computation

Type theory

natural deduction metalanguage, practical foundations

  1. type formation rule
  2. term introduction rule
  3. term elimination rule
  4. computation rule

type theory (dependent, intensional, observational type theory, homotopy type theory)

syntax object language

computational trinitarianism =
propositions as types +programs as proofs +relation type theory/category theory

logicset theory (internal logic of)category theorytype theory
propositionsetobjecttype
predicatefamily of setsdisplay morphismdependent type
proofelementgeneralized elementterm/program
cut rulecomposition of classifying morphisms / pullback of display mapssubstitution
introduction rule for implicationcounit for hom-tensor adjunctionlambda
elimination rule for implicationunit for hom-tensor adjunctionapplication
cut elimination for implicationone of the zigzag identities for hom-tensor adjunctionbeta reduction
identity elimination for implicationthe other zigzag identity for hom-tensor adjunctioneta conversion
truesingletonterminal object/(-2)-truncated objecth-level 0-type/unit type
falseempty setinitial objectempty type
proposition, truth valuesubsingletonsubterminal object/(-1)-truncated objecth-proposition, mere proposition
logical conjunctioncartesian productproductproduct type
disjunctiondisjoint union (support of)coproduct ((-1)-truncation of)sum type (bracket type of)
implicationfunction set (into subsingleton)internal hom (into subterminal object)function type (into h-proposition)
negationfunction set into empty setinternal hom into initial objectfunction type into empty type
universal quantificationindexed cartesian product (of family of subsingletons)dependent product (of family of subterminal objects)dependent product type (of family of h-propositions)
existential quantificationindexed disjoint union (support of)dependent sum ((-1)-truncation of)dependent sum type (bracket type of)
logical equivalencebijection setobject of isomorphismsequivalence type
support setsupport object/(-1)-truncationpropositional truncation/bracket type
n-image of morphism into terminal object/n-truncationn-truncation modality
equalitydiagonal function/diagonal subset/diagonal relationpath space objectidentity type/path type
completely presented setsetdiscrete object/0-truncated objecth-level 2-type/set/h-set
setset with equivalence relationinternal 0-groupoidBishop set/setoid with its pseudo-equivalence relation an actual equivalence relation
equivalence class/quotient setquotientquotient type
inductioncolimitinductive type, W-type, M-type
higher inductionhigher colimithigher inductive type
-0-truncated higher colimitquotient inductive type
coinductionlimitcoinductive type
presettype without identity types
set of truth valuessubobject classifiertype of propositions
domain of discourseuniverseobject classifiertype universe
modalityclosure operator, (idempotent) monadmodal type theory, monad (in computer science)
linear logic(symmetric, closed) monoidal categorylinear type theory/quantum computation
proof netstring diagramquantum circuit
(absence of) contraction rule(absence of) diagonalno-cloning theorem
synthetic mathematicsdomain specific embedded programming language

homotopy levels

semantics

Contents

Idea

A quantum programming language is a programming language for quantum computation.

In as far as data types in classical programming languages may and often are understood in terms of (dependent) type theory, quantum programming languages concern quantum data types such as “qbits” which may be understood via linear logic (Pratt (1992)) in (dependent) linear type theory (e.g. Abramsky & Duncan (2005); Duncan (2006); Dal Lago & Faggian (2012); Green et al (2013); Staton (2015)):

“A quantum programming language captures the ideas of quantum computation in a linear type theory.” [Staton (2015), p. 1]

Many existing quantum programming languages are in fact domain specific programming languages for the description of quantum circuits compiled from quantum logic gates, and as such often embedded into ambient type theories (eg. Quipper and QWIRE).

Other QPLs are more algorithmic (such as Q Sharp).

References

Quantum programming languages

The first proposal towards formalizing quantum programming languages was:

and early formalization via quantum lambda-calculus invoking linear logic/linear types (cf. Pratt 1992 etc.):

[Selinger (2016):] When the QPL workshop series was first founded, it was called “Quantum Programming Languages”. One year I wasn’t participating, and while I wasn’t looking they changed the name to “Quantum Physics and Logic” — same acronym!

Back in those days in the early 21st century we were actually trying to do programming languages for quantum computing [[Selinger & Valiron 2004]], but the sad thing is: In those days nobody really cared. [...][...]

Now it’s 15 years later and several of these parameters have changed: There has been a renewed interest, from government agencies and also from companies who are actually building quantum computers. [...][...].

So now people are working on quantum programming languages again.

Exposition of the general idea of quantum programming languages for classically controlled quantum computation with an eye towards the Quipper-language:

On quantum programming languages (programming languages for quantum computation):

General:

See also:

Surveys of existing languages:

  • Simon Gay, Quantum programming languages: Survey and bibliography, Mathematical Structures in Computer Science16(2006) (doi:10.1017/S0960129506005378, pdf)

  • Sunita Garhwal, Maryam Ghorani , Amir Ahmad, Quantum Programming Language: A Systematic Review of Research Topic and Top Cited Languages, Arch Computat Methods Eng 28, 289–310 (2021) (doi:10.1007/s11831-019-09372-6)

  • B. Heim et al., Quantum programming languages, Nat Rev Phys 2 (2020) 709–722 [[doi:10.1038/s42254-020-00245-7]]

Quantum programming via quantum logic understood as linear type theory interpreted in symmetric monoidal categories:

The corresponding string diagrams are known in quantum computation as quantum circuit diagrams:

Typed\;functional programming languages for quantum computation:

QPL:

QML:

quantum IO monad:

Quipper:

QWIRE:

CoqQ:


On Q Sharp:

  • Kartik Singhal, Kesha Hietala, Sarah Marshall, Robert Rand, Q# as a Quantum Algorithmic Language, Proceedings of Quantum Physics and Logic (2022) [[arXiv:2206.03532]]

On classically controlled quantum computation:

Quantum programming via dependent linear type theory/indexed monoidal (∞,1)-categories:

specifically with Quipper:

See also QS.

On quantum software engineering:

On software verification:

with QWIRE:

for Quipper with QPMC:

  • Linda Anticoli, Carla Piazza, Leonardo Taglialegne, Paolo Zuliani, Towards Quantum Programs Verification: From Quipper Circuits to QPMC, In: Devitt S., Lanese I. (eds.) Reversible Computation. RC 2016, Lecture Notes in Computer Science 9720 Springer (2016) [[arXiv:1708.06312, doi:10.1007/978-3-319-40578-0_16]]

with CoqQ: Ying et al. (2022)

Last revised on November 15, 2023 at 17:24:21. See the history of this page for a list of all contributions to it.