Function spaces for orbit-finite sets
Logic in Computer Science
2024-04-09 v1 Formal Languages and Automata Theory
Logic
Abstract
Orbit-finite sets are a generalisation of finite sets, and as such support many operations allowed for finite sets, such as pairing, quotienting, or taking subsets. However, they do not support function spaces, i.e. if X and Y are orbit-finite sets, then the space of finitely supported functions from X to Y is not orbit-finite. In this paper we propose two solutions to this problem: one is obtained by generalising the notion of orbit-finite set, and the other one is obtained by restricting it. In both cases, function spaces and the original closure properties are retained. Curiously, both solutions are "linear": the generalisation is based on linear algebra, while the restriction is based on linear logic.
Keywords
Cite
@article{arxiv.2404.05265,
title = {Function spaces for orbit-finite sets},
author = {Mikołaj Bojańczyk and Lê Thành Dũng Nguyên and Rafał Stefański},
journal= {arXiv preprint arXiv:2404.05265},
year = {2024}
}