Document Open Access Logo

Representing Guardedness in Call-By-Value

Author Sergey Goncharov

PDF

File

Thumbnail PDF
PDF
LIPIcs.FSCD.2023.34.pdf
  • Filesize: 0.8 MB
  • 21 pages

Document Identifiers

Subject Classification

ACM Subject Classification
  • Theory of computation → Categorical semantics
  • Theory of computation → Axiomatic semantics
Keywords
  • Fine-grain call-by-value
  • Abstract guardedness
  • Freyd category
  • Kleisli category
  • Elgot iteration

Metrics

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

Abstract

Like the notion of computation via (strong) monads serves to classify various flavours of impurity, including exceptions, non-determinism, probability, local and global store, the notion of guardedness classifies well-behavedness of cycles in various settings. In its most general form, the guardedness discipline applies to general symmetric monoidal categories and further specializes to Cartesian and co-Cartesian categories, where it governs guarded recursion and guarded iteration respectively. Here, even more specifically, we deal with the semantics of call-by-value guarded iteration. It was shown by Levy, Power and Thielecke that call-by-value languages can be generally interpreted in Freyd categories, but in order to represent effectful function spaces, such a category must canonically arise from a strong monad. We generalize this fact by showing that representing guarded effectful function spaces calls for certain parametrized monads (in the sense of Uustalu). This provides a description of guardedness as an intrinsic categorical property of programs, complementing the existing description of guardedness as a predicate on a category.

Cite As Get BibTex

Sergey Goncharov. Representing Guardedness in Call-By-Value. In 8th International Conference on Formal Structures for Computation and Deduction (FSCD 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 260, pp. 34:1-34:21, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023) https://doi.org/10.4230/LIPIcs.FSCD.2023.34

Author Details

Sergey Goncharov
  • Friedrich-Alexander-Universität Erlangen-Nürnberg, Germany

Acknowledgements

The author would like to thank anonymous reviewers of the present and previous editions of the paper for their diligence in their effort to improve it.

References

  1. Jiří Adámek, Horst Herrlich, and George Strecker. Abstract and concrete categories. John Wiley & Sons Inc., New York, 1990. Google Scholar
  2. Jiří Adámek, Stefan Milius, and Jiří Velebil. On rational monads and free iterative theories. In Proc. Category Theory and Computer Science (CTCS'02), volume 69 of Electron. Notes Theor. Comput. Sci., pages 23-46, 2002. Google Scholar
  3. Jiří Adámek, Stefan Milius, and Jiří Velebil. Equational properties of iterative monads. Inf. Comput., 208(12):1306-1348, 2010. Google Scholar
  4. Thorsten Altenkirch, Nils Danielsson, and Nicolai Kraus. Partiality, revisited - the partiality monad as a quotient inductive-inductive type. In Javier Esparza and Andrzej Murawski, editors, Foundations of Software Science and Computation Structures, FOSSACS 2017, volume 10203 of LNCS, pages 534-549, 2017. Google Scholar
  5. Steve Awodey. Category Theory. Oxford University Press, Inc., New York, NY, USA, 2nd edition, 2010. Google Scholar
  6. J. Bergstra, A. Ponse, and Scott Smolka, editors. Handbook of Process Algebra. Elsevier, 2001. Google Scholar
  7. Stephen Bloom and Zoltán Ésik. Iteration theories: the equational logic of iterative processes. Springer, 1993. Google Scholar
  8. Venanzio Capretta. General recursion via coinductive types. Log. Meth. Comput. Sci., 1(2), 2005. Google Scholar
  9. James Chapman, Tarmo Uustalu, and Niccolò Veltri. Quotienting the delay monad by weak bisimilarity. In Theoretical Aspects of Computing, ICTAC 2015, volume 9399 of LNCS, pages 110-125. Springer, 2015. Google Scholar
  10. J. Robin B. Cockett. Introduction to distributive categories. Mathematical Structures in Computer Science, 3(3):277-307, 1993. Google Scholar
  11. Martín H. Escardó and Cory M. Knapp. Partial Elements and Recursion via Dominances in Univalent Type Theory. In Valentin Goranko and Mads Dam, editors, 26th EACSL Annual Conference on Computer Science Logic (CSL 2017), volume 82 of Leibniz International Proceedings in Informatics (LIPIcs), pages 21:1-21:16, Dagstuhl, Germany, 2017. Schloss Dagstuhl-Leibniz-Zentrum fuer Informatik. Google Scholar
  12. M.P. Fiore. Axiomatic Domain Theory in Categories of Partial Maps. Distinguished Dissertations in Computer Science. Cambridge University Press, 2004. Google Scholar
  13. Bram Geron and Paul Blain Levy. Iteration and labelled iteration. In Proc. 32nd Conference on the Mathematical Foundations of Programming Semantics (MFPS 2016), volume 325 of ENTCS, pages 127-146. Elsevier, 2016. Google Scholar
  14. Sergey Goncharov. Uniform Elgot Iteration in Foundations. In Nikhil Bansal, Emanuela Merelli, and James Worrell, editors, 48th International Colloquium on Automata, Languages, and Programming (ICALP 2021), volume 198 of LIPIcs, pages 131:1-131:16. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2021. Google Scholar
  15. Sergey Goncharov, Renato Neves, and José Proenȩdillaca. Implementing hybrid semantics: From functional to imperative. In Volker Stolz Violet Ka I Pun, Adenilso da Silva Simão, editor, 17th International Colloquium on Theoretical Aspects of Computing (ICTAC 2020), 2020. Google Scholar
  16. Sergey Goncharov, Christoph Rauch, and Lutz Schröder. Unguarded recursion on coinductive resumptions. In Mathematical Foundations of Programming Semantics, MFPS 2015, volume 319 of ENTCS, pages 183-198. Elsevier, 2015. Google Scholar
  17. Sergey Goncharov, Christoph Rauch, and Lutz Schröder. A metalanguage for guarded iteration. Theoretical Computer Science, 880:111-137, 2021. Google Scholar
  18. Sergey Goncharov and Lutz Schröder. Guarded traced categories. In Christel Baier and Ugo Dal Lago, editors, Proc. 21th International Conference on Foundations of Software Science and Computation Structures (FoSSaCS 2018), LNCS. Springer, 2018. Google Scholar
  19. Sergey Goncharov, Lutz Schröder, Christoph Rauch, and Maciej Piróg. Unifying guarded and unguarded iteration. In Javier Esparza and Andrzej Murawski, editors, Foundations of Software Science and Computation Structures, FoSSaCS 2017, volume 10203 of LNCS, pages 517-533. Springer, 2017. Google Scholar
  20. George Janelidze and Gregory M Kelly. A note on actions of a monoidal category. Theory Appl. Categ, 9(61-91):02, 2001. Google Scholar
  21. Anders Kock. Strong functors and monoidal monads. Archiv der Mathematik, 23(1):113-120, 1972. Google Scholar
  22. Paul Blain Levy. Call-by-push-value: A subsuming paradigm. In Jean-Yves Girard, editor, TLCA, volume 1581 of Lecture Notes in Computer Science, pages 228-242. Springer, 1999. Google Scholar
  23. Paul Blain Levy. Call-By-Push-Value: A Functional/Imperative Synthesis (Semantics Structures in Computation, V. 2). Kluwer Academic Publishers, USA, 2004. Google Scholar
  24. Paul Blain Levy and Sergey Goncharov. Coinductive resumption monads: Guarded iterative and guarded elgot. In Proc. 8rd international conference on Algebra and coalgebra in computer science (CALCO 2019), LIPIcs. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2019. Google Scholar
  25. Paul Blain Levy, John Power, and Hayo Thielecke. Modelling environments in call-by-value programming languages. Inf. & Comp, 185:2003, 2002. Google Scholar
  26. Saunders Mac Lane. Categories for the Working Mathematician. Springer, 1971. Google Scholar
  27. R. Milner. Communication and concurrency. Prentice-Hall, 1989. Google Scholar
  28. Eugenio Moggi. A modular approach to denotational semantics. In Category Theory and Computer Science, CTCS 1991, volume 530 of LNCS, pages 138-139. Springer, 1991. Google Scholar
  29. Keiko Nakata and Tarmo Uustalu. A Hoare logic for the coinductive trace-based big-step semantics of While. Log. Meth. Comput. Sci., 11(1), 2015. Google Scholar
  30. Maciej Piróg and Jeremy Gibbons. The coinductive resumption monad. In Mathematical Foundations of Programming Semantics, MFPS 2014, volume 308 of ENTCS, pages 273-288, 2014. Google Scholar
  31. Gordon Plotkin and John Power. Adequacy for algebraic effects. In FoSSaCS'01, volume 2030 of LNCS, pages 1-24, 2001. Google Scholar
  32. A. J. Power and E. P. Robinson. Premonoidal categories and notions of computation. Mathematical Structures in Computer Science, 7(5):453-468, October 1997. Google Scholar
  33. A. John Power and Hayo Thielecke. Closed Freyd- and kappa-categories. In Proceedings of the 26th International Colloquium on Automata, Languages and Programming, ICAL '99, pages 625-634, Berlin, Heidelberg, 1999. Springer-Verlag. Google Scholar
  34. Dietmar Schumacher. Minimale und maximale tripelerzeugende und eine bemerkung zur tripelbarkeit. Archiv der Mathematik, 20(4):356-364, September 1969. Google Scholar
  35. Alex Simpson and Gordon Plotkin. Complete axioms for categorical fixed-point operators. In Logic in Computer Science, LICS 2000, pages 30-41, 2000. Google Scholar
  36. Sam Staton. Freyd categories are enriched Lawvere theories. Electron. Notes Theor. Comput. Sci., 303:197-206, March 2014. Google Scholar
  37. Tarmo Uustalu. Generalizing substitution. ITA, 37(4):315-336, 2003. Google Scholar
  38. Tarmo Uustalu and Varmo Vene. Comonadic notions of computation. Electron. Notes Theor. Comput. Sci., 203(5):263-284, 2008. 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-2025 Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact