Generalization techniques have many applications, including template construction, argument generalization, and indexing. Modern interactive provers can exploit advancement in generalization methods over expressive type theories to further develop proof generalization techniques and other transformations. So far, investigations concerned with anti-unification (AU) over $\lambda$-terms and similar type theories have focused on developing algorithms for well-studied variants. These variants forbid the nesting of generalization variables, restrict the structure of their arguments, and are \textit{unitary}. Extending these methods to more expressive variants is important to applications. We consider the case of nested generalization variables and show that the AU problem is \textit{nullary} (using \textit{capture-avoiding} substitutions), even when the arguments to free variables are severely restricted.

翻译：泛化技术有许多应用，包括模板构造、参数泛化和索引。现代交互式证明器可以利用表达性类型理论上泛化方法的进步，进一步开发证明泛化技术及其他变换。迄今为止，关于λ项及类似类型理论上反统一（AU）的研究，主要集中于为已深入研究的变体开发算法。这些变体禁止泛化变量的嵌套，限制其参数的结构，并且是*单元*的。将这些方法扩展到更具表达性的变体对于应用至关重要。我们考虑了嵌套泛化变量的情况，并表明即使自由变量的参数受到严格限制，AU问题也是*零元*的（使用*避免捕获*替换）。