Repository logo
 

Locally Nameless Sets

Published version
Peer-reviewed

Type

Article

Change log

Abstract

jats:p This paper provides a new mathematical foundation for the locally nameless representation of syntax with binders, one informed by nominal techniques. It gives an equational axiomatization of two key locally nameless operations, "variable opening" and "variable closing" and shows that a lot of the locally nameless infrastructure can be defined from that in a syntax-independent way, including crucially a "shift" functor for name binding. That functor operates on a category whose objects we call jats:italiclocally nameless sets</jats:italic> . Functors combining shift with sums and products have initial algebras that recover the usual locally nameless representation of syntax with binders in the finitary case. We demonstrate this by uniformly constructing such an initial locally nameless set for each instance of Plotkin's notion of binding signature. We also show by example that the shift functor is useful for locally nameless sets of a semantic rather than a syntactic character. The category of locally nameless sets is proved to be isomorphic to a known topos of finitely supported M-sets, where M is the full transformation monoid on a countably infinite set. A corollary of the proof is that several categories that have been used in the literature to model variable renaming operations on syntax with binders are all equivalent to each other and to the category of locally nameless sets. </jats:p>

Description

Keywords

name binding, locally nameless, metatheory of syntax, cofinite quantification, category theory, initial algebra, Agda

Journal Title

Proceedings of the ACM on Programming Languages

Conference Name

Journal ISSN

2475-1421
2475-1421

Volume Title

7

Publisher

Association for Computing Machinery (ACM)
Relationships
Is supplemented by: