论文标题
一个或一无
One or Nothing: Anti-unification over the Simply-Typed Lambda Calculus
论文作者
论文摘要
概括技术具有许多应用，包括模板构建，参数概括和索引。现代互动抛弃可以利用表达类型理论的概括方法中的进步，以进一步开发证明概括技术和其他转换。到目前为止，针对$λ$ terms和类似类型的反统一（AU）的调查重点是开发研究良好变体的算法。这些变体禁止概括变量的嵌套，限制其参数的结构，并且是\ textit {unital}。将这些方法扩展到更具表现力的变体对应用程序很重要。我们考虑嵌套概括变量的情况，并表明AU问题是\ textIt {nullary}（使用\ textit {captution-aver-avoiding}替换），即使在严格限制了自由变量的参数时。
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 $λ$-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.
