A Dependency Pair Framework for Relative Termination of Term Rewriting
本文提出了一种新型的标注依赖对（ADPs）框架，用于证明项重写系统的相对终止，并在工具AProVE中实现，对比现有工具展现了其有效性。
2024-04-23 cs.LO
A type-based termination criterion for dependently-typed higher-order rewrite systems
一些作者设计了基于类型的终止标准ML类语言允许非结构递归调用。我们将这些工作扩展到一般的重写和依赖类型，从而为构造演算中的重写和β-还原的组合提供了一个强大的终止标准。
2006-10-11 cs.LO cs.PL
Probabilistic Termination by Monadic Affine Sized Typing (Long Version)
我们引入了一个系统的一元仿射大小的类型，这基本上概括了通常的大小类型，并允许这种方式来捕捉概率高阶程序几乎肯定终止。超越普通的、强规范化而不失去可靠性是一项艰巨的任务，如果没有更丰富的、定量的类型概念，而且没有施加一些亲和性约束，这是无法完成的。建议的类型系统是强大的，足以类型的经典例子的概率终止程序，如随机游走。类型化程序被证明几乎必然终止的方法是基于归约的，但需要对该技术进行实质性的修改。
2017-01-15 cs.LO cs.PL
From Innermost to Full Almost-Sure Termination of Probabilistic Term Rewriting
本文将项重写系统中由最内终止推导完全终止的语法准则适配至概率环境，证明分析最内重写的几乎必然终止（AST）即可证明概率项重写系统的完全AST，并在工具AProVE中实现与评估了该贡献。
2024-02-12 cs.LO
The Annotated Dependency Pair Framework for Almost-Sure Termination of Probabilistic Term Rewriting
本文将依赖对技术扩展到概率项重写系统，提出带标注依赖对框架以自动证明完全与最内层重写下的几乎必然终止性，并在 AProVE 中实现验证。
2025-06-05 cs.LO
Dependency Pairs for Expected Innermost Runtime Complexity and Strong Almost-Sure Termination of Probabilistic Term Rewriting
本文提出首个用于概率项重写系统最内层重写的依赖对框架，以分析期望复杂度并证明强几乎必然终止，并在AProVE中实现，展示了其优势。
2025-10-15 cs.LO
Linear Termination over N is Undecidable
本文证明了项重写系统在自然数上的线性多项式解释终止问题不可判定，且新证明比先前更简单，同时扩展至有理数和实数。
2023-07-27 cs.LO
Termination of Cycle Rewriting by Transformation and Matrix Interpretation
我们提出的技术，以证明终止循环重写，即字符串重写的周期，这是字符串的开始和结束连接。我们的主要技术是将循环重写转换为字符串重写，然后应用最先进的技术来证明字符串重写系统的终止性。我们提出了三个这样的转换，并证明他们都是健全的和完整的。这样，不仅变换系统的串重写的终止意味着原始循环重写系统的终止，对于非终止也可以得出类似的结论。除了这种转换的方法，我们提出了一个统一的框架矩阵的解释，涵盖了大多数早期的方法来自动证明终止循环重写。我们所有的技术都用于证明终止和相对终止。我们提出了几个实验显示我们的技术的力量。
2017-03-16 cs.LO
From Innermost to Full Probabilistic Term Rewriting: Almost-Sure Termination, Complexity, and Modularity
本文提出在概率术语重写系统中，通过分析最内重写下的几乎确定终止来证明完整终止，并探讨其复杂性与模块性。
2025-12-11 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
Annotated Dependency Pairs for Full Almost-Sure Termination of Probabilistic Term Rewriting
本文改进带注释的依赖对框架，将概率项重写的几乎必然终止分析从最内层策略扩展到完全重写，并细化基本项场景，在AProVE中实现验证。
2025-01-22 cs.LO
Size-based termination of higher-order rewriting
我们提供了一个通用的和模块化的标准终止简单类型的$λ$ -演算扩展的功能符号定义的用户定义的重写规则。根据Hughes、Pareto和Sabry对使用定点运算符和模式匹配定义的函数的研究，有几个标准使用类型规则来限制函数调用中参数的高度。在本文中，我们将这种方法扩展到基于重写的函数定义和更一般的用户定义的大小概念。
2018-02-20 cs.LO
On the relation between size-based termination and semantic labelling
我们调查两个独立开发的终止技术之间的关系。一方面，基于大小类型的终止（sized-typesbasedtermination，SBT）使用带有大小表达式和Girard的reductioncandidates注释的类型，并且仅适用于使用构造函数匹配的系统。另一方面，语义标记通过用其参数的语义注释每个函数符号来转换重写系统，并且适用于任何重写系统。首先，我们介绍了一个简化版本的SBT的简单类型的Alzuda演算。然后，我们给出了新的证明的正确性SBT使用语义标签，在第一和高阶的情况下。因此，我们表明，SBT可以扩展到使用定义的符号（例如，关联函数）匹配的系统。
2009-06-23 cs.LO
Disproving (Positive) Almost-Sure Termination of Probabilistic Term Rewriting via Random Walks
RWTH Aachen University（亚琛工业大学）
本文提出首个自动反驳概率项重写系统（正）几乎必然终止性的技术，通过将随机游走嵌入计算来定量分析循环的存在性和计数。
2026-05-28 cs.LO
Quantum Term Rewrite Systems: Applications to Complexity Analysis
Université de Lorraine, CNRS, Inria, LORIA（洛林大学、法国国家科学研究中心、法国国家信息与自动化研究所、洛林信息学与自动化学研究所）
研究将项重写系统扩展为量子项重写系统，通过适配技术获终止性证书及归约长度界限，划定一类可终止的QTRS，其可编译成特定量子电路族，且对量子电路通用，还给出量子多项式时间可计算函数类的特征。
2026-07-23 cs.LO
Dependency Tuples for Almost-Sure Innermost Termination of Probabilistic Term Rewriting (Short WST Version)
本研究将依赖对框架适配至概率场景，提出用于证明概率项重写系统几乎必然最内层终止的依赖元组方法，并在工具AProVE中实现以验证其效力。
2023-07-19 cs.LO
On Singleton Self-Loop Removal for Termination of LCTRSs with Bit-Vector Arithmetic
本文针对带位向量算术的逻辑约束项重写系统，提出一种基于有向无环图的依赖对处理器，以解决单例自环依赖对问题，并给出无环图存在的充分条件及特定情况下的简化。
2023-07-26 cs.LO
Proving Almost-Sure Innermost Termination of Probabilistic Term Rewriting Using Dependency Pairs
本文将经典依赖对框架扩展至概率项重写系统，用于证明几乎必然最内层终止性，并在 AProVE 工具中实现以验证其能力。
2023-06-03 cs.LO
Termination Proofs in the Dependency Pair Framework May Induce Multiple Recursive Derivational Complexity
我们研究了重写系统的衍生复杂性，其终止是可证明的依赖对框架中使用的处理器减少对，依赖图，或子项标准。我们证明了这样的系统的衍生复杂性是有界的多重递归函数，提供的衍生复杂性所采用的基本技术是最多的多重递归。此外，我们证明了这个上界是紧的。
2011-03-25 cs.LO
Type safety of rewrite rules in dependent types
依赖类型论的表达能力可以通过对一些附加的计算规则取模来识别类型来扩展。但是，为了保持类型检查的可判定性或系统的逻辑一致性，必须确保这些用户定义的重写规则保持类型。本文给出了一种利用Knuth-Beneficiary完备化检验该性质的新方法。
2020-10-30 cs.LO cs.PL
Higher-order dependency pairs
Arts和Giesl证明了一阶重写系统的终止可以归结为对它的“依赖对”的研究。我们扩展这些结果重写系统简单类型的可计算性技术，通过使用泰特的可计算性。
2018-04-24 cs.LO
Non-Termination of Logic Programs Using Patterns
univ-reunion（留尼汪大学）
本文提出了一种基于模式的逻辑程序非终止性检测方法，通过新展开技术生成无限集合的有限重写序列，并通过实验验证其有效性。
2026-08-10 cs.LO
Static Dependency Pair Method based on Strong Computability for Higher-Order Rewrite Systems
高阶重写系统（HRS）和简单类型项重写系统（STRS）是函数式程序的计算模型。我们最近提出了一个非常强大的方法，静态依赖对方法，这是基于强可计算性的概念，以证明终止STRS。在本文中，我们将该方法扩展到HRSs。由于HRSs包含λ-抽象而STRSs不包含λ-抽象，我们重新构造了静态依赖对方法以允许λ-抽象，并表明静态依赖对方法在没有新限制的情况下也能很好地工作在HRSs上。
2011-09-26 cs.LO
Polymorphic Higher-order Termination
我们概括的终止方法的高阶多项式的解释与impredicative多态性的设置。而不是使用弱单调泛函，我们解释的条款在一个适当的扩展系统F-Ω。这使得重写规则的直接解释成为可能，而重写规则基本上使用了非谓词多态性。此外，我们的概括简化了非多态设置的方法的适用性，允许编码的归纳数据类型。作为我们的方法的潜力的一个例子，我们证明了一个完整的直觉二阶命题逻辑置换转换的实质性片段的终止。
2019-04-22 cs.LO
Proving Termination of Unfolding Graph Rewriting for General Safe Recursion
本文给出了一种新的展开图重写的终止性证明和复杂性分析，展开图重写是一种特殊的无限图重写，它表达了安全递归的一般形式。我们引入了一个终止顺序的条款序列连同长期图的解释成序列的条款。展开图重写规则表示一般的安全递归可以成功地嵌入到终止顺序的解释，产生多项式的运行时复杂度。此外，推广的展开图重写规则的定义一般安全递归，我们提出了一个新的标准的多项式运行时复杂性的无限GRS和多项式大小的范式在无限GRS。
2014-06-20 cs.CC cs.LO math.LO
Hydra Battles and AC Termination
本文提出用带AC符号的重写系统编码赫拉克勒斯与九头蛇之战，可忠实建模任意策略，并通过类型引入、多类型语义标签和新的AC-MPO归约序证明其终止性。
2025-06-25 cs.LO
Termination in Concurrency, Revisited
本文从终止性视角比较了 $π$-演算进程的两种类型系统（基于权重的方法与线性逻辑的 Curry-Howard 对应），揭示了它们之间的精确联系及其支持的客户端/服务器交互类别。
2023-08-02 cs.LO
New results on rewrite-based satisfiability procedures
程序分析和验证需要决策过程根据数据结构的理论进行推理。理论T中的许多问题都可以归结为基文字集的可满足性问题。如果一个可靠的完备的一阶逻辑推理系统保证在T-可满足性问题上终止，那么使用该系统和公平搜索计划的任何定理证明策略都是T-可满足性过程。我们证明了基于重写的一阶引擎的终止记录，整数偏移量，整数偏移模和列表的理论。我们给出了一个模块性定理，说明终止理论的组合的充分条件，每个终止。上述理论以及其他理论都满足这些条件。我们介绍了这些理论及其组合的几套基准测试，包括参数合成基准测试的可扩展性，和现实世界的问题，以测试性能的巨大的文字集。我们比较重写的定理证明器E与有效性检查器CVC和CVC Lite。与通用证明器无法与具有内置理论的推理机竞争的民间传说相反，实验总体上有利于定理证明器，表明重写方法不仅优雅且概念简单，而且具有重要的实际意义。
2008-06-01 cs.AI cs.LO
Termination of Rewriting with Right-Flat Rules Modulo Permutative Theories
我们提出了可判定性的结果终止类的长期重写系统模置换理论。终端和最里面的终止模置换理论被证明是可判定的长期重写系统（TRS），其右手边的条款被限制为浅（变量发生在深度最多一个）和线性（每个变量发生在最多一次）。最内层终止模置换理论也被证明是可判定的浅TRS。我们首先表明，一个浅TRS可以转化为一个平面（只有变量和常数发生在深度1）TRS，同时保持终止和最内层终止。然后证明了可判定性的结果表明：（a）右平坦右线性（平坦）TRS，非终止（分别，最内非终止）意味着从平坦项开始的非终止，和（b）右平坦TRS，从给定项开始的非终止导子的存在是可判定的。在消极的一面，我们显示PSPACE-硬的终止和最内终止浅右线性TRS，和undecidability终止平坦的TRS。
2010-08-25 cs.LO
Loops under Strategies ... Continued
虽然有许多方法可以自动证明术语重写系统的终止性，但到目前为止，只有少数技术可以自动证明其终止性。几乎所有这些技术都试图找到循环，其中循环的存在意味着重写系统的非终止性。然而，大多数程序设计语言使用特定的求值策略，而循环检测技术通常不考虑策略。因此，即使重写系统有一个循环，它仍然可能在某些策略下终止。因此，我们的目标是开发决策程序，可以确定是否一个给定的循环也是一个循环下各自的评估策略。在早期的工作中，这样的程序是为最内层，最外层和上下文敏感的评估策略。在目前的论文中，我们建立在这项工作的基础上，并制定这样的决策程序的重要战略，如最左最内，最左最外，（最大）平行最内，（最大）平行最外，和禁止模式（概括最内，最外，和上下文敏感的战略）。通过这种方式，我们获得了自动反驳这些策略下终止的第一种方法。
2010-12-27 cs.CC cs.LO
A Complete Dependency Pair Framework for Almost-Sure Innermost Termination of Probabilistic Term Rewriting
本文针对概率项重写系统的 iAST 问题，重新定义依赖对并引入新转换，将不完备的依赖元组方法发展为完备的概率 DP 框架，且在 AProVE 中验证其证明能力显著提升。
2024-02-29 cs.LO
Refinement Types as Higher Order Dependency Pairs
细化类型是一种对函数式程序进行深入分析的方法。依赖对方法是证明重写系统可终止性的一种非常有效的方法，然而将其推广到高阶重写系统仍然是一个活跃的研究对象。我们观察到，细化类型的变体允许我们表达一种形式的高阶依赖对标准，只使用信息的类型级别，我们证明了这个标准的正确性。
2011-01-24 cs.LO
A static higher-order dependency pair framework
我们重新审视了证明高阶项重写终止性的静态依赖对方法，并在许多方面对其进行了扩展：（1）我们引入了一种新的重写形式主义，设计用于高阶重写的终止性证明，具有元变量的代数泛函系统。(2)我们提供了一个语法检查的合理性标准，使该方法适用于一个大类的重写系统。(3)我们提出了一个模块化的依赖对框架，这种高阶设置。(4)我们引入了一个细粒度的概念，形成和可计算的链，使框架更强大。(5)我们制定了几个现有的和新的终止证明技术在我们的框架内的处理器的形式。该框架已在（全自动）高阶终止工具WANDA中实现。
2019-04-04 cs.LO cs.PL
Transforming Outermost into Context-Sensitive Rewriting
我们定义了两个转换从长期重写系统（TRS）上下文敏感的TRS在这样一种方式，即终止的目标系统意味着最外层终止的原始系统。在基于“上下文扩展”的转换中，每个最外面的重写步骤都由转换后的系统中的一个步骤来建模。这个转换原来是完整的左线性TRS类。第二个转换被称为“动态标记”，并导致更小尺寸的上下文敏感的TRS。在这里，每个建模步骤都与少量辅助步骤相邻。因此，国家的最先进的上下文敏感的重写终止方法成为可用于证明终止最外层重写。这两种转换都已在Jambox中实现，使其成为最后一版年度终止竞争的最外层重写类别中最成功的工具。
2010-06-29 cs.LO
Automated verification of termination certificates
为了增加用户的信心，许多自动定理证明器提供可以独立验证的证书。在本文中，我们报告了我们的进展，在开发一个独立的工具，用于检查证书的正确性终止长期重写系统，并正式证明其正确性的证明助手Coq。为此，我们使用Coq的提取机制和库上的重写理论和终止称为CoLoR。
2012-12-11 cs.LO cs.MS cs.SE
Rewriting modulo in Deduction modulo
我们研究的终止重写模一组方程的代数构造演算，扩展的构造演算的功能和谓词定义的高阶重写规则。在以前的工作中，我们定义了一般的语法条件的基础上的概念，可计算的闭包，以确保终止的组合重写和β-减少。在这里，我们表明，这一结果是保留时，考虑重写模一组方程，如果这些方程产生的等价类是有限的，方程是线性的，并满足一般的语法条件，也基于可计算闭包的概念。这包括方程，如结合性和交换性，并提供了一个原始的处理终止模方程。
2006-10-11 cs.LO
Extending Context-Sensitivity in Term Rewriting
我们提出了一个广义版本的上下文敏感性的术语重写的基础上的“禁止模式”的概念。基本想法是，如果要收缩的Redex具有特定形状并出现在特定上下文中，则应禁止重写步骤。这种形状和背景是通过禁止模式来表达的。特别是，我们分析了这种新的方法和常用的上下文敏感性的概念，在长期重写之间的关系，以及从计算的角度来看，重写与禁止模式的可行性。后一种可行性的特点是要求限制重写关系产生改进的终止行为，同时仍然足够强大，以计算有意义的结果。在某些类的重写系统与禁止模式的两种性质的充分准则。
2010-01-25 cs.LO
SAT Solving for Argument Filterings
本文介绍了一种与依赖对有关的字典式路径序的命题编码。这有利于SAT求解器的终止性分析的术语重写系统的依赖对方法的基础上的应用。我们解决两个主要的相互关联的问题，并将它们编码为命题公式的可满足性问题，可以有效地处理SAT解决：（1）字典路径顺序与\emph{argument filtering}一起定向一组不等式的组合搜索;（2）参数过滤的选择如何影响必须定向的一组不等式。我们已经在终止证明程序AProVE中实现了我们的贡献。大量的实验表明，通过我们的编码和SAT求解器的应用程序，获得了数量级的加速，以及增加终止证明功率。
2006-05-17 cs.LO
Type-Based Termination for Futures
本文将顺序语言中的大小类型终止性检查方法适配到并发场景，通过扩展半公理化相继式演算提出大小类型细化方案，借助无限宽有限深的类型推导树和新颖逻辑关系论证，实现基于futures的函数式并发程序的终止性验证。
2024-04-15 cs.LO cs.PL
Satisfying KBO Constraints
本文提出了两种新的方法来有效地证明具有Knuth-Beneficiary阶的重写系统的终止性。权函数和优先级的约束编码在（伪）命题逻辑和由此产生的公式进行测试的可满足性。任何令人满意的分配表示权重函数和优先级，使得所诱导的Knuth-Benidorm顺序将编码重写系统的规则从左到右定向。
2007-04-03 cs.LO cs.SC
Solving Partial Order Constraints for LPO Termination
本文介绍了一种新的命题编码的推理偏序。未指定偏序中的符号被视为取整数值的变量，并被解释为该顺序中的索引。对于n个符号上的偏序语句，每个索引用log2n个命题变量表示，符号之间的偏序约束以位表示为模型。我们说明了我们的方法来确定长期重写系统的LPO终止的应用。实验结果是明确的，指示数量级的加速比与当前实现的LPO终止。所提出的编码是通用的和相关的其他应用程序，涉及命题推理偏序。
2005-12-16 cs.LO cs.PL cs.SC
Modular Complexity Analysis for Term Rewriting
所有目前的调查，以分析衍生复杂性的长期重写系统是基于一个单一的终止方法，可能之前的转换。然而，由于直接标准的权力有限，专门使用直接标准是有问题的。为了克服这一限制，本文介绍了一个模块化的框架，它允许推断（多项式）上界的复杂性，长期重写系统结合不同的标准。由于其基本思想是基于相对重写，我们研究如何矩阵的解释和匹配边界可以使用和扩展相对重写的复杂性，分别。模块化框架被证明比传统的设置更强大。此外，结果已经实施，实验表明，显着的增益功率。
2014-03-29 cs.LO
Tools in Term Rewriting for Education
项重写是图灵完备的计算模型。当教授给计算机科学的学生时，传达了计算的关键属性以及在抽象层面上分析程序的技术。本文给出了一个快速的术语重写的介绍，并提出了几个自动工具来分析由因斯布鲁克大学的计算逻辑组开发的术语重写系统。这些工具包括终止工具TTT2、汇流证明器CSI、完成工具mkbTT和KBCV、复杂性工具TcT、策略工具AutoStrat以及FORT，FORT是重写系统的可判定类的一阶理论的判定过程的实现。除了在研究中的应用，这个软件库也被证明是非常宝贵的教学，例如，在多个版本的国际暑期学校重写。
2020-02-28 cs.LO
String Diagram Rewrite Theory I: Rewriting with Frobenius Structure
弦图是一种强大而直观的图形语法，起源于对对称monoidal范畴的研究。在过去的几年中，它们已经在各种计算结构的建模中得到应用，在计算机科学、物理学、控制理论、语言学和生物学等领域。在许多这样的提议中，所描述的系统的转换被建模为图的重写规则。这些发展需要弦图重写的数学基础：尽管术语的重写理论是很好理解的，但弦图的二维性质带来了额外的挑战。这项工作系统化和扩展了一系列最近的会议论文奠定了这样的基础。作为第一步，我们专注于重写系统的情况下，具有Frobenius代数的弦图解理论。这种情况普遍存在于各种方法中：例如，在线性动力系统的代数语义中，弗罗贝纽斯结构模拟电路的布线;在分类量子力学中，它们模拟相互作用的量子可观测量。我们的工作介绍了一个组合的解释弦图重写模Frobenius结构，在双推出超图重写。此外，我们证明了这种解释是健全的和完整的。在最后一部分中，我们还看到，该方法可以推广到模型重写模多个Frobenius结构。作为概念的证明，我们展示了如何从这些结果中得出一个终止策略的相互作用双代数，一个重要的重写理论在量子电路和信号流图的研究。
2022-02-03 cs.LO math.CT
Towards an HRS Category in TermCOMP
University of Innsbruck（因斯布鲁克大学）
本文定义了一个语法子类，使得HRS重写与TermCOMP高阶类别中的beta优先策略重写等价，为TermCOMP中建立HRS子类别奠定基础。
2026-06-25 cs.LO
Automated Termination Proofs for Logic Programs by Term Rewriting
RWTH Aachen（亚琛工业大学）；TU Eindhoven（埃因霍温理工大学）；University of Innsbruck（因斯布鲁克大学）
逻辑程序的可终止性分析有两种方法：“转换”法和“直接”法。直接方法直接在逻辑程序的基础上证明终止。转换方法将一个逻辑程序转换成一个项重写系统（TRS），然后分析所得到的TRS的终止。因此，转换方法使以前为TRS开发的所有方法也可用于逻辑程序。然而，大多数现有的转换的适用性是相当有限的，因为它们只能用于逻辑程序的某些子类。(Most它们中的一个仅限于模式良好的程序。）在本文中，我们改进这些转换，使它们成为适用于任何明确的逻辑程序。为了用TRS模拟逻辑程序的行为，我们稍微修改了重写的概念，允许无限项。我们表明，我们的转换结果TRS这确实是适合自动终止分析。与大多数其他逻辑程序的终止方法相比，我们的技术也适用于逻辑程序设计，而不需要发生检查，这是在实践中通常使用的。我们在终止证明程序AProVE中实现了我们的方法，并在大量示例中成功地对其进行了评估。
2008-09-01 cs.AI cs.LO cs.PL
Consistency and Completeness of Rewriting in the Calculus of Constructions
向基于Curry-Howard同构的证明助手（例如Coq）添加重写可以极大地提高工具的可用性。不幸的是，添加任意一组重写规则可能会使底层的形式系统变得不可判定和不一致。虽然确保类型检查的终止性和汇合性以及可判定性的方法已经在一定程度上得到了研究，但逻辑一致性迄今为止很少受到关注。在本文中，我们表明，一致性是正规性的后果，这反过来又遵循重写规则定义的所有功能是完整的假设。我们提供了一个声音和终止，但不一定完整的算法来验证这个属性。该算法接受所有的定义，遵循相关的模式匹配计划Coquand和研究的McBride在他的博士论文。它还通过重写接受许多定义，包含偏离标准模式匹配的规则。
2008-09-15 cs.LO cs.SC
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
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
Automating the Diagram Method to Prove Correctness of Program Transformations
我们报告的自动化技术，以证明程序转换的正确性，在高阶程序演算，这可能允许递归让绑定，因为它们发生在功能程序设计语言。如果程序转换保持了程序的观察语义，那么它就是正确的。在我们的LRSX工具中，所谓的图方法是通过结合高阶元语言上的α重命名的统一、匹配和推理来自动化的，并且通过编码来自动化归纳证明到术语重写系统的终止问题中。我们解释的技术，我们说明了使用的工具，我们报告的实验。
2019-02-22 cs.LO cs.PL
Theory of higher order interpretations and application to Basic Feasible Functions
本文提出高阶解释理论，通过完备格上的最小不动点表达程序解释，并用高阶多项式限制解释，在任意阶上刻画了基本可行函数。
2020-12-11 cs.CC cs.LO cs.PL
Decidability of Type-checking in the Calculus of Algebraic Constructions with Size Annotations
自从Val Tannen的先驱工作简单类型的类演算和一阶重写的组合（LICS'88），许多作者都通过将其扩展到更丰富的类型类演算和重写范式，最终在演算像代数结构的演算。这些工作提供了理论基础的类型理论的证明助手的功能和谓词定义的定向高阶方程。这种定义包含了基于归纳的定义，更容易编写，并提供了更多的自动化。另一方面，检查用户定义的重写规则是强规范化和融合的，并且在与beta约简结合时保持类型检查的可判定性，则更加困难。大多数终止标准依赖于期限结构。在以前的工作中，我们扩展到依赖类型和高阶重写，“大小类型”的概念由几位作者在ML类语言的简单框架中研究，并证明了它保持了强规范化。本文件的主要贡献是双重的。首先，证明了在带尺寸标注的代数构造演算中，只要尺寸标注所产生的约束集是可满足的，并且允许最一般的解，则类型推断和类型检验问题是可判定的.其次，我们证明了一个大小代数足够丰富的捕获通常的归纳为基础的定义和更多的后来的属性。
2006-09-11 cs.LO cs.PL
Theorem Proving and Algebra
这本书可以被看作是一个文本的定理证明，使用技术，从一般代数，否则作为一个文本的一般代数说明和具体的实际练习，在定理证明。这本书考虑了几个不同的逻辑系统，包括一阶逻辑，霍恩子句逻辑，等式逻辑和一阶逻辑与平等。同样，几种不同的证明范式被认为是。然而，我们确实强调等式逻辑，为了简单起见，我们只使用OBJ 3软件系统，尽管它以一种相当灵活的方式使用。我们不追求机械化证明的崇高目标，就像数学家们引以为傲的那样;相反，我们寻求采取措施为计算机科学家开发软件和硬件提供有用的证明。这一较为适度的目标具有既可实现又有实际好处的优点。内容包括：多类签名、代数和同态;项代数和代换;方程和满足;条件方程;方程推导及其完备性;条件方程的推导;常数定理;理论的解释和等价;项重写、终止、汇合和范式;抽象重写系统;标准模型、抽象数据类型、初始化和归纳;重写和演绎模方程;一阶逻辑、模型和证明规划;二阶代数;排序代数和重写;模块;统一和完成;以及隐藏代数。与此同时，还将逐步介绍OBJ 3、群论应用、各种抽象数据类型（如数制、列表和堆栈）、命题演算、硬件验证、λ演算、函数程序的正确性以及其他主题。
2021-01-16 cs.LO cs.PL cs.SC
