Regular Expressions with Dynamic Name Binding

Abstract

Nominal Kleene algebra (NKA) is a formalism to specify trace languages with name generation; it extends standard regular expressions with a name binding construct. NKA has been proved complete over a natural nominal language model. Moreover, it has been shown that NKA expressions can be translated into a species of nondeterministic nominal automata, thus providing one half of a Kleene theorem. The other half is known to fail, i.e. there are nominal languages that can be accepted by a nominal automaton but are not definable in NKA. In the present work, we introduce a calculus of regular expressions with dynamic name binding. It satisfies the full Kleene theorem, i.e. it is equivalent to a natural species of nominal automata, and thus strictly more expressive than NKA. We show that containment checking in our calculus is decidable in EXPSPACE, and in fact has polynomial fixed-parameter space complexity. The known EXPSPACE bound for containment of NKA expressions follows.