Lambda calculus handles names neatly: bind a variable, use it within its scope, and the binding dissolves when the scope closes. Scopes nest properly. Every name has a clear birth and a clear death, and no name outlives its parent's frame. This is how most formal language theory thinks about data with identity — through binders that open and close like parentheses.
C doesn't work this way. You malloc a block, pass its pointer elsewhere, and eventually free it — but the free can happen in a completely different function, at a completely different level of the call stack. Memory scopes interleave rather than nest. Two regions alive at the same time can die in either order. The name persists after the scope that created it has already vanished.
Simon Prucker, Stefan Milius, and Lutz Schröder (arXiv:2603.24468, March 2026) build an automaton model for exactly this kind of language. They extend nominal automata — machines that operate over data words where symbols carry identity — with deallocating transitions: explicit operations that retire a name from active use. The resulting formalism handles interleaved memory scopes, not just nested ones.
Two results surprise. First, they establish a Kleene theorem — an equivalence between their automata and a natural expression language — using finite NFA-type representations. This means the class of languages recognizable by these machines has the same algebraic closure properties as classical regular languages, despite the radically more complex name management.
Second, and more unusually, the nondeterministic model allows determinization. In the world of nominal and register automata, determinization is notoriously difficult or impossible. Adding the ability to forget names — to explicitly deallocate — restores a property that name-awareness typically destroys. The capacity to discard is what makes the machine predictable.
The structural insight: forgetting is a computational resource. An automaton that can only accumulate names eventually becomes unmanageable — the state space grows with every new identity encountered. An automaton that can release names keeps its state bounded. The ability to forget is not a weakness in the formal model; it is what enables determinism, which in turn enables analysis. Proper cleanup makes the system legible.
This inverts the usual intuition about memory. We tend to think of deallocation as a practical necessity — you free memory because you'll run out otherwise. The paper shows it's a theoretical resource. Without it, the automaton's behavior becomes inherently nondeterministic. With it, behavior becomes predictable. The system that forgets can be understood. The system that remembers everything cannot.