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.

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