Frédéric Blanqui
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 中实现验证。
In this paper we generalize the DP framework to a relative DP framework, where a so called split is possible.
We study the derivational complexity of rewrite systems whose termination is provable in the dependency pair framework using the processors for reduction pairs, dependency graphs, or the subterm criterion. We show that the derivational complexity of such systems is bounded by a multiple recursive function, provided the derivational complexity induced by the employed base techniques is at most multiple recursive. Moreover we show that this upper bound is tight.
Refinement types are a well-studied manner of performing in-depth analysis on functional programs. The dependency pair method is a very powerful method used to prove termination of rewrite systems; however its extension to higher order rewrite systems is still the object of active research. We observe that a variant of refinement types allow us to express a form of higher-order dependency pair criterion that only uses information at the type level, and we prove the correctness of this criterion.
Higher-order rewrite systems (HRSs) and simply-typed term rewriting systems (STRSs) are computational models of functional programs. We recently proposed an extremely powerful method, the static dependency pair method, which is based on the notion of strong computability, in order to prove termination in STRSs. In this paper, we extend the method to HRSs. Since HRSs include λ-abstraction but STRSs do not, we restructure the static dependency pair method to allow λ-abstraction, and show that the static dependency pair method also works well on HRSs without new restrictions.
In recent years, two higher-order extensions of the powerful dependency pair approach for termination analysis of first-order term rewriting have been defined: the static and the dynamic approach. Both approaches offer distinct advantages and disadvantages. However, a grand unifying theory is thus far missing, and both approaches lack the modularity present in the dependency pair framework commonly used in first-order rewriting. Moreover, neither approach can be used to prove non-termination. In this paper, we aim to address this gap by defining a higher-order dependency pair framework, integr…
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中实现，对比现有工具展现了其有效性。
We extend the higher-order termination method of dynamic dependency pairs to Algebraic Functional Systems (AFSs). In this setting, simply typed lambda-terms with algebraic reduction and separate β-steps are considered. For left-linear AFSs, the method is shown to be complete. For so-called local AFSs we define a variation of usable rules and an extension of argument filterings. All these techniques have been implemented in the higher-order termination tool WANDA.
Dependency pairs are a key concept at the core of modern automated termination provers for first-order term rewriting systems. In this paper, we introduce an extension of this technique for a large class of dependently-typed higher-order rewriting systems. This extends previous resultsby Wahlstedt on the one hand and the first author on the other hand to strong normalization and non-orthogonal rewriting systems. This new criterion is implemented in the type-checker Dedukti.
We introduce a modified version of the well-known dependency pair framework that is suitable for the termination analysis of rewriting under forbidden pattern restrictions. By attaching contexts to dependency pairs that represent the calling contexts of the corresponding recursive function calls, it is possible to incorporate the forbidden pattern restrictions in the (adapted) notion of dependency pair chains, thus yielding a sound and complete approach to termination analysis. Building upon this contextual dependency pair framework we introduce a dependency pair processor that simplifies prob…
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中实现以验证其效力。
Rewriting is a framework for reasoning about functional programming. The dependency pair criterion is a well-known mechanism to analyze termination of term rewriting systems. Functional specifications with an operational semantics based on evaluation are related, in the rewriting framework, to the innermost reduction relation. This paper presents a PVS formalization of the dependency pair criterion for the innermost reduction relation: a term rewriting system is innermost terminating if and only if it is terminating by the dependency pair criterion. The paper also discusses the application of …
The static dependency pair method is a method for proving the termination of higher-order rewrite systems a la Nipkow. It combines the dependency pair method introduced for first-order rewrite systems with the notion of strong computability introduced for typed lambda-calculi. Argument filterings and usable rules are two important methods of the dependency pair framework used by current state-of-the-art first-order automated termination provers. In this paper, we extend the class of higher-order systems on which the static dependency pair method can be applied. Then, we extend argument filteri…
We study the derivational complexity induced by the dependency pair method, enhanced with standard refinements. We obtain upper bounds on the derivational complexity induced by the dependency pair method in terms of the derivational complexity of the base techniques employed. In particular we show that the derivational complexity induced by the dependency pair method based on some direct technique, possibly refined by argument filtering, the usable rules criterion, or dependency graphs, is primitive recursive in the derivational complexity induced by the direct method. This implies that the de…
We show how polynomial path orders can be employed efficiently in conjunction with weak innermost dependency pairs to automatically certify polynomial runtime complexity of term rewrite systems and the polytime computability of the functions computed. The established techniques have been implemented and we provide ample experimental data to assess the new method.
We revisit the static dependency pair method for proving termination of higher-order term rewriting and extend it in a number of ways: (1) We introduce a new rewrite formalism designed for general applicability in termination proving of higher-order rewriting, Algebraic Functional Systems with Meta-variables. (2) We provide a syntactically checkable soundness criterion to make the method applicable to a large class of rewrite systems. (3) We propose a modular dependency pair framework for this higher-order setting. (4) We introduce a fine-grained notion of formative and computable chains to re…
This article is concerned with automated complexity analysis of term rewrite systems. Since these systems underlie much of declarative programming, time complexity of functions defined by rewrite systems is of particular interest. Among other results, we present a variant of the dependency pair method for analysing runtime complexities of term rewrite systems automatically. The established results significantly extent previously known techniques: we give examples of rewrite systems subject to our methods that could previously not been analysed automatically. Furthermore, the techniques have be…
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求解器的应用程序，获得了数量级的加速，以及增加终止证明功率。
We describe a formalization of higher-order rewriting theory and formally prove that an AFS is strongly normalizing if it can be interpreted in a well-founded domain. To do so, we use Coq, which is a proof assistant based on dependent type theory. Using this formalization, one can implement several termination techniques, like the interpretation method or dependency pairs, and prove their correctness. Those implementations can then be extracted to OCaml, which results in a verified termination checker.
扫码添加微信好友，提出您的宝贵建议 👇
💡 备注请填写：网站反馈
发表机构由 AI 从论文文本抽取，如发现错误，欢迎反馈修正建议。