Confluence of Conditional Term Rewrite Systems via Transformations
条件项重写是项重写的一种直观而复杂的扩展。为了从无条件重写的更简单的框架中受益，已经定义了转换以消除条件项重写系统的条件。最近的研究结果提供了条件项重写系统通过转换的融合标准，但他们仅限于CTRS与某些语法特性，如弱左线性。这些语法属性意味着转换对于给定的CTRS是合理的。本文展示了如何使用转换来证明汇流的操作终止，右稳定的确定性条件项重写系统，而无需合理性限制。为了这个目的，它表明，某些重写策略，特别是几乎U-渴望和内心的重写，总是意味着健全。
2017-01-03 cs.LO
String Diagram Rewrite Theory III: Confluence with and without Frobenius
在本文中，我们解决的问题证明合流字符串图重写，这是以前被证明是组合特征的双推出重写接口（DPOI）（标记）超图。对于没有接口的标准DPO重写，终止重写系统的汇合通常是不可判定的。然而，我们在这里表明，DPOI的汇合，因此字符串图重写，是可判定的。我们应用这一结果给出了用临界对分析判定有无Frobenius结构的对称Monoidal理论的局部收敛性的有效方法。对于后者，我们引入了新的概念的关键对，这使得一个关键对的多个连接被提升到一个任意的上下文中，尽管强大的非局部约束放在重写在一个通用的对称monoidal理论的路径可连接性。
2022-04-18 cs.LO
Rewriting Modulo βin the λΠ-Calculus Modulo
Modulo是一个依赖类型的Algorithm的变体，其中beta转换扩展了用户定义的重写规则。它是一个表达性的逻辑框架，并已被用于以浅层次的方式编码逻辑和类型系统。基本的性质，如主题归约或类型的唯一性，一般不适用于Muda-Pi-calculus Modulo。然而，如果由重写规则与β-归约一起生成的重写系统是汇合的，则它们成立。但这限制太多了。为了处理不融合来自于beta-约简和重写规则之间的干扰的情况，在它们的左手边，我们引入了重写模beta的概念，用于对beta-Pi-演算模进行重写。我们证明了重写模beta的汇合足以确保主题减少和类型的唯一性。我们通过将π演算模编码到高阶重写系统（HRS）中来实现我们的目标。因此，我们也使合流的结果，可用于HRSs的Pudda-Pi-演算模。
2015-07-29 cs.LO
Termination of canonical context-sensitive rewriting and productivity of rewrite systems
程序的终止，即，不存在无限的计算，确保了所有初始表达式的范式的存在，从而为函数式程序的规范化语义的定义提供了必要的成分。然而，在惰性函数式语言中，无限的数据结构通常作为计算的结果来交付。例如，所有素数的列表可以作为数值表达式或数据结构的永不结束的流返回。如果允许这样的流，要求终止是无望的。在这种情况下，生产力的概念可以用来提供一个无限数据结构计算的帐户，因为它“捕捉了可计算性的概念，无限列表程序的进展”（B.A. Sijtsma，On the Productivity of Recursive List Definitions，ACM Transactions on程序设计语言and Systems 11（4）：633-649，1989）。然而，在领域的长期重写系统，这可以被看作是（一阶，无类型，无条件）的功能程序，上下文敏感重写（CSR）的终止已被证明相当于重写系统的生产力，通过适当的转换。通过这种方式，可以使用证明CSR终止的工具来证明生产力。在术语重写中，CSR是当仅允许对函数符号的选定参数进行约简时产生的重写限制。在本文中，我们表明，众所周知的CSR的计算能力的结果是有用的，以更好地了解现有的重写系统的生产力和终止CSR之间的联系，并获得更强大的技术来证明重写系统的生产力。
2015-12-22 cs.LO cs.PL
Extending Context-Sensitivity in Term Rewriting
我们提出了一个广义版本的上下文敏感性的术语重写的基础上的“禁止模式”的概念。基本想法是，如果要收缩的Redex具有特定形状并出现在特定上下文中，则应禁止重写步骤。这种形状和背景是通过禁止模式来表达的。特别是，我们分析了这种新的方法和常用的上下文敏感性的概念，在长期重写之间的关系，以及从计算的角度来看，重写与禁止模式的可行性。后一种可行性的特点是要求限制重写关系产生改进的终止行为，同时仍然足够强大，以计算有意义的结果。在某些类的重写系统与禁止模式的两种性质的充分准则。
2010-01-25 cs.LO
Linear Compressed Pattern Matching for Polynomial Rewriting (Extended Abstract)
本文是一个扩展的抽象分析的长期重写的重写规则中的条款，以及长期重写压缩的单例树文法（STG）。这种形式的压缩比节点共享或将项表示为dag更一般，因为部分树（上下文）也可以在压缩中共享。在第一部分中，高效，但复杂的算法检测适用性的重写规则下STG压缩构造和分析。第二部分将这些结果应用于项重写序列。子匹配的主要结果是，找到一个左线性规则的redex可以在多项式时间STG压缩下执行。重写和（单位置或并行）重写步骤的主要含义是：（i）在STG压缩下，n个重写步骤可以在非确定性多项式时间内执行。(ii)在STG压缩下，对于左线性重写规则，可以在多项式时间内执行n个重写步骤的序列，以及（iii）对于压缩重写规则，其中左手侧或者是DAG压缩的，或者是地面和STG压缩的，以及STG压缩的目标项，可以在多项式时间内执行n个重写步骤。
2013-02-26 cs.DS cs.LO
Confluent terminating extensional lambda-calculi with surjective pairing and terminal type
对于具有满射对和终端类型的Adjuda演算，Curien和Di Cosmo受到Knuth-Benzen完备化的启发，引入了一个合流重写系统，该系统（1）扩展了朴素重写系统，（2）在上下文下是稳定的。重写系统具有（i）将终端类型的项重写为项常数 * 的规则，除非项不是 *，（ii）用于函数类型和产品类型的可拓性的重写规则，以及中介重写规则（i）和（ii）的重写规则。Curien和Di Cosmo假设，由于（iii），任何归约方法都不能证明Curien-Di Cosmo重写系统的强正规化（SN），并且他们将SN保持开放。通过将Girard的约化方法相对化到无 * 项上，证明了它们的重写的SN性和多态扩张的SN性。相对化之所以有效，是因为：对于任何SN项t，以及对于在$t$中未出现的终端类型的任何变量z，所有出现的终端类型的 * 被变量z替换的t是SN。
2018-05-05 cs.LO
Dynamic Tracing: a graphical language for rewriting protocols
本研究将Set_*范畴的追踪幺半结构中的隐式转换过程显式化，推广到更多追踪Kleisli范畴并给出推测性追踪算子，为图重写计算提供形式化图形语法。
2023-05-01 cs.LO math.CT math.LO
Efficient Implementation of Rewriting Revisited Technical Report
最近，已经引入了许多技术，允许（自动化）的术语重写系统（TRS）的运行时复杂性的分类。在早期的工作中，作者已经表明，对于合流TRS，最内层多项式运行时复杂性导致定义的函数的多时间可计算性。本文将上述结果推广到完全重写。根据我们以前的工作，我们利用图重写。我们给出了一个新的证明充分重写，允许一个精确的控制复制的资源图重写。总之，我们完整地描述了重写的图灵机（简称TM）上的实现。我们表明，TRS的运行时复杂性和TM的运行时复杂性是多项式相关的。我们的结果加强了重写系统的复杂性是真实地表示通过推导的长度的证据。此外，我们的结果允许分类的非确定性多时间计算的基础上的重写系统的运行时复杂性分析。
2011-06-08 cs.CC cs.LO
A type-based termination criterion for dependently-typed higher-order rewrite systems
一些作者设计了基于类型的终止标准ML类语言允许非结构递归调用。我们将这些工作扩展到一般的重写和依赖类型，从而为构造演算中的重写和β-还原的组合提供了一个强大的终止标准。
2006-10-11 cs.LO cs.PL
The Annotated Dependency Pair Framework for Almost-Sure Termination of Probabilistic Term Rewriting
本文将依赖对技术扩展到概率项重写系统，提出带标注依赖对框架以自动证明完全与最内层重写下的几乎必然终止性，并在 AProVE 中实现验证。
2025-06-05 cs.LO
Interacting Monoidal Structures with Applications in Computing
本文在$n$重幺半范畴中定义$n$重幺半群与余幺半群对象，给出通信协议及布尔半环模代数等实例，服务于并发理论与更高维重写。
2024-11-06 cs.LO math.CT
A Set-Theoretic Framework for Parallel Graph Rewriting
我们解决的问题，属性图变换，并提出了一种新的算法方法来定义并行图变换允许重叠。我们首先介绍一些图结构上的抽象操作。然后，我们将重写规则的概念定义为$L \supseteq K \supseteq M \subseteq R$形式的三个包含。我们提供了六个条件，并行图重写关系应该理想地满足，这导致我们定义两个不同的完全并行图重写关系。一个中心概念的正则性的匹配被证明是等价于这六个条件，并平等的这两个关系。此外，我们利用可能发生在$L$，$K$，$M$和$R$中的对称性，并定义另一对重写关系，这些重写关系可以分解出可能的许多等价匹配，直到它们的公共对称性。这些定义和相应的证明相结合的操作图与群论的概念，从而说明了我们的框架的相关性。
2018-08-09 cs.LO
From Innermost to Full Almost-Sure Termination of Probabilistic Term Rewriting
本文将项重写系统中由最内终止推导完全终止的语法准则适配至概率环境，证明分析最内重写的几乎必然终止（AST）即可证明概率项重写系统的完全AST，并在工具AProVE中实现与评估了该贡献。
2024-02-12 cs.LO
A Lower Bound of the Number of Rewrite Rules Obtained by Homological Methods
本文利用同调方法为项重写系统等价公理集的数量提供更优下界，并实现程序在64个完整TRS上验证。
2022-09-20 cs.LO math.AC math.LO
Parallel Graph Rewriting with Overlapping Rules
我们解决的问题，同时转换的网络表示为图形。粗略地说，可以区分两种类型的同时或并行重写关系在复杂的结构，如图：（i）那些并行转换不相交的子图，因此可以模拟连续的纯粹的顺序和局部变换和（ii）那些同时转换重叠的子图。在后一种情况下，并行变换一般不能通过连续的局部重写步骤来模拟。我们调查这最后一个问题的重叠图变换系统的框架。由于图的并行变换一般不产生图，我们首先提出了保证图的并行重写关系封闭的一些充分条件。然后重点介绍和讨论了图上的两种并行重写关系。一个关系是功能性的，从而确定性的，另一个是不功能的，我们提出了充分的条件，确保其汇合。
2017-01-24 cs.FL cs.LO
Confluence Criteria for Logically Constrained Rewrite Systems (Full Version)
本文把Huet和Toyama的强封闭及平行封闭临界对判据推广到逻辑约束重写系统，并实现于新工具crest中，附有实验数据。
2024-11-11 cs.LO
Subsumptions of Algebraic Rewrite Rules
本文定义代数重写规则间的包含关系为规则态射，使规则与子规则同时应用等价于单独应用包含规则，并通过全局相干变换在DPO等重写环境中实现。
2023-12-14 cs.LO cs.PL math.CT
Unique Normal Forms in Infinitary Weakly Orthogonal Term Rewriting
有限项和无穷项重写理论在正交重写系统中得到了广泛的发展，但在弱正交重写系统中的发展程度较低。在本文中，我们提出了一些贡献，后者的情况下，弱正交性，临界对被接纳，只要他们是平凡的。我们开始与现在经典的压缩引理，作为一种工具，建立无穷汇流，因此独特的无穷范式的属性，弱正交TRS的情况下，不包含折叠重写规则的细化。这种限制的无重叠是至关重要的，是在一个简单的TRS的阐述是弱正交的，但有两个崩溃的规则。事实证明，所有通常的理论都戏剧性地崩溃了。最后，我们建立了一个积极的事实：钻石性质的无限发展弱正交TRS，通过详细的分析，由范奥斯特罗姆有限的情况下。
2009-11-05 cs.LO
Open Graphs and Monoidal Theories
弦图是推理物理过程、逻辑电路、张量网络和许多其他组成结构的强大工具。这些图的显著特征是边不需要连接到两端的顶点，并且这些未连接的端部可以被解释为图的输入和输出。在本文中，我们给出了一个具体的结构字符串图使用一种特殊类型的图称为开图。虽然开图的范畴本身不是粘合剂，我们引入了选择性粘合函子的概念，并表明这样的函子嵌入开图的范畴到类型图的环境粘合剂范畴。使用这个函子，开图的范畴继承了类型图的范畴的“足够的粘附性”来执行双推出（DPO）图重写。我们的理论的一个突出特点是，它确保重写系统是“类型安全”的意义上，重写尊重的输入和输出。这种形式主义使我们能够安全地编码计算模型的有趣结构，例如评估动态，具有简洁，明确的重写规则，而图形表示吸收了许多繁琐的细节。虽然拓扑形式主义存在的弦图，我们的建设是谨慎的，有限的，并享有可判定的算法组成和重写。我们还展示了如何开图可以参数化的图形签名，类似于monoidal签名的Joyal和街，定义类型的顶点的图形语言和约束，它们可以如何连接。利用类型开图，我们可以构造自由对称幺半范畴、PROPs和更一般的monoidal理论。因此，开图为我们提供了一个在幺半范畴中进行机械化推理的工具。
2010-11-18 cs.LO math.CT
Categorical E-Graphs for Lambda Calculi
University of Birmingham（伯明翰大学）；Kyoto University and Huawei Central Software Institute（京都大学和华为中央软件研究所）
针对 e-graphs 缺乏变量绑定支持的问题，本文基于范畴论框架扩展至闭对称幺半范畴，利用层次超图实现绑定，并提出双推重写机制，证明其与项重写的等价性。
2026-06-26 cs.LO math.CT
Termination of Cycle Rewriting by Transformation and Matrix Interpretation
我们提出的技术，以证明终止循环重写，即字符串重写的周期，这是字符串的开始和结束连接。我们的主要技术是将循环重写转换为字符串重写，然后应用最先进的技术来证明字符串重写系统的终止性。我们提出了三个这样的转换，并证明他们都是健全的和完整的。这样，不仅变换系统的串重写的终止意味着原始循环重写系统的终止，对于非终止也可以得出类似的结论。除了这种转换的方法，我们提出了一个统一的框架矩阵的解释，涵盖了大多数早期的方法来自动证明终止循环重写。我们所有的技术都用于证明终止和相对终止。我们提出了几个实验显示我们的技术的力量。
2017-03-16 cs.LO
Confluence via strong normalisation in an algebraic λ-calculus with rewriting
线性-代数演算和代数演算是用任意线性组合项扩展的无类型代数代数演算。前者以重写系统的形式呈现线性代数的公理，而后者使用等式。当重写时，代数演算不是融合的，除非增加进一步的限制。我们提供了一个类型系统的线性代数演算强制执行强规范化，这给回汇合。类型系统允许在系统F中进行抽象解释。
2012-03-28 cs.LO
Combining typing and size constraints for checking the termination of higher-order conditional rewrite systems
在以前的工作中，第一作者扩展到高阶重写和依赖类型中使用类型中的大小注释，这是一种终止证明技术，称为基于类型或大小的终止，最初为ML类程序开发。在这里，我们通过考虑条件重写和显式量化以及对大小注释的约束更进一步。这允许更精确地描述函数输出的大小如何取决于其输入的大小。因此，我们可以检查更多函数的终止。首先给出了一个基于约束求解的通用类型检测算法。然后，我们给出了Presburger算法中的一个带约束的终止准则。据我们所知，这是高阶条件重写的第一个终止准则，考虑到终止的条件。
2006-09-11 cs.LO
Recovering Commutation of Logically Constrained Rewriting and Equivalence Transformations (Full Version)
Niigata University（新潟大学）；University of Innsbruck（因斯布鲁克大学）；Nagoya University（名古屋大学）
本文提出了一种新的最一般约束重写方法，使逻辑约束重写与等价变换可交换，从而解决实现中的搜索空间问题。
2025-12-15 cs.LO
Tools in Term Rewriting for Education
项重写是图灵完备的计算模型。当教授给计算机科学的学生时，传达了计算的关键属性以及在抽象层面上分析程序的技术。本文给出了一个快速的术语重写的介绍，并提出了几个自动工具来分析由因斯布鲁克大学的计算逻辑组开发的术语重写系统。这些工具包括终止工具TTT2、汇流证明器CSI、完成工具mkbTT和KBCV、复杂性工具TcT、策略工具AutoStrat以及FORT，FORT是重写系统的可判定类的一阶理论的判定过程的实现。除了在研究中的应用，这个软件库也被证明是非常宝贵的教学，例如，在多个版本的国际暑期学校重写。
2020-02-28 cs.LO
Dependency Pairs for Expected Innermost Runtime Complexity and Strong Almost-Sure Termination of Probabilistic Term Rewriting
本文提出首个用于概率项重写系统最内层重写的依赖对框架，以分析期望复杂度并证明强几乎必然终止，并在AProVE中实现，展示了其优势。
2025-10-15 cs.LO
Situation Calculus by Term Rewriting
UNC Chapel Hill（北卡罗来纳大学教堂山分校）
一个版本的情况演算中的情况表示为一阶项。流利度可以从术语结构中计算出来，并且对情境的动作对应于对术语的重写规则。在某些情况下，仅依赖于或影响流畅度子集的动作可以被描述为对术语的子术语进行操作的重写规则。如果行动是双向的，那么有效的完成方法可以用来解决规划问题。这种情况和行动的表示与Thielscher \cite{Thielscher98}的流畅演算最相似，只是这种表示更灵活，并且更多地使用了子项结构。给出了一些例子，并提出了一些一般的方法来构造这样的重写规则集。本文于2019年12月23日提交给FSCD 2020。
2020-06-30 cs.AI cs.LO
Modular Complexity Analysis for Term Rewriting
所有目前的调查，以分析衍生复杂性的长期重写系统是基于一个单一的终止方法，可能之前的转换。然而，由于直接标准的权力有限，专门使用直接标准是有问题的。为了克服这一限制，本文介绍了一个模块化的框架，它允许推断（多项式）上界的复杂性，长期重写系统结合不同的标准。由于其基本思想是基于相对重写，我们研究如何矩阵的解释和匹配边界可以使用和扩展相对重写的复杂性，分别。模块化框架被证明比传统的设置更强大。此外，结果已经实施，实验表明，显着的增益功率。
2014-03-29 cs.LO
Representing Nonterminating Rewriting with $\mathbf{F}_2^μ$
我们指定一个二阶类型系统$\mathbf{F}_2^μ$，它是为表示非终止而定制的。重写系统$\mathcal{R}$中的项$t$的非终止迹对应于生产性驻留者$e$，使得$\mathbf{F}_2^μ$中的$Γ_{\mathcal{R}} \vdash e : t$，其中$Γ_{\mathcal{R}}$是表示重写系统的环境。我们证明了生产率检查$\mathbf{F}_2^μ$是可判定的，通过映射到$λ$ -Y演算。提出了一种基于二阶匹配的$\mathbf{F}_2^μ$类型检测算法。我们实现了一个概念证明类型检查器的类型检查算法。
2017-06-02 cs.LO
A Dependency Pair Framework for Relative Termination of Term Rewriting
本文提出了一种新型的标注依赖对（ADPs）框架，用于证明项重写系统的相对终止，并在工具AProVE中实现，对比现有工具展现了其有效性。
2024-04-23 cs.LO
Guided Unfoldings for Finding Loops in Standard Term Rewriting
在本文中，我们重新考虑展开为基础的技术，我们已经介绍了检测循环在标准项重写。我们通过指导展开过程，在重写规则中使用区分位置来改进它。这导致展开的深度优先计算，而原始技术是宽度优先。我们已经在工具NTI中实现了这种新方法，并在一系列重写系统上将其与前一种方法进行了比较。我们得到的结果是有希望的（更好的时间，更成功的证明）。
2018-11-08 cs.LO cs.PL
Complexity of Conditional Term Rewriting
我们提出了一个面向条件项重写系统满足一定的限制复杂性的概念。这个概念是现实的，因为它不仅测量成功的计算，而且测量导致失败的规则应用程序的部分计算。无条件的上下文敏感的重写系统的转换，反映了这种复杂性的概念，以及一种技术，以获得运行时和派生的复杂性界限，这种转换的结果。
2017-03-22 cs.LO
Annotated Dependency Pairs for Full Almost-Sure Termination of Probabilistic Term Rewriting
本文改进带注释的依赖对框架，将概率项重写的几乎必然终止分析从最内层策略扩展到完全重写，并细化基本项场景，在AProVE中实现验证。
2025-01-22 cs.LO
From Innermost to Full Probabilistic Term Rewriting: Almost-Sure Termination, Complexity, and Modularity
RWTH Aachen University（亚琛工业大学）
本文提出在概率术语重写系统中，通过分析最内重写下的几乎确定终止来证明完整终止，并探讨其复杂性与模块性。
2025-12-11 cs.LO
Graph Rewriting and Relabeling with PBPO+: A Unifying Theory for Quasitoposes
本文提出PBPO+方法，通过强匹配增强对模式嵌入的控制，证明其可统一PBPO、AGREE和DPO，并适用于带标签图和属性图的重写。
2023-05-25 cs.LO
Equational reasoning with context-free families of string diagrams
字符串图提供了一种直观的语言，以图形方式表达相互作用的进程网络。弦图的离散表示，称为弦图，允许通过双推出重写进行机械化等式推理。然而，人们往往希望表达的不仅仅是单个方程，而是任意大小的图之间的整个方程族。为了做到这一点，我们定义了一类上下文无关文法，称为B-ESG文法，它适用于定义整个系列的字符串图，至关重要的是，字符串图重写规则。我们表明，这些语法的语言成员资格和匹配枚举问题是可判定的，因此，有一个算法重写字符串图根据B-ESG重写模式。我们还表明，它是可能的原因，在语法的水平，通过提供一个简单的方法，转换语法的字符串图重写，并显示受理的诱导B-ESG重写模式。
2015-10-13 cs.FL cs.LO math.CT
Interactions between Causal Structures in Graph Rewriting Systems
图重写形式主义是一个强大的方法来建模复杂的分子系统。它们捕捉分子相互作用的内在并发性，从而实现机制的正式概念（部分有序的事件集），解释系统如何在给定一组重写规则的情况下实现特定结果。然后，验证从给定模型中出现的机制是否符合关于它们相互干扰的经验观察是有用的。在这项工作中，我们的目标是确定实现X的机制中的特定事件是否阻止或促进实现Y的机制中的特定事件的发生。这种检查也可用来假设使示范机制符合观察结果的规则。我们定义了一个严格的框架，用于定义由图形重写规则系统引起的机制之间的干扰（积极或消极）的概念，并用于确定是否可以实现两种机制作为输入的断言的影响。
2019-01-03 cs.CE cs.LO
Consistency and Completeness of Rewriting in the Calculus of Constructions
向基于Curry-Howard同构的证明助手（例如Coq）添加重写可以极大地提高工具的可用性。不幸的是，添加任意一组重写规则可能会使底层的形式系统变得不可判定和不一致。虽然确保类型检查的终止性和汇合性以及可判定性的方法已经在一定程度上得到了研究，但逻辑一致性迄今为止很少受到关注。在本文中，我们表明，一致性是正规性的后果，这反过来又遵循重写规则定义的所有功能是完整的假设。我们提供了一个声音和终止，但不一定完整的算法来验证这个属性。该算法接受所有的定义，遵循相关的模式匹配计划Coquand和研究的McBride在他的博士论文。它还通过重写接受许多定义，包含偏离标准模式匹配的规则。
2008-09-15 cs.LO cs.SC
Disproving (Positive) Almost-Sure Termination of Probabilistic Term Rewriting via Random Walks
RWTH Aachen University（亚琛工业大学）
本文提出首个自动反驳概率项重写系统（正）几乎必然终止性的技术，通过将随机游走嵌入计算来定量分析循环的存在性和计数。
2026-05-28 cs.LO
String Diagrams for Monoidal Categories, in Rocq
Plume team, CNRS, LIP, ENS de Lyon, UMR 5668（PLUME团队，法国国家科学研究中心，里昂高等师范学院计算机实验室）
Rocq库提供图形化重写步骤和自动推断MacLane同构，用于单子范畴的可视化与形式证明。
2026-02-23 cs.LO
A Modal Logic for Termgraph Rewriting
我们提出了一个模态逻辑量身定制的描述图变换，并讨论了它的一些属性。我们专注于一类特殊的图，称为termgraphs。它们是一阶项，增加了共享和循环。Termgraphs允许一个描述经典的数据结构（可能与指针），如双向链表，循环列表等，我们展示了如何建议的逻辑可以忠实地描述（一）termgraphs以及（二）应用termgraphs重写规则（即匹配和替换）和（iii）计算范式相对于一个给定的重写系统。我们还展示了如何建议的逻辑，这是更具表现力的命题动态逻辑，可以用来指定形状的经典数据结构（如二叉树，循环列表等）。
2010-03-23 cs.LO cs.PL cs.SC
Automated Strategy Invention for Confluence of Term Rewrite Systems
University of Innsbruck（因斯布鲁克大学）；Shanghai Jiao Tong University（上海交通大学）；Czech Technical University in Prague（布拉格捷克技术大学）；University of Melbourne（墨尔本大学）
针对项重写系统合流性证明中参数选择复杂的问题，研究者用机器学习构建首个学习引导的自动合流性证明器，生成大型数据集，改进的CSI证明器性能超越人工策略，解决了此前无自动证明的若干问题。
2025-07-31 cs.AI cs.LO
ZX-Calculus and Extended Hypergraph Rewriting Systems I: A Multiway Approach to Categorical Quantum Information Theory
范畴量子力学和Wolfram模型提供了不同但互补的方法来研究组合结构上的图形重写系统与物理学基础之间的关系;本文的目的是在Coecke和Duncan的ZX演算形式主义的背景下开始阐明这两种方法之间的形式对应关系，用于图解地推理量子比特之间的线性映射。在简要总结了相关的形式主义，并提出了一个明确的公式的Wolfram模型的粘合剂类别和双推出重写系统，我们说明了如何图形重写的ZX演算可以嵌入和实现在更广泛的背景下Wolfram模型多路系统，并举例说明我们专门为此目的开发的软件框架（ZXMultiwaySystem）的一些功能。最后，我们提出了一个证明（连同一个明确计算的例子）的方法的基础上的狄克逊和基辛格的多路演化图和分支图的Wolfram模型是自然赋予monoidal结构的基础上rulial组成，而且，兼容的monoidal产品的ZX图。
2020-10-05 cs.DM cs.LO
Proof Theory at Work: Complexity Analysis of Term Rewrite Systems
本论文主要研究“项重写系统的复杂性”。此外，大部分的工作涉及的“自动化”这样的复杂性分析。本导言的目的是以一种易于理解的方式介绍主要思想，使公众能够了解所介绍的结果。有些技术性的问题，必然会被过于简单化。
2009-12-30 cs.CC cs.LO cs.SC
On Causal Equivalence by Tracing in String Rewriting
我们介绍证明字符串重写系统，并使用这些，表明从文献中已知的各种概念的等价减少可以被视为不同的观点的因果等价的概念。特别是，我们表明，置换等价类（如已知的从微积分和长期重写）是唯一表示的迹图（从物理学称为因果图）和所谓的贪婪的多步减少（如已知的代数）。我们提出了从前者到后者的有效映射，拓扑多排序TM，反之亦然，证明项代数[[]]。
2023-03-28 cs.LO
Natural Transformations as Rewrite Rules and Monad Composition
本文提出用字符串重写方法验证单子复合等范畴论构造，通过重写系统的合流性刻画单子，并给出伴随的重写范畴表征。
2019-01-08 cs.LO
Rewriting in Free Hypergraph Categories
我们研究重写方程理论的对称monoidal类别的情况下，有一个可分离的Frobenius monoid的每个对象。这些类别，也称为超图类别，越来越相关：弗罗贝纽斯结构最近出现在跨学科应用中，包括量子过程，动力系统和自然语言处理的研究。在这项工作中，我们给出了一个组合特征的箭头的一个自由超图范畴的标记超图的余跨度，并建立一个精确的对应重写模Frobenius结构一方面和双推出重写超图。这种解释允许使用超图上的结果，以确保在一个自由超图类别重写的汇合的可判定性。我们的研究结果概括了以前的方法，其中只考虑由单个对象（道具）生成的类别。
2018-01-03 cs.LO
Rewriting and Completeness of Sum-Over-Paths in Dyadic Fragments of Quantum Computing
本文为量子计算中的路径求和形式化方法提出一组新的重写规则，证明其对 Toffoli-Hadamard 片段完备且终止但不合流，并将其推广到用于量子傅里叶变换的二进片段，同时支持任意项的求和与拼接。
2024-03-06 cs.LO quant-ph
Wiring diagrams as normal forms for computing in symmetric monoidal categories
范畴论的应用通常涉及对称monoidal范畴（SMC），其中抽象过程或操作可以串联或并行组成。然而，到2020年，仍然缺乏与SMC合作的计算工具。我们提出了一个“无偏”的方法来实现对称monoidal类别，操作的基础上有向，非循环布线图。因为SMC的交换定律和其他定律在布线图中保持一致，所以不需要重写规则来比较图。我们讨论的数学运算的接线图，以及其实施的软件包Catlab。
2021-01-26 cs.DM cs.LO
