Higher-order dependency pairs
Frédéric Blanqui
Arts和Giesl证明了一阶重写系统的终止可以归结为对它的“依赖对”的研究。我们扩展这些结果重写系统简单类型的可计算性技术，通过使用泰特的可计算性。
Arts and Giesl proved that the termination of a first-order rewrite system can be reduced to the study of its "dependency pairs". We extend these results to rewrite systems on simply typed lambda-terms by using Tait's computability technique.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
继续探索
Higher-Order Constrained Dependency Pairs for (Universal) Computability
本文将静态依赖对框架适配至逻辑约束简单类型项重写系统（LCSTRSs），并提出通用可计算性概念以实现开放世界终止性分析。
The Annotated Dependency Pair Framework for Almost-Sure Termination of Probabilistic Term Rewriting
本文将依赖对技术扩展到概率项重写系统，提出带标注依赖对框架以自动证明完全与最内层重写下的几乎必然终止性，并在 AProVE 中实现验证。
A Relative Dependency Pair Framework
在本文中，我们推广的DP框架到一个相对DP框架，其中所谓的分裂是可能的。
Termination Proofs in the Dependency Pair Framework May Induce Multiple Recursive Derivational Complexity
我们研究了重写系统的衍生复杂性，其终止是可证明的依赖对框架中使用的处理器减少对，依赖图，或子项标准。我们证明了这样的系统的衍生复杂性是有界的多重递归函数，提供的衍生复杂性所采用的基本技术是最多的多重递归。此外，我们证明了这个上界是紧的。
Refinement Types as Higher Order Dependency Pairs
细化类型是一种对函数式程序进行深入分析的方法。依赖对方法是证明重写系统可终止性的一种非常有效的方法，然而将其推广到高阶重写系统仍然是一个活跃的研究对象。我们观察到，细化类型的变体允许我们表达一种形式的高阶依赖对标准，只使用信息的类型级别，我们证明了这个标准的正确性。
Static Dependency Pair Method based on Strong Computability for Higher-Order Rewrite Systems
高阶重写系统（HRS）和简单类型项重写系统（STRS）是函数式程序的计算模型。我们最近提出了一个非常强大的方法，静态依赖对方法，这是基于强可计算性的概念，以证明终止STRS。在本文中，我们将该方法扩展到HRSs。由于HRSs包含λ-抽象而STRSs不包含λ-抽象，我们重新构造了静态依赖对方法以允许λ-抽象，并表明静态依赖对方法在没有新限制的情况下也能很好地工作在HRSs上。
The unified higher-order dependency pair framework
近年来，针对一阶项重写终止性分析的强大依赖对方法，定义了两种高阶扩展：静态方法和动态方法。这两种方法都有明显的优点和缺点。然而，一个大统一的理论是迄今为止失踪，这两种方法缺乏模块化的依赖对框架中常用的一阶重写。此外，这两种方法都不能用来证明不终止。在本文中，我们的目标是通过定义一个高阶依赖对框架，将这两种方法集成到一个共享的正式设置来解决这个差距。该框架已在（全自动）高阶终止工具WANDA中实现。
Proving Almost-Sure Innermost Termination of Probabilistic Term Rewriting Using Dependency Pairs
本文将经典依赖对框架扩展至概率项重写系统，用于证明几乎必然最内层终止性，并在 AProVE 工具中实现以验证其能力。
A Dependency Pair Framework for Relative Termination of Term Rewriting
本文提出了一种新型的标注依赖对（ADPs）框架，用于证明项重写系统的相对终止，并在工具AProVE中实现，对比现有工具展现了其有效性。
Dynamic Dependency Pairs for Algebraic Functional Systems
本文将动态依赖对的高阶终止方法推广到代数泛函系统。在这种情况下，考虑了具有代数约化和单独β-步骤的简单类型化的非线性项。对于左线性AFS，该方法是完整的。对于所谓的本地AF，我们定义了可用规则的变体和参数过滤的扩展。所有这些技术都已在高阶端接工具WANDA中实现。
Dependency Pairs Termination in Dependent Type Theory Modulo Rewriting
依赖项对是现代自动终止证明器的核心概念，用于一阶项重写系统。在本文中，我们介绍了一个扩展的依赖型高阶重写系统的一大类这种技术。这扩展了以前的结果Wahlstedt一方面和第一作者另一方面强规范化和非正交重写系统。这个新的标准在类型检查器Dedukti中实现。
Termination of Rewriting with and Automated Synthesis of Forbidden Patterns
我们介绍了一个修改后的版本，著名的依赖对框架，是适合于禁止模式限制下的重写终止分析。通过将上下文附加到表示相应递归函数调用的调用上下文的依赖对，可以将禁止模式限制合并到依赖对链的（适应的）概念中，从而产生可靠且完整的终止分析方法。建立在这个上下文依赖对框架，我们引入了一个依赖对处理器，通过分析依赖对的上下文信息，简化了问题。此外，我们展示了如何使用这个处理器来合成禁止模式适合于一个给定的长期重写系统的飞行在终止分析。
A Complete Dependency Pair Framework for Almost-Sure Innermost Termination of Probabilistic Term Rewriting
本文针对概率项重写系统的 iAST 问题，重新定义依赖对并引入新转换，将不完备的依赖元组方法发展为完备的概率 DP 框架，且在 AProVE 中验证其证明能力显著提升。
Dependency Pairs for Expected Innermost Runtime Complexity and Strong Almost-Sure Termination of Probabilistic Term Rewriting
本文提出首个用于概率项重写系统最内层重写的依赖对框架，以分析期望复杂度并证明强几乎必然终止，并在AProVE中实现，展示了其优势。
Annotated Dependency Pairs for Full Almost-Sure Termination of Probabilistic Term Rewriting
本文改进带注释的依赖对框架，将概率项重写的几乎必然终止分析从最内层策略扩展到完全重写，并细化基本项场景，在AProVE中实现验证。
Dependency Tuples for Almost-Sure Innermost Termination of Probabilistic Term Rewriting (Short WST Version)
本研究将依赖对框架适配至概率场景，提出用于证明概率项重写系统几乎必然最内层终止的依赖元组方法，并在工具AProVE中实现以验证其效力。
Formalizing the Dependency Pair Criterion for Innermost Termination
重写是一个推理函数式编程的框架。依赖对准则是一种众所周知的分析术语重写系统终止的机制。在重写框架中，具有基于评估的操作语义的功能规范与最内层的归约关系相关。本文给出了最内层约简关系的依赖对准则的PVS形式化：一个项重写系统是最内层可终止的当且仅当它被依赖对准则终止。本文还讨论了该准则在功能规格说明终止性检查中的应用。
Argument filterings and usable rules in higher-order rewrite systems
静态依赖对方法是一种证明高阶重写系统可终止性的方法。它结合了一阶重写系统中引入的依赖对方法和类型化可重写演算中引入的强可计算性概念。参数过滤和可用规则是当前一阶自动终止证明器使用的依赖对框架的两个重要方法。在本文中，我们扩展了一类高阶系统上的静态依赖对方法可以应用。然后，我们扩展参数过滤和可用的规则，高阶重写，从而提供了一个强大的自动终止证明高阶重写系统的基础。
The Derivational Complexity Induced by the Dependency Pair Method
我们研究了依赖对方法引起的衍生复杂性，增强了标准的改进。我们得到的依赖对方法的基础技术的派生复杂性方面的派生复杂性的上界。特别是，我们表明，衍生复杂性的依赖对方法的基础上，一些直接的技术，可能细化参数过滤，可用的规则标准，或依赖图，是原始递归的衍生复杂性的直接方法。这意味着基于传统终止顺序（如KBO、LPO和MPO）的依赖对方法的标准应用所引起的推导复杂度与这些顺序作为唯一终止技术应用时完全相同。
Dependency Pairs and Polynomial Path Orders
我们展示了如何多项式路径顺序可以有效地结合弱最内层依赖对自动认证多项式的长期重写系统的运行时复杂性和计算的函数的多时间可计算性。所建立的技术已经实施，我们提供了充足的实验数据来评估新方法。
A static higher-order dependency pair framework
我们重新审视了证明高阶项重写终止性的静态依赖对方法，并在许多方面对其进行了扩展：（1）我们引入了一种新的重写形式主义，设计用于高阶重写的终止性证明，具有元变量的代数泛函系统。(2)我们提供了一个语法检查的合理性标准，使该方法适用于一个大类的重写系统。(3)我们提出了一个模块化的依赖对框架，这种高阶设置。(4)我们引入了一个细粒度的概念，形成和可计算的链，使框架更强大。(5)我们制定了几个现有的和新的终止证明技术在我们的框架内的处理器的形式。该框架已在（全自动）高阶终止工具WANDA中实现。
Automated Complexity Analysis Based on the Dependency Pair Method
本文关注的是术语重写系统的自动复杂性分析。由于这些系统是声明式编程的基础，因此重写系统定义的函数的时间复杂度特别令人感兴趣。在其他结果中，我们提出了一个变种的依赖对方法分析运行时的复杂性，长期重写系统自动。已建立的结果显着程度以前已知的技术：我们给出的重写系统的例子，我们的方法，以前不能自动分析。此外，这些技术已经在蒂罗尔复杂性工具中实现。我们提供了大量的数值数据评估的可行性的方法。
Termination of Innermost-Terminating Right-Linear Overlay Term Rewrite Systems
本文证明右线性覆盖项重写系统终止当且仅当内most终止，通过模拟性质展示无限最小依赖对链的等价性。
On Singleton Self-Loop Removal for Termination of LCTRSs with Bit-Vector Arithmetic
本文针对带位向量算术的逻辑约束项重写系统，提出一种基于有向无环图的依赖对处理器，以解决单例自环依赖对问题，并给出无环图存在的充分条件及特定情况下的简化。
SAT Solving for Argument Filterings
本文介绍了一种与依赖对有关的字典式路径序的命题编码。这有利于SAT求解器的终止性分析的术语重写系统的依赖对方法的基础上的应用。我们解决两个主要的相互关联的问题，并将它们编码为命题公式的可满足性问题，可以有效地处理SAT解决：（1）字典路径顺序与\emph{argument filtering}一起定向一组不等式的组合搜索;（2）参数过滤的选择如何影响必须定向的一组不等式。我们已经在终止证明程序AProVE中实现了我们的贡献。大量的实验表明，通过我们的编码和SAT求解器的应用程序，获得了数量级的加速，以及增加终止证明功率。
Formalizing Higher-Order Termination in Coq
我们描述了高阶重写理论的形式化，并正式证明了AFS是强规范化的，如果它可以解释在一个良好的基础域。为此，我们使用Coq，它是一个基于依赖类型论的证明助手。使用这种形式化，可以实现几种终止技术，如解释方法或依赖对，并证明它们的正确性。然后可以将这些实现提取到OCaml中，这会产生经过验证的终止检查器。
扫码添加微信好友，提出您的宝贵建议 👇
💡 备注请填写：网站反馈
发表机构由 AI 从论文文本抽取，如发现错误，欢迎反馈修正建议。