E-unification for Second-Order Abstract Syntax

TL;DR

This paper introduces a flexible framework for second-order unification in abstract syntax with variable binding, extending higher-order unification to arbitrary equational theories and proving the correctness of the unification procedure.

Contribution

It presents a novel unification procedure for second-order abstract syntax that merges higher-order and equational unification techniques, with proven soundness and completeness.

Findings

Developed a unification procedure for second-order abstract syntax.

Proved the procedure's soundness and completeness.

Enabled flexible handling of variable binding without specific calculus constraints.

Abstract

Higher-order unification (HOU) concerns unification of (extensions of) $\lambda$-calculus and can be seen as an instance of equational unification ($E$-unification) modulo $\beta\eta$-equivalence of $\lambda$-terms. We study equational unification of terms in languages with arbitrary variable binding constructions modulo arbitrary second-order equational theories. Abstract syntax with general variable binding and parametrised metavariables allows us to work with arbitrary binders without committing to $\lambda$-calculus or use inconvenient and error-prone term encodings, leading to a more flexible framework. In this paper, we introduce $E$-unification for second-order abstract syntax and describe a unification procedure for such problems, merging ideas from both full HOU and general $E$-unification. We prove that the procedure is sound and complete.