Equivariant and Nominal SOS (Abstract)
Many kinds of names occurring in programming languages and logical
calculi are "atomic", in the sense that the structure of a name is
immaterial: all that matters are distinctions between names and the
association of names to the things named. One says that a semantic
construct involving such atomic names is "equivariant" if its meaning
is preserved under the operation of permuting the atoms. A simple, but
useful, result about finitary inductive definitions shows that
equivariant relations already abound for structural operational
semantics carried out in ordinary (naive) set theory. However, to
really exploit the power of this permutation-oriented viewpoint for
general inductive and co-inductive definitions (such as occur in
concurrency theory) and for modelling locality and abstraction of
names, requires a modest change of foundation to "nominal sets". This
is a mathematical framework with names as atoms that makes
equivariance ubiquitous and can express the crucial property of
"freshness" of names in a syntax-independent way.
Last modified: Tue Aug 31 09:54:04 BST 2004