Infinitary Term Graph Rewriting
术语图重写提供了一种通过避免重复以有效方式实现术语重写的形式体系。无穷项重写被用来研究无穷项约简序列。这样的无限约简可以用来推理惰性求值。在本文中，我们结合术语图重写和无限项重写，从而解决懒惰评估的两个组成部分：非严格性和共享。此外，我们展示了我们的理论基础，基于度量空间和一个完整的半格，提供了一个统一的框架，长期重写和长期图重写。这使得研究这两个世界之间的对应关系成为可能。作为一个例子，我们展示了如何健全的长期图重写w.r.t.项重写可以扩展到无穷大设置。
2011-07-04 cs.LO cs.PL
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
Higher-order port-graph rewriting
受生物学启发的端口图框架已成功地用于指定复杂系统。它是PORGY建模工具的基础。为了方便规范的证明规范化程序，通过图重写，在本文中，我们添加了高阶功能，原来的端口图语法，随着广义概念的图形态射。我们提供了一个匹配算法，使实现高阶端口图重写PORGY，从而可以直观地研究建模系统的动态。我们说明了表达能力的高阶端口图的证明网减少系统的例子。
2012-11-17 cs.LO
Modes of Convergence for Term Graph Rewriting
项图重写提供了一种简单的机制来表示受限形式的无穷项重写。无穷项重写与项图重写之间的对应关系已经得到了一定程度的研究。然而，这一努力是削弱了缺乏一个适当的对应的无限重写的一方的长期图。我们的目标是填补这一空白，设计了两种模式的收敛的基础上分别为一个度量的偏序图。由此获得的结构概括了相应的模式的收敛，通常是在无穷项重写研究。我们认为，这产生了一个共同的框架，在其中长期重写和长期图重写可以研究。为了证实我们的主张，我们比较了术语图和术语上的收敛性。特别是，我们表明，长期图上的收敛模式是保守的扩展，相应的模式收敛的条款，并保存unravelling长期图的条款。此外，我们发现，许多已知的无穷项重写的属性被保留。这包括两种收敛模式的内在完备性，以及通过偏序收敛是度量收敛的保守扩展。
2012-05-31 cs.LO cs.PL
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
Strategic Port Graph Rewriting: An Interactive Modelling and Analysis Framework
我们提出战略portgraph重写的基础上实现可视化建模和分析工具。其目标是促进规范，分析和模拟复杂的系统，使用端口图。系统由初始图和图重写规则的集合以及用户定义的控制规则应用的策略来表示。策略语言包括处理图遍历和管理图中的重写位置的构造。我们给出了一个小步骤的操作语义的语言，并描述了其实现的图形转换和可视化工具PORGY。
2014-07-30 cs.LO cs.SE
Convergence in Infinitary Term Graph Rewriting Systems is Simple (Extended Abstract)
在这个扩展的摘要中，我们提出了一个简单的方法来收敛项图，使我们能够统一项图重写和无穷项重写。这种方法是基于偏序和度量的术语图。这些结构是无穷项重写中使用的相应结构的简单概括。我们将我们的简单方法与我们之前开发的更复杂的方法进行比较，并表明这种新方法在许多方面都更优越。唯一不利的财产，我们能够确定，即失败的弱度量和偏序收敛之间的充分对应，是通过采用强收敛纪律纠正。
2013-02-26 cs.LO cs.PL
Graph Rewriting and Relabeling with PBPO+: A Unifying Theory for Quasitoposes
本文提出PBPO+方法，通过强匹配增强对模式嵌入的控制，证明其可统一PBPO、AGREE和DPO，并适用于带标签图和属性图的重写。
2023-05-25 cs.LO
Proving Termination of Unfolding Graph Rewriting for General Safe Recursion
本文给出了一种新的展开图重写的终止性证明和复杂性分析，展开图重写是一种特殊的无限图重写，它表达了安全递归的一般形式。我们引入了一个终止顺序的条款序列连同长期图的解释成序列的条款。展开图重写规则表示一般的安全递归可以成功地嵌入到终止顺序的解释，产生多项式的运行时复杂度。此外，推广的展开图重写规则的定义一般安全递归，我们提出了一个新的标准的多项式运行时复杂性的无限GRS和多项式大小的范式在无限GRS。
2014-06-20 cs.CC cs.LO math.LO
AGREE -- Algebraic Graph Rewriting with Controlled Embedding (Long Version)
在文献中提出的几种代数图变换方法都确保了如果一个项被规则保留，那么它与嵌入它的上下文图的连接也是如此。但是，在某些应用中，例如在克隆一个项目时，需要为原始项目和副本指定不同的嵌入。因此，我们提出了这些方法的保守扩展，其中规则可以指定如何更改保留项的嵌入，通常是通过删除某些连接。
2015-06-08 cs.LO
Realizing evaluation strategies by hierarchical graph rewriting
我们讨论的实现评价策略的并发约束为基础的功能语言CCFL的翻译模式编译CCFL程序时，到层次图重写语言LMNtal。LMNtal支持表达本地计算和描述本地计算空间之间的过程和规则的迁移，允许对典型的评估策略进行清晰而简单的编码。
2010-09-20 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
Non-simplifying Graph Rewriting Termination
LORIA（洛林信息学及其应用研究实验室）；Université de Lorraine（洛林大学）；Inria Nancy Grand-Est（法国国家信息与自动化研究所南锡大东部中心）
到目前为止，自然语言处理（NLP）中的大量工作依赖于树作为核心数学结构来表示语言信息（例如Chomsky的工作）。然而，有些语言现象并不能很好地处理树。在以前的论文中，我们展示了用图来编码语言结构和使用图重写规则来计算这些结构的好处。出于一些语言学上的考虑，图重写的特征在于两个特征：第一，沿着计算没有节点创建，第二，有非局部边修改。在这些假设下，我们证明了一致终止是不可判定的，非一致终止是可判定的。我们描述了两个终止技术的基础上的重量，我们给这些重写系统的推导长度的复杂性界。
2013-02-26 cs.CC cs.CL cs.LO
Graph rewriting with polarized cloning
我们处理的问题，图转换，特别注重节点克隆。我们提出了一种新的方法，图重写节点可以克隆零，一次或多次。节点可以与其所有关联边、仅与其传出边、仅与其传入边或不与其关联边一起克隆。因此，我们继承了以前的工作，如倍半推出，异构推出和自适应星文法的方法。重写规则被定义为一个跨度，其中右手边和左手边是图，而界面是极化图。一个极化图是在节点上赋予某些注释的图。克隆节点的方式由其极化注释指示。我们使用这些注释设计图转换与极化克隆。我们展示了如何克隆一个节点可以建立根据不同的可能的极化，并定义一个重写步骤作为一个最后的回调补充，然后推出。这被称为极化倍半推出方法。我们还提供了一个算法演示所提出的图变换与极化克隆。
2012-04-24 cs.LO
Towards Practicable Algorithms for Rewriting Graph Queries beyond DL-Lite
本文提出一种针对扩展DL-Lite的ELHI受限片段中导航查询的重写技术，将查询转为Cypher以支持Neo4j图数据库，并在认知神经科学用例上验证了有效性。
2025-04-23 cs.DB cs.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
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
On Causal Equivalence by Tracing in String Rewriting
我们介绍证明字符串重写系统，并使用这些，表明从文献中已知的各种概念的等价减少可以被视为不同的观点的因果等价的概念。特别是，我们表明，置换等价类（如已知的从微积分和长期重写）是唯一表示的迹图（从物理学称为因果图）和所谓的贪婪的多步减少（如已知的代数）。我们提出了从前者到后者的有效映射，拓扑多排序TM，反之亦然，证明项代数[[]]。
2023-03-28 cs.LO
Equivalence Hypergraphs: DPO Rewriting for Monoidal E-Graphs
本文为e-graph给出半格富集笛卡尔范畴的范畴论语义，将其推广至幺半范畴，提出e-hypergraph作为态射的可靠完备组合表示，并实现了适用于这类结构的DPO重写。
2025-05-20 cs.LO math.CT
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
Efficient Graph Rewriting
图变换是图的基于规则的修改，是一门可以追溯到20世纪70年代的学科。图重写规则的声明性质是有代价的。一般来说，在宿主图中匹配固定规则的左侧图需要多项式时间。为了提高匹配性能，Dörr建议为规则和宿主图配备可区分的根结点。这个模型是由Plump和Bak实现的，但不幸的是，它不是可逆的。我们解决这个问题，定义根使用部分功能到两点集，而不是指向图的根结点。我们证明了一个新的结果，一类图的树可以识别的根GT系统在线性时间，给定的输入图的有界度。最后，我们定义了一个新的概念的合流模垃圾和非垃圾的关键对，这是足够的，只需要强大的可连接性的非垃圾的关键对建立合流模垃圾。
2021-01-01 cs.CC cs.LO cs.PL
Parallel Graph Rewriting with Overlapping Rules
我们解决的问题，同时转换的网络表示为图形。粗略地说，可以区分两种类型的同时或并行重写关系在复杂的结构，如图：（i）那些并行转换不相交的子图，因此可以模拟连续的纯粹的顺序和局部变换和（ii）那些同时转换重叠的子图。在后一种情况下，并行变换一般不能通过连续的局部重写步骤来模拟。我们调查这最后一个问题的重叠图变换系统的框架。由于图的并行变换一般不产生图，我们首先提出了保证图的并行重写关系封闭的一些充分条件。然后重点介绍和讨论了图上的两种并行重写关系。一个关系是功能性的，从而确定性的，另一个是不功能的，我们提出了充分的条件，确保其汇合。
2017-01-24 cs.FL cs.LO
Efficient Implementation of Evaluation Strategies via Token-Guided Graph Rewriting
在实现评价策略的计算，正确性和效率的实施是有效的关注。虽然正确性的概念是由评估策略决定的，但关于效率，可以探索更大的设计空间，特别是空间与时间效率之间的权衡。我们通过引入一个抽象的按需调用机器来研究这种权衡，这是受到Girard的交互几何的启发，一个结合了令牌传递和图形重写的机器。这项工作提出了一个扩展的机器，另外容纳左到右和右到左调用的价值战略。我们显示的健全性和完整性的扩展机器方面的每一个呼叫的需要和两个呼叫的价值战略。分析其执行的时间成本将机器归类为“高效”的抽象机器分类法。
2018-02-19 cs.LO cs.PL
Blind graph rewriting systems
我们考虑一个简单的（可能是最简单的）随机存取存储器的结构。这种结构可以用来构建一个通用的系统，几乎空的处理器，即，我们证明了这样的系统的处理器可能有空的指令集，在一个更强大的方式比现有的ZISC（零指令集计算机的人工神经网络的想法的基础上）和NISC架构（无指令集计算）。更确切地说，处理器将被禁止分析存储在存储器中的任何信息，后者是这种机器的唯一状态。这篇论文将覆盖这个想法的一个孤立的方面，特别是，提供嵌入到系统中的逻辑操作，而没有任何内置的条件语句。
2012-04-16 cs.FL cs.LO
Dynamic Tracing: a graphical language for rewriting protocols
本研究将Set_*范畴的追踪幺半结构中的隐式转换过程显式化，推广到更多追踪Kleisli范畴并给出推测性追踪算子，为图重写计算提供形式化图形语法。
2023-05-01 cs.LO math.CT math.LO
Graph Creation, Visualisation and Transformation
我们描述了一个工具来创建，编辑，可视化和计算的交互网络-一种形式的图形重写系统。这个名为GraphPaper的编辑器允许用户使用直观的用户界面创建和编辑图形及其转换规则。编辑器使用TULIP系统的功能，这使我们能够访问丰富的可视化算法。交互网不仅是一种图的形式化描述，而且是一种基于重写的计算模型。我们讨论了图重写策略和语言来表达它们，以执行战略互动网络重写。
2010-03-23 cs.LO cs.PL cs.SE
Unfolding of Finite Concurrent Automata
我们考虑可识别的跟踪重写系统与水平正规上下文（RTL）。如果一个跟踪语言的元素的Foata范式集合是正则的，则该跟踪语言是水平正则的。我们证明了RTL的重写图是字自动的。因此，它的一阶理论是可判定的。然后，我们证明了具有可达关系的有限并发自动机的并发开折是RTL图。由此可见，具有这种展开的可达性谓词（FO[Reach]理论）的一阶理论是可判定的。据了解，这一性质也适用于地面项重写图。我们提供了有限并发自动机的并发展开失败的地面长期重写图的例子。无限网格树（对于无限网格的每个顶点，都有一条从该顶点到无限网格副本原点的边）就是这样一种展开。我们证明了无限格树不是基项重写图。我们由此得到了一类新的具有可判定FO[Reach]理论的图.
2018-10-05 cs.FL cs.LO
Structured Operational Semantics for Graph Rewriting
进程演算和图转换系统提供了具有标记转换语义的反应系统模型。虽然进程演算的语义是组合的，但一般来说，图转换系统的情况并非如此。因此，这篇文章的目标是获得一个组合语义图转换系统类似的结构操作语义（SOS）米尔纳的演算通信系统（CCS）。本文介绍了图变换系统的标准标号变迁语义的SOS式公理化。第一个结果是它等同于所谓的借用上下文技术。不幸的是，公理化不是以预期的方式组成的，因为没有规则捕获子系统的“内部”通信。主要结果表明，这样的规则是可导的，如果给定的图转换系统享有一定的属性，我们称之为“互补的行动”。这种系统的典型例子是交互网络。我们还讨论了出现的问题，如果“行动的互补性”被违反。
2011-08-02 cs.DC cs.LO
A Generalized Concurrent Rule Construction for Double-Pushout Rewriting
双推出重写是一种已建立的基于规则的图和类图对象转换的分类方法。它的标准结果之一是并发规则的构造和与之相关的并发定理：两个规则的顺序应用可以等价地被一个并发规则的应用所取代，反之亦然。我们通过引入广义并发规则（GCR）来扩展和推广这个结果。它们的区别在于，它们允许识别和保留被第一个基础规则删除而被第二个基础规则创建的元素。我们将这种新的规则组合置于现有的规则组合中，得到了它的广义并发定理，并在与并发定理相同的一般框架下进行了工作，即在M-粘着范畴中通过规则配置应用条件的双重推出重写.
2021-05-05 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
Reversibility and Composition of Rewriting in Hierarchies
Univ Lyon（里昂大学）；EnsL（里昂高等师范学院）；UCBL（里昂第一大学）；CNRS（法国国家科学研究中心）
在本文中，我们研究了基于倍半推出重写的图变换如何被反转以及重写的组合如何被构造。我们说明了这种可逆性和组合可以用来设计一个审计跟踪系统的个人图和图层次结构。这为我们提供了一种紧凑的方式来维护对象的更新历史，包括其多个版本。所设计的框架的主要应用程序是一个审计跟踪更新的知识表示的层次结构的图形。因此，我们引入了规则层次结构的概念，它代表了整个层次结构的转换，研究规则层次结构如何可以应用于层次结构和分析的条件下，这种应用是可逆的。然后，我们提出了一个理论，用于构建连续层次重写的组合。用于在具有属性的简单图的层次结构中进行转换的原型审计跟踪系统作为ReGraph Python库的一部分实现。
2020-12-03 cs.AI cs.DB 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
Interactions between Causal Structures in Graph Rewriting Systems
图重写形式主义是一个强大的方法来建模复杂的分子系统。它们捕捉分子相互作用的内在并发性，从而实现机制的正式概念（部分有序的事件集），解释系统如何在给定一组重写规则的情况下实现特定结果。然后，验证从给定模型中出现的机制是否符合关于它们相互干扰的经验观察是有用的。在这项工作中，我们的目标是确定实现X的机制中的特定事件是否阻止或促进实现Y的机制中的特定事件的发生。这种检查也可用来假设使示范机制符合观察结果的规则。我们定义了一个严格的框架，用于定义由图形重写规则系统引起的机制之间的干扰（积极或消极）的概念，并用于确定是否可以实现两种机制作为输入的断言的影响。
2019-01-03 cs.CE cs.LO
A Category of Surface-Embedded Graphs
引入曲面嵌入图重写的范畴形式化方法，通过明确记录边界的双推出重写新表述与旋转系统，将曲面拓扑纳入其中以表示非对称弦图。
2023-07-31 cs.LO
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
Sesqui-Pushout Rewriting: Concurrency, Associativity and Rule Algebra Framework
Sesqui-pushout（SqPO）重写是图形和其他类型结构的变换的变体，其适合粘合剂类别的框架，其中可以实现未知上下文中的删除。我们提供了第一个帐户的并发性定理这一重要类型的重写，我们证明了这些理论的结合性的一种形式的额外的数学属性。然后可以利用结合性来构造所谓的规则代数（SqPO类型），基于该规则代数，特别是可以实现用于随机SqPO重写系统的连续时间马尔可夫链的通用框架。
2019-12-20 cs.DM cs.LO
In-place Graph Rewriting with Interaction Nets
当一个算法不需要任何额外的内存来执行超过一个小的常量时，它就是就地的，或者说是就地运行的。有许多算法是有效的，因为这个功能，因此它是算法的一个重要方面。在大多数程序设计语言中，算法何时可以就地运行并不明显，而且通常也不清楚实现是否尊重这一思想。在本文中，我们研究交互网络作为一种形式主义，我们可以直接，直观地看到，算法是到位的，而且实现将尊重它是到位的。然而，并不是所有的算法都可以就地运行。尽管如此，我们仍然可以使用相同的语言，但现在我们可以注释可以就地运行的算法部分。我们提出了一个规则的注释，并给出了一个算法，通过分析的相互作用规则，自动找到这个。
2016-09-13 cs.LO cs.PL
String Diagram Rewrite Theory II: Rewriting with Symmetric Monoidal Structure
对称monoidal理论（SMTs）以一种使它们适合表达资源敏感系统的方式概括了代数理论，其中变量不能随意复制或丢弃。在SMT中，传统的树状术语被弦图所取代，弦图是一种拓扑实体，可以直观地认为是电线和盒子的图。最近，弦图作为一种图形语法越来越受欢迎，可以在不同的领域推理计算模型，包括程序设计语言语义学、电路理论、量子力学、语言学和控制理论。在应用中，通常将SMT中出现的方程实现为重写规则是方便的。这就提出了挑战，延长传统的长期重写理论，这已经发展为代数理论，弦图。在本文中，我们开发了一个数学理论的串图改写SMT。我们的方法利用了在本系列的第一篇论文中介绍的某些图的弦图重写和双推出（DPO）重写之间的对应关系。只有当SMT包含Frobenius代数结构时，这种对应才是合理的。在目前的工作中，我们将展示如何建立一个类似的对应任意SMT，一旦一个适当的概念DPO重写（我们称之为凸）被确定。作为概念证明，我们使用我们的方法来显示两个感兴趣的SMT的终止：Frobenius半代数和双代数。
2022-09-14 cs.LO math.CT math.LO
A Modal Logic for Termgraph Rewriting
我们提出了一个模态逻辑量身定制的描述图变换，并讨论了它的一些属性。我们专注于一类特殊的图，称为termgraphs。它们是一阶项，增加了共享和循环。Termgraphs允许一个描述经典的数据结构（可能与指针），如双向链表，循环列表等，我们展示了如何建议的逻辑可以忠实地描述（一）termgraphs以及（二）应用termgraphs重写规则（即匹配和替换）和（iii）计算范式相对于一个给定的重写系统。我们还展示了如何建议的逻辑，这是更具表现力的命题动态逻辑，可以用来指定形状的经典数据结构（如二叉树，循环列表等）。
2010-03-23 cs.LO cs.PL cs.SC
Rewriting for Symmetric Monoidal Categories with Commutative (Co)Monoid Structure
本文研究弦图重写中比完整 Frobenius 结构更弱的交换幺半群结构，并通过超图双推出重写的可靠且完备解释刻画了模去交换幺半群等式的弦图重写。
2025-01-30 cs.LO math.CT
Needed Computations Shortcutting Needed Steps
我们定义了一个基于构造函数的强顺序图重写系统的编译方案，它可以缩短一些必要的步骤。目标代码是另一个基于构造器的图重写系统。当使用最内层策略时，该系统是对原系统的归一化。因此，目标代码可以容易地由各种程序设计语言中的渴望函数实现。我们修改这个目标代码的方式，避免了一些计算所需的步骤的合同的全部或部分建设。当以这种方式计算范式时，与原始系统中的普通重写计算相比，减少了存储器消耗和执行时间。
2015-05-27 cs.LO cs.PL
Equational reasoning with context-free families of string diagrams
字符串图提供了一种直观的语言，以图形方式表达相互作用的进程网络。弦图的离散表示，称为弦图，允许通过双推出重写进行机械化等式推理。然而，人们往往希望表达的不仅仅是单个方程，而是任意大小的图之间的整个方程族。为了做到这一点，我们定义了一类上下文无关文法，称为B-ESG文法，它适用于定义整个系列的字符串图，至关重要的是，字符串图重写规则。我们表明，这些语法的语言成员资格和匹配枚举问题是可判定的，因此，有一个算法重写字符串图根据B-ESG重写模式。我们还表明，它是可能的原因，在语法的水平，通过提供一个简单的方法，转换语法的字符串图重写，并显示受理的诱导B-ESG重写模式。
2015-10-13 cs.FL cs.LO math.CT
A Visual Analytics Approach to Compare Propagation Models in Social Networks
描述社交网络中的社会影响的许多传播模型可以在文献中找到。这使得在特定情况下难以选择适当的模式。选择最相关的模型需要能够客观地比较它们。这种比较只能以描述基于共同形式主义但又独立于它们的模型为代价。我们建议使用图重写来正式描述传播机制作为根据策略应用的本地转换规则。当这种方法得到专用于图重写的可视化分析框架的支持时，它是有意义的。本文首先介绍了我们的方法来描述一些传播模型作为一个图重写问题。然后，我们说明了我们的可视化分析框架如何允许交互式地操纵模型，并强调它们的差异的基础上计算的模拟轨迹的措施。
2015-04-10 cs.LO cs.SI
A new criterion for $\mathcal{M}, \mathcal{N}$-adhesivity, with an application to hierarchical graphs
粘着范畴为重写理论的代数方法提供了一个抽象的框架，其中许多一般性的结果可以被改写和统一证明。然而，检查模型是否满足粘附性属性有时远非立即。在本文中，我们提出了一个新的标准给出了一个充分条件$\mathcal{M}, \mathcal{N}$ -adhesivity，原来的概念的adhesivity的推广。我们将其应用到几个现有的类别，特别是层次图，一种形式主义，是出了名的难以适应的模具代数方法重写和各种替代的定义浮动。
2022-06-15 cs.LO math.CT math.LO
Attributed Hierarchical Port Graphs and Applications
我们提出属性层次端口图（AHP）作为端口图的扩展，旨在促进复杂系统的模块化端口图模型的设计。层次分析法由许多相互连接的层组成，其中每一层定义一个端口图，其节点可以链接到层次结构更低的层;属性用于存储用户定义的数据以及可视化和运行时系统参数。我们还概括了战略端口图重写的概念（一种特殊的图形转换系统，端口图重写规则由用户定义的策略控制），以处理AHP后单推出的方法。我们概述了两个领域的应用程序的例子：功能编程和金融建模。
2018-02-19 cs.LO cs.SE cs.SI
On linear rewriting systems for Boolean logic and some applications to proof theory
近年来，线性规则在结构证明理论中发挥了越来越重要的作用。已经观察到，布尔逻辑中所有合理的线性推理规则的集合已经是coNP-完全的，即每个布尔重言式都可以写成（左和右）线性重写规则。本文研究仅由线性推理组成的系统的性质。我们的主要结果是，在这样一个系统中的任何“非平凡”的衍生物的长度是由一个多项式约束。因此，除非coNP=NP，否则不存在多项式时间可判定的可靠和完整的线性推理系统。我们从术语重写，布尔函数理论和图论中提取工具和概念，以获得一些所需的中间结果。与此同时，我们在这些领域之间建立了几个联系，据我们所知，这些联系尚未提出，并构成了一个丰富的理论框架，用于推理布尔逻辑的线性TRS。
2016-12-27 cs.LO
Undecidability of Confluence for Binary Length-Reducing Cycle Rewriting
该研究证明固定字母表{0,1}上二元长度归约循环重写系统的合流性不可判定，通过编译确定性验证器为加权循环系统再转成二元长度归约系统完成证明，区分了循环与字符串重写。
2026-08-20 cs.FL cs.LO
Combinatorial Conversion and Moment Bisimulation for Stochastic Rewriting Systems
本文提出组合转换与矩互模拟方法，用于分析随机重写系统动力学，并展示图形重写系统与离散重写系统间的矩互模拟关系，为应用化学反应系统分析技术铺路。
2020-07-09 cs.DM cs.LO math-ph
Deduction as Reduction
演绎系统和图重写系统进行了比较，在一个共同的范畴框架。这导致了一种改进的演绎方法在图解逻辑。
2010-11-05 cs.LO math.CT
Rewriting and Completeness of Sum-Over-Paths in Dyadic Fragments of Quantum Computing
本文为量子计算中的路径求和形式化方法提出一组新的重写规则，证明其对 Toffoli-Hadamard 片段完备且终止但不合流，并将其推广到用于量子傅里叶变换的二进片段，同时支持任意项的求和与拼接。
2024-03-06 cs.LO quant-ph
