Sequences of Rewrites: A Categorical Interpretation
在马丁-洛夫的内涵类型论中，同一性类型是一个被大量使用和研究的概念。原因是，它是最近发现的，类型论和同伦论之间的联系。身份类型最初的主要问题是，它们很难理解和使用。利用这一事实作为动机，Queiroz & Gabbay（1994）提出了一个更简单的身份类型公式，并由de Queiroz & de Oliveira（2013）进一步发展。在这个公式中，标识类型的元素被视为重写序列（或计算路径）。与该新实体的逻辑规则一起，存在称为LND_{EQS} -RWS的重写序列之间的归约规则系统。该系统使用标记的自然演绎（即Prawitz的自然演绎加上派生项）构建，并负责确定如何重写重写序列，从而产生新的重写序列。在这种情况下，我们提出了一个范畴的解释，这个新的实体，使用的对象和重写的规则作为态射的类型。此外，我们表明，我们的解释是根据一些已知的结果，如类型有一个群胚结构。我们也解释更复杂的结构，比如由一系列重写的重写所形成的结构。
2015-02-15 cs.LO math.CT
Completeness of Sum-Over-Paths for Toffoli-Hadamard and the Dyadic Fragments of Quantum Computation
路径求和（Sum-Over-Paths）形式主义是一种符号化地操纵描述量子系统的线性映射的方法，并且是用于此类系统的形式验证的工具。本文给出了一组新的重写规则，并证明了它对量子力学中最简单的近似普适片断“Toffoli-Hadamard”是完备的.我们表明，重写是终止的，但不汇合（这是预期的普遍性的片段）。我们使用路径求和和图形语言ZH-Calculus之间的联系来做到这一点，并展示了公理化如何转化为后者。最后，我们展示了如何丰富的重写系统，以达到完整的二进片段的量子计算-通过添加相位门与二进倍数的$π$的托夫里-阿达玛门集-特别是在量子傅立叶变换。
2022-11-07 cs.LO quant-ph
Extending Context-Sensitivity in Term Rewriting
我们提出了一个广义版本的上下文敏感性的术语重写的基础上的“禁止模式”的概念。基本想法是，如果要收缩的Redex具有特定形状并出现在特定上下文中，则应禁止重写步骤。这种形状和背景是通过禁止模式来表达的。特别是，我们分析了这种新的方法和常用的上下文敏感性的概念，在长期重写之间的关系，以及从计算的角度来看，重写与禁止模式的可行性。后一种可行性的特点是要求限制重写关系产生改进的终止行为，同时仍然足够强大，以计算有意义的结果。在某些类的重写系统与禁止模式的两种性质的充分准则。
2010-01-25 cs.LO
Rewriting and Completeness of Sum-Over-Paths in Dyadic Fragments of Quantum Computing
本文为量子计算中的路径求和形式化方法提出一组新的重写规则，证明其对 Toffoli-Hadamard 片段完备且终止但不合流，并将其推广到用于量子傅里叶变换的二进片段，同时支持任意项的求和与拼接。
2024-03-06 cs.LO quant-ph
Computational Paths -- An approach in the $LND_{EQ}-TRS_{2}$ system
本文提出基于计算路径概念的标号演绎系统LND$_{ED-}$TRS，将其作为同类型项间的相等关系应用于同伦理论，并证明计算路径可用于完成$LND_{EQ}-TRS_{2}$重写系统的证明。
2023-11-17 cs.LO
Formalizing Computational Paths and Fundamental Groups in Lean
本文在Lean 4中形式化了计算路径理论，并通过六个代数拓扑例子展示了其在同伦计算中的应用。
2025-11-25 cs.FL cs.LO
On the Groupoid Model of Computational Paths
本文的主要目的是研究计算路径的数学性质。最初由de Queiroz \& Gabbay（1994）提出的“序列或重写”，计算路径被认为是Martin Löf的内涵类型论的单位类型的项，因为这些路径可以被看作是两个计算对象之间的命题相等的根据。从这个角度来看，这项工作的目的是表明，一个属性的身份类型是目前的计算路径。我们指的是这样一个事实，即单位类型诱导了一个广群结构，如Hofmann \& Streicher（1994）所提出的。使用范畴语义，我们表明，计算路径诱导广群结构。我们还表明，计算路径能够诱导更高的范畴结构。
2016-09-08 cs.LO
Topological Semantics for Scoped Computational Paths
Microsoft, USA（微软）；Centro de Informática, Universidade Federal de Pernambuco, Brazil（伯南布哥联邦大学信息学院）；Departamento de Matemática, Universidade Federal Rural de Pernambuco, Brazil（伯南布哥联邦农村大学数学系）
本文为带作用域的重写表示给出拓扑语义，构造带典范上域群胚结构的商箭头空间，证明拓扑一致性准则与充分条件，给出同伦类实现映射性质，以圆、环面为例分类，Lean开发包验证定理。
2026-09-15 cs.LO math.AT
On Computational Paths and the Fundamental Groupoid of a Type
本文的主要目的是研究计算路径的数学性质。计算路径最初是由de Queiroz \& Gabbay（1994）提出的“重写序列”，它可以被看作是两个计算对象之间的命题相等成立的基础.利用计算路径和范畴语义，我们取类型论中的任何类型$A$，并构造了该类型的广群.我们将此群胚称为类型$A$的基本群胚，因为它与使用单位类型的同伦解释获得的群胚相似。主要的区别在于，计算路径不仅仅是语义解释，而是类型论语法的实体。我们还扩展了我们的结果，使用计算路径来构建更高层次的基本群胚。
2015-09-21 cs.LO
An alternative approach to the calculation of fundamental groups based on labeled natural deduction
在这项工作中，我们使用一个标记的演绎系统的基础上的概念，计算路径（重写序列）之间的等式相同类型的两个条款。我们还定义了一个术语重写系统，用于在这些计算路径之间进行计算，建立等式之间的等式。我们使用一个基于计算路径概念的标号演绎系统（重写序列），以获得一些结果的代数拓扑和支持的Seifet-Van Kampen定理，我们将计算，在某种程度上不复杂的比一个在数学\cite{Munkres}和同伦类型论的技术\cite{hott}，基本群的克莱因布洛特$\mathbb{K}^2$，圆环$\mathbb{T}^2$和双孔圆环$\mathbb{M}_2=\mathbb{T}^2\# \mathbb{T}^2$（两个圆环的连通和）。
2019-06-19 cs.LO math.AT
Predicative Lexicographic Path Orders: An Application of Term Rewriting to the Region of Primitive Recursive Functions
本文提出了一种新的终止顺序{ \em谓词词典路径顺序}（PLPO），它是对词典路径顺序的一种句法限制。以及字典式路径顺序，几个非平凡的原始递归方程，例如，带参数替换的原始递归式、非嵌套多重递归或简单嵌套递归都可以用PLPO定向。然而，可以示出PLPO仅在兼容重写系统的导出长度上诱导原始递归上界。这产生了一个经典事实的替代证明，即原始递归函数类在这些非平凡原始递归方程下是封闭的。
2014-06-02 cs.LO math.LO
Tools in Term Rewriting for Education
项重写是图灵完备的计算模型。当教授给计算机科学的学生时，传达了计算的关键属性以及在抽象层面上分析程序的技术。本文给出了一个快速的术语重写的介绍，并提出了几个自动工具来分析由因斯布鲁克大学的计算逻辑组开发的术语重写系统。这些工具包括终止工具TTT2、汇流证明器CSI、完成工具mkbTT和KBCV、复杂性工具TcT、策略工具AutoStrat以及FORT，FORT是重写系统的可判定类的一阶理论的判定过程的实现。除了在研究中的应用，这个软件库也被证明是非常宝贵的教学，例如，在多个版本的国际暑期学校重写。
2020-02-28 cs.LO
On Singleton Self-Loop Removal for Termination of LCTRSs with Bit-Vector Arithmetic
本文针对带位向量算术的逻辑约束项重写系统，提出一种基于有向无环图的依赖对处理器，以解决单例自环依赖对问题，并给出无环图存在的充分条件及特定情况下的简化。
2023-07-26 cs.LO
Abstract Framework for All-Path Reachability Analysis toward Safety and Liveness Verification (Full Version)
Graduate School of Informatics, Nagoya University（名古屋大学大学院信息学研究科）
本文重构了针对ARs的部分有效性抽象框架，建立了ARs和LCTRSs部分有效性的推理规则一一对应关系，并引入总有效性概念以支持活性验证，证明了证明图的无环性是总有效性的充要条件。
2026-06-29 cs.LO
A Topological Application of Labelled Natural Deduction
我们使用一个标记的演绎系统的基础上的概念，计算路径（重写序列）之间的等式相同类型的两个条款。我们还定义了一个术语重写系统，用于在这些计算路径之间进行计算，建立等式之间的等式。然后，我们继续展示这里的主要结果：使用这个系统来计算圆、环面和实射影平面的基本群。
2021-05-09 cs.LO math.AT
Propositional equality, identity types, and direct computational paths
在证明论中，规范证明的概念是相当基本的，并且通常被认为是理所当然的，一个句子的规范证明必须是唯一的，直到某些次要的句法细节（例如，变量的变化）。当建立一个证明理论的平等之一是面临着一个相当意想不到的情况下，可能没有一个唯一的规范证明的平等声明。事实上，在（1994 - 5）建议的形式化证明命题平等的库里-霍华德风格，我们已经发现了这样一个特点。霍夫曼和施特雷彻（Hofmann & Streicher，1994）完全独立地在一个不同的环境中展示了如何建立马丁-洛夫的类型论的模型，其中恒等式类型的规范证明的唯一性不成立。这里的意图是表明，通过考虑重写和替换的序列，这是一个相当自然的事实，即两个（或更多）不同的证明可能是规范的，并且没有一个比另一个更好。通过将等式的证明看作重写（或计算）路径，这种方法将符合最近提出的类型论和同伦论之间通过单位类型的联系，因为单位类型的元素将具体地是路径（或同伦）。
2013-08-05 cs.LO
A proof theoretic study of abstract termination principles
我们进行了一个证明理论的分析，在一个抽象的设置递归路径顺序的良好基础。我们概述了一个非常普遍的终止原则，并提取其良好的基础证明subrecursive范围的大小推导树，可以定义在哥德尔的系统T加酒吧递归。然后，我们进行了这些条款的复杂性分析，并演示了如何将其应用于约束的衍生复杂性的长期重写系统。
2019-02-22 cs.LO math.LO
On the Calculation of Fundamental Groups in Homotopy Type Theory by Means of Computational Paths
同伦类型论中最有趣的实体之一是单位类型。它产生了一个有趣的解释的平等，因为人们可以语义解释之间的平等两项相同类型的收集同伦路径之间的点相同的空间。由于这只是一种语义解释，最近德奎罗斯、拉莫斯和德奥利维拉提出了在同伦类型论的语法中加入路径。在这些作品中，作者提出了一个被称为“计算路径”的实体，由De Queiroz和Gabbay在1994年提出，并表明它可以用来形式化的身份类型。我们已经发现，有可能使用这些计算路径作为工具，以实现一个中心结果的代数拓扑和同伦类型论：计算基本群的表面。我们回顾了计算路径的概念和$LND_{EQ}-TRS$，这是一个长期重写系统提出的De Oliveira在1994年计算路径之间的映射冗余。然后，我们继续计算基本群的圆，圆柱，M{<$}bius带，环面和真正的射影平面。此外，我们表明，使用的计算路径，使这些计算简单和直接，而同样的结果是很难获得使用传统的编码-编码-解码方法的同伦类型论。
2018-05-17 cs.LO
On the Identity Type as the Type of Computational Paths
我们引入了一种新的方式形式化的内涵的身份类型的基础上，一个实体被称为计算路径可以被解释为身份类型的条款。我们的方法得益于我们的消除规则易于理解和使用。我们明确这一点，构造一些相关类型的条款，使用我们提出的消除规则。我们还表明，身份类型，我们的方法所定义的，诱导广群结构。这个结果与Hofmann \& Streicher（1994）揭示的传统的恒等式诱导群胚的事实是一致的。
2015-04-18 cs.LO
A categorical construction for the computational definition of vector spaces
Lambda-S是一阶λ演算的扩展，它统一了量子计算中的两种不可克隆方法。一种是禁止变量重复，而另一种是考虑所有的代数线性函数的代数项。Lambda-S的类型系统有一个构造函数S，使得类型A被认为是向量空间的基，而S（A）是它的跨度。Lambda-S也可以被看作是一种用于向量空间的计算操作的语言：向量空间公理作为重写系统给出，描述要执行的计算步骤。本文给出了Lambda-S*（Lambda-S的一个片段）的抽象范畴语义，证明了S可以解释为笛卡尔范畴和加法对称monoidal范畴之间的一个连接关系中两个函子的合成.右伴随是一个遗忘函子U，它隐藏在语言中，在计算推理中起着核心作用。
2020-04-11 cs.LO math.CT math.LO
