PaperlayerView exact revision on arXiv

Source-linked AI summary

Automata theory in nominal sets

Mikołaj Bojańczyk, Bartek Klin, Sławomir Lasota

arXiv:1402.0897v2cs.LOcs.FL

TL;DR

The paper studies automata for languages over structured infinite alphabets, where data descriptions may not uniquely determine values. It models alphabet structure through automorphism groups and develops a nominal-set framework using orbit finiteness, while establishing results for nominal automata.

  • Problem

    Automata must handle infinite alphabets with structure, but data descriptions do not uniquely determine values and require well-behaved notions of automata.

  • Method

    The paper captures alphabet structure through automorphism groups and transfers classical automata definitions to nominal sets by replacing finiteness with orbit finiteness.

  • Results

    Reachable deterministic G-automata over nominal alphabets have nominal state G-sets, and the framework develops automata theory across arbitrary symmetries.

  • Takeaways & Limitations

    Automorphism groups provide the organizing abstraction for structured infinite alphabets and their recognizing automata.

  • Takeaways & Limitations

    Determinization does not generally preserve orbit-finite state spaces, and closure under complementation fails essentially in every symmetry.

Abstract

from arXiv · show

We study languages over infinite alphabets equipped with some structure that can be tested by recognizing automata. We develop a framework for studying such alphabets and the ensuing automata theory, where the key role is played by an automorphism group of the alphabet. In the process, we generalize nominal sets due to Gabbay and Pitts.

1. Introduction

The paper develops automata theory for infinite alphabets by representing alphabet structure through automorphism groups and generalizing nominal sets across data symmetries. It replaces ordinary finiteness with orbit finiteness, connects the framework to existing automata models, and develops effective representations for further computational models.

  • Motivation: Infinite alphabets are studied as data values equipped with structure that automata can access through relations such as equality, order, graphs, or partial orders.
  • Motivation: Automorphisms capture alphabet structure: all bijections for unordered data values and monotone bijections for totally ordered data values.
  • Nominal sets for arbitrary symmetries: A data symmetry consists of a data set and a group of bijections acting on it, with languages required to be closed under that group action.
  • Nominal sets for arbitrary symmetries: The framework generalizes nominal sets by requiring each element to have a finite support of data values whose fixing preserves that element.
  • Automata theory in arbitrary symmetries: Classical automata definitions are transferred to nominal sets by replacing finiteness with orbit finiteness, enabling automata theory across arbitrary symmetries.
  • Automata theory in arbitrary symmetries: The paper relates its models to finite-memory and ordered-data automata, supplies an infinite-alphabet Myhill–Nerode theorem for deterministic automata, and discusses Fraïssé symmetries.
  • Effective representation: The paper develops effective representations of orbit-finite nominal sets, relations, and functions, supporting nominal versions of automata, grammars, and other computational models.

2. Group actions and data symmetries

This section defines data symmetries as group actions on data and develops the associated notions of orbits, equivariance, nominal alphabets, and languages. Orbit-finite G-sets provide the finite-like objects used for automata over structured infinite alphabets.

  • Group actions: A group action is a function X × G → X satisfying identity and composition laws, making X a G-set.
  • Data symmetries: A data symmetry is a set D together with a subgroup G ≤ Sym(D), with examples including equality, total order, integer translation, and classical symmetries.
  • Group actions: The action of G extends pointwise from data values to tuples, words, infinite words, and subsets of data values.
  • Orbits: An orbit is the set of elements reachable from one element under the group action, and an orbit-finite G-set has finitely many such orbits.
  • Orbits: Orbit structure depends on the symmetry: P(D) is not orbit finite under equality, while D² has two equality orbits and three total-order orbits.
  • Equivariant relations and functions: Equivariant subsets are unions of orbits, while equivariant functions preserve the group action and compose to form the category G-Set.
  • Languages: A nominal alphabet is an orbit-finite G-set A, and a G-language is an equivariant subset of the word set A* under the pointwise action.

3. G-automata

G-automata generalize classical automata to G-sets by replacing finiteness with orbit finiteness and requiring equivariant components. Their syntactic construction yields an infinite-alphabet Myhill–Nerode theorem characterizing recognition by deterministic orbit-finite G-automata.

  • G-automata: G-automata replace finite alphabets and state spaces with orbit-finite G-sets, while initial states, accepting states, and transitions must be equivariant.The automaton definition otherwise follows the classical model, and accepted languages are G-languages.
  • Deterministic G-automata: Deterministic G-automata use a transition function, have a singleton initial state, and may be studied through reachability from that state.A reachable state is one obtained by processing some input word from the initial state.
  • Deterministic G-automata: In the equality symmetry, a six-orbit deterministic automaton can store up to two ordered data values before deciding acceptance.Its state space contains three singleton orbits and three infinite orbits, including equal and unequal ordered pairs.
  • Deterministic G-automata: An alternative six-orbit automaton stores unequal data values as unordered pairs, yielding an equivariant surjection from the ordered representation but no reverse equivariant function.This representation is more abstract because it ignores the order of the stored values.
  • Myhill–Nerode theorem: For a G-language, Myhill–Nerode equivalence is equivariant, so its quotient carries a G-set structure and defines a reachable deterministic syntactic G-automaton.The transition maps an equivalence class [w] and letter a to the class [wa].
  • Myhill–Nerode theorem: A language over an orbit-finite G-set is recognized by a deterministic orbit-finite G-automaton exactly when its Myhill–Nerode equivalence has orbit-finitely many classes.The syntactic automaton is a homomorphic image of every reachable deterministic G-automaton recognizing the same language, and homomorphic automata recognize the same language.

4. Nominal G-sets

Nominal G-sets restrict G-sets to elements with finite supports relative to a data symmetry, enabling structured study of infinite alphabets. The section also identifies representation obstacles and motivates restricting to symmetries with least supports and related properties.

  • Representation: Cartesian products can destroy orbit finiteness: a single-orbit G-set may have a square with infinitely many orbits.The example constructs pairs distinguished by arbitrarily large intersection cardinalities.
  • Definition: A nominal G-set is a G-set in which every element has a finite support consisting of data values.A finite set C supports x when every group bijection fixing C also fixes x.
  • Definition: Nominal G-sets generalize nominal sets to arbitrary data symmetries, including equality, total order, and integer symmetries.For example, D* is nominal because the letters appearing in a word support that word.
  • Representation: Equality symmetry has only countably many non-isomorphic single-orbit nominal G-sets, despite having uncountably many non-isomorphic single-orbit G-sets in general.The nominal-set restriction removes the broader equality-symmetry pathology described by Fact 4.1.
  • Representation: Integer symmetry yields uncountably many equivariant functions Z × Z → Z, making concrete representations of arbitrary nominal automata infeasible.For any function g : Z → Z, the transition function δ_g is equivariant.
  • Representation: The paper therefore later restricts to data symmetries with least supports and other desirable properties to obtain finitary representations.Equality and total-order symmetries admit least supports, whereas integer symmetry does not.

5. Nominal G-automata

Nominal G-automata extend automata theory to orbit-finite nominal sets, retaining a Myhill–Nerode characterization for deterministic automata while exposing major nondeterministic closure failures.

  • Nominal automata: Nominal G-automata require nominal alphabets and state spaces, and reachable deterministic automata over nominal alphabets automatically have nominal state sets.This follows because the reachable-state map is equivariant and images of nominal sets under equivariant functions are nominal.
  • Deterministic automata: For orbit-finite nominal alphabets, a language is recognized by a G-DFA exactly when its Myhill–Nerode equivalence has orbit-finite classes.The result is the nominal G-set version of the Myhill–Nerode theorem.
  • Nondeterministic automata: Determinization can fail because the powerset of an orbit-finite set may have infinitely many orbits.The subset construction can therefore produce a nominal deterministic automaton whose state space is not orbit finite.
  • Nondeterministic automata: Allowing ε-transitions does not change the expressive power of G-NFA, because they can be eliminated while preserving equivariance.The resulting transition relation remains equivariant.
  • Closure properties: G-NFA are closed under union and concatenation, but complementation fails in the equality symmetry.The non-closure under complementation is witnessed by languages whose complements require all input letters to be distinct.
  • Closure properties: Intersection is not preserved by G-NFA in arbitrary symmetries, but is recovered for well-behaved symmetries where products of orbit-finite nominal sets remain controlled.The paper links intersection closure to closure under products.

6. Relationship with finite memory automata

The paper relates nominal G-automata to finite memory automata over finite-label/data alphabets, proving expressive equivalence while showing that nominal automata support richer local symmetries.

  • Finite memory automata: Every equivariant subset of partial data tuples is expressible as a Boolean combination of equality constraints.With finitely many names, this yields an orbit-finite nominal configuration space.
  • Finite memory automata: Finite memory automata use finite control, finitely many registers, partial register valuations, and equality constraints to process finite-label/data words.Configurations combine a control state with a partial valuation of registers by data values.
  • Nondeterministic equivalence: For alphabets A = A_fin × D, finite memory automata and G-NFA recognize exactly the same languages.The equivalence also characterizes G-NFA state spaces as C × (D ∪ ⊥)^n with finitely many initial states.
  • Nondeterministic equivalence: Every orbit-finite nominal set can be represented as an equivariant image of a structured set of the form C × (D ∪ ⊥)^n.This representation underpins the translation from G-NFA to finite memory automata.
  • Local symmetry: Nominal G-NFA are richer structurally because they allow local symmetries, such as storing an unordered pair, which finite memory automata cannot represent directly.Consequently, finite memory automata do not generally minimize: their syntactic automata may be homomorphic but not isomorphic images.
  • Deterministic equivalence: The deterministic versions are likewise equivalent: deterministic finite memory automata and G-DFA recognize the same languages over A_fin × D.The proof requires a support-preserving equivariant lifting lemma to retain determinism.

7. Other models and perspectives

The nominal-set framework extends beyond finite automata to grammars, pushdown automata, and other computation models, while classical equivalences and closure properties must be rechecked.

  • Pushdown models: Nominal pushdown automata use orbit-finite nominal state and stack alphabets, with orbit-finite equivariant transition relations.Orbit-finiteness prevents transitions from pushing arbitrarily large words in one step.
  • Context-free models: Nominal context-free grammars replace finite alphabets and nonterminal sets with orbit-finite nominal sets and require productions to be equivariant.This transfers the classical grammar definition to nominal sets.
  • Pushdown models: Nominal pushdown automata and nominal context-free grammars are expressively equivalent by essentially classical constructions.The paper also gives a nominal pushdown treatment of palindromes using data values on the stack.
  • Other models: The framework can be applied to two-way automata, Turing machines, Petri nets, and related models, but classical constructions may fail in the nominal setting.Failures arise in part because finite powersets need not preserve orbit-finiteness and because choice principles can fail.
  • Other models: Nominal alternating finite automata are more powerful than nominal nondeterministic finite automata.The language of words with pairwise distinct letters is given as an example recognized by a nominal alternating automaton.

Part 2. Finite representations of nominal sets and automata

The paper turns to finite representations because abstract nominal definitions alone do not make algorithmic automata questions effectively manipulable.

  • Motivation: Nominal definitions are insufficient for algorithmic results such as minimization and emptiness testing, which require finite representations of nominal data structures.The classical algorithms operate in polynomial time for deterministic finite automata, motivating effective nominal representations.
  • Representation program: The paper develops progressively more concrete finite representations for nominal G-sets and equivariant functions under assumptions on the underlying data symmetry.These representations support later applications to deterministic and nondeterministic G-automata.

8. G-set representation

The section represents single-orbit G-sets as coset spaces of subgroups and characterizes equivariant maps through subgroup inclusions. For nominal G-sets, the representation restricts to open subgroups, yielding an equivalent categorical description.

  • Coset representations: Every single-orbit G-set is isomorphic to a coset space [[H]]c, and each such coset space is itself a single-orbit G-set.The coset space is G/Hr with the action (Hπ) · σ = H(πσ).
  • Coset representations: Single-orbit coset spaces [[H]]c and [[K]]c are isomorphic exactly when H and K are conjugate subgroups.Thus the representation is determined up to conjugacy rather than by a unique subgroup.
  • Equivariant maps: Equivariant functions from [[H]]c to a G-set correspond bijectively to elements whose stabilizer contains H.For Y = [[K]]c, these elements are precisely cosets Kπ satisfying πH ⊆ Kπ.
  • Categorical form: The category of single-orbit G-sets is equivalent to a category whose objects are subgroups H ≤G and whose morphisms are suitable cosets Kπ.A morphism from H to K is represented by a coset satisfying πH ⊆Kπ.
  • Limits of generality: There are uncountably many non-conjugate subgroups of Sym(D) when D is countably infinite, showing that arbitrary orbit-finite G-sets cannot generally be presented by finite means.This motivates restricting attention to more concrete representations under additional symmetry assumptions.
  • Nominal restriction: For nominal G-sets, single-orbit spaces correspond exactly to open subgroups, so the categorical representation restricts from arbitrary subgroups to open ones.A subgroup is open when it contains GC for some finite support C.

9. Well-behaved symmetries

The section identifies least supports and fungibility as structural conditions that enable concrete finite representations of nominal G-sets. Under these conditions, single-orbit nominal sets and their equivariant maps can be encoded by finite support structures.

  • Least supports: Least supports are characterized by closure of subgroup supports under intersection: GC ≤H and GD ≤H imply GC∩D ≤H.This condition is equivalent to a symmetry admitting least supports.
  • Least supports: The equality and total order symmetries admit least supports, although minimal supports may otherwise be incomparable or have different cardinalities.The general setting can lack a unique least support even when minimal supports exist.
  • Fungibility: A finite set is fungible when each of its elements can be moved while all other elements remain fixed; equality and total order symmetries are fungible, but integer symmetry is not.In integer symmetry, fixing 1 necessarily fixes 2, so {1,2} is not fungible.
  • Fungibility: For symmetries admitting least supports, every finite fungible set is the least support of extG(S), while fungibility alone suffices for this conclusion for every finite set.The result also states that an existing least support of an open subgroup must be fungible.
  • Finite representations: With least supports, single-orbit nominal G-sets have finite representations [[C,S]]e, where C is finite and S is a subgroup of the restricted symmetry.The subgroup relation satisfies [[C,S]]e ≤[[D,T]]e iff D ⊆C and S|D ≤T.
  • Finite representations: Equivariant maps between these representations are represented by injective functions extending to permutations and respecting the local symmetries, modulo ≡T.This gives a concrete finite description of both objects and morphisms.
  • Consequences: For countable D and symmetries admitting least supports, there are only countably many non-isomorphic single-orbit nominal G-sets.This contrasts with the uncountable subgroup variety possible for arbitrary G-sets.

10. Fra¨ıss´e symmetries

Fra¨ıss´e symmetries arise from automorphism groups of countable homogeneous universal structures and support a finite structure-based representation of nominal sets. Under well-behavedness, Cartesian products can also be computed from finitely many relational configurations.

  • Fra¨ıss´e symmetries: A Fra¨ıss´e symmetry is obtained from the automorphism group of the countable Fra¨ıss´e limit of a Fra¨ıss´e class.The limit is universal for the class's finite structures and homogeneous for finite-substructure isomorphisms.
  • Fra¨ıss´e symmetries: A well-behaved Fra¨ıss´e symmetry is one that admits least supports and is fungible.Not every Fra¨ıss´e symmetry satisfies both properties.
  • Structure representations: Single-orbit nominal sets over a well-behaved Fra¨ıss´e symmetry are represented by a finite structure A and a local symmetry group S ≤Aut(A).The semantics consists of embeddings of A into the Fra¨ıss´e limit, quotiented by the local symmetry.
  • Structure representations: Equivariant maps between structure representations are represented by embeddings u:B→A satisfying uS ⊆Tu, modulo ≡T.This is the structure-level counterpart of the finite support representation.
  • Cartesian products: Cartesian products are classified by the partial isomorphism between two embedded structures and the relational structure on their amalgamated sum.These configurations are invariant under the group action and induce an equivariant map to a finite disjoint union.
  • Cartesian products: If the signature is finite and class membership is decidable, all possible product configurations can be effectively enumerated, yielding computable representations of [[A,1]] ×[[B,1]].The resulting product representation is finite because only finitely many ρ and C are possible.
  • Cartesian products: For equality symmetry, D(n) ×D has n+1 orbits, while D(<n) ×D has 2n+1 orbits.These examples illustrate how product orbit counts can be computed from relational overlap patterns.

11. Fra¨ıss´e automata

Fra¨ıss´e automata provide finite, register-based representations of deterministic nominal automata over well-behaved Fra¨ıss´e symmetries. Their symbolic transitions encode how new input data relates to stored register structures.

  • Scope and implementation: The concrete representation is mathematically more complex than the abstract nominal-automaton definitions, and the paper presents abstract algorithmic formulations as more productive for implementation.A general-purpose language can translate abstract algorithms into finite representations implicitly.
  • Symbolic transitions: Annotations describe the possible structural comparisons between a newly read input value and the registers in the current state.They correspond to orbits of the product between a state's representation and the input alphabet.
  • Automaton model: A Fra¨ıss´e K-automaton has finitely many control states, a finite structure representation of registers for each state, initial and accepting states, and symbolic transitions.Configurations pair a control state with an embedding of its register structure into the Fra¨ıss´e limit.
  • Symbolic transitions: On input d, the automaton extends the current valuation with d, applies the symbolic transition for the resulting annotation, and updates the state and valuation.The update is defined by composing the transition's embedding with the extended valuation.
  • Representation theorem: Every reachable orbit-finite deterministic nominal automaton over a well-behaved Fra¨ıss´e symmetry is isomorphic to a Fra¨ıss´e K-automaton.This establishes the finite register-style representation for the reachable automata of interest.
  • Language characterization: For languages over the Fra¨ıss´e limit, recognition by a GK-DFA, recognition by a Fra¨ıss´e K-automaton, and orbit-finiteness of the syntactic quotient are equivalent.The three conditions provide abstract, finite-representation, and Myhill–Nerode characterizations.
  • Examples: For total order symmetry, Fra¨ıss´e automata use ordered registers and monotone valuations to compare input data with stored values.They are expressively equivalent to deterministic finite-memory automata in the stated singleton-alphabet setting.
  • Examples: For graph symmetry, registers form a graph and transitions can test whether a new input is connected to stored nodes; this automaton model was not previously studied to the authors' knowledge.The graph structure is inherited from embeddings into the random graph.
Loading 1402.0897v2…