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.

翻译：高阶合一涉及$\lambda$-演算（的扩展）的合一问题，可视为在$\lambda$-项的$\beta\eta$-等价模下等式合一的一个实例。我们研究具有任意变量绑定结构的语言中项在任意二阶等式理论模下的等式合一问题。具有通用变量绑定和参数化元变量的抽象语法使我们能够在不依赖$\lambda$-演算或使用不便且易错的项编码的情况下处理任意绑定子，从而构建更灵活的框架。本文引入二阶抽象语法的E-合一，并描述此类问题的合一过程，融合了完全高阶合一与通用E-合一的思想。我们证明该过程是可靠且完备的。