类型论与重写
Type theory and rewriting
摘要：
我们研究的属性，特别是终止，依赖类型系统的λ演算和重写。
英文摘要：
We study the properties, in particular termination, of dependent types systems for lambda calculus and rewriting.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
继续探索
相关论文
通过变换和矩阵解释终止循环重写
Termination of Cycle Rewriting by Transformation and Matrix Interpretation
我们提出的技术，以证明终止循环重写，即字符串重写的周期，这是字符串的开始和结束连接。我们的主要技术是将循环重写转换为字符串重写，然后应用最先进的技术来证明字符串重写系统的终止性。我们提出了三个这样的转换，并证明他们都是健全的和完整的。这样，不仅变换系统的串重写的终止意味着原始循环重写系统的终止，对于非终止也可以得出类似的结论。除了这种转换的方法，我们提出了一个统一的框架矩阵的解释，涵盖了大多数早期的方法来自动证明终止循环重写。我们所有的技术都用于证明终止和相对终止。我们提出了几个实验显示我们的技术的力量。
cs.LO
项重写与逻辑编程中的二元非终止性
Binary Non-Termination in Term Rewriting and Logic Programming
该研究提出一种新的句法准则，可在包含简化项重写与逻辑编程的抽象场景中实现非终止性的自动检测。
cs.LO
从线性项重写到保持终止性的图重写
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+重写。
cs.LO
使用大小变化原理终止$λ$ $Π$模重写（工作正在进行中）
Termination of $λ$$Π$ modulo rewriting using the size-change principle (work in progress)
大小变化终止原理最初被用来研究一阶函数程序的终止问题。在这项工作中，我们表明，它也可以用来研究终止高阶重写系统中的依赖类型扩展LF。
cs.LO
从概率项重写的最内几乎必然终止到完全几乎必然终止
From Innermost to Full Almost-Sure Termination of Probabilistic Term Rewriting
本文将项重写系统中由最内终止推导完全终止的语法准则适配至概率环境，证明分析最内重写的几乎必然终止（AST）即可证明概率项重写系统的完全AST，并在工具AProVE中实现与评估了该贡献。
cs.LO
依赖类型论模重写中的依赖对终止性
Dependency Pairs Termination in Dependent Type Theory Modulo Rewriting
依赖项对是现代自动终止证明器的核心概念，用于一阶项重写系统。在本文中，我们介绍了一个扩展的依赖型高阶重写系统的一大类这种技术。这扩展了以前的结果Wahlstedt一方面和第一作者另一方面强规范化和非正交重写系统。这个新的标准在类型检查器Dedukti中实现。
cs.LO
更多相关论文收起更多论文
基于重叠闭包的稀疏分片终止字符串重写
Sparse Tiling through Overlap Closures for Termination of String Rewriting
我们在字符串重写中过度近似可达集，这是由可接受因子（称为瓦片）定义的语言。一个稀疏的瓦片集只包含那些在派生中可到达的瓦片，并且通过完成自动机来构造。利用语义标记的稀疏分片定义的部分代数，我们得到了一个证明局部终止性的变换方法。利用前向闭包的已知结果和重叠闭包的新特征，我们分别获得了证明终止性和相对终止性的方法。我们报告显示这些方法的强度的实验。
cs.LO
基于规模的高阶重写终止
Size-based termination of higher-order rewriting
我们提供了一个通用的和模块化的标准终止简单类型的$λ$ -演算扩展的功能符号定义的用户定义的重写规则。根据Hughes、Pareto和Sabry对使用定点运算符和模式匹配定义的函数的研究，有几个标准使用类型规则来限制函数调用中参数的高度。在本文中，我们将这种方法扩展到基于重写的函数定义和更一般的用户定义的大小概念。
cs.LO
重写策略的终止：一种通用方法
Termination of rewriting strategies: a generic approach
我们提出了一个通用的终止证明方法重写下的策略，基于一个明确的归纳终止属性。重写树的基础条款的证明树，交替应用缩小和抽象的步骤产生的模型。归纳原理是通过抽象机制来应用的，在抽象机制中，术语被表示其任何范式的变量所替换。归纳排序不是先验给出的，而是用排序约束定义的，在证明过程中递增设置。抽象约束可以用来控制收缩机制，众所周知，收缩机制很容易发散。然后为最内层、最外层和局部策略实例化泛型方法。
cs.LO
从最内到完整概率术语重写：几乎确定终止、复杂性与模块性
From Innermost to Full Probabilistic Term Rewriting: Almost-Sure Termination, Complexity, and Modularity
RWTH Aachen University（亚琛工业大学）
本文提出在概率术语重写系统中，通过分析最内重写下的几乎确定终止来证明完整终止，并探讨其复杂性与模块性。
cs.LO
概率项重写系统几乎必然终止性的带标注依赖对框架
The Annotated Dependency Pair Framework for Almost-Sure Termination of Probabilistic Term Rewriting
本文将依赖对技术扩展到概率项重写系统，提出带标注依赖对框架以自动证明完全与最内层重写下的几乎必然终止性，并在 AProVE 中实现验证。
cs.LO
项重写与逻辑编程中的非终止性
Non-Termination in Term Rewriting and Logic Programming
本文在统一框架下定义循环与二元链两种非终止形式，提出检测二元链的语法判据，并通过NTI在2023年终止竞赛中与领先分析器比较验证其有效性。
cs.LO
禁止模式重写的终止与自动合成
Termination of Rewriting with and Automated Synthesis of Forbidden Patterns
我们介绍了一个修改后的版本，著名的依赖对框架，是适合于禁止模式限制下的重写终止分析。通过将上下文附加到表示相应递归函数调用的调用上下文的依赖对，可以将禁止模式限制合并到依赖对链的（适应的）概念中，从而产生可靠且完整的终止分析方法。建立在这个上下文依赖对框架，我们引入了一个依赖对处理器，通过分析依赖对的上下文信息，简化了问题。此外，我们展示了如何使用这个处理器来合成禁止模式适合于一个给定的长期重写系统的飞行在终止分析。
cs.LO
用于概率项重写系统几乎必然最内层终止的依赖元组（WST短篇版本）
Dependency Tuples for Almost-Sure Innermost Termination of Probabilistic Term Rewriting (Short WST Version)
本研究将依赖对框架适配至概率场景，提出用于证明概率项重写系统几乎必然最内层终止的依赖元组方法，并在工具AProVE中实现以验证其效力。
cs.LO
使用依赖对证明概率项重写的几乎必然最内层终止性
Proving Almost-Sure Innermost Termination of Probabilistic Term Rewriting Using Dependency Pairs
本文将经典依赖对框架扩展至概率项重写系统，用于证明几乎必然最内层终止性，并在 AProVE 工具中实现以验证其能力。
cs.LO
概率项重写的期望最内层运行时复杂度与强几乎必然终止的依赖对方法
Dependency Pairs for Expected Innermost Runtime Complexity and Strong Almost-Sure Termination of Probabilistic Term Rewriting
本文提出首个用于概率项重写系统最内层重写的依赖对框架，以分析期望复杂度并证明强几乎必然终止，并在AProVE中实现，展示了其优势。
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。
cs.LO
将Outermost转换为上下文相关重写
Transforming Outermost into Context-Sensitive Rewriting
我们定义了两个转换从长期重写系统（TRS）上下文敏感的TRS在这样一种方式，即终止的目标系统意味着最外层终止的原始系统。在基于“上下文扩展”的转换中，每个最外面的重写步骤都由转换后的系统中的一个步骤来建模。这个转换原来是完整的左线性TRS类。第二个转换被称为“动态标记”，并导致更小尺寸的上下文敏感的TRS。在这里，每个建模步骤都与少量辅助步骤相邻。因此，国家的最先进的上下文敏感的重写终止方法成为可用于证明终止最外层重写。这两种转换都已在Jambox中实现，使其成为最后一版年度终止竞争的最外层重写类别中最成功的工具。
cs.LO
通过随机游走反驳概率项重写的（正）几乎必然终止性
Disproving (Positive) Almost-Sure Termination of Probabilistic Term Rewriting via Random Walks
RWTH Aachen University（亚琛工业大学）
本文提出首个自动反驳概率项重写系统（正）几乎必然终止性的技术，通过将随机游走嵌入计算来定量分析循环的存在性和计数。
cs.LO
带注释的依赖对用于概率项重写的完全几乎必然终止
Annotated Dependency Pairs for Full Almost-Sure Termination of Probabilistic Term Rewriting
本文改进带注释的依赖对框架，将概率项重写的几乎必然终止分析从最内层策略扩展到完全重写，并细化基本项场景，在AProVE中实现验证。
cs.LO
概率重写与渐近行为：关于终止性与唯一正规形
Probabilistic Rewriting and Asymptotic Behaviour: on Termination and Unique Normal Forms
本文针对概率重写系统，研究结果唯一性（唯一极限分布），提出证明技术以分析和比较归约策略，为概率演算的操作性分析提供工具。
cs.LO
LCTRS的终止
Termination of LCTRSs
逻辑约束项重写系统（LCTRS）提供了一个通用的框架与约束项重写。我们讨论了一个简单的依赖对的方法来证明终止LCTRS。我们看到，现有的技术以自然的方式转移到受约束的设置。
cs.LO
项重写相对终止的依赖对框架
A Dependency Pair Framework for Relative Termination of Term Rewriting
本文提出了一种新型的标注依赖对（ADPs）框架，用于证明项重写系统的相对终止，并在工具AProVE中实现，对比现有工具展现了其有效性。
cs.LO
用于概率项重写几乎必然最内层终止的完备依赖对框架
A Complete Dependency Pair Framework for Almost-Sure Innermost Termination of Probabilistic Term Rewriting
本文针对概率项重写系统的 iAST 问题，重新定义依赖对并引入新转换，将不完备的依赖元组方法发展为完备的概率 DP 框架，且在 AProVE 中验证其证明能力显著提升。
cs.LO
在模演绎中重写模
Rewriting modulo in Deduction modulo
我们研究的终止重写模一组方程的代数构造演算，扩展的构造演算的功能和谓词定义的高阶重写规则。在以前的工作中，我们定义了一般的语法条件的基础上的概念，可计算的闭包，以确保终止的组合重写和β-减少。在这里，我们表明，这一结果是保留时，考虑重写模一组方程，如果这些方程产生的等价类是有限的，方程是线性的，并满足一般的语法条件，也基于可计算闭包的概念。这包括方程，如结合性和交换性，并提供了一个原始的处理终止模方程。
cs.LO
结合类型和大小约束检查高阶条件重写系统的终止性
Combining typing and size constraints for checking the termination of higher-order conditional rewrite systems
在以前的工作中，第一作者扩展到高阶重写和依赖类型中使用类型中的大小注释，这是一种终止证明技术，称为基于类型或大小的终止，最初为ML类程序开发。在这里，我们通过考虑条件重写和显式量化以及对大小注释的约束更进一步。这允许更精确地描述函数输出的大小如何取决于其输入的大小。因此，我们可以检查更多函数的终止。首先给出了一个基于约束求解的通用类型检测算法。然后，我们给出了Presburger算法中的一个带约束的终止准则。据我们所知，这是高阶条件重写的第一个终止准则，考虑到终止的条件。
cs.LO
三维重写的终止顺序
Termination orders for 3-dimensional rewriting
本文研究了3-测谎仪作为一个框架重写的二维词。将项重写系统转化为具有显式资源管理的3-polygraphs，并研究了每个系统的计算性质。最后，给出了Z/2 Z-向量空间（交换）理论的收敛3-多道图。为了证明这些结果，它是解释如何手工制作一类终止订单的3-多道。
cs.LOmath.CT
左线性项重写系统终止性的多道图
Polygraphs for termination of left-linear term rewriting systems
利用Albert Burroni的多道生理记录图证明了左线性项重写系统（TRS）的终止性。我们将所考虑的TRS转换成一个最小尺寸的测谎仪，其终止性是用测谎仪解释证明的，然后我们回到TRS上的属性。我们回顾伊夫拉丰的一般翻译的TRS到测谎仪和已知的链接之间的终止属性。我们给出了几个条件的原始TRS，包括作为一个一阶函数程序，以确保我们可以减少的多道转换的大小。我们还证明了充分条件的最小的翻译，意味着终止原来的TRS的polygraphic解释。最后给出了与通常的多项式解释方法相比较的例子。
cs.LOmath.CT
用有限自动机证明循环与非循环不可终止性
Proving Looping and Non-Looping Non-Termination by Finite Automata
提出了一种新的证明项重写非终止性的方法。其基本思想是找到一个非空的项的正则语言，它在重写下是封闭的，并且不包含范式。它是自动化的，用一个有固定数量状态的树自动机来表示语言，并用SAT公式来表达上述要求。这个公式的可满足性意味着不终止。我们的方法成功的许多例子，所有早期的技术失败，例如从组合逻辑的S规则。
cs.LO
高阶重写的多项式解释
Polynomial Interpretations for Higher-Order Rewriting
弱单调代数的终止方法，在HRS形式主义中被定义为高阶重写，提供了很大的力量，但近年来很少使用。我们适应和扩展这种方法的替代形式主义的代数功能系统，其中简单类型的代数演算与代数约简相结合。使用这一理论，我们定义高阶多项式的解释，并显示如何实现这种技术的挑战可以解决。终止工具WANDA中提供了完整的实现。
cs.LO
Collatz猜想的自动化方法
An Automated Approach to the Collatz Conjecture
我们探讨Collatz猜想及其变种通过终止字符串重写的镜头。我们构建了一个重写系统，模拟迭代应用Collatz函数对应的混合二元-三元表示的正整数字符串。我们证明了这个重写系统的终止等价于Collatz猜想。我们还证明，以前研究的重写系统，模拟Collatz函数使用一元表示不承认终止证明，通过自然矩阵的解释，即使使用依赖对。为了证明我们的方法在数学上有趣的语句的可行性，我们实现了一个最小的终止证明，使用自然/北极矩阵的解释，我们发现自动化证明的非平凡的削弱Collatz猜想。虽然我们没有成功地证明Collatz猜想，我们相信，这里的想法代表了一个有趣的新方法。
cs.LO
一般安全递归展开图重写终止性的证明
Proving Termination of Unfolding Graph Rewriting for General Safe Recursion
本文给出了一种新的展开图重写的终止性证明和复杂性分析，展开图重写是一种特殊的无限图重写，它表达了安全递归的一般形式。我们引入了一个终止顺序的条款序列连同长期图的解释成序列的条款。展开图重写规则表示一般的安全递归可以成功地嵌入到终止顺序的解释，产生多项式的运行时复杂度。此外，推广的展开图重写规则的定义一般安全递归，我们提出了一个新的标准的多项式运行时复杂性的无限GRS和多项式大小的范式在无限GRS。
cs.CCcs.LOmath.LO
最内终止依赖对准则的形式化
Formalizing the Dependency Pair Criterion for Innermost Termination
重写是一个推理函数式编程的框架。依赖对准则是一种众所周知的分析术语重写系统终止的机制。在重写框架中，具有基于评估的操作语义的功能规范与最内层的归约关系相关。本文给出了最内层约简关系的依赖对准则的PVS形式化：一个项重写系统是最内层可终止的当且仅当它被依赖对准则终止。本文还讨论了该准则在功能规格说明终止性检查中的应用。
cs.LOcs.PL
使用正则语言的非终止性
Non-termination using Regular Languages
我们描述了一种方法来证明非循环不终止，即长期重写系统不承认循环减少。作为非终止证书，我们采用常规（树）自动机。
cs.LO
认证高阶多项式解释
Certifying Higher-Order Polynomial Interpretations
本文提出一种认证高阶项重写系统终止性证明的方法，通过形式化多项式解释方法，并将终止性分析工具Wanda的输出转换为Coq脚本以验证证明的有效性。
cs.LO
非简化图重写终止
Non-simplifying Graph Rewriting Termination
LORIA（洛林信息学及其应用研究实验室）；Université de Lorraine（洛林大学）；Inria Nancy Grand-Est（法国国家信息与自动化研究所南锡大东部中心）
到目前为止，自然语言处理（NLP）中的大量工作依赖于树作为核心数学结构来表示语言信息（例如Chomsky的工作）。然而，有些语言现象并不能很好地处理树。在以前的论文中，我们展示了用图来编码语言结构和使用图重写规则来计算这些结构的好处。出于一些语言学上的考虑，图重写的特征在于两个特征：第一，沿着计算没有节点创建，第二，有非局部边修改。在这些假设下，我们证明了一致终止是不可判定的，非一致终止是可判定的。我们描述了两个终止技术的基础上的重量，我们给这些重写系统的推导长度的复杂性界。
cs.CCcs.CLcs.LO
基于Girard约化概念的$λ$ -项重写关系的终止性
Termination of rewrite relations on $λ$-terms based on Girard's notion of reducibility
本文将Girard为证明多态$λ$ -演算中的$β$ -约简的终止性而引入的约简概念加以推广，利用可计算闭包的概念证明了$λ$ -项上的各种重写关系的终止性，包括模某些方程理论的重写和匹配模$β$ $η$的重写.这为各种高阶重写框架提供了一个强大的终止准则，包括Klop的简单类型组合约简系统和Nipkow的高阶重写系统。
cs.LOmath.LO
九头蛇之战与AC终止性
Hydra Battles and AC Termination
本文提出用带AC符号的重写系统编码赫拉克勒斯与九头蛇之战，可忠实建模任意策略，并通过类型引入、多类型语义标签和新的AC-MPO归约序证明其终止性。
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之间的联系，并获得更强大的技术来证明重写系统的生产力。
cs.LOcs.PL
可逆布尔电路重写的终止性作为一个自由3-范畴问题
Termination of Rewriting on Reversible Boolean Circuits as a Free 3-Category Problem
本文将一类表现力等同经典电路的可逆布尔电路表示为自由3-范畴Toff，通过定义到3-范畴Move的非保恒等函子追踪导线移动，从而证明电路重写的终止性。
cs.LOmath.CT
使用半环上的加权类型图证明图变换系统的终止性
Proving Termination of Graph Transformation Systems using Weighted Type Graphs over Semirings
本文提出基于有序半环的加权类型图方法，将矩阵解释推广到图重写，通过权重递减证明图变换系统的均匀终止性，并在工具Grez中实现。
cs.FLcs.LO
基于类型的高阶重写系统的终止准则
A type-based termination criterion for dependently-typed higher-order rewrite systems
一些作者设计了基于类型的终止标准ML类语言允许非结构递归调用。我们将这些工作扩展到一般的重写和依赖类型，从而为构造演算中的重写和β-还原的组合提供了一个强大的终止标准。
cs.LOcs.PL
关于在Agda中形式化抽象重写
A Formalization of Abstract Rewriting in Agda
Appalachian State University（阿巴拉契亚州立大学）
本文在Agda中形式化了抽象重写系统，改进了终止和连通性标准，并通过lambda演算示例展示了其应用。
cs.LOmath.LO
利用项重写实现逻辑程序的自动终止性证明
Automated Termination Proofs for Logic Programs by Term Rewriting
RWTH Aachen（亚琛工业大学）；TU Eindhoven（埃因霍温理工大学）；University of Innsbruck（因斯布鲁克大学）
逻辑程序的可终止性分析有两种方法：“转换”法和“直接”法。直接方法直接在逻辑程序的基础上证明终止。转换方法将一个逻辑程序转换成一个项重写系统（TRS），然后分析所得到的TRS的终止。因此，转换方法使以前为TRS开发的所有方法也可用于逻辑程序。然而，大多数现有的转换的适用性是相当有限的，因为它们只能用于逻辑程序的某些子类。(Most它们中的一个仅限于模式良好的程序。）在本文中，我们改进这些转换，使它们成为适用于任何明确的逻辑程序。为了用TRS模拟逻辑程序的行为，我们稍微修改了重写的概念，允许无限项。我们表明，我们的转换结果TRS这确实是适合自动终止分析。与大多数其他逻辑程序的终止方法相比，我们的技术也适用于逻辑程序设计，而不需要发生检查，这是在实践中通常使用的。我们在终止证明程序AProVE中实现了我们的方法，并在大量示例中成功地对其进行了评估。
cs.AIcs.LOcs.PL
统一高阶依赖对框架
The unified higher-order dependency pair framework
近年来，针对一阶项重写终止性分析的强大依赖对方法，定义了两种高阶扩展：静态方法和动态方法。这两种方法都有明显的优点和缺点。然而，一个大统一的理论是迄今为止失踪，这两种方法缺乏模块化的依赖对框架中常用的一阶重写。此外，这两种方法都不能用来证明不终止。在本文中，我们的目标是通过定义一个高阶依赖对框架，将这两种方法集成到一个共享的正式设置来解决这个差距。该框架已在（全自动）高阶终止工具WANDA中实现。
cs.LO
Coq中高阶终止的形式化
Formalizing Higher-Order Termination in Coq
我们描述了高阶重写理论的形式化，并正式证明了AFS是强规范化的，如果它可以解释在一个良好的基础域。为此，我们使用Coq，它是一个基于依赖类型论的证明助手。使用这种形式化，可以实现几种终止技术，如解释方法或依赖对，并证明它们的正确性。然后可以将这些实现提取到OCaml中，这会产生经过验证的终止检查器。
cs.LO
面向（通用）可计算性的高阶约束依赖对
Higher-Order Constrained Dependency Pairs for (Universal) Computability
本文将静态依赖对框架适配至逻辑约束简单类型项重写系统（LCSTRSs），并提出通用可计算性概念以实现开放世界终止性分析。
cs.LO
关于项重写系统几个图性质不可判定性的统一证明的注记
A Note on a Unifying Proof of the Undecidability of Several Diagrammatic Properties of Term Rewriting Systems
本文对项重写系统的几个图形性质的不可判定性给出了一个简单的统一证明，这些性质包括：局部合流性、强合流性、菱形性、次交换性和后继项的存在性。其思想是将图灵机的配置编码为项，然后在这些项上定义一个合适的关系，使得图灵机的终止性等价于图形属性的可满足性。
cs.LO
终止项重写系统的小项可达性及相关问题
Small Term Reachability and Related Problems for Terminating Term Rewriting Systems
本文研究终止项重写系统中是否可到达大小不超过 n 的项，按终止性证明方法给出 NP、N2ExpTime/NExpTime 与 PSpace 等复杂性分类，并分析合流性及大项变体的影响。
cs.LO
使用模式的逻辑程序非终止性
Non-Termination of Logic Programs Using Patterns
univ-reunion（留尼汪大学）
本文提出了一种基于模式的逻辑程序非终止性检测方法，通过新展开技术生成无限集合的有限重写序列，并通过实验验证其有效性。
cs.LO
关于类型概率λ演算中合流问题的一个注记
A Note on Confluence in Typed Probabilistic Lambda Calculi
关于概率重写的主题，有几个研究不同系统的终止和汇合的作品。在用λ演算模拟量子计算时，我们发现了一个具有概率重写规则和强归一化项的系统。我们研究的影响，在概率重写，仿射变量和战略的整体融合，在这个强规范化的概率演算的小修改。
cs.LO
用于实际简化过程的封装
Encapsulation for Practical Simplification Procedures
利用ACL 2证明了两种简化方法的性质。程序的复杂性不同，但解决了相同的编程问题，在决议/paramodulation定理证明系统的背景下出现的。术语重写是这两个过程的核心，但重写过程本身的细节是无关紧要的。ACL 2封装构造用于断言重写函数的存在并声明其某些属性。终止，不可还原性，和健全的性能，建立了每个程序。ACL 2中封装机制的可用性被认为是快速有效地验证此类算法的关键。
cs.LO
星游戏与九头蛇
Star Games and Hydras
本文通过引入星游戏简化递归路径排序的表述，并直接证明了九头蛇战役的终止性，同时提供了量化版本及未来研究方向。
cs.LO
一个静态高阶依赖对框架
A static higher-order dependency pair framework
我们重新审视了证明高阶项重写终止性的静态依赖对方法，并在许多方面对其进行了扩展：（1）我们引入了一种新的重写形式主义，设计用于高阶重写的终止性证明，具有元变量的代数泛函系统。(2)我们提供了一个语法检查的合理性标准，使该方法适用于一个大类的重写系统。(3)我们提出了一个模块化的依赖对框架，这种高阶设置。(4)我们引入了一个细粒度的概念，形成和可计算的链，使框架更强大。(5)我们制定了几个现有的和新的终止证明技术在我们的框架内的处理器的形式。该框架已在（全自动）高阶终止工具WANDA中实现。
cs.LOcs.PL
用树自动机证否非擦除单一组合子演算的终止性（完整版）
Disproving Termination of Non-Erasing Sole Combinatory Calculus with Tree Automata (Full Version)
针对单一组合子演算的终止性问题，改进基于SAT求解器的树自动机构造方法，成功证否了8个此前悬而未决的非擦除组合子的终止性。
cs.FLcs.LO
线性逻辑的范畴归约系统
A categorical reduction system for linear logic
图追逐不是一件容易的任务。如果我们有一个机械的方法来判断给定的两个态射是否彼此相等，则相干性在广义上成立。一个简单的方法是将一个相关的范畴转化为一个演算，其中图追踪的指令以重写规则的形式给出。我们将这一思想应用于线性逻辑的范畴语义。我们直接在语义的自由范畴上建立了一个演算。它使我们能够执行图表追踪，本质上是由重写规则领导的单向计算。我们验证了这种演算的弱终止性质。这为图表追踪的机械化迈出了第一步。
cs.LO
构造演算中重写的一致性和完全性
Consistency and Completeness of Rewriting in the Calculus of Constructions
向基于Curry-Howard同构的证明助手（例如Coq）添加重写可以极大地提高工具的可用性。不幸的是，添加任意一组重写规则可能会使底层的形式系统变得不可判定和不一致。虽然确保类型检查的终止性和汇合性以及可判定性的方法已经在一定程度上得到了研究，但逻辑一致性迄今为止很少受到关注。在本文中，我们表明，一致性是正规性的后果，这反过来又遵循重写规则定义的所有功能是完整的假设。我们提供了一个声音和终止，但不一定完整的算法来验证这个属性。该算法接受所有的定义，遵循相关的模式匹配计划Coquand和研究的McBride在他的博士论文。它还通过重写接受许多定义，包含偏离标准模式匹配的规则。
cs.LOcs.SC
通过高阶重写与元组解释刻画基本可行泛函
A Characterization of Basic Feasible Functionals Through Higher-Order Rewriting and Tuple Interpretations
本文利用高阶项重写中多项式有界的 cost-size 解释，证明了其可表示的泛函类恰好等价于第二型基本可行泛函类 BFF₂。
cs.CCcs.LO
通过广义加权类型图终止图变换系统
Termination of Graph Transformation Systems via Generalized Weighted Type Graphs
Vrije Universiteit Amsterdam（阿姆斯特丹自由大学）
本文提出了一种改进的加权类型图方法，用于证明图变换系统的终止性，并将其推广到其他范畴。
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。
cs.LO
