skip to main content
10.1145/2676726.2676999acmconferencesArticle/Chapter ViewAbstractPublication PagespoplConference Proceedingsconference-collections
research-article

Algebraic Effects, Linearity, and Quantum Programming Languages

Published: 14 January 2015 Publication History

Abstract

We develop a new framework of algebraic theories with linear parameters, and use it to analyze the equational reasoning principles of quantum computing and quantum programming languages. We use the framework as follows:
we present a new elementary algebraic theory of quantum computation, built from unitary gates and measurement;
we provide a completeness theorem or the elementary algebraic theory by relating it with a model from operator algebra;
we extract an equational theory for a quantum programming language from the algebraic theory;
we compare quantum computation with other local notions of computation by investigating variations on the algebraic theory.

References

[1]
S. Abramsky and B. Coecke. A categorical semantics of quantum protocols. In Proc. LICS 2004, 2004.
[2]
J. Aczél. On mean values. Bull. Am. Math. Soc., 54:392--400, 1948.
[3]
R. Adams. QPEL: Quantum program and effect language. In Proc. QPL 2014, 2014. To appear.
[4]
D. Ahman and S. Staton. Normalization by evaluation and algebraic effects. In Proc. MFPS XXIX, pages 51--69, 2013.
[5]
T. Altenkirch, J. Chapman, and T. Uustalu. Monads need not be endofunctors. In FOSSACS 2010.
[6]
T. Altenkirch and A. Green. The Quantum IO Monad. In Semantic Techniques in Quantum Computation. CUP, 2009.
[7]
J. Baez and J. Dolan. From finite sets to Feynman diagrams. In Mathematics Unlimited -- 2001 and Beyond. Springer, 2001.
[8]
N. Benton and P. Wadler. Linear logic, monads and the lambda calculus. In LICS 1996.
[9]
C. Berger, P.-A. Melliès, and M. Weber. Monads with arities and their associated theories. J. Pure Appl. Algebra, 216, 2012.
[10]
S. L. Bloom and Z. Esik. Iteration Theories: The Equational Logic of Iterative Processes. Springer, 1993.
[11]
I. Cervesato and F. Pfenning. A Linear Logical Framework. Inform. Comput., 179(1):19--75, 2002.
[12]
G. Chiribella, G. M. D'Ariano, and P. Perinotti. Informational derivation of quantum theory. Phys. Rev. A, 84, 2011.
[13]
K. Cho. Semantics for a quantum programming language by operator algebras. In Proc. QPL 2014, 2014. To appear.
[14]
B. Coecke and R. Duncan. Interacting quantum observables. In Proc. ICALP 2008, pages 298--310, 2008.
[15]
V. Danos, E. Kashefi, and P. Panangaden. The measurement calculus. J. ACM, 54(2), 2007.
[16]
P. A. Fillmore. A User's Guide to Operator Algebras. Wiley-Interscience, 1996.
[17]
M. Fiore. Notes on combinatorial functors. Draft, 2001.
[18]
M. P. Fiore and C.-K. Hur. Second-order equational logic. In CSL'10.
[19]
A. S. Green, P. L. Lumsdaine, N. J. Ross, P. Selinger, and B. Valiron. Quipper: a scalable quantum programming language. In PLDI 2013.
[20]
L. Hardy. Reformulating and reconstructing quantum theory. arXiv:1104.2066, 2011.
[21]
C. Heunen, A. Kissinger, and P. Selinger. Completely positive projections and biproducts. arXiv:1308.4557.
[22]
B. Jacobs. On block structures in quantum computation. In Proc. MFPS XXIX, 2013.
[23]
G. Janelidze and G. Kelly. A note on actions of a monoidal category. Theory Appl. Categ., 9(4), 2001.
[24]
O. Kammar and G. D. Plotkin. Algebraic foundations for effect-dependent optimisations. In POPL 2012, pages 349--360, 2012.
[25]
G. M. Kelly and A. J. Power. Adjunctions whose counits are coequalisers. J. Pure Appl. Algebra, 89:163--179, 1993.
[26]
F. E. J. Linton. Autonomous equational categories. J. Math. Mech., 15:637--642, 1966.
[27]
O. Malherbe, P. J. Scott, and P. Selinger. Presheaf models of quantum computation: an outline. In Computation, Logic, Games, and Quantum Foundations. Springer, 2013.
[28]
P.-A. Melliès. Local stores in string diagrams. In RTA-TLCA 2014.
[29]
P.-A. Melliès. Segal condition meets computational effects. In Proc. LICS 2010, pages 150--159, 2010.
[30]
R. E. Møgelberg and S. Staton. Linear usage of state. Logical Methods Comput. Sci., 10(1), 2014.
[31]
M. A. Nielsen and I. L. Chuang. Quantum Computation and Quantum Information. CUP, 2011.
[32]
P. W. O'Hearn. On bunched typing. J. Funct. Program., 2003.
[33]
M. Pagani, P. Selinger, and B. Valiron. Applying quantitative semantics to higher-order quantum computing. In Proc. POPL 2014.
[34]
V. Paulsen. Completely Bounded Maps and Operator Algebras. CUP, 2003.
[35]
G. Plotkin. Some varieties of equational logic. In Algebra, meaning and computation. Springer, 2006.
[36]
G. D. Plotkin and J. Power. Notions of computation determine mon- ads. In Proc. FOSSACS'02, 2002.
[37]
G. D. Plotkin and J. Power. Algebraic operations and generic effects. Applied Categorical Structures, 11(1):69--94, 2003.
[38]
J. Power. Generic models for computational effects. Theor. Comput. Sci., 364(2):254--269, 2006.
[39]
J. Power. Indexed Lawvere theories for local state. In Models, logics and higher-dimensional categories: a tribute to the work of Mihály Makkai, pages 213--230. American Mathematical Society, 2011.
[40]
J. Power and M. Tanaka. Binding signatures for generic contexts. In Proc. TLCA 2005, volume 308--323, 2005.
[41]
M. Rennela. Towards a quantum domain theory: Order-enrichment and fixpoints in W*-algebras. In Proc. MFPS XXX, 2014.
[42]
P. Selinger. Towards a quantum programming language. Mathematical Structures in Computer Science, 14(4):527--586, 2004.
[43]
P. Selinger. Generators and relations for n-qubit Clifford operators. arXiv:1310.6813, 2013.
[44]
I. Stark. Categorical models for local names. LISP and Symb. Comp., 9(1):77--107, 1996.
[45]
S. Staton. An algebraic presentation of predicate logic. In FOSSACS 2013.
[46]
S. Staton. Completeness for algebraic theories of local state. In FOSSACS 2010.
[47]
S. Staton. Instances of computational effects. In LICS 2013.
[48]
S. Staton. Two cotensors in one. In Proc. MFPS XXV, 2009.
[49]
S. Staton. Freyd categories are enriched lawvere theories. In Proc. Workshop on Algebra, Coalgebra and Topology, volume 303 of ENTCS, pages 197--206, 2013.
[50]
S. Staton and P. B. Levy. Universal properties for impure programming languages. In POPL 2013, 2013.
[51]
A. van Tonder. A lambda calculus for quantum computation. SIAM J. Comput., 33(5):1109--1135, 2004.
[52]
J. Vicary. Higher semantics of quantum protocols. In LICS 2012.
[53]
J. K. Vizzotto, G. R. Librelotto, and A. Sabry. Reasoning about general quantum programs over mixed states. In SBMF 2009, 2009.
[54]
M. Ying and Y. Feng. An algebraic language for distributed quantum computing. IEEE Trans. Computers, 58(6):728--743, 2009.
[55]
M. Ying, N. Yu, and Y. Feng. Alternation in quantum programming: from superposition of data to superposition of programs. arXiv:1402.5172, 2014.

Cited By

View all
  • (2024)How to Bake a Quantum ΠProceedings of the ACM on Programming Languages10.1145/36746258:ICFP(1-29)Online publication date: 15-Aug-2024
  • (2024)Algebraic Effects Meet Hoare Logic in Cubical AgdaProceedings of the ACM on Programming Languages10.1145/36328988:POPL(1663-1695)Online publication date: 5-Jan-2024
  • (2024)With a Few Square Roots, Quantum Computing Is as Easy as PiProceedings of the ACM on Programming Languages10.1145/36328618:POPL(546-574)Online publication date: 5-Jan-2024
  • Show More Cited By

Recommendations

Comments

Information & Contributors

Information

Published In

cover image ACM Conferences
POPL '15: Proceedings of the 42nd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages
January 2015
716 pages
ISBN:9781450333009
DOI:10.1145/2676726
  • cover image ACM SIGPLAN Notices
    ACM SIGPLAN Notices  Volume 50, Issue 1
    POPL '15
    January 2015
    682 pages
    ISSN:0362-1340
    EISSN:1558-1160
    DOI:10.1145/2775051
    • Editor:
    • Andy Gill
    Issue’s Table of Contents
Permission to make digital or hard copies of all or part of this work for personal or classroom use is granted without fee provided that copies are not made or distributed for profit or commercial advantage and that copies bear this notice and the full citation on the first page. Copyrights for components of this work owned by others than the author(s) must be honored. Abstracting with credit is permitted. To copy otherwise, or republish, to post on servers or to redistribute to lists, requires prior specific permission and/or a fee. Request permissions from [email protected].

Sponsors

In-Cooperation

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 14 January 2015

Permissions

Request permissions for this article.

Check for updates

Author Tags

  1. algebraic effects
  2. monads.
  3. quantum computation

Qualifiers

  • Research-article

Funding Sources

Conference

POPL '15
Sponsor:

Acceptance Rates

POPL '15 Paper Acceptance Rate 52 of 227 submissions, 23%;
Overall Acceptance Rate 860 of 4,328 submissions, 20%

Upcoming Conference

POPL '26

Contributors

Other Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

  • Downloads (Last 12 months)66
  • Downloads (Last 6 weeks)4
Reflects downloads up to 19 Feb 2025

Other Metrics

Citations

Cited By

View all
  • (2024)How to Bake a Quantum ΠProceedings of the ACM on Programming Languages10.1145/36746258:ICFP(1-29)Online publication date: 15-Aug-2024
  • (2024)Algebraic Effects Meet Hoare Logic in Cubical AgdaProceedings of the ACM on Programming Languages10.1145/36328988:POPL(1663-1695)Online publication date: 5-Jan-2024
  • (2024)With a Few Square Roots, Quantum Computing Is as Easy as PiProceedings of the ACM on Programming Languages10.1145/36328618:POPL(546-574)Online publication date: 5-Jan-2024
  • (2024)Enriched Presheaf Model of Quantum FPCProceedings of the ACM on Programming Languages10.1145/36328558:POPL(362-392)Online publication date: 5-Jan-2024
  • (2024)Scoped Effects as Parameterized Algebraic TheoriesProgramming Languages and Systems10.1007/978-3-031-57262-3_1(3-21)Online publication date: 5-Apr-2024
  • (2022)Algebraic reasoning of Quantum programs via non-idempotent Kleene algebraProceedings of the 43rd ACM SIGPLAN International Conference on Programming Language Design and Implementation10.1145/3519939.3523713(657-670)Online publication date: 9-Jun-2022
  • (2019)Universal Properties in Quantum TheoryElectronic Proceedings in Theoretical Computer Science10.4204/EPTCS.287.12287(213-223)Online publication date: 31-Jan-2019
  • (2019)Quantum channels as a categorical completion2019 34th Annual ACM/IEEE Symposium on Logic in Computer Science (LICS)10.1109/LICS.2019.8785700(1-13)Online publication date: Jun-2019
  • (2019)How to prove decidability of equational theories with second-order computation analyser SOLJournal of Functional Programming10.1017/S095679681900015729Online publication date: 24-Dec-2019
  • (2017)How to prove your calculus is decidable: practical applications of second-order algebraic theories and computationProceedings of the ACM on Programming Languages10.1145/31102661:ICFP(1-28)Online publication date: 29-Aug-2017
  • Show More Cited By

View Options

Login options

View options

PDF

View or Download as a PDF file.

PDF

eReader

View online with eReader.

eReader

Figures

Tables

Media

Share

Share

Share this Publication link

Share on social media