Strong Nominal Semantics for Fixed-Point Constraints

TL;DR

This paper extends nominal algebra with fixed-point constraints, providing a sound semantics using strong nominal sets, and explores different formulations to ensure soundness in reasoning about languages with binders.

Contribution

Introduction of fixed-point constraints into nominal algebra with two formulations to ensure sound semantics using strong nominal sets.

Findings

Fixed-point constraints extend nominal algebra.

Two formulations achieve soundness with strong nominal sets.

Counter-example shows limitations of nominal sets without constraints.

Abstract

Nominal algebra includes $\alpha$-equality and freshness constraints on nominal terms endowed with a nominal set semantics that facilitates reasoning about languages with binders. Nominal unification is decidable and unitary, however, its extension with equational axioms such as Commutativity (which has a finitary first-order unification type) is no longer finitary unless permutation fixed-point constraints are used. In this paper, we extend the notion of nominal algebra by introducing fixed-point constraints and provide a sound semantics using strong nominal sets. We show, by providing a counter-example, that the class of nominal sets is not a sound denotation for this extended nominal algebra. To recover soundness we propose two different formulations of nominal algebra, one obtained by restricting to a class of fixed-point contexts that are in direct correspondence with freshness contexts and another obtained by using a different set of derivation rules.