Infinitary Term Rewriting for Weakly Orthogonal Systems: Properties and Counterexamples
我们提出了一些贡献的无穷重写弱正交项重写系统的理论，其中的关键对可能会出现，他们是平凡的。我们证明了无穷唯一范式属性失败的一个例子的弱正交TRS与两个折叠规则。通过翻译这个例子，我们表明，这个属性也失败的无穷大-beta-eta-calculus。作为积极的结果，我们得到了以下几点：无穷汇流，因此无穷唯一的范式属性，保持弱正交TRS不包含崩溃的规则。为此，我们改进了压缩引理。此外，我们建立了三角形和菱形性质的无限多步骤（完整的发展）在弱正交TRS，通过细化早期的集群分析有限的情况下。
2014-06-05 cs.LO
A Coinductive Framework for Infinitary Rewriting and Equational Reasoning (Extended Version)
我们提出了一个共归纳的框架，定义无穷类似物的方程推理和重写统一的方式。我们定义关系=^infty，无限等式推理的概念，和->^infty，无限重写的标准概念如下：=^infty：= nu R。（<-_root + ->_root + lift（R））^* ->^infty：= mu R. nu S（->_root + lift（R））^* ; lift（S）其中lift（R）：= {（f（s_1，.，s_n），f（t_1，.，t_n））|s_1 R t_1，.，s_n R t_n } + id，其中mu是最小不动点算子，nu是最大不动点算子.该设置捕获任意序数长度的重写序列，但它既不需要序数也不需要度量收敛。这使得该框架特别适合于定理证明器中的形式化。
2015-05-05 cs.LO
Modularity of Convergence and Strong Convergence in Infinitary Rewriting
术语重写系统的属性被称为模块化当且仅当它们在不相交的联合下被保留（并被其反映），即当组合两个具有不相交签名的术语重写系统时。收敛性是无穷项重写系统的性质，即所有约简序列都收敛到一个极限。强收敛还要求约简序列中的redex位置移动任意深度。在本文中，它表明，收敛和强收敛是模块化的非崩溃的无穷项重写系统的性质，提供（收敛）的长期指标是粒度。这概括了度量\infty之外的已知模块性结果。
2010-09-06 cs.FL cs.LO
Unique Normal Forms in Infinitary Weakly Orthogonal Term Rewriting
有限项和无穷项重写理论在正交重写系统中得到了广泛的发展，但在弱正交重写系统中的发展程度较低。在本文中，我们提出了一些贡献，后者的情况下，弱正交性，临界对被接纳，只要他们是平凡的。我们开始与现在经典的压缩引理，作为一种工具，建立无穷汇流，因此独特的无穷范式的属性，弱正交TRS的情况下，不包含折叠重写规则的细化。这种限制的无重叠是至关重要的，是在一个简单的TRS的阐述是弱正交的，但有两个崩溃的规则。事实证明，所有通常的理论都戏剧性地崩溃了。最后，我们建立了一个积极的事实：钻石性质的无限发展弱正交TRS，通过详细的分析，由范奥斯特罗姆有限的情况下。
2009-11-05 cs.LO
Proof terms for infinitary rewriting, progress report
我们将证明项的概念推广到超限归约领域。证明项表示在一阶项格式中的约简，从而促进它们的形式分析。我们表明，任何超限减少可以忠实地表示为一个无穷证明项，这是唯一的，无穷，结合性。我们主要使用的证明条款是在定义的置换等价超限减少，置换方程的基础上。这个定义涉及到一个等式逻辑的变体，适用于处理无限对象。通过证明项证明了压缩属性，建立了原始约简和压缩约简之间的置换等价性。
2014-02-12 cs.LO
Projections for infinitary rewriting
项重写中的证明项是约简序列的表示方法，更一般地说是收缩活动的表示方法，允许区分例如同时约简和顺序约简。有限性、一阶、左线性项重写的证明项在Terese书的第8章中描述。在以前的工作中，我们定义了有限证明项形式主义的扩展，它允许描述无穷一阶项重写中的收缩，并给出了置换等价的特征。在这项工作中，我们讨论了如何可能无限重写序列的投影可以使用证明项建模。同样，这个基础是Terese在8.7节中描述的有限重写的投影的特征。我们扩展到无限重写，并完善它的特点，通过精确描述的作用，结构对等的概念的发展中发挥的投影。我们提出的表征产生一个明确的表达，即一个证明项，它描述了一个无穷约简在另一个无穷约简上的投影。为了说明投影的工作，我们展示了如何通过各自的投影获得一个（可能是无限的）约简的公共约简和一个使其成为一部分的单步的。我们表明，通过几个例子，所提出的定义产生预期的行为也超出了这个结果所涵盖的情况下。最后，我们讨论了极限的概念是如何用于我们的无限约化投影的定义。
2016-09-22 cs.LO
Partial Order Infinitary Term Rewriting
我们研究了无穷项重写的另一种模型。而不是一个度量的条款，偏序部分条款的形式化收敛的减少。我们认为，一个弱的和强的收敛性的概念，并表明，度量模型的收敛性与偏序模型限制总条款。因此，偏序收敛构成了度量收敛的保守扩展，它还提供了不同水平的发散之间的细粒度区分。第二部分主要研究正交系的强收敛性。主要结果是，度量模型和偏序模型之间的差距可以通过扩展的条款重写系统的额外规则来弥合。这些扩展是著名的Böhm扩展。基于这一结果，我们能够建立-相反的度量设置-正交系统都是无限合流和无限规范化的偏序设置。偏序模型所允许的唯一无穷范式是Böhm树。
2014-06-02 cs.LO
Compression for Coinductive Rewriting and the Cut-Elimination of Non-Wellfounded Proofs
Université Paris Cité（巴黎西岱大学）；CNRS（法国国家科学研究中心）；IRIF（IRIF实验室）；DISI, Università di Bologna（博洛尼亚大学DISI）；INRIA Picube
本文提出了一种通用方法，用于处理混合归纳与共归纳的语法对象，应用于无穷重构及非非良好基础证明的切消。
2026-08-24 cs.LO
Infinitary Combinatory Reduction Systems: Normalising Reduction Strategies
我们研究无穷组合归约系统（iCRS）的规范化归约策略。我们证明了所有的公平，outermost公平，和所需的公平的策略是规范化的正交，完全扩展的iCRS。这些事实适当地概括了一些结果规范化战略在一阶无穷重写，并提供了第一个例子规范化战略的无穷λ演算。
2010-02-25 cs.LO
Realizing evaluation strategies by hierarchical graph rewriting
我们讨论的实现评价策略的并发约束为基础的功能语言CCFL的翻译模式编译CCFL程序时，到层次图重写语言LMNtal。LMNtal支持表达本地计算和描述本地计算空间之间的过程和规则的迁移，允许对典型的评估策略进行清晰而简单的编码。
2010-09-20 cs.LO cs.PL
Efficient Implementation of Evaluation Strategies via Token-Guided Graph Rewriting
在实现评价策略的计算，正确性和效率的实施是有效的关注。虽然正确性的概念是由评估策略决定的，但关于效率，可以探索更大的设计空间，特别是空间与时间效率之间的权衡。我们通过引入一个抽象的按需调用机器来研究这种权衡，这是受到Girard的交互几何的启发，一个结合了令牌传递和图形重写的机器。这项工作提出了一个扩展的机器，另外容纳左到右和右到左调用的价值战略。我们显示的健全性和完整性的扩展机器方面的每一个呼叫的需要和两个呼叫的价值战略。分析其执行的时间成本将机器归类为“高效”的抽象机器分类法。
2018-02-19 cs.LO cs.PL
From Linear Term Rewriting to Graph Rewriting with Preservation of Termination
将项重写系统（TRS）编码为图重写系统通常会失去全局终止性，这意味着编码不会在所有图上终止。例如，终止TRS规则a（b（x））-> b（a（x））的典型编码可以沿着a和b的循环无限地适用。最近，我们介绍了PBPO+，一个图重写形式主义，其中规则采用类型图来指定转换和控制规则的适用性。在本文中，我们表明，PBPO+允许一个自然的编码的线性TRS规则，保持终止全球。这个结果是对其他重写形式主义建模的一个步骤，例如λ演算和高阶重写，以保留终止和汇合等属性的方式使用图重写。此外，我们希望编码可以作为一个指南，提升TRS终止方法PBPO+重写。
2021-12-21 cs.LO
Drag Rewriting
本文提出基于drags的图重写代数框架，通过根与芽的连接及和积运算扩展了图、dag与项重写模型。
2024-06-27 cs.LO
Term Graph Rewriting and Parallel Term Rewriting
术语图重写和术语重写之间的关系很好理解：由于共享，单个术语图缩减可能对应于多个术语缩减。还已知的是，如果允许项图包含循环，则一个项图约简可以对应于无限多个项约简。我们强调，这一事实可以从两个方面来解释。根据“顺序解释”，项图约简对应于项约简的无限序列，如Kennaway等人在无限项的完整度量空间上使用强收敛导子形式化的。相反，根据“并行解释”，项图约简对应于在有理项中的无限集合的redex的并行约简。我们正式后一个概念，利用完整的偏序的无限和可能的部分条款，我们强调，这种解释允许解释的结果，减少循环赎回的几种方法，长期图重写。
2011-02-14 cs.LO
Patch Graph Rewriting (Extended Version)
图重写的基本原理是逐步替换主图内部的子图。在这样的替换步骤中的一个挑战是补丁图的治疗，包括那些边缘的主机图，接触的子图，但不是它的一部分。我们引入补丁图重写框架，一个可视化的图形重写语言与精确的形式语义。这种语言在两个方面具有丰富的表现力。首先，规则可以灵活地约束与匹配子图接触的面片的允许形状。其次，规则可以自由地转换补丁。虽然框架被设计为易于理解，但它包含了许多图重写的方法。
2020-08-19 cs.LO
Categorical Abstract Rewriting Systems and Functoriality of Graph Transformation
重写系统通常被定义为给定对象集上的二元关系。这个简单的定义被用来描述重写的各种属性，如终止，合流，范式等。在本文中，我们引入了一个新的概念，抽象重写范畴的框架。然后，我们定义了重写系统的函性性质。这种特性有时称为垂直合成。我们表明，大多数图变换系统是函的，并提供了一个反例的图变换系统，这是不是函的。
2011-05-31 cs.LO
Semantics-Preserving DPO-Based Term Graph Rewriting
术语图重写作为函数程序执行的“概念实现”和编译器中的数据流优化是重要的。定义术语图转换规则应用程序的一种方法是通过完善的和直观的双推出（DPO）的方法，我们提出了一个新的结果证明这种基于DPO的术语图重写的语义保存。
2019-02-06 cs.LO
Extending the Overlap Graph for Gene Assembly in Ciliates
基因组装是一个复杂的生物过程，已经通过字符串和图形重写系统进行了形式化研究和建模。最近，一般（分子内）模型的限制，称为简单的基因组装，已被引入。这种限制后来被定义为字符串重写系统。我们表明，通过扩展重叠图的概念，可以定义一个图形重写系统的三种类型的规则，使简单的基因组装。事实证明，这个图重写系统比其对应的字符串重写系统涉及的较少。最后，我们给出了这两种类型的图重写规则的“权力”的特征。由于这些字符串重写系统和图重写系统的等价性，所给出的特征可以被带到字符串重写系统中。
2007-12-20 cs.LO
Parallel Independence in Attributed Graph Rewriting
为了定义图变换的并发规则的同时应用，我们在以前的工作中采用了一种结构的属性图稳定的工会。我们分析的后果并行独立性，一个属性的特点，诉诸顺序重写的可能性。这个性质不仅取决于规则的左边，就像在图重写的代数方法中一样，而且取决于规则的右边。然后，它表明，三种可能的定义并行重写，只有一个是方便的平行独立性。
2021-02-04 cs.LO
In-place Graph Rewriting with Interaction Nets
当一个算法不需要任何额外的内存来执行超过一个小的常量时，它就是就地的，或者说是就地运行的。有许多算法是有效的，因为这个功能，因此它是算法的一个重要方面。在大多数程序设计语言中，算法何时可以就地运行并不明显，而且通常也不清楚实现是否尊重这一思想。在本文中，我们研究交互网络作为一种形式主义，我们可以直接，直观地看到，算法是到位的，而且实现将尊重它是到位的。然而，并不是所有的算法都可以就地运行。尽管如此，我们仍然可以使用相同的语言，但现在我们可以注释可以就地运行的算法部分。我们提出了一个规则的注释，并给出了一个算法，通过分析的相互作用规则，自动找到这个。
2016-09-13 cs.LO cs.PL
Higher-order port-graph rewriting
受生物学启发的端口图框架已成功地用于指定复杂系统。它是PORGY建模工具的基础。为了方便规范的证明规范化程序，通过图重写，在本文中，我们添加了高阶功能，原来的端口图语法，随着广义概念的图形态射。我们提供了一个匹配算法，使实现高阶端口图重写PORGY，从而可以直观地研究建模系统的动态。我们说明了表达能力的高阶端口图的证明网减少系统的例子。
2012-11-17 cs.LO
Graph Rewriting and Relabeling with PBPO+
我们扩展了强大的Pullback-Pushout（PBPO）方法，用于强匹配的图重写。我们的方法称为\pbpostrong，对宿主图中模式的嵌入施加更多控制，这对于一大类图重写系统很重要。此外，我们表明，\pbpostrong是非常适合重写标记图和某些类别的属性图。为了这个目的，我们采用一个标签集上的格结构，并使用保序图态射。我们认为，我们的方法是更简单，更普遍的文献中相关的重新标记方法。
2021-06-25 cs.LO
A PBPO+ Graph Rewriting Tutorial
我们提供了一个教程介绍代数图重写形式主义PBPO+。我们展示了如何PBPO+可以通过组成几个简单的构建块，并作为一个例子模型的二叉决策图的约简规则。一路上，我们评论如何替代设计决策导致相关的形式主义在文献中，如DPO。最后，我们详细地比较了鲍德隆的双回调方法。
2023-03-28 cs.LO
Graph Creation, Visualisation and Transformation
我们描述了一个工具来创建，编辑，可视化和计算的交互网络-一种形式的图形重写系统。这个名为GraphPaper的编辑器允许用户使用直观的用户界面创建和编辑图形及其转换规则。编辑器使用TULIP系统的功能，这使我们能够访问丰富的可视化算法。交互网不仅是一种图的形式化描述，而且是一种基于重写的计算模型。我们讨论了图重写策略和语言来表达它们，以执行战略互动网络重写。
2010-03-23 cs.LO cs.PL cs.SE
Strategic Port Graph Rewriting: An Interactive Modelling and Analysis Framework
我们提出战略portgraph重写的基础上实现可视化建模和分析工具。其目标是促进规范，分析和模拟复杂的系统，使用端口图。系统由初始图和图重写规则的集合以及用户定义的控制规则应用的策略来表示。策略语言包括处理图遍历和管理图中的重写位置的构造。我们给出了一个小步骤的操作语义的语言，并描述了其实现的图形转换和可视化工具PORGY。
2014-07-30 cs.LO cs.SE
Graph Rewriting and Relabeling with PBPO+: A Unifying Theory for Quasitoposes
本文提出PBPO+方法，通过强匹配增强对模式嵌入的控制，证明其可统一PBPO、AGREE和DPO，并适用于带标签图和属性图的重写。
2023-05-25 cs.LO
Needed Computations Shortcutting Needed Steps
我们定义了一个基于构造函数的强顺序图重写系统的编译方案，它可以缩短一些必要的步骤。目标代码是另一个基于构造器的图重写系统。当使用最内层策略时，该系统是对原系统的归一化。因此，目标代码可以容易地由各种程序设计语言中的渴望函数实现。我们修改这个目标代码的方式，避免了一些计算所需的步骤的合同的全部或部分建设。当以这种方式计算范式时，与原始系统中的普通重写计算相比，减少了存储器消耗和执行时间。
2015-05-27 cs.LO cs.PL
AGREE -- Algebraic Graph Rewriting with Controlled Embedding (Long Version)
在文献中提出的几种代数图变换方法都确保了如果一个项被规则保留，那么它与嵌入它的上下文图的连接也是如此。但是，在某些应用中，例如在克隆一个项目时，需要为原始项目和副本指定不同的嵌入。因此，我们提出了这些方法的保守扩展，其中规则可以指定如何更改保留项的嵌入，通常是通过删除某些连接。
2015-06-08 cs.LO
Proceedings 6th International Workshop on Computing with Terms and Graphs
本卷包含第六届国际计算与术语和图形研讨会（TERMGRAPH 2011）的会议记录。该研讨会于2011年4月2日在德国萨尔布吕肯举行，作为第十四届欧洲软件理论与实践联合会议（ETAPS 2011）的一部分。术语和图重写的研究范围从理论问题到实际问题。图计算以自然和无缝的方式处理公共子表达式的共享，并提高了空间和时间上的计算效率。共享是无处不在的几个研究领域，例如：建模的第一和高阶长期重写（无环或循环）图重写，建模的生物或化学抽象机，实现技术的程序设计语言。术语图也用于自动定理证明和符号计算系统中的共享结构。本次研讨会的目的是汇集研究人员在不同领域的术语和图形转换，并促进他们的互动，提供一个论坛，提出新的想法和工作进展，并使新来者了解当前的活动在术语图重写。这些会议记录包含六篇已接受的论文和三篇受邀演讲的摘要。所有提交的材料都经过了仔细的评审。被接受的论文的主题范围很广，包括术语图重写的理论方面，证明方法，语义以及术语图转换的应用问题。
2011-02-11 cs.LO cs.PL cs.SE
Efficient Graph Rewriting
图变换是图的基于规则的修改，是一门可以追溯到20世纪70年代的学科。图重写规则的声明性质是有代价的。一般来说，在宿主图中匹配固定规则的左侧图需要多项式时间。为了提高匹配性能，Dörr建议为规则和宿主图配备可区分的根结点。这个模型是由Plump和Bak实现的，但不幸的是，它不是可逆的。我们解决这个问题，定义根使用部分功能到两点集，而不是指向图的根结点。我们证明了一个新的结果，一类图的树可以识别的根GT系统在线性时间，给定的输入图的有界度。最后，我们定义了一个新的概念的合流模垃圾和非垃圾的关键对，这是足够的，只需要强大的可连接性的非垃圾的关键对建立合流模垃圾。
2021-01-01 cs.CC cs.LO cs.PL
Computational category-theoretic rewriting
本研究将范畴论规范应用于图重写领域，在有限展示C-sets抽象层实现高效算法，提供可扩展的开源库以支持多种数据结构上的重写操作。
2023-03-31 cs.LO
Rewriting Abstract Structures: Materialization Explained Categorically
本文开发了一个抽象的（过近似）语义的双重推出重写的图形和图形类对象。重点是所谓的物化的左手边从抽象的图形，在以前的工作中的一个中心概念。第一个贡献是一个访问，一般性的解释，如何物化产生的普遍属性和分类结构，特别是部分地图分类，在一个拓扑。其次，我们引入了一个扩展丰富的对象注释，并给出了一个精确的表征最强的后置条件，这是有效地计算在某些假设下。
2019-02-13 cs.LO
Graph rewriting with polarized cloning
我们处理的问题，图转换，特别注重节点克隆。我们提出了一种新的方法，图重写节点可以克隆零，一次或多次。节点可以与其所有关联边、仅与其传出边、仅与其传入边或不与其关联边一起克隆。因此，我们继承了以前的工作，如倍半推出，异构推出和自适应星文法的方法。重写规则被定义为一个跨度，其中右手边和左手边是图，而界面是极化图。一个极化图是在节点上赋予某些注释的图。克隆节点的方式由其极化注释指示。我们使用这些注释设计图转换与极化克隆。我们展示了如何克隆一个节点可以建立根据不同的可能的极化，并定义一个重写步骤作为一个最后的回调补充，然后推出。这被称为极化倍半推出方法。我们还提供了一个算法演示所提出的图变换与极化克隆。
2012-04-24 cs.LO
Proving Termination of Unfolding Graph Rewriting for General Safe Recursion
本文给出了一种新的展开图重写的终止性证明和复杂性分析，展开图重写是一种特殊的无限图重写，它表达了安全递归的一般形式。我们引入了一个终止顺序的条款序列连同长期图的解释成序列的条款。展开图重写规则表示一般的安全递归可以成功地嵌入到终止顺序的解释，产生多项式的运行时复杂度。此外，推广的展开图重写规则的定义一般安全递归，我们提出了一个新的标准的多项式运行时复杂性的无限GRS和多项式大小的范式在无限GRS。
2014-06-20 cs.CC cs.LO math.LO
A Set-Theoretic Framework for Parallel Graph Rewriting
我们解决的问题，属性图变换，并提出了一种新的算法方法来定义并行图变换允许重叠。我们首先介绍一些图结构上的抽象操作。然后，我们将重写规则的概念定义为$L \supseteq K \supseteq M \subseteq R$形式的三个包含。我们提供了六个条件，并行图重写关系应该理想地满足，这导致我们定义两个不同的完全并行图重写关系。一个中心概念的正则性的匹配被证明是等价于这六个条件，并平等的这两个关系。此外，我们利用可能发生在$L$，$K$，$M$和$R$中的对称性，并定义另一对重写关系，这些重写关系可以分解出可能的许多等价匹配，直到它们的公共对称性。这些定义和相应的证明相结合的操作图与群论的概念，从而说明了我们的框架的相关性。
2018-08-09 cs.LO
Proceedings Tenth International Workshop on Computing with Terms and Graphs
本卷包含了在TERMGRAPH 2018上发表的论文的精选，这是第十版的术语和图形计算国际研讨会。图和图转换系统在计算机科学的许多领域中使用：表示数据结构和算法，定义计算模型，作为研究复杂系统的通用建模工具等。这一领域的研究涉及一系列理论和实际问题，包括一阶和高阶项重写的建模，（非循环或循环）图重写，图形框架，如交互网络和共享图（最优归约），重写函数程序分析演算，程序设计语言的图形归约实现，图形演算建模并发和移动计算，面向对象系统，图作为生物或化学系统的模型，以及在共享结构上工作的自动推理和符号计算系统。以前的TERMGRAPH在巴塞罗那（2002年），罗马（2004年），维也纳（2006年），布拉加（2007年），约克（2009年），萨尔布吕肯（2011年），罗马（2013年），维也纳（2014年）和埃因霍温（2016年）举行。TERMGRAPH 2018隶属于FSCD，FSCD是FLOC的一部分。
2019-02-05 cs.LO cs.PL
Non-simplifying Graph Rewriting Termination
LORIA（洛林信息学及其应用研究实验室）；Université de Lorraine（洛林大学）；Inria Nancy Grand-Est（法国国家信息与自动化研究所南锡大东部中心）
到目前为止，自然语言处理（NLP）中的大量工作依赖于树作为核心数学结构来表示语言信息（例如Chomsky的工作）。然而，有些语言现象并不能很好地处理树。在以前的论文中，我们展示了用图来编码语言结构和使用图重写规则来计算这些结构的好处。出于一些语言学上的考虑，图重写的特征在于两个特征：第一，沿着计算没有节点创建，第二，有非局部边修改。在这些假设下，我们证明了一致终止是不可判定的，非一致终止是可判定的。我们描述了两个终止技术的基础上的重量，我们给这些重写系统的推导长度的复杂性界。
2013-02-26 cs.CC cs.CL cs.LO
On Causal Equivalence by Tracing in String Rewriting
我们介绍证明字符串重写系统，并使用这些，表明从文献中已知的各种概念的等价减少可以被视为不同的观点的因果等价的概念。特别是，我们表明，置换等价类（如已知的从微积分和长期重写）是唯一表示的迹图（从物理学称为因果图）和所谓的贪婪的多步减少（如已知的代数）。我们提出了从前者到后者的有效映射，拓扑多排序TM，反之亦然，证明项代数[[]]。
2023-03-28 cs.LO
A Modal Logic for Termgraph Rewriting
我们提出了一个模态逻辑量身定制的描述图变换，并讨论了它的一些属性。我们专注于一类特殊的图，称为termgraphs。它们是一阶项，增加了共享和循环。Termgraphs允许一个描述经典的数据结构（可能与指针），如双向链表，循环列表等，我们展示了如何建议的逻辑可以忠实地描述（一）termgraphs以及（二）应用termgraphs重写规则（即匹配和替换）和（iii）计算范式相对于一个给定的重写系统。我们还展示了如何建议的逻辑，这是更具表现力的命题动态逻辑，可以用来指定形状的经典数据结构（如二叉树，循环列表等）。
2010-03-23 cs.LO cs.PL cs.SC
Towards Practicable Algorithms for Rewriting Graph Queries beyond DL-Lite
本文提出一种针对扩展DL-Lite的ELHI受限片段中导航查询的重写技术，将查询转为Cypher以支持Neo4j图数据库，并在认知神经科学用例上验证了有效性。
2025-04-23 cs.DB cs.LO
Adhesive category theory for graph rewriting in Rocq
ENS de Lyon, CNRS, UCBL1, LIP, Plume team, UMR 5668（里昂高等师范学院，法国国家科学研究中心，里昂第一大学，信息学实验室，Plume团队）
本文设计了Rocq库用于粘性范畴理论，形式化了图重写理论中的Church-Rosser定理和并发定理，并提供了多个实例。
2026-03-02 cs.LO
Proving Termination of Graph Transformation Systems using Weighted Type Graphs over Semirings
本文提出基于有序半环的加权类型图方法，将矩阵解释推广到图重写，通过权重递减证明图变换系统的均匀终止性，并在工具Grez中实现。
2023-10-11 cs.FL cs.LO
Datapath Verification via Word-Level E-Graph Rewriting
提出一种基于e-graph数据结构的字级位宽相关重写框架，辅助datapath等价性检查，通过生成中间证明使工业工具实现收敛并将证明时间缩减至6倍。
2023-08-01 cs.AR cs.LO
Thermodynamic graph-rewriting
我们开发了一种新的热力学方法来随机图重写。成分是一组有限的可逆图重写规则称为生成规则，一组有限的连接图P称为能量模式和能量成本函数。其思想是，生成器通过显示哪些变换是可能的来定义定性动态，而能量模式和成本函数指定任何可达图的长期概率$π$。给定生成器和能量模式，我们构造了一组有限的规则，其中（i）具有与生成器相同的定性转移系统;以及（ii）当配备适当的速率时，定义了一个连续时间马尔可夫链，其中$π$是唯一的不动点。建设依赖于使用的网站图和技术的“增长政策”的量化规则的完善，这是独立的利益。动态的定性和长期定量方面之间的这种分工导致对现实模型的直观和简洁的描述（参见S4和S5中的示例）。它还保证了物理一致性（也称为详细平衡），否则已知是不可判定的，这对某些应用程序很重要。最后，它导致模型的参数化，这在某些应用中也是一个重要的问题。
2015-06-23 cs.LO q-bio.MN
Equivalence Hypergraphs: DPO Rewriting for Monoidal E-Graphs
本文为e-graph给出半格富集笛卡尔范畴的范畴论语义，将其推广至幺半范畴，提出e-hypergraph作为态射的可靠完备组合表示，并实现了适用于这类结构的DPO重写。
2025-05-20 cs.LO math.CT
Parallel Graph Rewriting with Overlapping Rules
我们解决的问题，同时转换的网络表示为图形。粗略地说，可以区分两种类型的同时或并行重写关系在复杂的结构，如图：（i）那些并行转换不相交的子图，因此可以模拟连续的纯粹的顺序和局部变换和（ii）那些同时转换重叠的子图。在后一种情况下，并行变换一般不能通过连续的局部重写步骤来模拟。我们调查这最后一个问题的重叠图变换系统的框架。由于图的并行变换一般不产生图，我们首先提出了保证图的并行重写关系封闭的一些充分条件。然后重点介绍和讨论了图上的两种并行重写关系。一个关系是功能性的，从而确定性的，另一个是不功能的，我们提出了充分的条件，确保其汇合。
2017-01-24 cs.FL cs.LO
A Generalized Concurrent Rule Construction for Double-Pushout Rewriting
双推出重写是一种已建立的基于规则的图和类图对象转换的分类方法。它的标准结果之一是并发规则的构造和与之相关的并发定理：两个规则的顺序应用可以等价地被一个并发规则的应用所取代，反之亦然。我们通过引入广义并发规则（GCR）来扩展和推广这个结果。它们的区别在于，它们允许识别和保留被第一个基础规则删除而被第二个基础规则创建的元素。我们将这种新的规则组合置于现有的规则组合中，得到了它的广义并发定理，并在与并发定理相同的一般框架下进行了工作，即在M-粘着范畴中通过规则配置应用条件的双重推出重写.
2021-05-05 cs.LO
Blind graph rewriting systems
我们考虑一个简单的（可能是最简单的）随机存取存储器的结构。这种结构可以用来构建一个通用的系统，几乎空的处理器，即，我们证明了这样的系统的处理器可能有空的指令集，在一个更强大的方式比现有的ZISC（零指令集计算机的人工神经网络的想法的基础上）和NISC架构（无指令集计算）。更确切地说，处理器将被禁止分析存储在存储器中的任何信息，后者是这种机器的唯一状态。这篇论文将覆盖这个想法的一个孤立的方面，特别是，提供嵌入到系统中的逻辑操作，而没有任何内置的条件语句。
2012-04-16 cs.FL cs.LO
Unfolding of Finite Concurrent Automata
我们考虑可识别的跟踪重写系统与水平正规上下文（RTL）。如果一个跟踪语言的元素的Foata范式集合是正则的，则该跟踪语言是水平正则的。我们证明了RTL的重写图是字自动的。因此，它的一阶理论是可判定的。然后，我们证明了具有可达关系的有限并发自动机的并发开折是RTL图。由此可见，具有这种展开的可达性谓词（FO[Reach]理论）的一阶理论是可判定的。据了解，这一性质也适用于地面项重写图。我们提供了有限并发自动机的并发展开失败的地面长期重写图的例子。无限网格树（对于无限网格的每个顶点，都有一条从该顶点到无限网格副本原点的边）就是这样一种展开。我们证明了无限格树不是基项重写图。我们由此得到了一类新的具有可判定FO[Reach]理论的图.
2018-10-05 cs.FL cs.LO
On Term Rewriting Systems Having a Rational Derivation
几种类型的术语重写系统可以通过它们的规则重叠的方式来区分。特别是，我们定义了前缀，后缀，自底向上和自顶向下的系统，概括了类似的类的话。我们的目的是研究这类系统的派生关系（即重写关系的自反闭包和传递闭包），并在可能的情况下给出一个有限的机制来刻画它，利用基于有限图文法的有理关系的概念，我们证明了任何自底向上、自顶向下或后缀系统的派生都是有理的，而前缀系统的派生可以是非递归的.
2007-05-28 cs.LO
Structured Operational Semantics for Graph Rewriting
进程演算和图转换系统提供了具有标记转换语义的反应系统模型。虽然进程演算的语义是组合的，但一般来说，图转换系统的情况并非如此。因此，这篇文章的目标是获得一个组合语义图转换系统类似的结构操作语义（SOS）米尔纳的演算通信系统（CCS）。本文介绍了图变换系统的标准标号变迁语义的SOS式公理化。第一个结果是它等同于所谓的借用上下文技术。不幸的是，公理化不是以预期的方式组成的，因为没有规则捕获子系统的“内部”通信。主要结果表明，这样的规则是可导的，如果给定的图转换系统享有一定的属性，我们称之为“互补的行动”。这种系统的典型例子是交互网络。我们还讨论了出现的问题，如果“行动的互补性”被违反。
2011-08-02 cs.DC cs.LO
A Category of Surface-Embedded Graphs
引入曲面嵌入图重写的范畴形式化方法，通过明确记录边界的双推出重写新表述与旋转系统，将曲面拓扑纳入其中以表示非对称弦图。
2023-07-31 cs.LO
Proceedings 7th International Workshop on Computing with Terms and Graphs
本卷包含第七届国际术语和图形计算研讨会（TERMGRAPH 2013）的会议记录。研讨会于2013年3月23日在意大利罗马举行，作为第十六届欧洲软件理论与实践联合会议（ETAPS 2013）的一部分。术语和图重写的研究范围从理论问题到实际问题。图计算以自然和无缝的方式处理公共子表达式的共享，并提高了空间和时间上的计算效率。共享是无处不在的几个研究领域，作为见证的建模的第一和高阶长期重写（无环或循环）图重写，生物或化学抽象机的建模，以及程序设计语言的实现技术：许多实现功能，逻辑，面向对象，并发和移动演算是基于长期图。术语图也用于自动定理证明和符号计算系统中的共享结构。本次研讨会的目的是汇集研究人员在不同领域的术语和图形转换，并促进他们的互动，提供一个论坛，提出新的想法和工作进展，并使新来者了解当前的活动在术语图重写。这些会议记录包含六篇已接受的论文和两篇特邀演讲的摘要。所有提交的材料都经过了仔细的评审。接受的论文的主题范围很广，包括术语图重写，并发，语义以及术语图转换的应用问题的理论方面。
2013-02-25 cs.LO cs.SC
Complexity of Deciding Syntactic Equivalence up to Renaming for Term Rewriting Systems (Extended Version)
从程序转换的问题的动机，八个概念之间的同构术语重写系统的定义，分析和分类。这些概念包括全局同构，其中变量和函数符号的重命名对于系统的所有项重写规则都是相同的，局部同构，其中每个规则使用单个重命名，以及组合，其中一个符号集被全局重命名，而另一个符号集被局部重命名。保存语义属性，如可转换性和终止分析不同的同构概念。引入了项重写系统的模板和极大范式的概念，并给出了有效计算它们的算法。配备这些技术，同构的基本决策问题的复杂性进行了分析，并被证明是有效的解决或证明是完整的图同构复杂性类。
2022-11-30 cs.LO
