2024/04/08 by Bojańczyk, Mikołaj, Nguyên, Lê Thành Dũng, Stefański, Rafał
#FOS: Computer and information sciences #FOS: Mathematics #Formal Languages and Automata Theory (cs.FL) #Logic (math.LO) #Logic in Computer Science (cs.LO)
paper · doi:10.48550/arxiv.2404.05265
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.