Dependency Pairs for Expected Innermost Runtime Complexity and Strong Almost-Sure Termination of Probabilistic Term Rewriting
本文提出首个用于概率项重写系统最内层重写的依赖对框架，以分析期望复杂度并证明强几乎必然终止，并在AProVE中实现，展示了其优势。
2025-10-15 cs.LO
Complexity of Conditional Term Rewriting
我们提出了一个面向条件项重写系统满足一定的限制复杂性的概念。这个概念是现实的，因为它不仅测量成功的计算，而且测量导致失败的规则应用程序的部分计算。无条件的上下文敏感的重写系统的转换，反映了这种复杂性的概念，以及一种技术，以获得运行时和派生的复杂性界限，这种转换的结果。
2017-03-22 cs.LO
A Modular Lean 4 Framework for Confluence and Strong Normalization of Lambda Calculi with Products and Sums
Microsoft（微软）；Centro de Informática, Universidade Federal de Pernambuco（伯南布哥联邦大学计算机中心）；Departamento de Matemática, Universidade Federal Rural de Pernambuco（伯南布哥联邦农村大学数学系）
本文提出了一种模块化Lean 4框架，用于证明λ演算及其扩展的连通性和强规范性，通过三种经典证明技术实现，并展示了完整的机械证明。
2025-12-10 cs.LO
Efficient Implementation of Rewriting Revisited Technical Report
最近，已经引入了许多技术，允许（自动化）的术语重写系统（TRS）的运行时复杂性的分类。在早期的工作中，作者已经表明，对于合流TRS，最内层多项式运行时复杂性导致定义的函数的多时间可计算性。本文将上述结果推广到完全重写。根据我们以前的工作，我们利用图重写。我们给出了一个新的证明充分重写，允许一个精确的控制复制的资源图重写。总之，我们完整地描述了重写的图灵机（简称TM）上的实现。我们表明，TRS的运行时复杂性和TM的运行时复杂性是多项式相关的。我们的结果加强了重写系统的复杂性是真实地表示通过推导的长度的证据。此外，我们的结果允许分类的非确定性多时间计算的基础上的重写系统的运行时复杂性分析。
2011-06-08 cs.CC cs.LO
Analysing Parallel Complexity of Term Rewriting
我们重新审视并行最里面的长期重写作为一个模型的并行计算归纳数据结构，并提供了相应的概念的运行时复杂度参数的大小的开始长期。我们提出了自动技术，以获得上界和下界的并行重写的复杂性，使现有的技术的顺序复杂性的直接重用。该方法的适用性和精度证明了相对较轻的努力，在扩展的程序分析工具AProVE和众多的基准从文献中的实验。
2022-08-01 cs.LO cs.PL
Exponential Lower Bounds and Separation for Query Rewriting
我们建立连接的电路和计算单调布尔函数的公式的大小和一阶和非递归的数据重写OWL 2 QL本体的合取查询的大小之间。我们使用已知的下限和分离结果从电路复杂性证明类似的结果，不使用非签名常数的重写的大小。例如，我们表明，在最坏的情况下，积极的存在和非递归的数据库重写是指数比原来的查询更长;非递归的数据库重写一般指数比积极的存在重写更简洁;而一阶重写可以是超多项式比积极的存在重写更简洁。
2012-05-13 cs.LO
Runtime Complexity Analysis of Logically Constrained Rewriting
逻辑约束重写系统（LCTRS）是一种通用且高效的重写形式主义，可用于从各种编程范式建模程序，以及编译器和SMT求解器中的简化系统。在本文中，我们研究技术来分析最坏情况下的运行时复杂性的LCTRS。为此，我们利用以前开发的分解技术之间的协同作用，由Avanzini等人重写的标准项。与交替的时间和大小的整数程序的边界近似Brockschloven等人。并适应这些技术适当的LCTRS。此外，我们提供了新的模块化技术，利用循环边界的递归方程，产生次线性边界。我们已经实现了TCT的方法来测试我们的方法的可行性。
2020-12-11 cs.CC cs.LO
Small Term Reachability and Related Problems for Terminating Term Rewriting Systems
本文研究终止项重写系统中是否可到达大小不超过 n 的项，按终止性证明方法给出 NP、N2ExpTime/NExpTime 与 PSpace 等复杂性分类，并分析合流性及大项变体的影响。
2025-10-14 cs.LO
Tuple Interpretations for Higher-Order Rewriting
我们开发了一类代数解释的许多排序和高阶项重写系统，需要考虑类型信息。具体而言，基类型项被映射到自然数的\emph{tuples}，高阶项被映射到这些元组之间的函数。元组可以携带与类型相关的信息;例如，$\mathsf{nat}$类型的项可以与表示其评估成本和大小的对$(\mathsf{cost}, \mathsf{size})$相关联。这类解释导致了比运行时或派生复杂性更细粒度的复杂性概念，这使得它对于获得高阶重写系统的复杂性界限特别有用。我们表明，重写系统兼容元组的解释承认有限的界限上的推导高度。此外，我们演示了如何机械地构建元组的解释，以及如何定向$β$和$η$减少我们的技术。最后，我们将我们的方法与运行时的复杂性，并证明特定的解释形状意味着一定的运行时的复杂性界限。
2021-05-03 cs.LO cs.SC
On Complexity Bounds and Confluence of Parallel Term Rewriting
LIP (UMR CNRS/ENS Lyon/UCB Lyon1/Inria)（LIP（法国国家科学研究中心/里昂高等师范学院/里昂第一大学/法国国家信息与自动化研究所联合研究单位））；Birkbeck, University of London（伦敦大学伯贝克学院）；University Grenoble Alpes（格勒诺布尔阿尔卑斯大学）
本文研究并行内最重写模型的复杂度界限与连通性，提出自动技术推导并行重写复杂度的上下界，通过扩展AProVE工具验证方法的有效性。
2024-09-02 cs.LO cs.PL
Proving Confluence in the Confluence Framework with CONFident
Universidad Politécnica de Madrid（马德里理工大学）；Universitat Politècnica de València（瓦伦西亚理工大学）
本文介绍Confluence框架，用于通过分而治之的模块化策略证明和反驳连通性，并在CONFident中实现。该方法能自动证明和反驳广义项重写系统的连通性，包括选择性重写函数符号的参数和一般条件规则。
2024-08-28 cs.LO cs.PL
Optimally Rewriting Formulas and Database Queries: A Confluence of Term Rewriting, Structural Decomposition, and Complexity
King’s College London（伦敦国王学院）；Univ. Artois, CNRS, Centre de Recherche en Informatique de Lens (CRIL)（阿图瓦大学、法国国家科学研究中心、伦斯信息学研究中心）
本文研究了通过语法重写规则最小化逻辑等价句子宽度的问题，提出了一个算法以确定给定正则一阶句子在应用规则后的最小宽度句子，填补了该领域通用设置下的空白。
2026-04-15 cs.DB cs.LO
Tools in Term Rewriting for Education
项重写是图灵完备的计算模型。当教授给计算机科学的学生时，传达了计算的关键属性以及在抽象层面上分析程序的技术。本文给出了一个快速的术语重写的介绍，并提出了几个自动工具来分析由因斯布鲁克大学的计算逻辑组开发的术语重写系统。这些工具包括终止工具TTT2、汇流证明器CSI、完成工具mkbTT和KBCV、复杂性工具TcT、策略工具AutoStrat以及FORT，FORT是重写系统的可判定类的一阶理论的判定过程的实现。除了在研究中的应用，这个软件库也被证明是非常宝贵的教学，例如，在多个版本的国际暑期学校重写。
2020-02-28 cs.LO
Proving Termination of Unfolding Graph Rewriting for General Safe Recursion
本文给出了一种新的展开图重写的终止性证明和复杂性分析，展开图重写是一种特殊的无限图重写，它表达了安全递归的一般形式。我们引入了一个终止顺序的条款序列连同长期图的解释成序列的条款。展开图重写规则表示一般的安全递归可以成功地嵌入到终止顺序的解释，产生多项式的运行时复杂度。此外，推广的展开图重写规则的定义一般安全递归，我们提出了一个新的标准的多项式运行时复杂性的无限GRS和多项式大小的范式在无限GRS。
2014-06-20 cs.CC cs.LO math.LO
Equational Theories and Validity for Logically Constrained Term Rewriting (Full Version)
本文研究逻辑约束项重写的语义，定义受约束等式、等式理论及有效性，构建可靠推理系统并提出代数语义以判定无效性和新的一致性概念。
2024-07-05 cs.LO
Complexity Hierarchies and Higher-order Cons-free Term Rewriting
研究无cons高阶项重写系统，证明左线性且类型阶K的系统在无限制求值下刻画E^K TIME，首次隐式刻画E层级，并揭示非确定性的敏感性。
2017-08-04 cs.CC cs.LO
A New Term Rewriting Characterisation of ETIME functions
利用多时间和指数时间可计算函数的项重写特性，提出了一种新的约简序--ETIME路径序（Path Order for ETIME，简称POE*），它是ETIME可计算函数的完备约简序. ETIME的简化顺序与相关的复杂性类形成了鲜明的对比。
2013-12-30 cs.CC cs.LO
Analyzing Innermost Runtime Complexity Through Tuple Interpretations
重写中的时间复杂度自然被理解为将项减少到范式所需的步骤数。在重写社区中，建立这种度量的复杂性界限是一个众所周知的问题。绝大多数的技术，以找到这样的界限包括修改终止证明，以恢复复杂性信息。例如，这已经通过语义解释、递归路径顺序和依赖对来完成。在本文中，我们遵循相同的程序，通过裁剪元组解释来处理最内部的复杂性分析。元组解释将术语解释为保持范式的缩减成本和大小的上限的元组。与完全重写设置相比，当减少是最内层时，对成本分量的强单调要求被丢弃。这种对成本元组的弱化要求允许我们证明兼容性结果的最内层版本：如果术语重写系统中的所有规则都可以严格定向，则最内层的重写关系是有根据的。我们建立了必要的条件，元组的解释保证多项式边界的兼容系统的运行时，并描述了这样的解释搜索过程。
2023-03-23 cs.CC cs.LO
A term-rewriting characterization of PSPACE
Isabel Oitavem介绍了一个术语重写系统（TRS），它捕获了多项式空间可计算函数的FPS类。我们提出了一种替代TRS FPS。由此得到FPS是包含某些初始函数的最小类，且在特定运算下是闭的。事实证明，我们的特征是相对简单的，并建议一个统一的方法的空间复杂性。
2012-01-03 cs.LO math.LO
Modular Automatic Complexity Analysis of Recursive Integer Programs
RWTH Aachen University（亚琛工业大学）
本文提出了一种基于新排名函数的模块化方法，用于递归整数程序的自动复杂度分析，并通过KoAT工具验证了其有效性。
2026-01-06 cs.LO
A Characterization of Basic Feasible Functionals Through Higher-Order Rewriting and Tuple Interpretations
本文利用高阶项重写中多项式有界的 cost-size 解释，证明了其可表示的泛函类恰好等价于第二型基本可行泛函类 BFF₂。
2025-11-04 cs.CC cs.LO
Modular SAT-based techniques for reasoning tasks in team semantics
我们研究了团队语义中逻辑推理任务的复杂性。我们的主要重点是数据的复杂性模型检验，但我们也得到了新的结果，逻辑定义的计数和枚举问题。我们的方法是基于这些问题的模块化减少到相应的问题的各类布尔公式。我们说明了我们的方法，通过几个新的易处理性/难处理性的结果。
2022-04-01 cs.LO
Modular Runtime Complexity Analysis of Probabilistic While Programs
我们关心的是平均情况下运行时的复杂性分析的一个原型的命令式语言赋予原语的采样和概率选择。从非概率程序的模块化资源分析的已知方法的启发，我们研究如何获得概率程序的模块化运行时分析。
2019-08-23 cs.LO cs.PL
Uncurrying for Innermost Termination and Derivational Complexity
一阶应用项重写系统为高阶方面建模提供了一个自然的框架。在早期的工作中，我们介绍了一个uncurrying变换，这是终止保持和反射。在本文中，我们将探讨这种转换的行为最内层终止和（最内层）派生复杂性。我们证明了它反映了最内终止性和最内导复杂性，并保持和反映了多项式导复杂性。为了保持最内层终止性和最内层导子复杂性，我们给出了反例。因此，解卷积可以用作最内层终止证明的预处理变换，并建立推导复杂性的多项式上界和下界。此外，它可以用来建立上界的最内层的衍生复杂性，而它既不是健全的证明最内层的非终止性，也不是获得下界的最内层的衍生复杂性。
2011-02-18 cs.LO
Degrees of Undecidability in Rewriting
一阶项重写系统的各种性质的不可判定性是众所周知的。一个不可判定的属性可以根据定义它的公式的复杂性来分类，这就产生了一个由不同层次的不可判定性组成的层次结构，从使用一阶算术公式对属性进行分类的算术层次结构开始，一直到允许对函数变量进行量化的分析层次结构。在本文中，我们考虑一阶项重写系统的性质，并在这个层次中对它们进行分类。单个项的弱和强规范化是Sigma-0-1-完全的，而它们的统一版本以及带有极小标志的依赖对问题是Pi-0-2-完全的。我们发现，汇合是Pi-0-2-完全的单项和一致。出乎意料地，基项的弱汇合比开项的弱汇合更难。前一个性质是Pi-0-2-完全的，而后者是Sigma-0-1-完全的（因此是递归可递归的）。最令人惊讶的结果是没有极小标志的依赖对问题：我们证明这是Pi-1-1-完全的，这意味着这个属性超过了算术层次，本质上是解析的。
2009-02-26 cs.CC cs.LO
Higher-order Cons-free Interpreters
构造函数重写系统被称为无缺点的，如果任何出现在规则的rhs中的构造函数项必须是该规则的lhs的子项。粗略地说，这样的系统在其评估期间不能建立新的数据结构。在几位作者的早期工作中，（类型化）cons-free系统已经被用来通过改变类型的阶数和允许的递归形式来描述复杂性类，如多项式或指数时间或空间。本文研究了无缺点项重写的解释器构造问题。由于它们与对角化证明的联系，在隐式计算复杂性理论中研究复杂性类之间的分离结果时，解释器可能是有用的。我们感兴趣的解释器的类型顺序$k > 1$，可以解释任何条款的严格较低的类型顺序，而这给了我们一个众所周知的分离结果E $^k$时间$\subseteq$ E $^{k+1}$时间，希望是更精细的解释器与语法限制的约束可以用来获得一个概念的假对角化和被用来攻击开放的问题，在复杂性理论。
2017-11-09 cs.CC cs.LO
Pushout Attachments and Conditional Complexity of Executable Models
本文通过推出构造研究可执行模型的模块化扩展，提出语义判据和复杂性界限，区分语法与语义，揭示模块化偏好源于连接限制。
2026-09-23 cs.LO
Proof Theory at Work: Complexity Analysis of Term Rewrite Systems
本论文主要研究“项重写系统的复杂性”。此外，大部分的工作涉及的“自动化”这样的复杂性分析。本导言的目的是以一种易于理解的方式介绍主要思想，使公众能够了解所介绍的结果。有些技术性的问题，必然会被过于简单化。
2009-12-30 cs.CC cs.LO cs.SC
Complexity of Fractran and Productivity
在函数式程序设计语言中，使用无限结构是常见的做法。对于处理无限结构的程序的完全正确性，必须保证结果的每个有限部分都可以在多个步骤中计算。这被称为生产力。对于具有无限结构的编程，生产率是定义良好的结果中的终止对于具有有限结构的编程的意义。Fractran是Conway发明的一种简单的图灵完备程序设计语言。我们证明了Fractran程序是否在所有正整数上停止的问题是Pi^0_2-完全的。在函数式编程中，生产率通常是相对于内置评估策略的单个术语的属性。通过将Fractran程序编码为无限列表的规范，我们建立了即使对于最简单的规范，这种生产率的概念也是Pi^0_2-完全的。因此，它比终止个别条款更难。此外，我们还在项重写的框架下探讨了生产力概念的可能的推广，并证明了它们的计算复杂性是Pi^1_1-完备的，从而超过了一阶逻辑的表达能力。
2009-07-31 cs.LO
Towards the average-case analysis of substitution resolution in $λ$-calculus
替换解析支持$β$ -归约的计算特性，通过避免捕获的绑定变量项交换来补充其执行。唉，替换的元级定义，掩盖了一个非平凡的计算，把$β$ -归约变成了一个原子重写规则，尽管它的操作复杂度不同。在本文中，我们提出了一个有点间接的平均情况下分析的替代决议在经典的$λ$演算，在$λ\upsilon$，一个扩展的$λ$演算内化的显式替代的$\upsilon$演算的替代定量分析的基础上。在这个框架内，我们表明，对于任何固定的$n \geq 0$，一个均匀随机的概率，条件的大小，$λ\upsilon$ -长期$\upsilon$ -规范化在$n$正常顺序（即最左最外）减少步骤往往是一个可计算的限制，长期大小趋于无穷大。为此，我们建立了一个有效的层次结构$\left(\mathscr{G}_n\right)_n$的定期树文法分区$\upsilon$ -规范化条款到类的条款规范化在$n$正常顺序重写步骤。在我们的建设的主要技术成分是一个归纳的方法来建设$\mathscr{G}_{n+1}$出$\mathscr{G}_n$的基础上，反过来，有限的交集分区的算法建设，罗宾逊的统一算法的启发。最后，我们简要地讨论了我们的方法的应用程序，其他长期重写系统，集中在两个密切相关的形式主义，即完整的$λ\upsilon$演算和组合逻辑。
2018-12-11 cs.LO math.CO
Complexity Analysis of Precedence Terminating Infinite Graph Rewrite Systems
安全递归（或分支递归）的一般形式可以表示为一个无限图重写系统，该系统包含Dal Lago，Martini和Zorzi提出的展开图重写规则，其中每一个最内层重写的范式的大小是多项式有界的.每一个展开图重写规则在Middeldorp，Ohsaki和Zantema意义下都是优先终止的。虽然优先终止的无限重写系统覆盖了所有的原始递归函数，但本文考虑的是具有参数分离的优先终止的图重写系统，它构成了优先终止图重写系统的一个子类。我们证明了对于任意具有特定参数分离的优先终止无限图重写系统G，G的运行时复杂度和G中每个范式的大小都是多项式有界的.作为一个推论，我们得到了另一种证明的原始结果由Dal Lago等人。
2015-05-27 cs.CC cs.LO
CSPs with Global Modular Constraints: Algorithms and Hardness via Polynomial Representations
研究了在模M的不同选择下，当赋值在某个同余类中必须具有Hamming权时，布尔约束满足问题的复杂性.由于已知的易处理的布尔CSP的分类，这主要减少到三种情况下的研究：2-SAT，HORN-SAT和LIN-2（线性方程模2）。我们对这些相应问题在多项式时间内可解的模M进行分类，以及当它们不可解时（假设ETH）。我们的研究表明，这种模块化约束为这些经典的、经过充分研究的问题提供了惊人的丰富性，与复杂性理论和编码理论有着更广泛的联系。HORN-SAT情况与表示NAND函数mod M的多项式的覆盖复杂度有关。LIN-2的情况与表示OR函数mod M的多项式的稀疏性有关，这又与线性码和局部可解码码的模块化权重分布特性有关。在这两种情况下，我们的算法的分析以及硬度降低依赖于这些多项式表示，突出了我们的算法和显示硬度的小工具的硬情况之间有趣的代数共同点。这些新的多项式表示的复杂性措施值得进一步研究。我们研究的灵感来自于Nägele，Sudakov和Zenklusen最近的一项关于具有全局同余约束的子模最小化的工作。我们的HORN-SAT算法有很强的相似性，他们的算法，特别是相同的一套系统出现在这两种情况下。我们的多项式表示的连接导致一个更简单的分析这样的集合系统，也揭示了（但没有解决）的复杂性，子模最小化的同余要求模复合M。
2019-02-13 cs.CC cs.DS cs.IT
Higher-dimensional subdiagram matching
本文研究高维图重写中的子图匹配问题，在 diagrammatic sets 框架下提出任意维度的匹配算法，并证明在无环性条件下可将超多项式复杂度改进为多项式复杂度，同时分析了维度 4 的困难。
2023-04-18 cs.DS cs.LO math.CT
