Exact Unification and Admissibility

TL;DR

This paper introduces a new hierarchy of 'exact' unification types based on inclusion of unified identities, leading to smaller unifier sets and significant simplifications in certain algebraic classes.

Contribution

It defines and analyzes a novel 'exact' unification preordering that reduces unifier set sizes compared to standard methods, with algebraic interpretation inspired by Ghilardi's approach.

Findings

Exact unification often yields smaller unifier sets.

Classes with nullary unification type can have unitary or finitary exact type.

Significant reduction in unifier set size observed in key algebraic classes.

Abstract

A new hierarchy of "exact" unification types is introduced, motivated by the study of admissible rules for equational classes and non-classical logics. In this setting, unifiers of identities in an equational class are preordered, not by instantiation, but rather by inclusion over the corresponding sets of unified identities. Minimal complete sets of unifiers under this new preordering always have a smaller or equal cardinality than those provided by the standard instantiation preordering, and in significant cases a dramatic reduction may be observed. In particular, the classes of distributive lattices, idempotent semigroups, and MV-algebras, which all have nullary unification type, have unitary or finitary exact type. These results are obtained via an algebraic interpretation of exact unification, inspired by Ghilardi's algebraic approach to equational unification.