Nominal C-Unification

TL;DR

This paper introduces a sound and complete procedure for nominal C-unification, extending unification to include commutative operators within the nominal framework, formalized in Coq.

Contribution

It presents the first formalized, sound, and complete algorithm for nominal C-unification that handles commutative operators and transforms problems into fixpoint problems.

Findings

Formalized in Coq for correctness

Transforms problems into fixpoint problems

Provides algebraic solution techniques

Abstract

Nominal unification is an extension of first-order unification that takes into account the \alpha-equivalence relation generated by binding operators, following the nominal approach. We propose a sound and complete procedure for nominal unification with commutative operators, or nominal C-unification for short, which has been formalised in Coq. The procedure transforms nominal C-unification problems into simpler (finite families) of fixpoint problems, whose solutions can be generated by algebraic techniques on combinatorics of permutations.