Mathematical Structures in Computer Science


Two-level nominal sets and semantic nominal terms: an extension of nominal set theory for handling meta-variables


a1 School of Mathematical and Computer Sciences, Heriot-Watt University, Edinburgh, Scotland


Nominal sets are a sets-based first-order denotation for variables in logic and programming. In this paper we extend nominal sets to two-level nominal sets. These preserve much of the behaviour of nominal sets, including notions of variable and abstraction, but they include a denotation for both variables and meta-variables. Meta-variables are interpreted as infinite lists of distinct variable symbols. We use two-level sets to define, amongst other things, a denotation for meta-variable abstraction, and nominal style datatypes of syntax-with-binding with meta-variables. We discuss the connections between this and nominal terms and prove a soundness result.

(Received August 01 2010)

(Revised February 07 2011)

(Online publication May 27 2011)