Nominal Matching Logic with Fixpoints

This paper introduces Nominal Matching Logic (NML) and its extension with fixpoint operators, presenting a formalization of nominal logic as a matching logic theory. Published at CPP 2025 (the 14th ACM SIGPLAN International Conference on Certified Programs and Proofs), the work addresses the challenge of specifying and reasoning about programming languages and formal systems that feature binders --- constructs that introduce bound variables, such as $\lambda$-abstraction, universal quantification, and channel restriction. Nominal logic, developed by Gabbay and Pitts, provides powerful principles for reasoning about names and binding, including name swapping ($(a\; b) \cdot t$, the simultaneous transposition of names $a$ and $b$ throughout $t$), freshness ($a \# t$, asserting $a$ is not free in $t$), and the $\mathbf{N}$ (new-name) quantifier ($\mathbf{N} a.\, \varphi$). This paper shows that all of nominal logic can be faithfully embedded within matching logic, obtaining a theory called NLML (Nominal Logic as Matching Logic). The key technical contribution is showing that when NLML is extended with set variables and fixpoint operators (specifically the $\mu$-binder from matching $\mu$-logic), an $\alpha$-structural induction principle for any nominal binding signature can be derived. This induction principle is essential for proving properties of languages with binders, such as type preservation, confluence, and normalization of the $\lambda$-calculus.

Programming languages universally feature binding constructs: function definitions bind parameters, let-expressions bind local variables, quantifiers bind logical variables, and pattern matching binds pattern variables. Formally reasoning about programs and languages requires a rigorous treatment of these binders, which involves managing $\alpha$-equivalence (the principle that the choice of bound variable name is irrelevant), capture-avoiding substitution $t[s/x]$ (ensuring that free variables are not accidentally captured when substituting under a binder), and freshness (the ability to choose a variable name that does not conflict with existing names). The nominal approach, pioneered by Gabbay and Pitts in their foundational work on nominal sets, provides an elegant mathematical framework for these concepts based on the idea of name permutations and the finite support principle.

In the nominal approach, names (or atoms) are elements of a countably infinite set, and the key operation is swapping two names throughout a term or structure. A name $a$ is fresh for an object $x$ (written $a \# x$) if swapping $a$ with any other fresh name leaves $x$ unchanged. The $\mathbf{N}$ quantifier ($\mathbf{N} a.\, \varphi$), read "for some new $a$, $\varphi$ holds," asserts the existence of a fresh name satisfying a property. Nominal logic has been successfully applied in proof assistants (notably Nominal Isabelle) and has led to powerful induction principles for reasoning about abstract syntax with binding. However, nominal logic has traditionally existed as a standalone formalism, separate from the matching logic ecosystem that underpins the K framework for programming language semantics. This paper bridges that gap by embedding nominal logic within matching logic, thereby making nominal reasoning techniques available within the K framework and its associated verification tools.

Nominal sets provide the mathematical semantics for nominal logic. A nominal set is a set $X$ equipped with a group action of the group of finite permutations of names (the symmetric group $\mathfrak{S}$) on $X$, satisfying the finite support condition: every element $x \in X$ has a finite set of names $\text{supp}(x)$ such that any permutation fixing all names in $\text{supp}(x)$ also fixes $x$. Intuitively, $\text{supp}(x)$ is the set of "free names" of $x$. The freshness relation $a \# x$ holds when $a \notin \text{supp}(x)$, meaning that the name $a$ does not appear "free" in $x$.

The key constructions in nominal sets include the name-abstraction $[a]x$, which represents the equivalence class of pairs $(a, x)$ modulo $\alpha$-equivalence. Formally, $[a]x = [b]y$ if and only if there exists a fresh name $c$ such that $(c\; a) \cdot x = (c\; b) \cdot y$, where $(c\; a)$ denotes the swapping (transposition) of $c$ and $a$. The name-abstraction type $[\mathbb{A}]X$ is itself a nominal set, and it provides the mathematical model for binders. For example, the set of $\lambda$-terms modulo $\alpha$-equivalence can be defined as the initial algebra of the functor $T(X) = \mathbb{A} + X \times X + [\mathbb{A}]X$, where the three summands correspond to variables, applications, and $\lambda$-abstractions respectively. Nominal sets also support a notion of equivariance: a function $f : X \to Y$ between nominal sets is equivariant if $f(\pi \cdot x) = \pi \cdot f(x)$ for all permutations $\pi$, ensuring that $f$ treats all names uniformly.

The core technical construction of the paper is the embedding of nominal logic into matching logic, yielding the theory NLML. The matching logic signature is extended with symbols for names (atoms), name swapping, name abstraction, and the freshness predicate. Specifically, the signature includes:

• A sort $\mathsf{Name}$ for atoms/names, with constants $a, b, c, \ldots$
• A swapping operation $\mathsf{swap}(a, b, t)$, denoting the result of simultaneously swapping all occurrences of $a$ and $b$ in $t$
• A name-abstraction constructor $\mathsf{abs}(a, t)$, representing the abstraction $[a]t$
• A freshness predicate $a \# t$, defined as a matching logic pattern asserting that $a$ is not in the support of $t$

The axioms of NLML encode the properties of these operations as matching logic formulas. For example, the axiom for swapping being an involution is $\mathsf{swap}(a, b, \mathsf{swap}(a, b, t)) = t$. The axiom for $\alpha$-equivalence of name abstractions states:

$a \# t' \rightarrow (\mathsf{abs}(a, t) = \mathsf{abs}(a', \mathsf{swap}(a, a', t)))$

The freshness predicate is axiomatized to satisfy the expected properties: $a \# b$ when $a \neq b$ (freshness for distinct names), $\neg(a \# a)$ (a name is not fresh for itself), and the equivariance property $a \# t \leftrightarrow \mathsf{swap}(b, c, a) \# \mathsf{swap}(b, c, t)$. The $\mathbf{N}$ quantifier is defined in terms of the existential quantifier and freshness: $\mathbf{N} a.\, \varphi \;\equiv\; \exists a.\, (a \# \bar{x} \wedge \varphi)$, where $\bar{x}$ is the list of free variables of $\varphi$ other than $a$. The paper proves that NLML is a sound and faithful embedding of nominal logic, meaning that a judgment is provable in nominal logic if and only if the corresponding matching logic formula is provable in NLML.

The central motivation for extending NLML with fixpoint operators is the need for induction principles. Many important properties of languages with binders are proved by structural induction on terms, but because terms are considered modulo $\alpha$-equivalence, the induction principle must respect this equivalence. The standard structural induction principle does not suffice; what is needed is an $\alpha$-structural induction principle that allows the inductive hypothesis to be applied to $\alpha$-equivalent terms. In nominal logic, this takes the form:

To prove $P(t)$ for all terms $t$, it suffices to show:

• $P(a)$ for all names $a$ (variable case)
• $P(t_1) \wedge P(t_2) \rightarrow P(\mathsf{app}(t_1, t_2))$ (application case)
• For a fresh name $a$ (i.e., $a \# \bar{z}$ where $\bar{z}$ are the parameters of $P$): $P(t) \rightarrow P(\lambda a.\, t)$ (abstraction case)

The freshness side-condition in the abstraction case is what makes this an $\alpha$-structural (rather than merely structural) induction principle. By extending NLML with the least fixpoint operator $\mu X.\, \varphi$ from matching $\mu$-logic, the paper can express inductive definitions as fixpoints and derive the corresponding induction principles. The least fixpoint $\mu X.\, \varphi(X)$ is the smallest set $X$ satisfying $X = \varphi(X)$, and the associated induction principle states that for any property $P$, if $\varphi(P) \subseteq P$ then $\mu X.\, \varphi(X) \subseteq P$. The paper shows that by carefully constructing the functor $\varphi$ using the nominal constructions (particularly the $\mathbf{N}$ quantifier for the binder case), the resulting fixpoint induction principle yields exactly the $\alpha$-structural induction principle.

The derivation of the $\alpha$-structural induction principle is the main theorem of the paper. For a nominal binding signature $\Sigma$ (which specifies the constructors of the term language, indicating which arguments are names, which are terms, and which are abstractions), the paper defines the term sort $\mathsf{Term}$ as a least fixpoint:

$\mathsf{Term} \;=\; \mu X.\, \Big(\bigvee_{c \in \Sigma} \mathsf{constructor}_c(X)\Big)$

where each $\mathsf{constructor}_c(X)$ encodes the arguments of constructor $c$, using name-abstraction for binding positions. The $\alpha$-structural induction principle is then derived from the fixpoint induction rule. For the specific case of the $\lambda$-calculus, the term sort is:

$\mathsf{Term}_\lambda \;=\; \mu X.\, \Big(\mathsf{Name} \;\vee\; (X \wedge X) \;\vee\; \mathbf{N} a.\, \mathsf{abs}(a, X)\Big)$

The three disjuncts correspond to variables, applications, and $\lambda$-abstractions. The $\mathbf{N} a$ in the abstraction case ensures that the bound name $a$ is chosen fresh. From the fixpoint definition, the paper derives that for any predicate $P(t, \bar{z})$ (where $\bar{z}$ are additional parameters), if: (1) $P(a, \bar{z})$ holds for all names $a$; (2) $P(t_1, \bar{z}) \wedge P(t_2, \bar{z}) \rightarrow P(\mathsf{app}(t_1, t_2), \bar{z})$; and (3) for some fresh $a$ (i.e., $a \# \bar{z}$), $P(t, \bar{z}) \rightarrow P(\mathsf{abs}(a, t), \bar{z})$; then $P(t, \bar{z})$ holds for all terms $t$. This is precisely the $\alpha$-structural induction principle as it appears in nominal logic.

The paper illustrates the use of the derived $\alpha$-structural induction principle by proving several fundamental properties of the $\lambda$-calculus within the NLML + fixpoints framework. These include:

• Substitution lemma: The capture-avoiding substitution $t[s/x]$ is well-defined on $\alpha$-equivalence classes. The proof uses $\alpha$-structural induction on $t$, with the freshness condition in the abstraction case ensuring that the bound variable of the abstraction is chosen fresh for both $s$ and $x$, thereby avoiding capture.
• Properties of free variables: The set of free variables $\text{FV}(t)$ is well-defined and satisfies the expected equalities, such as $\text{FV}(\lambda a.\, t) = \text{FV}(t) \setminus \{a\}$ for fresh $a$.
• Size/depth properties: Structural metrics on terms (such as the depth of nesting) are well-defined modulo $\alpha$-equivalence.

These proofs demonstrate that the NLML + fixpoints framework provides a practical and rigorous foundation for reasoning about the $\lambda$-calculus and, by extension, about any language with binders whose abstract syntax can be described by a nominal binding signature. The paper notes that the proofs closely mirror informal mathematical practice, where one routinely says "choose $a$ fresh" and proceeds by induction on the structure of $\alpha$-equivalence classes.

The paper provides a detailed comparison with Nominal Isabelle, the most prominent tool for nominal reasoning in a proof assistant. Nominal Isabelle, developed by Urban and collaborators, provides an implementation of nominal logic within the Isabelle/HOL proof assistant, including automated support for defining nominal datatypes, proving equivariance lemmas, and applying the $\alpha$-structural induction principle. A key difference is that in Nominal Isabelle, the $\alpha$-structural induction principle is derived using the infrastructure of HOL (higher-order logic) and the specific axiomatization of nominal sets within Isabelle, whereas in this paper, the principle is derived purely within matching logic using the fixpoint operator.

An interesting technical difference highlighted by the paper is the treatment of freshness in the binder case of the induction principle. In Nominal Isabelle, the induction principle has built-in freshness constraints in the cases for binders: the inductive hypothesis for $\lambda a.\, t$ explicitly requires $a$ to be fresh for a specified set of parameters. In the NLML + fixpoints approach, the freshness condition emerges naturally from the $\mathbf{N}$ quantifier in the fixpoint definition, rather than being hardcoded into the induction principle. The paper argues that this provides a cleaner and more flexible treatment, though it acknowledges that Nominal Isabelle's approach has proven highly effective in practice. The paper also discusses connections with the earlier work by Chen and Rosu on defining binders using matching logic's existential quantifier, noting that the present approach using nominal logic is complementary: the existential-based approach is more syntactically lightweight, while the nominal approach provides richer reasoning principles including equivariance and the $\mathbf{N}$ quantifier.

The paper presents a proof system for NLML extended with fixpoints, building on the Hilbert-style proof system of matching $\mu$-logic. The proof system includes all the axioms and rules of matching $\mu$-logic (including the fixpoint induction rule, or Park's rule: if $\varphi[\psi/X] \rightarrow \psi$ then $\mu X.\, \varphi \rightarrow \psi$), together with the axioms of NLML for swapping, freshness, name-abstraction, and the $\mathbf{N}$ quantifier. Soundness of the proof system is established by constructing models in the category of nominal sets. Each matching logic model is built from a nominal set, where the group action of name permutations provides the semantics for the swapping operation, and the support function provides the semantics for the freshness predicate.

The least fixpoint $\mu X.\, \varphi$ is interpreted using the Knaster-Tarski theorem applied to the lattice of subsets of the nominal set, restricted to equivariant subsets (subsets that are closed under name permutations). The restriction to equivariant subsets is necessary to ensure that the fixpoint respects the nominal structure --- in particular, that the set of terms defined by the fixpoint is closed under $\alpha$-equivalence. The paper proves that all the axioms of NLML + fixpoints are sound with respect to these nominal set models, and that the derived $\alpha$-structural induction principle is a valid consequence of the fixpoint induction rule and the NLML axioms. The paper also discusses the question of completeness and notes that while full completeness of matching $\mu$-logic is an open problem in general, the specific theories considered in the paper (such as the theory of $\lambda$-terms) admit complete axiomatizations.

The paper makes a significant contribution to the theory of formal reasoning about languages with binders by showing that nominal logic can be faithfully embedded in matching logic and that the crucial $\alpha$-structural induction principle can be derived within this framework using fixpoint operators. This result has important implications for the K framework and the broader matching logic ecosystem, because it means that all the powerful nominal reasoning techniques --- including equivariance, the $\mathbf{N}$ quantifier, and $\alpha$-structural induction --- are available within matching logic without requiring any extension to the logic itself (beyond the already-established fixpoint operators of matching $\mu$-logic).

The work complements the earlier approach of Chen and Rosu (ICFP 2020) for defining binders using matching logic's existential quantifier. While that approach offers a more lightweight encoding suitable for defining operational semantics in K, the nominal approach provides richer reasoning principles that are essential for metatheoretic proofs (such as type preservation and strong normalization). Together, the two approaches give matching logic a comprehensive toolkit for handling binders, covering both the definitional and the reasoning aspects. The paper suggests several directions for future work, including mechanizing the proofs in a proof assistant, extending the approach to more complex binding patterns (such as telescopic and recursive binders), and investigating the connections with cubical type theory and homotopy type theory.