Summary
Handling systems that involve names and data can be tricky when the system depends only on a limited set of special values. This paper studies how to define meanings (semantics) that stay consistent when you swap around unrelated values, focusing on infinite sets with certain symmetries. The authors show that, even in complex infinite setups, important mathematical tools called fixed points exist and can be found efficiently when considering how these special values affect the system. They demonstrate how this theory applies to computer models like automata and program semantics, helping ensure consistent reasoning about programs using these infinite yet structured data sets.
What this means in practice
- •For program verification teams: Guarantee convergence of fixed-point computations in program analyses involving infinite but structured data.
- •For security software developers: Implement monitors for authorization systems that handle dynamic and infinite sets of users and permissions efficiently.
A theory result. No direct application yet.
Abstract
Semantics for systems with names and data often depends on finitely many distinguished values. The theory of finitely supported structures treats this dependence through invariance under permutations fixing a finite context. We develop this approach to semantics over arbitrary permutation groups and arbitrary infinite sets of atoms. The central difficulty is that finitely supported predicate spaces need not be complete lattices. We prove that, for predicates valued in a complete lattice with trivial atom action, every monotone finitely supported transformer nevertheless has least and greatest fixed points. These lie in the complete lattice determined by the transformer's context and coincide with the fixed points of every compatible monotone ambient extension equivariant under its stabilizer. Support-transfer bounds track dependencies through semantic constructions, while uniform finiteness yields finite convergence. For Boolean predicates, $m$ context-stabilizer orbits on the carrier suffice for convergence after at most $m$ iterations, even when the supported predicate lattice is orbit-infinite. We apply these results to automata, operational and modal semantics, abstract interpretation, and resource rewriting. Ultrahomogeneous atom structures in finite relational signatures yield finite cell representations, illustrated by an authorization monitor. The resulting account separates semantic existence, finite convergence, and effective computation.