Document Open Access Logo

A Profunctorial Scott Semantics

Author Zeinab Galal

PDF
Thumbnail PDF

File

LIPIcs.FSCD.2020.16.pdf
  • Filesize: 0.58 MB
  • 18 pages

Document Identifiers

Author Details

Zeinab Galal
  • Université de Paris, IRIF, CNRS, Paris, France

Acknowledgements

I thank Thomas Ehrhard, Marcelo Fiore, Chaitanya Leena Subramaniam and Christine Tasson for helpful discussions on this article and the referees for their valuable feedback.

Cite AsGet BibTex

Zeinab Galal. A Profunctorial Scott Semantics. In 5th International Conference on Formal Structures for Computation and Deduction (FSCD 2020). Leibniz International Proceedings in Informatics (LIPIcs), Volume 167, pp. 16:1-16:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2020)
https://doi.org/10.4230/LIPIcs.FSCD.2020.16

Abstract

In this paper, we study the bicategory of profunctors with the free finite coproduct pseudo-comonad and show that it constitutes a model of linear logic that generalizes the Scott model. We formalize the connection between the two models as a change of base for enriched categories which induces a pseudo-functor that preserves all the linear logic structure. We prove that morphisms in the co-Kleisli bicategory correspond to the concept of strongly finitary functors (sifted colimits preserving functors) between presheaf categories. We further show that this model provides solutions of recursive type equations which provides 2-dimensional models of the pure lambda calculus and we also exhibit a fixed point operator on terms.

Subject Classification

ACM Subject Classification
  • Theory of computation → Linear logic
  • Theory of computation → Categorical semantics
Keywords
  • Linear Logic
  • Scott Semantics
  • Profunctors

Metrics

  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    0
    PDF Downloads
    0
    Metadata Views

References

  1. Jirí Adámek, Jirí Rosický, and Enrico. M. Vitale. Algebraic theories: a categorical introduction to general algebra. Cambridge University Press, 2011. Google Scholar
  2. Jean Bénabou. Distributors at work, 2000. Lecture notes written by Thomas Streicher. URL: https://www2.mathematik.tu-darmstadt.de/~streicher/FIBR/DiWo.pdf.
  3. Gian Luca Cattani and Glynn Winskel. Profunctors, open maps and bisimulation. Mathematical Structures in Computer Science, 15:553-614, June 2005. URL: https://doi.org/10.1017/S0960129505004718.
  4. Geoff S. H. Cruttwell. Normed Spaces and the Change of Base for Enriched Categories. PhD dissertation, Dalhousie University, 2008. Google Scholar
  5. Thomas Ehrhard. Collapsing non-idempotent intersection types. Leibniz International Proceedings in Informatics, LIPIcs, 16, September 2012. URL: https://doi.org/10.4230/LIPIcs.CSL.2012.259.
  6. Thomas Ehrhard. The Scott model of Linear Logic is the extensional collapse of its relational model. Theoretical Computer Science, 424:20-45, 2012. 26 pages. URL: https://doi.org/10.1016/j.tcs.2011.11.027.
  7. Thomas Ehrhard. An introduction to differential linear logic: proof-nets, models and antiderivatives. Math. Struct. Comput. Sci., 28(7):995-1060, 2018. URL: https://doi.org/10.1017/S0960129516000372.
  8. Thomas Ehrhard and Laurent Regnier. The differential lambda-calculus. Theor. Comput. Sci., 309(1):1-41, December 2003. URL: https://doi.org/10.1016/S0304-3975(03)00392-X.
  9. Marcelo Fiore. Analytic functors between presheaf categories over groupoids. Theor. Comput. Sci., 546:120-131, 2014. URL: https://doi.org/10.1016/j.tcs.2014.03.004.
  10. Marcelo Fiore, Nicola Gambino, Martin Hyland, and Glynn Winskel. The cartesian closed bicategory of generalised species of structures. J. Lond. Math. Soc. (2), 77(1):203-220, 2008. URL: https://doi.org/10.1112/jlms/jdm096.
  11. Marcelo Fiore, Nicola Gambino, Martin Hyland, and Glynn Winskel. Relative pseudomonads, kleisli bicategories, and substitution monoidal structures. Selecta Mathematica, 24:2791-2830, November 2017. URL: https://doi.org/10.1007/s00029-017-0361-3.
  12. Marcelo Fiore and André Joyal. Theory of para-toposes. Talk at the Category Theory 2015 Conference, Departamento de Matematica, Universidade de Aveiro, Portugal, 2015. Google Scholar
  13. Jean-Yves Girard. Linear logic. Theor. Comput. Sci., 50:1-102, 1987. URL: https://doi.org/10.1016/0304-3975(87)90045-4.
  14. Michael Huth. Linear domains and linear maps. In Proceedings of the 9th International Conference on Mathematical Foundations of Programming Semantics, page 438–453, Berlin, Heidelberg, 1993. Springer-Verlag. Google Scholar
  15. Michael Huth, Achim Jung, and Klaus Keimel. Linear types and approximation. Mathematical Structures in Computer Science, 10, May 1994. URL: https://doi.org/10.1017/S0960129500003200.
  16. Gregory M. Kelly. Basic Concepts of Enriched Category Theory. Lecture note series / London mathematical society. Cambridge University Press, 1982. Google Scholar
  17. Tom Leinster. Basic bicategories. In E-print math.CT/9810017, 1998. Google Scholar
  18. Paul-André Melliès. Categorical semantics of linear logic. In In: Interactive Models of Computation and Program Behaviour, Panoramas et Synthèses 27, Société Mathématique de France 1?196, 2009. Google Scholar
  19. Federico Olimpieri. Intersection type distributors, 2020. URL: http://arxiv.org/abs/2002.01287.
  20. Maria Cristina Pedicchio and Walter Tholen. Categorical foundations : special topics in order, topology, algebra, and Sheaf theory. Cambridge University Press, 2003. URL: https://doi.org/10.1017/CBO9781107340985.
  21. Michael B. Smyth and Gordon D. Plotkin. The category-theoretic solution of recursive domain equations. In Proceedings of the 18th Annual Symposium on Foundations of Computer Science, SFCS ’77, page 13–17, USA, 1977. IEEE Computer Society. URL: https://doi.org/10.1109/SFCS.1977.30.
  22. Glynn Winskel. A linear metalanguage for concurrency. In Algebraic Methodology and Software Technology, 7th International Conference, AMAST '98, pages 42-58. Springer, June 1998. URL: https://doi.org/10.1007/3-540-49253-4_6.
  23. Glynn Winskel. Linearity and nonlinearity in distributed computation. In Linear Logic in Computer Science. Cambridge University Press, 2004. URL: https://doi.org/10.1017/CBO9780511550850.005.
  24. Glynn Winskel. Strategies as profunctors. In Frank Pfenning, editor, Foundations of Software Science and Computation Structures, pages 418-433, Berlin, Heidelberg, 2013. Springer Berlin Heidelberg. Google Scholar
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail
© 2023-2024 Schloss Dagstuhl – LZI GmbH Imprint Privacy Contact