Challenges
Datasets
Workspaces
Papers
Discussions
Leaderboard
Log inSign up
Challenges
Datasets
Workspaces
Papers
Discussions
Leaderboard
Blog
Job Board
Q3AS

© 2026 Aqora Quantum S.A.S.

TermsPrivacyLegal Notice

Electronic Notes in Theoretical Computer Science

A Hierarchy of Quantum Semantics

Simon Perdrix

Published Nov 1, 2008• 6 citations
Publisher

Abstract

Several domains [S. Abramsky. A Cook's tour of a simple quantum programming language. 3rd International Symposium on Domain Theory, Xi'an, China, May 2004; B. Coecke and K. Martin. A partial order on classical and quantum states. Technical report, PRG-RR-02-07, 2002; Ph. Jorrand and S. Perdrix. Towards a quantum calculus. In To appear in Proceedings of the 4th International Workshop on Quantum Programming Languages, ENTCS, 2006; P. Selinger. Towards a quantum programming language. Mathematical Structures in Computer Science, 14(4):527–586, 2004] can be used to define the semantics of quantum programs. Among them Abramsky [S. Abramsky. A Cook's tour of a simple quantum programming language. 3rd International Symposium on Domain Theory, Xi'an, China, May 2004] has introduced a semantics based on probabilistic power domains, whereas the one by Selinger [P. Selinger. Towards a quantum programming language. Mathematical Structures in Computer Science, 14(4):527–586, 2004] associates with every program a completely positive map. In this paper, we mainly introduce a semantical domain based on admissible transformations, i.e. multisets of linear operators. In order to establish a comparison with existing domains, we introduce a simple quantum imperative language (QIL), equipped with three different denotational semantics, called pure, observable, and admissible respectively. The pure semantics is a natural extension of probabilistic (classical) semantics and is similar to the semantics proposed by Abramsky [S. Abramsky. A Cook's tour of a simple quantum programming language. 3rd International Symposium on Domain Theory, Xi'an, China, May 2004]. The observable semantics, à la Selinger [P. Selinger. Towards a quantum programming language. Mathematical Structures in Computer Science, 14(4):527–586, 2004], associates with any program a superoperator over density matrices. Finally, we introduce an admissible semantics which associates with any program an admissible transformation. These semantics are not equivalent, but exact abstraction [P. Cousot. Types as abstract interpretations. In POPL, pages 316–331, 1997] or interpretation relations are established between them, leading to a hierarchy of quantum semantics.

DOI
10.1016/j.entcs.2008.10.028

Related papers

Towards a Quantum Calculus

Philippe Jorrand, Simon Perdrix

The aim of this paper is to introduce a general model of quantum computation, the quantum calculus: both unitary transformations and projective measurements are allowed; furthermore a complete classical control, including conditional structures and loops, is available. Complementary to its operational semantics, we introduce a pure denotational semantics for the quantum calculus. Based on probabilistic power domains [Jones, C. and G. D. Plotkin, A probabilistic powerdomain of evaluations, in: LICS, 1989, pp. 186–195. URL http://homepages.inf.ed.ac.uk/gdp/publications/Prob_Powerdomain.pdf], this pure denotational semantics associates with any description of a computation in the quantum calculus its action in a mathematical setting. Adequacy between operational and pure denotational semantics is established. Additionally to this pure denotational semantics, an observable denotational semantics is introduced. Following the work by Selinger, this observable denotational semantics is based on density matrices and super-operators. Finally, we establish an exact abstraction connection between these two semantics.

Electronic Notes in Theoretical Computer Science•Jul 1, 2008•2 citations

De-linearizing Linearity: Projective Quantum Axiomatics From Strong Compact Closure

Bob Coecke

Elaborating on our joint work with Abramsky in [S. Abramsky, B. Coecke, B. (2004) A categorical semantics of quantum protocols. Proceedings of the 19th Annual IEEE Symposium on Logic in Computer Science (LiCS'04), IEEE Computer Science Press. Extended version including proofs at arXiv:quant-ph/0402130, S. Abramsky, B. Coecke, (2005) Abstract physical traces. Theory and Applications of Categories 14, 111–124] we further unravel the linear structure of Hilbert spaces into several constituents. Some prove to be very crucial for particular features of quantum theory while others obstruct the passage to a formalism which is not saturated with physically insignificant global phases. First we show that the bulk of the required linear structure is purely multiplicative, and arises from the strongly compact closed tensor which, besides providing a variety of notions such as scalars, trace, unitarity, self-adjointness and bipartite projectors [S. Abramsky, B. Coecke, B. (2004) A categorical semantics of quantum protocols. Proceedings of the 19th Annual IEEE Symposium on Logic in Computer Science (LiCS'04), IEEE Computer Science Press. Extended version including proofs at arXiv:quant-ph/0402130, S. Abramsky, B. Coecke, (2005) Abstract physical traces. Theory and Applications of Categories 14, 111–124], also provides Hilbert-Schmidt norm, Hilbert-Schmidt inner-product, and in particular, the preparation-state agreement axiom which enables the passage from a formalism of the vector space kind to a rather projective one, as it was intended in the (in)famous Birkhoff & von Neumann paper [G. Birkhoff, J. von Neumann, (1936) The logic of quantum mechanics. Annals of Mathematics 37, 823–843]. Next we consider additive types which distribute over the tensor, from which measurements can be build, and the correctness proofs of the protocols discussed in [S. Abramsky, B. Coecke, (2004) A categorical semantics of quantum protocols. Proceedings of the 19th Annual IEEE Symposium on Logic in Computer Science (LiCS'04), IEEE Computer Science Press. Extended version including proofs at arXiv:quant-ph/0402130] carry over to the resulting weaker setting. A full probabilistic calculus is obtained when the trace is moreover linear and satisfies the diagonal axiom, which brings us to a second main result, characterization of the necessary and sufficient additive structure of a both qualitatively and quantitatively effective categorical quantum formalism without redundant global phases. Along the way we show that if in a category a (additive) monoidal tensor distributes over a strongly compact closed tensor, then this category is always enriched in commutative monoids.

arXiv:quant-ph/0506134•Electronic Notes in Theoretical Computer Science•Mar 1, 2007•60 citations

Quantum Patterns and Types for Entanglement and Separability

Simon Perdrix

As a first step toward a notion of quantum data structures, we introduce a typing system for reflecting entanglement and separability. This is presented in the context of classically controlled quantum computation where a classical program controls a sequence of quantum operations, i.e. unitary transformations and measurements acting on a quantum memory. Abstract models for such quantum computations are the Quantum Random Access Machine (QRAM [E. Knill, Conventions for Quantum Pseudocode, LANL report LAUR-96-2724, 1996]) and the Classically-Controlled Quantum Turing Machine (CQTM [S. Perdrix, Ph. Jorrand, Classically-Controlled Quantum Computation, arXiv:quant-ph/0407008, to appear in Mathematical Structures in Computer Science]). Several quantum programming languages follow this model [S. Bettelli, T. Calarco, L. Serafini, Toward an architecture for quantum programming, Eur. Phys. J. D 25 (2) (2003) 181–200, S.J. Gay, R. Nagarajan, Communicating quantum processes, Proceedings of the 32nd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, Jens Palsberg and Martin Abadi (Eds.), POPL 2005, January 12–14, 2005, pp. 145–157, M. Lalire, Ph. Jorrand, A process algebraic approach to concurrent and distributed quantum computation: operational semantics, Proceedings of the 2nd International Workshop on Quantum Programming Languages, 2004, pp. 109–126, J.W. Sanders, P. Zuliani, Quantum Programming, Mathematics of Program Construction, Springer LNCS 1837, 80–99, 2000, P. Selinger, Towards a Quantum Programming Language, Mathematical Structures in Computer Science 14 (4) (2004) 527–586]. Among them, the functional language defined by Valiron [B. Valiron, Quantum Typing, Proceedings of the 2nd International Workshop on Quantum Programming Languages, 2004, pp. 163–178] is the basis for the language developed in this paper. This is work in progress.

Electronic Notes in Theoretical Computer Science•Mar 1, 2007•22 citations

On a Fully Abstract Model for a Quantum Linear Functional Language

Peter Selinger, Benoît Valiron

This paper studies the linear fragment of the programing language for quantum computation with classical control described in [Selinger, P. and B. Valiron, A lambda calculus for quantum computation with classical control, in: P. Urzyczyn, editor, Proceedings of the Seventh International Conference on Typed Lambda Calculi and Applications (TLCA 2005), Lecture Notes in Computer Science 3461 (2005), pp. 354–368]. We sketch the language, and discuss equivalence of terms. We also describe a fully abstract denotational semantics based on completely positive maps.

Electronic Notes in Theoretical Computer Science•Jul 1, 2008•45 citations

Predicate Transformer Semantics of Quantum Programs

Mingsheng Ying, Runyao Duan, Yuan Feng +1 more

This chapter presents a systematic exposition of predicate transformer semantics for quantum programs. It is divided into two parts: The first part reviews the state transformer (forward) semantics of quantum programs according to Selinger's suggestion of representing quantum programs by superoperators and elucidates D'Hondt-Panangaden's theory of quantum weakest preconditions in detail. In the second part, we develop a quite complete predicate transformer semantics of quantum programs based on Birkhoff-von Neumann quantum logic by considering only quantum predicates expressed by projection operators. In particular, the universal conjunctivity and termination law of quantum programs are proved, and Hoare's induction rule is established in the quantum setting. 8.1 Introduction In the mid-1990s Shor and Grover discovered, respectively, the famous quantum factoring and searching algorithms. Their discoveries indicated that in principle quantum computers offer a way to accomplish certain computational tasks much more efficiently than classical computers, and thus stimulated an intensive investigation in quantum computation. Since then a substantial effort has been made to develop the theory of quantum computation, to find new quantum algorithms, and to exploit the physical techniques needed in building functional quantum computers, including in particular fault tolerance techniques. Currently, quantum algorithms are expressed mainly at the very low level of quantum circuits. In the history of classical computation, however, it was realized long time ago that programming languages provide a technique that allows us to think about a problem that we intend to solve in a high-level, conceptual way, rather than the details of implementation.

Cambridge University Press eBooks•Nov 30, 2009•35 citations

Axiomatic Description of Mixed States From Selinger's CPM-construction

Bob Coecke

We recast Selinger's CPM-construction of mixed states completely positive maps [P. Selinger (2007) Dagger compact closed categories and completely positive maps. In: Proceedings of the 3rd International Workshop on Quantum Programming Languages (QPL 2005), Electronic Notes in Theoretical Computer Science 170, 139–163. Available from Peter Selinger's homepage] as an axiomatization of maximally mixed states. This axiomatization also guarantees categories of completely positive maps to satisfy the preparation-state agreement axiom of [Coecke, B. (2007) De-linearizing linearity: projective quantum axiomatics from strong compact closure. In: Proceedings of the 3rd International Workshop on Quantum Programming Languages (QPL 2005), Electronic Notes in Theoretical Computer Science 170, 49–72. E-print: arXiv:quant-ph/0506134], and admits a physical interpretation in terms of purification of mixed states and CPMs. Internal traces, which are crucial in quantum information theory, are the adjoints to these maximally mixed states.

Electronic Notes in Theoretical Computer Science•Jul 1, 2008•38 citations
Several domains [S. Abramsky. A Cook's tour of a simple quantum programming language. 3rd International Symposium on Domain Theory, Xi'an, China, May 2004; B. Coecke and K. Martin. A partial order on classical and quantum states. Technical report, PRG-RR-02-07, 2002; Ph. Jorrand and S. Perdrix. Towards a quantum calculus. In To appear in Proceedings of the 4th International Workshop on Quantum Programming Languages, ENTCS, 2006; P. Selinger. Towards a quantum programming language. Mathematical Structures in Computer Science, 14(4):527–586, 2004] can be used to define the semantics of quantum programs. Among them Abramsky [S. Abramsky. A Cook's tour of a simple quantum programming language. 3rd International Symposium on Domain Theory, Xi'an, China, May 2004] has introduced a semantics based on probabilistic power domains, whereas the one by Selinger [P. Selinger. Towards a quantum programming language. Mathematical Structures in Computer Science, 14(4):527–586, 2004] associates with every program a completely positive map. In this paper, we mainly introduce a semantical domain based on admissible transformations, i.e. multisets of linear operators. In order to establish a comparison with existing domains, we introduce a simple quantum imperative language (QIL), equipped with three different denotational semantics, called pure, observable, and admissible respectively. The pure semantics is a natural extension of probabilistic (classical) semantics and is similar to the semantics proposed by Abramsky [S. Abramsky. A Cook's tour of a simple quantum programming language. 3rd International Symposium on Domain Theory, Xi'an, China, May 2004]. The observable semantics, à la Selinger [P. Selinger. Towards a quantum programming language. Mathematical Structures in Computer Science, 14(4):527–586, 2004], associates with any program a superoperator over density matrices. Finally, we introduce an admissible semantics which associates with any program an admissible transformation. These semantics are not equivalent, but exact abstraction [P. Cousot. Types as abstract interpretations. In POPL, pages 316–331, 1997] or interpretation relations are established between them, leading to a hierarchy of quantum semantics.
The aim of this paper is to introduce a general model of quantum computation, the quantum calculus: both unitary transformations and projective measurements are allowed; furthermore a complete classical control, including conditional structures and loops, is available. Complementary to its operational semantics, we introduce a pure denotational semantics for the quantum calculus. Based on probabilistic power domains [Jones, C. and G. D. Plotkin, A probabilistic powerdomain of evaluations, in: LICS, 1989, pp. 186–195. URL http://homepages.inf.ed.ac.uk/gdp/publications/Prob_Powerdomain.pdf], this pure denotational semantics associates with any description of a computation in the quantum calculus its action in a mathematical setting. Adequacy between operational and pure denotational semantics is established. Additionally to this pure denotational semantics, an observable denotational semantics is introduced. Following the work by Selinger, this observable denotational semantics is based on density matrices and super-operators. Finally, we establish an exact abstraction connection between these two semantics.
Elaborating on our joint work with Abramsky in [S. Abramsky, B. Coecke, B. (2004) A categorical semantics of quantum protocols. Proceedings of the 19th Annual IEEE Symposium on Logic in Computer Science (LiCS'04), IEEE Computer Science Press. Extended version including proofs at arXiv:quant-ph/0402130, S. Abramsky, B. Coecke, (2005) Abstract physical traces. Theory and Applications of Categories 14, 111–124] we further unravel the linear structure of Hilbert spaces into several constituents. Some prove to be very crucial for particular features of quantum theory while others obstruct the passage to a formalism which is not saturated with physically insignificant global phases. First we show that the bulk of the required linear structure is purely multiplicative, and arises from the strongly compact closed tensor which, besides providing a variety of notions such as scalars, trace, unitarity, self-adjointness and bipartite projectors [S. Abramsky, B. Coecke, B. (2004) A categorical semantics of quantum protocols. Proceedings of the 19th Annual IEEE Symposium on Logic in Computer Science (LiCS'04), IEEE Computer Science Press. Extended version including proofs at arXiv:quant-ph/0402130, S. Abramsky, B. Coecke, (2005) Abstract physical traces. Theory and Applications of Categories 14, 111–124], also provides Hilbert-Schmidt norm, Hilbert-Schmidt inner-product, and in particular, the preparation-state agreement axiom which enables the passage from a formalism of the vector space kind to a rather projective one, as it was intended in the (in)famous Birkhoff & von Neumann paper [G. Birkhoff, J. von Neumann, (1936) The logic of quantum mechanics. Annals of Mathematics 37, 823–843]. Next we consider additive types which distribute over the tensor, from which measurements can be build, and the correctness proofs of the protocols discussed in [S. Abramsky, B. Coecke, (2004) A categorical semantics of quantum protocols. Proceedings of the 19th Annual IEEE Symposium on Logic in Computer Science (LiCS'04), IEEE Computer Science Press. Extended version including proofs at arXiv:quant-ph/0402130] carry over to the resulting weaker setting. A full probabilistic calculus is obtained when the trace is moreover linear and satisfies the diagonal axiom, which brings us to a second main result, characterization of the necessary and sufficient additive structure of a both qualitatively and quantitatively effective categorical quantum formalism without redundant global phases. Along the way we show that if in a category a (additive) monoidal tensor distributes over a strongly compact closed tensor, then this category is always enriched in commutative monoids.
As a first step toward a notion of quantum data structures, we introduce a typing system for reflecting entanglement and separability. This is presented in the context of classically controlled quantum computation where a classical program controls a sequence of quantum operations, i.e. unitary transformations and measurements acting on a quantum memory. Abstract models for such quantum computations are the Quantum Random Access Machine (QRAM [E. Knill, Conventions for Quantum Pseudocode, LANL report LAUR-96-2724, 1996]) and the Classically-Controlled Quantum Turing Machine (CQTM [S. Perdrix, Ph. Jorrand, Classically-Controlled Quantum Computation, arXiv:quant-ph/0407008, to appear in Mathematical Structures in Computer Science]). Several quantum programming languages follow this model [S. Bettelli, T. Calarco, L. Serafini, Toward an architecture for quantum programming, Eur. Phys. J. D 25 (2) (2003) 181–200, S.J. Gay, R. Nagarajan, Communicating quantum processes, Proceedings of the 32nd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, Jens Palsberg and Martin Abadi (Eds.), POPL 2005, January 12–14, 2005, pp. 145–157, M. Lalire, Ph. Jorrand, A process algebraic approach to concurrent and distributed quantum computation: operational semantics, Proceedings of the 2nd International Workshop on Quantum Programming Languages, 2004, pp. 109–126, J.W. Sanders, P. Zuliani, Quantum Programming, Mathematics of Program Construction, Springer LNCS 1837, 80–99, 2000, P. Selinger, Towards a Quantum Programming Language, Mathematical Structures in Computer Science 14 (4) (2004) 527–586]. Among them, the functional language defined by Valiron [B. Valiron, Quantum Typing, Proceedings of the 2nd International Workshop on Quantum Programming Languages, 2004, pp. 163–178] is the basis for the language developed in this paper. This is work in progress.
This paper studies the linear fragment of the programing language for quantum computation with classical control described in [Selinger, P. and B. Valiron, A lambda calculus for quantum computation with classical control, in: P. Urzyczyn, editor, Proceedings of the Seventh International Conference on Typed Lambda Calculi and Applications (TLCA 2005), Lecture Notes in Computer Science 3461 (2005), pp. 354–368]. We sketch the language, and discuss equivalence of terms. We also describe a fully abstract denotational semantics based on completely positive maps.
This chapter presents a systematic exposition of predicate transformer semantics for quantum programs. It is divided into two parts: The first part reviews the state transformer (forward) semantics of quantum programs according to Selinger's suggestion of representing quantum programs by superoperators and elucidates D'Hondt-Panangaden's theory of quantum weakest preconditions in detail. In the second part, we develop a quite complete predicate transformer semantics of quantum programs based on Birkhoff-von Neumann quantum logic by considering only quantum predicates expressed by projection operators. In particular, the universal conjunctivity and termination law of quantum programs are proved, and Hoare's induction rule is established in the quantum setting. 8.1 Introduction In the mid-1990s Shor and Grover discovered, respectively, the famous quantum factoring and searching algorithms. Their discoveries indicated that in principle quantum computers offer a way to accomplish certain computational tasks much more efficiently than classical computers, and thus stimulated an intensive investigation in quantum computation. Since then a substantial effort has been made to develop the theory of quantum computation, to find new quantum algorithms, and to exploit the physical techniques needed in building functional quantum computers, including in particular fault tolerance techniques. Currently, quantum algorithms are expressed mainly at the very low level of quantum circuits. In the history of classical computation, however, it was realized long time ago that programming languages provide a technique that allows us to think about a problem that we intend to solve in a high-level, conceptual way, rather than the details of implementation.
We recast Selinger's CPM-construction of mixed states completely positive maps [P. Selinger (2007) Dagger compact closed categories and completely positive maps. In: Proceedings of the 3rd International Workshop on Quantum Programming Languages (QPL 2005), Electronic Notes in Theoretical Computer Science 170, 139–163. Available from Peter Selinger's homepage] as an axiomatization of maximally mixed states. This axiomatization also guarantees categories of completely positive maps to satisfy the preparation-state agreement axiom of [Coecke, B. (2007) De-linearizing linearity: projective quantum axiomatics from strong compact closure. In: Proceedings of the 3rd International Workshop on Quantum Programming Languages (QPL 2005), Electronic Notes in Theoretical Computer Science 170, 49–72. E-print: arXiv:quant-ph/0506134], and admits a physical interpretation in terms of purification of mixed states and CPMs. Internal traces, which are crucial in quantum information theory, are the adjoints to these maximally mixed states.