具有有理导数的术语重写系统

Strategies for linear rewriting systems: link with parallel rewriting and involutive divisions

We study rewriting systems whose underlying set of terms is equipped with a vector space structure over a given field. We introduce parallel rewriting relations, which are rewriting relations compatible with the vector space structure, as well as rewriting strategies, which consist in choosing one rewriting step for each reducible basis element of the vector space. Using these notions, we introduce the S-confluence property and show that it implies confluence. We deduce a proof of the diamond's lemma, based on strategies. We illustrate our general framework with rewriting systems over rational…

Tracelets and Tracelet Analysis Of Compositional Rewriting Systems

Taking advantage of a recently discovered associativity property of rule compositions, we extend the classical concurrency theory for rewriting systems over adhesive categories. We introduce the notion of tracelets, which are defined as minimal derivation traces that universally encode sequential compositions of rewriting rules. Tracelets are compositional, capture the causality of equivalence classes of traditional derivation traces, and intrinsically suggest a clean mathematical framework for the definition of various notions of abstractions of traces. We illustrate these features by introdu…

术语图重写与并行术语重写

Term Graph Rewriting and Parallel Term Rewriting

术语图重写和术语重写之间的关系很好理解：由于共享，单个术语图缩减可能对应于多个术语缩减。还已知的是，如果允许项图包含循环，则一个项图约简可以对应于无限多个项约简。我们强调，这一事实可以从两个方面来解释。根据“顺序解释”，项图约简对应于项约简的无限序列，如Kennaway等人在无限项的完整度量空间上使用强收敛导子形式化的。相反，根据“并行解释”，项图约简对应于在有理项中的无限集合的redex的并行约简。我们正式后一个概念，利用完整的偏序的无限和可能的部分条款，我们强调，这种解释允许解释的结果，减少循环赎回的几种方法，长期图重写。

通过重写实现线性化（长版本）

Linearization via Rewriting (Long Version)

本研究提出结构化资源λ演算，可内部将类型推导重写为线性化形式，兼具规范性与合流性，能表示所有强规范化λ项，是首个纯有穷、基于重写的内部线性化系统。

Tuple Interpretations for Higher-Order Rewriting

We develop a class of algebraic interpretations for many-sorted and higher-order term rewriting systems that takes type information into account. Specifically, base-type terms are mapped to \emph{tuples} of natural numbers and higher-order terms to functions between those tuples. Tuples may carry information relevant to the type; for instance, a term of type $\mathsf{nat}$ may be associated to a pair $(\mathsf{cost}, \mathsf{size})$ representing its evaluation cost and size. This class of interpretations results in a more fine-grained notion of complexity than runtime or derivational complexit…

术语重写的模块复杂度分析

Modular Complexity Analysis for Term Rewriting

所有目前的调查，以分析衍生复杂性的长期重写系统是基于一个单一的终止方法，可能之前的转换。然而，由于直接标准的权力有限，专门使用直接标准是有问题的。为了克服这一限制，本文介绍了一个模块化的框架，它允许推断（多项式）上界的复杂性，长期重写系统结合不同的标准。由于其基本思想是基于相对重写，我们研究如何矩阵的解释和匹配边界可以使用和扩展相对重写的复杂性，分别。模块化框架被证明比传统的设置更强大。此外，结果已经实施，实验表明，显着的增益功率。