Locally Nameless Sets


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: