Murdoch J Gabbay and Martin Hofmann (2008)

# Nominal Renaming Sets

In: Logic for Programming, Artificial Intelligence, and Reasoning, 15th International Conference, LPAR 2008, Doha, Qatar, November 22-27, 2008. Proceedings, ed. by Iliano Cervesato and Helmut Veith and Andrei Voronkov, vol. 5330, pp. 158-173, Springer. Lecture Notes in Computer Science (ISBN: 978-3-540-89438-4).

Nominal techniques are based on the idea of sets with a finitelysupported atoms-permutation action. We consider the idea of nominal renaming sets, which are sets with a finitelysupported atoms-renaming action; renamings can identify atoms, permutations cannot. We show that nominal$~$ renaming sets exhibit many of the useful qualities found in (permutative) nominal sets; an elementary sets-based presentation, inductive datatypes of syntax up to binding, cartesian closure,$~$ and being a topos. Unlike is the case for nominal sets, the notion of names-abstraction coincides with functional abstraction. Thus we obtain a concrete presentation of sheaves on the category of finite sets in the form of a category of sets with structure.

Document Actions