Document Open Access Logo

Slice Nondeterminism

Author Niels F. W. Voorneveld

PDF
Thumbnail PDF

File

LIPIcs.ITP.2023.31.pdf
  • Filesize: 0.8 MB
  • 19 pages

Document Identifiers

Author Details

Niels F. W. Voorneveld
  • Tallinn University of Technology, Estonia

Funding

  • Voorneveld, Niels F. W.: Supported by the ESF funded Estonian IT Academy research measure (project 2014-2020.4.05.19-0001)

Cite AsGet BibTex

Niels F. W. Voorneveld. Slice Nondeterminism. In 14th International Conference on Interactive Theorem Proving (ITP 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 268, pp. 31:1-31:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)
https://doi.org/10.4230/LIPIcs.ITP.2023.31

Abstract

This paper studies a technique for describing and formalising nondeterministic functions, using slice categories. Results of a nondeterministic function are modelled by an object of the slice category over the codomain of the function, which is an indexed family over the codomain. Two such families denote the same set of results if slice morphisms exist between them in both directions. We formulate the category of nondeterministic functions by expressing a set of possible results as an equivalence class of objects. If we allow families to use any indexing set, this category will be equivalent to the category of relations. When we limit ourselves to a smaller universe of indexing sets, we get a subcategory which more closely resembles nondeterministic programs. We compare this category with other representations of the category of relations, and see how many properties can be carried over, such as its product, coproduct and other monoidal structures. We can describe inductive nondeterministic structures by lifting free monads from the category of sets. Moreover, due to the intensional nature of the slice representation, nondeterministic processes are easily represented, such as interleaving concurrency and labelled transition systems. This paper has been formalised in Agda.

Subject Classification

ACM Subject Classification
  • Theory of computation → Categorical semantics
  • Theory of computation → Type theory
Keywords
  • Category theory
  • Agda
  • Slice category
  • Nondeterministic functions
  • Powerset

Metrics

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

Supplementary Materials

References

  1. Michael Gordon Abbott, Thorsten Altenkirch, and Neil Ghani. Containers: Constructing strictly positive types. Theoretical Computer Science, 342(1):3-27, 2005. URL: https://doi.org/10.1016/j.tcs.2005.06.002.
  2. Samson Abramsky. Domain theory in logical form. Ann. Pure Appl. Log., 51(1-2):1-77, 1991. URL: https://doi.org/10.1016/0168-0072(91)90065-T.
  3. Peter Aczel. Galois: a theory development project, 1993. In: A report on work in progress for the Turin meeting on the Representation of Logical Frameworks. Google Scholar
  4. Thorsten Altenkirch, Neil Ghani, Peter Hancock, Conor Mcbride, and Peter Morris. Indexed containers. Journal of Functional Programming, 25:e5, 2015. URL: https://doi.org/10.1017/S095679681500009X.
  5. Joyal Andre, Ross Street, and Dominic Verity. Traced monoidal categories. Mathematical Proceedings of the Cambridge Philosophical Society, 119:447-468, April 1996. URL: https://doi.org/10.1017/S0305004100074338.
  6. Jon Beck. Distributive laws. In B. Eckmann, editor, Seminar on Triples and Categorical Homology Theory, pages 119-140, Berlin, Heidelberg, 1969. Springer Berlin Heidelberg. URL: https://doi.org/10.1007/BFb0083084.
  7. Jean Bénabou. Introduction to bicategories. In Reports of the Midwest Category Seminar, pages 1-77, Berlin, Heidelberg, 1967. Springer Berlin Heidelberg. Google Scholar
  8. J. A. Bergstra and J. W. Klop. Algebra of communicating processes with abstraction. Theoretical Computer Science, 37:77-121, 1985. URL: https://doi.org/10.1016/0304-3975(85)90088-X.
  9. Gerhard Gierz, Karl Heinrich Hofmann, Klaus Keimel, Jimmie Lawson, Michael Mislove, and Dana S. Scott. Continuous Lattices and Domains. Cambridge University Press, Cambridge, 2003. Google Scholar
  10. C. A. R. Hoare. Communicating sequential processes. Commun. ACM, 21(8):666-677, August 1978. URL: https://doi.org/10.1145/359576.359585.
  11. Markus Holzer and Martin Kutrib. Reversible nondeterministic finite automata. In International Workshop on Reversible Computation, pages 35-51, May 2017. URL: https://doi.org/10.1007/978-3-319-59936-6_3.
  12. G. Kelly. The basic concepts of enriched category theory. Reprints in Theory and Applications of Categories [electronic only], 2005, January 2005. Google Scholar
  13. Yoshiki Kinoshita. A bicategorical analysis of E-categories. Mathematica Japonica, 47:157-170, 1998. Google Scholar
  14. Søren B. Lassen. Relational Reasoning about Functions and Nondeterminism. PhD thesis, University of Aarhus, 1998. Google Scholar
  15. Paul Blain Levy. Similarity quotients as final coalgebras. In Martin Hofmann, editor, FoSSaCS 2011, volume 6604 of LNCS, pages 27-41. Springer, 2011. URL: https://doi.org/10.1007/978-3-642-19805-2_3.
  16. Saunders MacLane. Categories for the Working Mathematician. Springer-Verlag, New York, 1971. Graduate Texts in Mathematics, Vol. 5. Google Scholar
  17. Rasmus Ejlers Møgelberg and Andrea Vezzosi. Two guarded recursive powerdomains for applicative simulation. In Ana Sokolova, editor, Proceedings of 37th Conference on Mathematical Foundations of Programming Semantics, MFPS 2021, volume 351 of Electron. Proc. in Theor. Comput. Sci., pages 200-217, 2021. URL: https://doi.org/10.4204/EPTCS.351.13.
  18. Gordon D. Plotkin. A powerdomain construction. Siam J. Comput., 5(3):452-487, 1976. URL: https://doi.org/10.1137/0205035.
  19. Gordon D. Plotkin and John Power. Adequacy for algebraic effects. In Furio Honsell and Marino Miculan, editors, FoSSaCS 2001, volume 2030 of LNCS, pages 1-24, 2001. URL: https://doi.org/10.1007/3-540-45315-6_1.
  20. Gordon D. Plotkin and Matija Pretnar. Handling algebraic effects. Log. Methods Comput. Sci., 9(4, article 23):1-36, 2013. URL: https://doi.org/10.2168/lmcs-9(4:23)2013.
  21. Albert Marchienus Thijs. Simulation and Fixpoint Semantics. PhD thesis, University of Groningen, 1996. URL: https://research.rug.nl/en/publications/simulation-and-fixpoint-semantics.
  22. Tarmo Uustalu. Stateful runners of effectful computations. Electron. Notes Theor. Comput. Sci., 319:403-421, 2015. URL: https://doi.org/10.1016/j.entcs.2015.12.024.
  23. Niccolò Veltri and Niels F. W. Voorneveld. Streams of approximations, equivalence of recursive effectful programs. In Ekaterina Komendantskaya, editor, Mathematics of Program Construction - 14th International Conference, MPC 2022, Tbilisi, Georgia, September 26-28, 2022, Proceedings, volume 13544 of Lecture Notes in Computer Science, pages 198-221. Springer, 2022. URL: https://doi.org/10.1007/978-3-031-16912-0_8.
  24. Niels F. W. Voorneveld. Runners for interleaving algebraic effects. In Helmut Seidl, Zhiming Liu, and Corina S. Pasareanu, editors, Theoretical Aspects of Computing - ICTAC 2022, pages 407-424, Cham, 2022. Springer International Publishing. 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