首页/论文/1102.3129

arXiv 1102.31292011-02cs.LOcs.AIcs.CCcs.PL

基于依赖对方法的自动复杂性分析

Automated Complexity Analysis Based on the Dependency Pair Method

Japan Advanced Institute of Science and Technology（日本北陆先端科学技术大学院大学）；University of Innsbruck（因斯布鲁克大学）

Nao Hirokawa, Georg Moser

备注：: 37 pages, submitted to Information & Computation

阅读 PDF ↗

arXiv 页面 ↗HTML 原文 ↗

摘要英文摘要相关论文

摘要：

本文关注的是术语重写系统的自动复杂性分析。由于这些系统是声明式编程的基础，因此重写系统定义的函数的时间复杂度特别令人感兴趣。在其他结果中，我们提出了一个变种的依赖对方法分析运行时的复杂性，长期重写系统自动。已建立的结果显着程度以前已知的技术：我们给出的重写系统的例子，我们的方法，以前不能自动分析。此外，这些技术已经在蒂罗尔复杂性工具中实现。我们提供了大量的数值数据评估的可行性的方法。

英文摘要：

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 been implemented in the Tyrolean Complexity Tool. We provide ample numerical data for assessing the viability of the method.

机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。

阅读原文

阅读 PDF ↗

arXiv 页面 ↗HTML 原文 ↗

本文内容

摘要英文摘要相关论文

机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。

继续探索

相关论文

依赖对方法引起的导数复杂性

The Derivational Complexity Induced by the Dependency Pair Method

University of Innsbruck（因斯布鲁克大学）

我们研究了依赖对方法引起的衍生复杂性，增强了标准的改进。我们得到的依赖对方法的基础技术的派生复杂性方面的派生复杂性的上界。特别是，我们表明，衍生复杂性的依赖对方法的基础上，一些直接的技术，可能细化参数过滤，可用的规则标准，或依赖图，是原始递归的衍生复杂性的直接方法。这意味着基于传统终止顺序（如KBO、LPO和MPO）的依赖对方法的标准应用所引起的推导复杂度与这些顺序作为唯一终止技术应用时完全相同。

2011-07-11cs.AIcs.CCcs.LO

禁止模式重写的终止与自动合成

Termination of Rewriting with and Automated Synthesis of Forbidden Patterns

我们介绍了一个修改后的版本，著名的依赖对框架，是适合于禁止模式限制下的重写终止分析。通过将上下文附加到表示相应递归函数调用的调用上下文的依赖对，可以将禁止模式限制合并到依赖对链的（适应的）概念中，从而产生可靠且完整的终止分析方法。建立在这个上下文依赖对框架，我们引入了一个依赖对处理器，通过分析依赖对的上下文信息，简化了问题。此外，我们展示了如何使用这个处理器来合成禁止模式适合于一个给定的长期重写系统的飞行在终止分析。

2010-12-27cs.LO

依赖对框架中的终止性证明可能导致多重递归导数复杂性

Termination Proofs in the Dependency Pair Framework May Induce Multiple Recursive Derivational Complexity

我们研究了重写系统的衍生复杂性，其终止是可证明的依赖对框架中使用的处理器减少对，依赖图，或子项标准。我们证明了这样的系统的衍生复杂性是有界的多重递归函数，提供的衍生复杂性所采用的基本技术是最多的多重递归。此外，我们证明了这个上界是紧的。

2011-03-25cs.LO

概率项重写的期望最内层运行时复杂度与强几乎必然终止的依赖对方法

Dependency Pairs for Expected Innermost Runtime Complexity and Strong Almost-Sure Termination of Probabilistic Term Rewriting

本文提出首个用于概率项重写系统最内层重写的依赖对框架，以分析期望复杂度并证明强几乎必然终止，并在AProVE中实现，展示了其优势。

2025-10-15cs.LO

On the Parameterized Complexity of Synthesizing Boolean Petri Nets With Restricted Dependency (Technical Report)

The problem of $τ$-synthesis consists in deciding whether a given directed labeled graph $A$ is isomorphic to the reachability graph of a Boolean Petri net $N$ of type $τ$. In case of a positive decision, $N$ should be constructed. For many Boolean types of nets, the problem is NP-complete. This paper deals with a special variant of $τ$-synthesis that imposes restrictions for the target net $N$: we investigate \emph{dependency $d$-restricted $τ$-synthesis (DR$τ$S)} where each place of $N$ can influence and be influenced by at most $d$ transitions. For a type $τ$, if $τ$-synthesis is NP-complet…

2020-07-24cs.CCcs.LO

高阶重写系统中的参数过滤和可用规则

Argument filterings and usable rules in higher-order rewrite systems

静态依赖对方法是一种证明高阶重写系统可终止性的方法。它结合了一阶重写系统中引入的依赖对方法和类型化可重写演算中引入的强可计算性概念。参数过滤和可用规则是当前一阶自动终止证明器使用的依赖对框架的两个重要方法。在本文中，我们扩展了一类高阶系统上的静态依赖对方法可以应用。然后，我们扩展参数过滤和可用的规则，高阶重写，从而提供了一个强大的自动终止证明高阶重写系统的基础。

2011-09-20cs.LO

更多相关论文收起更多论文

相依对与多项式路序

Dependency Pairs and Polynomial Path Orders

我们展示了如何多项式路径顺序可以有效地结合弱最内层依赖对自动认证多项式的长期重写系统的运行时复杂性和计算的函数的多时间可计算性。所建立的技术已经实施，我们提供了充足的实验数据来评估新方法。

2011-06-08cs.AIcs.CCcs.LO

Dependency Pairs Termination in Dependent Type Theory Modulo Rewriting

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.

2019-10-22cs.LO

Automated Sized-Type Inference and Complexity Analysis

This paper introduces a new methodology for the complexity analysis of higher-order functional programs, which is based on three components: a powerful type system for size analysis and a sound type inference procedure for it, a ticking monadic transformation and a concrete tool for constraint solving. Noticeably, the presented methodology can be fully automated, and is able to analyse a series of examples which cannot be handled by most competitor methodologies. This is possible due to various key ingredients, and in particular an abstract index language and index polymorphism at higher ranks…

2017-04-19cs.LOcs.PL

带注释的依赖对用于概率项重写的完全几乎必然终止

Annotated Dependency Pairs for Full Almost-Sure Termination of Probabilistic Term Rewriting

本文改进带注释的依赖对框架，将概率项重写的几乎必然终止分析从最内层策略扩展到完全重写，并细化基本项场景，在AProVE中实现验证。

2025-01-22cs.LO

A Novel Loop Fission Technique Inspired by Implicit Computational Complexity

This work explores an unexpected application of Implicit Computational Complexity (ICC) to parallelize loops in imperative programs. Thanks to a lightweight dependency analysis, our algorithm allows splitting a loop into multiple loops that can be run in parallel, resulting in gains in terms of execution time similar to state-of-the-art automatic parallelization tools when both are applicable. Our graph-based algorithm is intuitive, language-agnostic, proven correct, and applicable to all types of loops, even if their loop iteration space is unknown statically or at compile time, if they are n…

2022-05-18cs.LOcs.PL

通过三角弱非线性循环实现整数程序的自动化复杂度分析（WST短篇版本）

Automated Complexity Analysis of Integer Programs via Triangular Weakly Non-Linear Loops (Short WST Version)

本研究提出一种模块化方法，将三角弱非线性循环的运行时间界研究成果用于整数程序复杂度分析，通过计算子程序局部界并提升为全局界，实现了现有顶尖工具无法完成的复杂度分析。

2023-07-19cs.LO

一种具有相似证明复杂度的证明练习自动生成功方法

A method for the automated generation of proof exercises with comparable levels of proving complexity

University of Brasília（巴西利亚大学）；Federal University of Santa Catarina（圣卡塔琳娜联邦大学）；Metrópole Digital Institute, Federal University of Rio Grande do Norte（北里奥格兰德联邦大学大都市数字研究所）

本文提出了一种自动生成功具有相似证明复杂度的证明练习的方法，通过分析规则和表aux证明结构来实现。

2026-03-07cs.LO

面向自动推理器复杂性分析的自动化推理工具

Towards an Automated Reasoning Tool for Complexity Analysis of Automated Reasoners

Universidad Politécnica de Madrid (UPM)（马德里理工大学）；IMDEA Software Institute（IMDEA软件研究所）；Spanish Council for Scientific Research (CSIC)（西班牙国家研究委员会）；Computer Science Laboratory of Sorbonne University (LIP6)（索邦大学计算机科学实验室）；STMicroelectronics（意法半导体）

提出一种自动化工具，通过高阶抽象解释和递归方程求解，简化自动推理领域复杂算法的复杂度分析，支持用户提供关键度量和引理。

2026-06-23cs.LO

有限复杂度饱和序的自动综合

Automated Synthesis of a Finite Complexity Ordering for Saturation

本文提出了一种新的方法来饱和一组子句，使得A < B对每个原子A和B都蕴涵Var（A）{ \subseteq } Var（B）.这个条件是由任何原子排序与字典序，递归，或多集路径排序项兼容。我们的饱和过程是基于先验有序分辨率和其主要的新颖性是在飞行中建设的有限复杂性原子排序。与通常的冗余相反，我们给出了一个新的冗余概念，并证明了在饱和期间，先验有序分辨率的非冗余推理也是后验有序分辨率的推理。我们还证明了，如果一组S的条款是饱和的原子排序如上所述，那么一个条款C是否从S是可判定的问题。

2012-03-11cs.LO

Dependency-based Compositional Synthesis (Full Version)

Despite many recent advances, reactive synthesis is still not really a practical technique. The grand challenge is to scale from small transition systems, where synthesis performs well, to complex multi-component designs. Compositional methods, such as the construction of dominant strategies for individual components, reduce the complexity significantly, but are usually not applicable without extensively rewriting the specification. In this paper, we present a refinement of compositional synthesis that does not require such an intervention. Our algorithm decomposes the system into a sequence o…

2020-10-08cs.LO

Type-Based Analysis of Logarithmic Amortised Complexity

We introduce a novel amortised resource analysis couched in a type-and-effect system. Our analysis is formulated in terms of the physicist's method of amortised analysis, and is potential-based. The type system makes use of logarithmic potential functions and is the first such system to exhibit *logarithmic amortised complexity*. With our approach we target the automated analysis of self-adjusting data structures, like splay trees, which so far have only manually been analysed in the literature. In particular, we have implemented a semi-automated prototype, which successfully analyses the zig-…

2021-01-31cs.LOcs.PL

目标完整性：整数程序的自动化复杂性分析

Targeting Completeness: Automated Complexity Analysis of Integer Programs

本文研究周期性有理可解循环（prs-loops）子类，提出模块化方法计算局部边界并提升为全局边界，结合程序转换技术扩大适用范围，在KoAT工具中实现并验证了对整数程序自动化复杂性分析的完整性。

2025-08-12cs.LO

Automated Amortised Resource Analysis for Term Rewrite Systems

In this paper we establish an automated amortised resource analysis for term rewrite systems. The method is presented in an annotated type system and gives rise to polynomial bounds on the innermost runtime complexity of the analysed term rewrite system. Our analysis does not restrict the input rewrite system in any way so that rewrite systems may serve as abstractions of first-order, eagerly evaluated functional programs over user-defined inductive data-types. This facilitates integration in a general framework for resource analysis of programs. In particular, we have implemented the method a…

2018-11-22cs.LO

具有两种类型确定描述的描述逻辑：复杂性、表达性和自动推理

Description Logics with Two Types of Definite Descriptions: Complexity, Expressiveness, and Automated Deduction

本文提出两种扩展描述逻辑ALC的确定描述变体，分析其复杂性、表达性及自动推理方法，展示ALCι_G在表达性上的优势及实现的有效性。

2025-12-07cs.LO