More Web Proxy on the site http://driver.im/

research-article

Open access

A computational interpretation of compact closed categories: reversible programming with negative and fractional types

Authors:

Chao-Hong Chen,

Amr SabryAuthors Info & Claims

Proceedings of the ACM on Programming Languages, Volume 5, Issue POPL

Article No.: 9, Pages 1 - 29

https://doi.org/10.1145/3434290

Published: 04 January 2021 Publication History

Abstract

Compact closed categories include objects representing higher-order functions and are well-established as models of linear logic, concurrency, and quantum computing. We show that it is possible to construct such compact closed categories for conventional sum and product types by defining a dual to sum types, a negative type, and a dual to product types, a fractional type. Inspired by the categorical semantics, we define a sound operational semantics for negative and fractional types in which a negative type represents a computational effect that ``reverses execution flow'' and a fractional type represents a computational effect that ``garbage collects'' particular values or throws exceptions.

Specifically, we extend a first-order reversible language of type isomorphisms with negative and fractional types, specify an operational semantics for each extension, and prove that each extension forms a compact closed category. We furthermore show that both operational semantics can be merged using the standard combination of backtracking and exceptions resulting in a smooth interoperability of negative and fractional types. We illustrate the expressiveness of this combination by writing a reversible SAT solver that uses backtracking search along freshly allocated and de-allocated locations. The operational semantics, most of its meta-theoretic properties, and all examples are formalized in a supplementary Agda package.

References

[1]

Samson Abramsky. 2005. A structural approach to reversible computatTheoior. nC. omput. Sci. 347 ( December 2005 ), 441-464. Issue 3.

[2]

S. Abramsky and B. Coecke. 2004. A categorical semantics of quantum protocoPlrso. cIenedings of the 19th Annual IEEE Symposium on Logic in Computer Science, 200441. 5-425.

[3]

Samson Abramsky, Simon Gay, and Rajagopal Nagarajan. 1996. Interaction Categories and the Foundations of Typed Concurrent Programming. InProceedings of the NATO Advanced Study Institute on Deductive Program De (Msiganrktoberdorf, Germany). Springer-Verlag, Berlin, Heidelberg, 35-113.

[4]

S. Abramsky, E. Haghverdi, and P. Scot. 2002. Geometry of interaction and linear combinatory algeMbaraths. ematical Structures in Computer Scienc1e2, 5 ( 2002 ).

[5]

Samson Abramsky and Radha Jagadeesan. 1994. New foundations for the geometry of interInacf.tCionm.put. 111 (May 1994 ), 53-119. Issue 1.

[6]

Bogdan Aman, Gabriel Ciobanu, Robert Glück, Robin Kaarsgaard, Jarkko Kari, Martin Kutrib, Ivan Lanese, Claudio Antares Mezzina, Łukasz Mikulski, Rajagopal Nagarajan, Iain Phillips, G. Michele Pinna, Luca Prigioniero, Irek Ulidowski, and Germán Vidal. 2020. Foundations of Reversible Computati.onSpringer International Publishing, Cham, 1-4h0.ttps: //doi.org/10.1007/978-3-030-47361-7_1

[7]

Zena M. Ariola, Hugo Herbelin, and Amr Sabry. 2009. A type-theoretic foundation of delimited continHuiaghteiorns. Order Symbol. Comput. 22 ( September 2009 ), 233-273. Issue 3.

[8]

Jean Bénabou. 1963. Catégories avec multiplicatCi o.nR. de l' Académie des Sciences de Paris256, 9 ( 1963 ), 1887-1890.

[9]

Jean Bénabou. 1964. Algèbre élémentaire dans les catégories avec multipliCca. Rt.ioAnc.ad. Sci. Paris258, 9 ( 1964 ), 771-774.

[10]

C. H. Bennet. 1973. Logical reversibility of computatioIBnM. J. Res. Dev. 17 (November 1973 ), 525-532. Issue 6.

[11]

Charles H. Bennet. 1989. Time/Space Trade-Ofs for Reversible Computation. SIAM J. Comput.18, 4 ( 1989 ), 766-776. https://doi.org/10.1137/0218053

Digital Library

[12]

A. Blass. 1995. Seven trees in oneJo. urnal of Pure and Applied Algebra103, 1-21 ( 1995 ).

[13]

William J. Bowman, Roshan P. James, and Amr Sabry. 2011. Dagger Traced Symmetric Monoidal Categories and Reversible Programming. InRC 2011.

[14]

Jacques Carete and Amr Sabry. 2016. Computing with Semirings and Weak Rig Groupoids. EInSOP (Lecture Notes in Computer Science, Vol. 9632.)Springer, 123-148.

[15]

Siu Man Chan. 2013P.ebble Games and Complexit y.Ph.D. Dissertation. EECS Department, University of California, Berkeley. http://www2.eecs.berkeley.edu/Pubs/TechRpts/2013/EECS-2013-145.html

[16]

Chao-Hong Chen, Vikraman Choudhury, Jacques Carete, and Amr Sabry. 2020. Fractional TypeRs.eIvnersible Computatio, n Ivan Lanese and Mariusz Rawski (Eds.). Springer International Publishing, Cham, 169-186.

[17]

Stephen Clark, Bob Coecke, and Mehrnoosh Sadrzadeh. 2008. A Compositional Distributional Model of MPreoacneeind-g. ings of the Second Symposium on Quantum Interaction (QI-2008 () 2008 ), 133-140.

[18]

Tristan Crolard. 2001. Subtractive lo gTheiocr. etical Computer Science 254, 1-2 ( 2001 ), 151-185. https://doi.org/10.1016/ S0304-3975 ( 99 ) 00124-3

Digital Library

[19]

Tristan Crolard. 2004. A Formulae-as-Types Interpretation of Subtractive JLoougrinca. l of Logic and Computatio1n4, 4 ( 2004 ), 529-570.

[20]

Pierre-Louis Curien and Hugo Herbelin. 2000. The Duality of Computation.PIrnoceedings of the Fifth ACM SIGPLAN International Conference on Functional Programming (ICFP. 'A0s0s)ociation for Computing Machinery, New York, NY, USA, 233-243. https://doi.org/10.1145/351240.351262

Digital Library

[21]

Andrzej Filinski. 1989. Declarative Continuations: an Investigation of Duality in Programming Language Semantics. In Category Theory and Computer Science.

[22]

Andrzej Filinski. 1992. Linear ContinuationsP.rIonceedings of the 19th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages(Albuquerque, New Mexico, USA() POPL '92). Association for Computing Machinery, New York, NY, USA, 27-38. https://doi.org/10.1145/143165.143174

Digital Library

[23]

Marcelo Fiore. 2004. Isomorphisms of Generic Recursive Polynomial Types. PrInoceedings of the 31st ACM SIGPLANSIGACT Symposium on Principles of Programming Language(sVenice, Italy()POPL '04). Association for Computing Machinery, New York, NY, USA, 77-88. https://doi.org/10.1145/964001.964008

Digital Library

[24]

Marcelo Fiore. 2015. An Axiomatics and a Combinatorial Model of Creation/Annihilation Operatoras. rX(2i0v1:155). 06. 06402[math.CT].

[25]

M. P. Fiore, R. Di Cosmo, and V. Balat. 2006. Remarks on Isomorphisms in Typed Calculi with Empty and Sum Types. Annals of Pure and Applied Logic141, 1-2 ( 2006 ), 35-50.

[26]

E. Fredkin and T. Tofoli. 1982. Conservative logiIcn. ternational Journal of Theoretical Physics21, 3 ( 1982 ), 219-253.

[27]

J.Y. Girard. 1989. Geometry of interaction 1: Interpretation of SystSteumdFie.s in Logic and the Foundations of Mathematics 127 ( 1989 ), 221-260.

[28]

Robert Glück and Robin Kaarsgaard. 2018. A Categorical Foundation for Structured Reversible Flowchart Languages. Electronic Notes in Theoretical Computer Scienc3e36 ( 2018 ), 155-171. https://doi.org/10.1016/j.entcs. 2018. 03. 02The1 hTirty-third Conference on the Mathematical Foundations of Programming Semantics (MFPS XXXIII).

[29]

Alexander S. Green, Peter LeFanu Lumsdaine, Neil J. Ross, Peter Selinger, and Benoît Valiron. 2013. Quipper: A Scalable uQantum Programming Language. In Proceedings of the 34th ACM SIGPLAN Conference on Programming Language Design and Implementation (Seatle, Washington, USA)( PLDI '13). ACM, New York, NY, USA, 333-342.

[30]

Chris Heunen, Robin Kaarsgaard, and Marti Karvonen. 2018. Reversible Efects as Inverse ArrowEsl. ectronic Notes in hTeoretical Computer Science 341 ( 2018 ), 179-199. https://doi.org/10.1016/j.entcs. 2018. 11. 00P9roceedings of the ThirtyFourth Conference on the Mathematical Foundations of Programming Semantics (MFPS XXXIV).

[31]

Chris Heunen and Marti Karvonen. 2015. Reversible Monadic ComputinEgle. ctronic Notes in Theoretical Computer Science 319 ( 2015 ), 217-237. https://doi.org/10.1016/j.entcs. 2015. 12. 01The431st Conference on the Mathematical Foundations of Programming Semantics (MFPS XXXI).

[32]

Christiaan Heunen and Jamie Vicary. 201C9a. tegories for quantum theory: an introduct.iOoxnford University Press, United Kingdom.

[33]

Furio Honsell and Marina Lenisa. 2004. “ Wave-Style” Geometry of Interaction Models in Rel Are Graph-Like LambdaModels. InTypes for Proofs and Program,sStefano Berardi, Mario Coppo, and Ferruccio Damiani (Eds.). Springer Berlin Heidelberg, Berlin, Heidelberg, 242-258.

[34]

Jason Z.S. Hu and Jacques Carete. 2020. Proof-relevant Category Theory in Agda. (2020h).ttps://arxiv.org/abs/ 2005.0705.9

[35]

Roshan P. James and Amr Sabry. 2012a. Information Efects. IPnroceedings of the 39th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Language(sPhiladelphia, PA, USA() POPL '12). Association for Computing Machinery, New York, NY, USA, 73-84. https://doi.org/10.1145/2103656.2103667

Digital Library

[36]

Roshan P. James and Amr Sabry. 2012b. The Two Dualities of Computation : Negative and Fractional Typ. esTechnical Report. Indiana University.

[37]

Roshan P James and Amr Sabry. 2014. Theseus: A high level language for reversible computingW. Ionrk-in-progress report in the Conference on Reversible Computat.ion

[38]

Roshan P James, Zachary Sparks, Jacques Carete, and Amr Sabry. 2013. Fractional types. ( 2013 ).

[39]

A. Joyal, R. Street, and D. Verity. 1996. Traced monoidal categorieMsa. tInhematical Proceedings of the Cambridge Philosophical Societ.yCambridge Univ Press.

[40]

Robin Kaarsgaard and Niccolò Veltri. 2019. En Garde! Unguarded Iteration for Reversible Computation in the Delay Monad. Lecture Notes in Computer Scien(c2e019), 366-384. https://doi.org/10.1007/978-3-030-33636-3_13

[41]

J. Kastl. 1979. Inverse CategorieSst.udien zur Algebra und ihre Anwendungen7 ( 1979 ), 51-60.

[42]

G.M. Kelly and M.L. Laplaza. 1980. Coherence for compact closed categJooruiersn. al of Pure and Applied Algebra19 ( 1980 ), 193-213. https://doi.org/10.1016/ 0022-4049 ( 80 ) 90101-2

[43]

G Maxwell Kelly. 1972. Many-variable functorial calculuCs. oIh. eIrnence in categorie.sSpringer, 66-105.

[44]

Miguel L. Laplaza. 1972. Coherence for distributivityC.oIhnerence in Categorie,sG.M. Kelly, M. Laplaza, G. Lewis, and Saunders Mac Lane (Eds.). Lecture Notes in Mathematics, Vol. 281. Springer Verlag, Berlin, 29-65.

[45]

D. Loeb. 1992. Sets with a negative number of elemenAtdsv.ances in Mathematic9s1, 1 ( 1992 ), 64-74.

[46]

Ian Mackie. 1995. The Geometry of Interaction Machine. IPnroceedings of the 22nd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages(San Francisco, California, US(AP)OPL '95). Association for Computing Machinery, New York, NY, USA, 198-208. https://doi.org/10.1145/199448.199483

Digital Library

[47]

Ian Mackie. 2011. Reversible Higher-order ComputationsW.Ionrkshop on Reversible Computati o.n

[48]

Saunders MacLane. 1963. Natural associativity and commutatRiivcietyIn.stitute Pamphlet-Rice University Stud4ie9s, 4 ( 1963 ).

[49]

Jonathan Oppenheim, Robert W Spekkens, and Andreas Winter. 2005. A classical analogue of negative infoarmXiavtion. preprint quant-ph/0511247 ( 2005 ).

[50]

P. Panangaden and É.O. Paquete. 2011. A Categorical Presentation of Quantum Computation with Anyo. nSspringer Berlin Heidelberg, Berlin, Heidelberg, 983-1025.

[51]

R Penrose. 1971. Applications of negative dimensional tensoCros. mInbinatorial Mathematics and its Applicati.oAncsademic Press.

[52]

James Propp. 2002. Euler measure as generalized cardinality. (200a2r)X.iv:math/0203289[math.CO].

[53]

Cecylia Rauszer. 1974a. A formalization of the propositional calculus of H-SBtuldoigaicL. ogica33 ( 1974 ), 23-34. Issue 1.

[54]

C. Rauszer. 1974b. Semi-boolean algebras and their applications to intuitionistic logic with dualFoupnedraamtoenrst. a Mathematicae83 ( 1974 ), 219-249.

[55]

C. Rauszer. 1980. An algebraic and Kripke-style approach to a certain extension of intuitionisticDliossgeirct. atIniones Mathmatica.eVol. 167. Institut Mathématique de l' Académie Polonaise des Sciences.

[56]

Udday S. Reddy. 1991. Acceptors as values: Functional programming in classical linear logic. (Dec. 1991 ). Manuscript.

[57]

Lídia del Rio, Johan Åberg, Renato Renner, Oscar Dahlsten, and Vlatko Vedral. 2011. The thermodynamic meaning of negative entropyN. ature474, 7349 ( 2011 ), 61-63. https://doi.org/10.1038/nature10123

[58]

Amr Sabry, Benoît Valiron, and Juliana Kaizer Vizzoto. 2018. From Symmetric Patern-Matching to Quantum Control. In Foundations of Software Science and Computation Struct,uCrehsristel Baier and Ugo Dal Lago (Eds.). Springer International Publishing, Cham, 348-364.

[59]

Stephen H. Schanuel. 1991. Negative sets have Euler characteristic and dimenCsiaotneg. oInry Theory, Aurelio Carboni, Maria Cristina Pedicchio, and Guiseppe Rosolini (Eds.). Springer Berlin Heidelberg, Berlin, Heidelberg, 379-385.

[60]

Peter Selinger. 2001. Control categories and duality: on the categorical semantics of the lambda-mMuatchaelmcualtuicsa.l. Structures in Comp. Sc1i.1 (April 2001 ), 207-260. Issue 2.

[61]

Peter Selinger. 2011. A Survey of Graphical Languages for Monoidal CategorNiews. SIntructures for Physic, sBob Coecke (Ed.). Lecture Notes in Physics, Vol. 813. Springer Berlin / Heidelberg, 289-355.

[62]

Zachary Sparks and Amr Sabry. 2014. Superstructural Reversible Logic3.rdInInternational Workshop on Linear.ity

[63]

Michael Kirkedal Thomsen, Robin Kaarsgaard, and Mathias Soeken. 2015. Ricercar: A Language for Describing and Rewriting Reversible Circuits with Ancillae and Its Permutation SemaRnetviecrss.iIbnle Computatio,nJean Krivine and Jean-Bernard Stefani (Eds.). Springer International Publishing, Cham, 200-215.

[64]

Tommaso Tofoli. 1980. Reversible Computing. InProceedings of the 7th Colloquium on Automata, Languages and Programming. Springer-Verlag, 632-644.

[65]

Philip Wadler. 2003. Call-by-value is dual to call-by-naImCeF.PIn'03: Proceedings of the eighth ACM SIGPLAN international conference on Functional programmi(nUgppsala, Sweden). ACM, New York, NY, USA, 189-201.https://doi.org/10.1145/ 944705.944723

Digital Library

[66]

Philip Wadler. 2005. Call-by-Value Is Dual to Call-by-Name-ReloadTeedrm.InRewriting and Applicatio n,sJürgen Giesl (Ed.). Springer Berlin Heidelberg, Berlin, Heidelberg, 185-203.

[67]

Tetsuo Yokoyama, Holger Bock Axelsen, and Robert Glück. 2016. Fundamentals of reversible flowchart lanThegou-ages. retical Computer Scienc6e11 ( 2016 ), 87-115. https://doi.org/10.1016/j.tcs. 2015. 07.046

Digital Library

[68]

Tetsuo Yokoyama and Robert Glück. 2007. A reversible programming language and its invertible self-interPpErePtMer. In (Nice, France). ACM, 144-153.

Cited By

Carette JHeunen CKaarsgaard RSabry A(2024)How to Bake a Quantum ΠProceedings of the ACM on Programming Languages10.1145/36746258:ICFP(1-29)Online publication date: 15-Aug-2024
https://dl.acm.org/doi/10.1145/3674625
MATSUDA KWANG M(2024) Sparcl : A language for partially invertible computation Journal of Functional Programming10.1017/S095679682300012634Online publication date: 26-Jan-2024
https://doi.org/10.1017/S0956796823000126
Ågren Thuné AMatsuda KWang M(2024)Reconciling Partial and Local InvertibilityProgramming Languages and Systems10.1007/978-3-031-57267-8_3(59-89)Online publication date: 6-Apr-2024
https://dl.acm.org/doi/10.1007/978-3-031-57267-8_3
Show More Cited By

Index Terms

A computational interpretation of compact closed categories: reversible programming with negative and fractional types
1. Theory of computation

Recommendations

Symmetries in reversible programming: from symmetric rig groupoids to reversible programming languages

The Pi family of reversible programming languages for boolean circuits is presented as a syntax of combinators witnessing type isomorphisms of algebraic data types. In this paper, we give a denotational semantics for this language, using weak groupoids à ...
The Interpretation of Intuitionistic Type Theory in Locally Cartesian Closed Categories -- an Intuitionistic Perspective

We give an intuitionistic view of Seely's interpretation of Martin-Lof's intuitionistic type theory in locally cartesian closed categories. The idea is to use Martin-Lof type theory itself as metalanguage, and E-categories, the appropriate notion of ...
Closed Types for Logic Programming

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image Proceedings of the ACM on Programming Languages

Proceedings of the ACM on Programming Languages Volume 5, Issue POPL

January 2021

1789 pages

EISSN:2475-1421

DOI:10.1145/3445980

Issue’s Table of Contents

Copyright © 2021 Owner/Author.

This work is licensed under a Creative Commons Attribution International 4.0 License.

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 04 January 2021

Published in PACMPL Volume 5, Issue POPL

Permissions

Request permissions for this article.

Request Permissions

Check for updates

Badges

Author Tags

Qualifiers

Research-article

Funding Sources

NSF (National Science Foundation)

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

6
Total Citations
View Citations
1,716
Total Downloads

Downloads (Last 12 months)251
Downloads (Last 6 weeks)24

Reflects downloads up to 13 Dec 2024

Other Metrics

View Author Metrics

Citations

Cited By

Carette JHeunen CKaarsgaard RSabry A(2024)How to Bake a Quantum ΠProceedings of the ACM on Programming Languages10.1145/36746258:ICFP(1-29)Online publication date: 15-Aug-2024
https://dl.acm.org/doi/10.1145/3674625
MATSUDA KWANG M(2024) Sparcl : A language for partially invertible computation Journal of Functional Programming10.1017/S095679682300012634Online publication date: 26-Jan-2024
https://doi.org/10.1017/S0956796823000126
Ågren Thuné AMatsuda KWang M(2024)Reconciling Partial and Local InvertibilityProgramming Languages and Systems10.1007/978-3-031-57267-8_3(59-89)Online publication date: 6-Apr-2024
https://dl.acm.org/doi/10.1007/978-3-031-57267-8_3
Matsuda KFrohlich SWang MWu N(2023)Embedding by UnembeddingProceedings of the ACM on Programming Languages10.1145/36078307:ICFP(1-47)Online publication date: 30-Aug-2023
https://dl.acm.org/doi/10.1145/3607830
Choudhury VKarwowski JSabry A(2022)Symmetries in reversible programming: from symmetric rig groupoids to reversible programming languagesProceedings of the ACM on Programming Languages10.1145/34986676:POPL(1-32)Online publication date: 12-Jan-2022
https://dl.acm.org/doi/10.1145/3498667
Heunen CKaarsgaard R(2022)Quantum information effectsProceedings of the ACM on Programming Languages10.1145/34986636:POPL(1-27)Online publication date: 12-Jan-2022
https://dl.acm.org/doi/10.1145/3498663

View Options

View options

PDF

View or Download as a PDF file.

eReader

View online with eReader.

Login options

Check if you have access through your login credentials or your institution to get full access on this article.

Full Access

Get this Article

Media

Figures

Other

Tables

View Issue’s Table of Contents