Function spaces for orbit-finite sets
Mikołaj Bojańczyk, Lê Thành Dũng Nguyên, Rafał Stefański
TL;DR
Orbit-finite sets provide a finite-like framework for nominal sets but fail to support orbit-finite function spaces, which impedes automata constructions on infinite alphabets. The authors present two linear-inspired remedies: (i) a single-use (copyless) category that enforces a symmetric monoidal closed structure, and (ii) a vector-space-based generalization that embeds in an orbit-finite setting; both approaches aim to preserve function spaces. The single-use approach defines an inductive, prime-function-based construction for X [0m→ Y on polynomial orbit-finite inputs, using X 520 Y via linear-type combinators to achieve closed function spaces, though currying remains an open challenge. The work highlights a principled pathway to recover function-space closure in orbit-finite settings, with implications for automata over infinite alphabets and potential extensions to broader relational structures.
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.