skip to main content
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
  • (2025)Algebraic language for the efficient representation and optimization of quantum circuitsPhysica Scripta10.1088/1402-4896/ad9fb6100:2(025107)Online publication date: 13-Jan-2025
  • (2025)Formalization of Quantum Intermediate Representations for code safetyJournal of Systems and Software10.1016/j.jss.2024.112236219:COnline publication date: 1-Jan-2025
  • (2023)Deconstructing the Calculus of Relations with Tape DiagramsProceedings of the ACM on Programming Languages10.1145/35712577:POPL(1864-1894)Online publication date: 9-Jan-2023
  • Show More Cited By

Recommendations

Comments

Information & Contributors

Information

Published In

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
  • 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
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].

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 14 January 2015
Published in SIGPLAN Volume 50, Issue 1

Check for updates

Author Tags

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

Qualifiers

  • Research-article

Funding Sources

Contributors

Other Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

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

Other Metrics

Citations

Cited By

View all
  • (2025)Algebraic language for the efficient representation and optimization of quantum circuitsPhysica Scripta10.1088/1402-4896/ad9fb6100:2(025107)Online publication date: 13-Jan-2025
  • (2025)Formalization of Quantum Intermediate Representations for code safetyJournal of Systems and Software10.1016/j.jss.2024.112236219:COnline publication date: 1-Jan-2025
  • (2023)Deconstructing the Calculus of Relations with Tape DiagramsProceedings of the ACM on Programming Languages10.1145/35712577:POPL(1864-1894)Online publication date: 9-Jan-2023
  • (2021)Quantum computing: A taxonomy, systematic review and future directionsSoftware: Practice and Experience10.1002/spe.303952:1(66-114)Online publication date: 7-Oct-2021
  • (2020)Theory and Practice of Second-Order Rewriting: Foundation, Evolution, and SOLFunctional and Logic Programming10.1007/978-3-030-59025-3_1(3-9)Online publication date: 2-Sep-2020
  • (2019)Quantum channels as a categorical completionProceedings of the 34th Annual ACM/IEEE Symposium on Logic in Computer Science10.5555/3470152.3470187(1-13)Online publication date: 24-Jun-2019
  • (2018)Polymorphic Rewrite Rules: Confluence, Type Inference, and Instance ValidationFunctional and Logic Programming10.1007/978-3-319-90686-7_7(99-115)Online publication date: 24-Apr-2018
  • (2017)Paschke DilationsElectronic Proceedings in Theoretical Computer Science10.4204/EPTCS.236.15236(229-244)Online publication date: 1-Jan-2017
  • (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
  • 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