Nominal terms extend first-order terms with binding. They lack some properties of first- and higher-order terms: Terms must be reasoned about in a context of ‘freshness assumptions’; it is not always possible to ‘choose a fresh variable symbol’ for a nominal term; it is not always possible to ‘α-convert a bound variable symbol’ or to ‘quotient by α-equivalence’; the notion of unifier is not based just on substitution. Permissive nominal terms closely resemble nominal terms but they recover these properties, and (...) in particular the ‘always fresh’ and ‘always rename’ properties. In the permissive world, freshness contexts are elided, equality is fixed, and the notion of unifier is based on substitution alone rather than on nominal terms’ notion of unification based on substitution plus extra freshness conditions. We prove that expressivity is not lost moving to the permissive case and provide an injection of nominal terms unification problems and their solutions into permissive nominal terms problems and their solutions. We investigate the relation between permissive nominal unification and higher-order pattern unification. We show how to translate permissive nominal unification problems and solutions in a sound, complete, and optimal manner, in suitable senses which we make formal. (shrink)

We consider two formalisations of the notion of a compositionalsemantics for a language, and find some equivalent statements in termsof substitutions. We prove a theorem stating necessary and sufficientconditions for the existence of a canonical compositional semanticsextending a given partial semantics, after discussing what features onewould want such an extension to have. The theorem involves someassumptions about semantical categories in the spirit of Husserl andTarski.

Nominal terms extend first-order terms with binding. They lack some properties of first- and higher-order terms: Terms must be reasoned about in a context of ‘freshness assumptions’; it is not always possible to ‘choose a fresh variable symbol’ for a nominal term; it is not always possible to ‘α-convert a bound variable symbol’ or to ‘quotient by α-equivalence’; the notion of unifier is not based just on substitution.Permissive nominal terms closely resemble nominal terms but they recover these properties, and in (...) particular the ‘always fresh’ and ‘always rename’ properties. In the permissive world, freshness contexts are elided, equality is fixed, and the notion of unifier is based on substitution alone rather than on nominal terms’ notion of unification based on substitution plus extra freshness conditions.We prove that expressivity is not lost moving to the permissive case and provide an injection of nominal terms unification problems and their solutions into permissive nominal terms problems and their solutions.We investigate the relation between permissive nominal unification and higher-order pattern unification. We show how to translate permissive nominal unification problems and solutions in a sound, complete, and optimal manner, in suitable senses which we make formal. (shrink)

Nominal logic is a variant of first-order logic in which abstract syntax with names and binding is formalized in terms of two basic operations: name-swapping and freshness. It relies on two important principles: equivariance (validity is preserved by name-swapping), and fresh name generation ("new" or fresh names can always be chosen). It is inspired by a particular class of models for abstract syntax trees involving names and binding, drawing on ideas from Fraenkel-Mostowski set theory: finite-support models in which each value (...) can depend on only finitely many names. Although nominal logic is sound with respect to such models, it is not complete. In this paper we review nominal logic and show why finite-support models are insufficient both in theory and practice. We then identify (up to isomorphism) the class of models with respect to which nominal logic is complete: ideal-supported models in which the supports of values are elements of a proper ideal on the set of names. We also investigate an appropriate generalization of Herbrand models to nominal logic. After adjusting the syntax of nominal logic to include constants denoting names, we generalize universal theories to nominal-universal theories and prove that each such theory has an Herbrand model. (shrink)