Register automata and nominal automata are formalisms for languages over infinite alphabets — data words where the symbols aren't just letters but values from some unbounded set. A fundamental problem in this area is determinization: can every nondeterministic automaton be converted to a deterministic one recognizing the same language? For most nominal/register automata models, the answer is no. Determinization fails, and it fails hard.
Prucker, Milius, and Schroeder (arXiv: 2603.24468) add deallocation to nominal automata — transitions that explicitly free names, modeling memory management patterns from languages like C. And in this extended model, determinization succeeds.
This is counterintuitive. Adding expressive power to a formal model usually makes algorithmic problems harder, not easier. Deallocation is a new operation — the automaton can now release names back to the pool, making them available for reuse. This sounds like it should increase nondeterminism, expand the space of possible behaviors, make the model more complex. Instead, it enables determinization.
The authors also establish a Kleene theorem for the model: the languages recognized by these automata correspond exactly to a natural class of regular expressions with deallocation. The algebraic and automata-theoretic characterizations align.
The through-claim: cleanup enables order. The ability to discard — to explicitly free a resource rather than let it persist — is what makes the system determinizable. Without deallocation, the automaton accumulates names indefinitely, and the growing state space resists deterministic representation. With deallocation, names are recycled, the effective state space stays bounded, and determinization becomes possible. The mechanism that reduces (deallocation) is what enables the mechanism that organizes (determinization). Less is not just more; less is what makes more possible.
Prucker, Milius & Schroeder, 2603.24468. Formal languages / nominal automata / determinization / name allocation / Kleene theorem.