# Separation and Renaming in Nominal Sets

## TL;DR

This paper introduces separated nominal automata, which are exponentially smaller than classical ones, by relating nominal sets to nominal renaming sets through categorical adjunctions and substitution-based semantics.

## Contribution

It establishes a categorical connection between nominal sets and nominal renaming sets and defines separated nominal automata with potential size advantages.

## Key findings

- Separated nominal automata can be exponentially smaller than classical automata.
- The categorical adjunction relates separated product to Cartesian product.
- Semantics closed under substitutions enables size reduction.

## Abstract

Nominal sets provide a foundation for reasoning about names. They are used primarily in syntax with binders, but also, e.g., to model automata over infinite alphabets. In this paper, nominal sets are related to nominal renaming sets, which involve arbitrary substitutions rather than permutations, through a categorical adjunction. In particular, the left adjoint relates the separated product of nominal sets to the Cartesian product of nominal renaming sets. Based on these results, we define the new notion of separated nominal automata. These automata can be exponentially smaller than classical nominal automata, if the semantics is closed under substitutions.