research-article

Species, Profunctors and Taylor Expansion Weighted by SMCC: A Unified Framework for Modelling Nondeterministic, Probabilistic and Quantum Programs

Authors:

Takeshi Tsukada,

Kazuyuki Asada,

C.-H. Luke OngAuthors Info & Claims

LICS '18: Proceedings of the 33rd Annual ACM/IEEE Symposium on Logic in Computer Science

Pages 889 - 898

https://doi.org/10.1145/3209108.3209157

Published: 09 July 2018 Publication History

Abstract

Motivated by a tight connection between Joyal's combinatorial species and quantitative models of linear logic, this paper introduces weighted generalised species (or weighted profunctors), where weights are morphisms of a given symmetric monoidal closed category (SMCC). For each SMCC W, we show that the category of W-weighted profunctors is a Lafont category, a categorical model of linear logic with exponential. As a model of programming languages, the construction of this paper gives a unified framework that induces adequate models of nondeterministic, probabilistic, algebraic and quantum programming languages by an appropriate choice of the weight SMCC.

References

[1]

Samson Abramsky, Radha Jagadeesan, and Pasquale Malacaria. 2000. Full Abstraction for PCF. Information and Computation 163, 2 (2000), 409--470.

Digital Library

[2]

Jean Bénabou. 1967. Introduction to bicategories. Springer Berlin Heidelberg, Berlin, Heidelberg, 1--77.

[3]

Jean Bénabou. 2000. Distributors at work. (2000). Course notes, TU Darmstadt.

[4]

François Bergeron, Gilbert Labelle, and Pierre Leroux. 1997. Combinatorial Species and Tree-like Structures. Cambridge Univ. Press.

[5]

Vincent Danos and Thomas Ehrhard. 2011. Probabilistic coherence spaces as a model of higher-order probabilistic computation. Inf. Comput. 209, 6 (2011), 966--991.

Digital Library

[6]

Thomas Ehrhard and Laurent Regnier. 2008. Uniformity and the Taylor expansion of ordinary lambda-terms. Theor. Comput. Sci. 403, 2-3 (2008), 347--372.

Digital Library

[7]

Thomas Ehrhard, Christine Tasson, and Michele Pagani. 2014. Probabilistic coherence spaces are fully abstract for probabilistic PCF. In POPL (2014). 309--320.

Digital Library

[8]

Marcelo P. Fiore. 2005. Mathematical Models of Computational and Combinatorial Structures. In FoSSaCS (2005). 25--46.

Digital Library

[9]

Marcelo P. Fiore, Nicola Gambino, J. Martin E. Hyland, and Glynn Winskel. 2007. The cartesian closed bicategory of generalised species of structures. J. London Maths. Soc. 77 (2007), 203--220.

[10]

Jean-Yves Girard. 1988. Normal functors, power series and λ-calculus. Ann. Pure Appl. Logic 37, 2 (1988), 129--177.

[11]

Esfandiar Haghverdi. 2001. Partially Additive Categories and Fully Complete Models of Linear Logic. In TLCA (2001). 197--216.

Digital Library

[12]

Esfandiar Haghverdi and Philip J. Scott. 2006. A categorical model for the geometry of interaction. Theor. Comput. Sci. 350, 2-3 (2006), 252--274.

Digital Library

[13]

Russell Harmer and Guy McCusker. 1999. A fully abstract game semantics for finite nondeterminism. In LICS (1999). 422--430.

Digital Library

[14]

Ryu Hasegawa. 2002. Two applications of analytic functors. Theor. Comput. Sci. 272, 1-2 (2002), 113--175.

Digital Library

[15]

Naohiko Hoshino. 2012. A Representation Theorem for Unique Decomposition Categories. Electr. Notes Theor. Comput. Sci. 286 (2012), 213--227.

Digital Library

[16]

J. M. E. Hyland and C.-H. Luke Ong. 2000. On Full Abstraction for PCF: I, II, and III. Information and Computation 163, 2 (2000), 285--408.

Digital Library

[17]

Andre Joyal. 1981. Une théorie combinatoire des séries formelles. Adv. Math. 42 (1981), 1--82.

[18]

Andre Joyal. 1986. Foncteurs analytiques et espèces de structures. In Combinatoire Énumérative. Lecture Notes in Mathematics, Vol. 1234. Springer, Berlin, 126--159.

[19]

James Laird. 2016. Fixed points in quantitative semantics. In LICS (2016). 347--356.

Digital Library

[20]

James Laird. 2017. From Qualitative to Quantitative Semantics - By Change of Base. In FoSSaCS (2017). 36--52.

Digital Library

[21]

Jim Laird, Giulio Manzonetto, Guy McCusker, and Michele Pagani. 2013. Weighted Relational Models of Typed Lambda-Calculi. In LICS (2013). 301--310.

Digital Library

[22]

François Lamarche. 1992. Quantitative Domains and Infinitary Algebras. Theor. Comput. Sci. 94, 1 (1992), 37--62.

Digital Library

[23]

R. B. B. Lucyshyn-Wright. 2016. Relative symmetric monoidal closed categories I: Autoenrichment and change of base. Theory and Applications of Categories 31 (2016), 138--174.

[24]

Damiano Mazza, Luc Pellissier, and Pierre Vial. 2018. Polyadic approximations, fibrations and intersection types. PACMPL 2, POPL (2018), 6:1--6:28.

Digital Library

[25]

Paul-André Melliès. 2003. Asynchronous games 1: Uniformity by group invariance. (2003). unpublished manuscript.

[26]

Paul-André Melliès. 2009. Categorical Semantics of Linear Logic. 1--196 pages.

[27]

Paul-André Melliès, Nicolas Tabareau, and Christine Tasson. 2009. An Explicit Formula for the Free Exponential Modality of Linear Logic. In ICALP (2009). 247--260.

Digital Library

[28]

Michele Pagani, Peter Selinger, and Benoît Valiron. 2014. Applying quantitative semantics to higher-order quantum computing. In POPL (2014). 647--658.

Digital Library

[29]

Luc Pellissier. 2017. Réduction et Approximation Linéaires. Ph.D. Dissertation. Université Paris 13.

[30]

Peter Selinger. 2004. Towards a quantum programming language. Mathematical Structures in Computer Science 14, 4 (2004), 56.

Digital Library

[31]

Peter Selinger and Benoît Valiron. 2008. On a Fully Abstract Model for a Quantum Linear Functional Language. Electronic Notes in Theoretical Computer Science 210, (2008), 123--137.

Digital Library

[32]

Takeshi Tsukada, Kazuyuki Asada, and C.-H. Luke Ong. 2017. Generalised species of rigid resource terms. In LICS (2017). 1--12.

[33]

Takeshi Tsukada and C.-H. Luke Ong. 2015. Nondeterminism in Game Semantics via Sheaves. In LICS (2015). 220--231

Digital Library

[34]

Lionel Vaux. 2009. The algebraic lambda calculus. Mathematical Structures in Computer Science 19, 5 (2009), 1029--1059.

Digital Library

Cited By

Tsukada TAsada K(2024)Enriched Presheaf Model of Quantum FPCProceedings of the ACM on Programming Languages10.1145/36328558:POPL(362-392)Online publication date: 5-Jan-2024
https://dl.acm.org/doi/10.1145/3632855
Paquet HSaville P(2023)Effectful Semantics in 2-Dimensional Categories: Premonoidal and Freyd BicategoriesElectronic Proceedings in Theoretical Computer Science10.4204/EPTCS.397.12397(190-209)Online publication date: 14-Dec-2023
https://doi.org/10.4204/EPTCS.397.12
Kerinec AManzonetto GOlimpieri F(2023)Why Are Proofs Relevant in Proof-Relevant Models?Proceedings of the ACM on Programming Languages10.1145/35712017:POPL(218-248)Online publication date: 11-Jan-2023
https://dl.acm.org/doi/10.1145/3571201
Show More Cited By

Index Terms

Species, Profunctors and Taylor Expansion Weighted by SMCC: A Unified Framework for Modelling Nondeterministic, Probabilistic and Quantum Programs
1. Theory of computation
  1. Logic
    1. Linear logic
  2. Semantics and reasoning
    1. Program semantics
      1. Denotational semantics

Recommendations

Derived Profunctors
Categorifying Computations into Components via Arrows as Profunctors

The notion of arrow by Hughes is an axiomatization of the algebraic structure possessed by structured computations in general. We claim that an arrow also serves as a basic component calculus for composing state-based systems as components-in fact, it ...
Profunctors, open maps and bisimulation

This paper studies fundamental connections between profunctors (that is, distributors, or bimodules), open maps and bisimulation. In particular, it proves that a colimit preserving functor between presheaf categories (corresponding to a profunctor) ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image ACM Conferences

LICS '18: Proceedings of the 33rd Annual ACM/IEEE Symposium on Logic in Computer Science

July 2018

960 pages

ISBN:9781450355834

DOI:10.1145/3209108

Copyright © 2018 ACM.

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 ACM 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

SIGLOG: ACM Special Interest Group on Logic and Computation
EACSL: European Association for Computer Science Logic
IEEE-CS\DATC: IEEE Computer Society

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 09 July 2018

Permissions

Request permissions for this article.

Request Permissions

Check for updates

Author Tags

Qualifiers

Research-article
Research
Refereed limited

Funding Sources

Conference

LICS '18

Sponsor:

SIGLOG
EACSL
IEEE-CS\DATC

LICS '18: 33rd Annual ACM/IEEE Symposium on Logic in Computer Science

July 9 - 12, 2018

Oxford, United Kingdom

Acceptance Rates

Overall Acceptance Rate 215 of 622 submissions, 35%

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

10
Total Citations
View Citations
177
Total Downloads

Downloads (Last 12 months)20
Downloads (Last 6 weeks)5

Reflects downloads up to 13 Nov 2024

Other Metrics

View Author Metrics

Citations

Cited By

Tsukada TAsada K(2024)Enriched Presheaf Model of Quantum FPCProceedings of the ACM on Programming Languages10.1145/36328558:POPL(362-392)Online publication date: 5-Jan-2024
https://dl.acm.org/doi/10.1145/3632855
Paquet HSaville P(2023)Effectful Semantics in 2-Dimensional Categories: Premonoidal and Freyd BicategoriesElectronic Proceedings in Theoretical Computer Science10.4204/EPTCS.397.12397(190-209)Online publication date: 14-Dec-2023
https://doi.org/10.4204/EPTCS.397.12
Kerinec AManzonetto GOlimpieri F(2023)Why Are Proofs Relevant in Proof-Relevant Models?Proceedings of the ACM on Programming Languages10.1145/35712017:POPL(218-248)Online publication date: 11-Jan-2023
https://dl.acm.org/doi/10.1145/3571201
Clairambault PForest S(2023)The Cartesian Closed Bicategory of Thin Spans of Groupoids2023 38th Annual ACM/IEEE Symposium on Logic in Computer Science (LICS)10.1109/LICS56636.2023.10175754(1-13)Online publication date: 26-Jun-2023
https://doi.org/10.1109/LICS56636.2023.10175754
Kerjean MLemay J(2023)Taylor Expansion as a Monad in Models of DiLL2023 38th Annual ACM/IEEE Symposium on Logic in Computer Science (LICS)10.1109/LICS56636.2023.10175753(1-13)Online publication date: 26-Jun-2023
https://doi.org/10.1109/LICS56636.2023.10175753
Clairambault POlimpieri FPaquet H(2023)From Thin Concurrent Games to Generalized Species of Structures2023 38th Annual ACM/IEEE Symposium on Logic in Computer Science (LICS)10.1109/LICS56636.2023.10175681(1-14)Online publication date: 26-Jun-2023
https://doi.org/10.1109/LICS56636.2023.10175681
Tsukada TAsada K(2022)Linear-Algebraic Models of Linear Logic as Categories of Modules over Σ-Semirings✱Proceedings of the 37th Annual ACM/IEEE Symposium on Logic in Computer Science10.1145/3531130.3533373(1-13)Online publication date: 2-Aug-2022
https://dl.acm.org/doi/10.1145/3531130.3533373
Jia XKornell ALindenhovius BMislove MZamdzhiev V(2022)Semantics for variational Quantum programmingProceedings of the ACM on Programming Languages10.1145/34986876:POPL(1-31)Online publication date: 12-Jan-2022
https://dl.acm.org/doi/10.1145/3498687
Olimpieri FGorla D(2021)Intersection type distributorsProceedings of the 36th Annual ACM/IEEE Symposium on Logic in Computer Science10.1109/LICS52264.2021.9470617(1-15)Online publication date: 29-Jun-2021
https://dl.acm.org/doi/10.1109/LICS52264.2021.9470617
Barbarossa DManzonetto G(2019)Taylor subsumes Scott, Berry, Kahn and PlotkinProceedings of the ACM on Programming Languages10.1145/33710694:POPL(1-23)Online publication date: 20-Dec-2019
https://dl.acm.org/doi/10.1145/3371069

View Options

Get Access

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 Publication

View options

PDF

View or Download as a PDF file.

eReader

View online with eReader.

Media

Figures

Other

Tables

View Table of Contents