nLab nominal set

Idea

A nominal set is a formalization of the idea of a set whose elements can have “variables” or “atoms” in them. Nominal sets are used in computer science to formalize notions of bound variables and alpha-equivalence.

Definition

A nominal set is an object of the Schanuel topos. One concrete description of this topos is that it is the category of G-sets for the group of permutations of the natural numbers topologized as a subspace of the Baire space of sequences. The continuity can be described as the finite support property below.

A nominal set is a set XX with an action of the group of permutations of natural numbers such that each element has finite support: for each xXx \in X there is some finite subset supp(x)Nsupp(x) \subseteq N such that if π\pi fixes supp(x)supp(x) then πx=x\pi \cdot x = x.

References

Related nnLab entries include Schanuel topos,

A survey:

  • Murdoch J. Gabbay, Foundations of nominal techniques: logic and semantics of variables in abstract syntax. Bulletin of Symbolic Logic 17:2, June 2011, 161-229

  • Wikipedia, Nominal techniques

In computer science, nominal sets were introduced in

  • Murdoch James Gabbay, A theory of inductive definitions with alpha-equivalence, PhD thesis, Cambridge 2001, pdf

See also

  • A. M. Pitts, Nominal sets, Cambridge University Press 2013

  • Daniela Petrisan, Algebra and topology over nominal sets, PhD thesis, Leicester 2010, pdf

  • M. J. Gabbay, A. M. Pitts, A NEW approach to abstract syntax with variable binding, Formal Aspects of Computing 13 (2002) pp.341-363. (draft)

Last revised on May 17, 2023 at 14:50:35. See the history of this page for a list of all contributions to it.