A unifying model of variables and names

We investigate a category theoretic model where both “variables” and “names”, usually viewed as separate notions, are particular cases of the more general notion of distinction. The key aspect of this model is to consider functors over the category of irreflexive, symmetric finite relations. The models previously proposed for the notions of “variables” and “names” embed faithfully in the new one, and initial algebra/final coalgebra constructions can be transferred from the formers to the latter. Moreover, the new model admits a definition of distinction-aware simultaneous substitutions. As a substantial application example, we give the first semantic interpretation of Miller-Tiu’s FO-lambda-nabla logic.