Towards nominal computation

Abstract

Nominal sets are a different kind of set theory, with a more relaxed notion of finiteness. They offer an elegant formalism for describing lambda-terms modulo alpha-conversion, or automata on data words. This paper is an attempt at defining computation in nominal sets. We present a rudimentary programming language, called Nlambda. The key idea is that it includes a native type for finite sets in the nominal sense. To illustrate the power of our language, we write short programs that process automata on data words.