License: 
Creative Commons Attribution 4.0 International license (CC BY 4.0)
When quoting this document, please refer to the following
DOI: 10.4230/LIPIcs.ITP.2023.31
URN: urn:nbn:de:0030-drops-184063
URL: http://dagstuhl.sunsite.rwth-aachen.de/volltexte/2023/18406/
Voorneveld, Niels F. W.
Slice Nondeterminism
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.
BibTeX - Entry
@InProceedings{voorneveld:LIPIcs.ITP.2023.31,
author = {Voorneveld, Niels F. W.},
title = {{Slice Nondeterminism}},
booktitle = {14th International Conference on Interactive Theorem Proving (ITP 2023)},
pages = {31:1--31:19},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-284-6},
ISSN = {1868-8969},
year = {2023},
volume = {268},
editor = {Naumowicz, Adam and Thiemann, Ren\'{e}},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/opus/volltexte/2023/18406},
URN = {urn:nbn:de:0030-drops-184063},
doi = {10.4230/LIPIcs.ITP.2023.31},
annote = {Keywords: Category theory, Agda, Slice category, Nondeterministic functions, Powerset}
}
