相关论文: Termination orders for 3-dimensional rewriting

Logically Constrained Term Rewriting Systems (LCTRSs) provide a general framework for term rewriting with constraints. We discuss a simple dependency pair approach to prove termination of LCTRSs. We see that existing techniques transfer to…

The relationship between Term Graph Rewriting and Term Rewriting is well understood: a single term graph reduction may correspond to several term reductions, due to sharing. It is also known that if term graphs are allowed to contain…

We study the properties, in particular termination, of dependent types systems for lambda calculus and rewriting.

In this document, we study a 3-polygraphic translation for the proofs of SKS, a formal system for classical propositional logic. We prove that the free 3-category generated by this 3-polygraph describes the proofs of classical propositional…

We study the notion of hierarchy in the context of visualizing textual data and navigating text collections. A formal framework for ``hierarchy'' is given by an ultrametric topology. This provides us with a theoretical foundation for…

Higher-dimensional rewriting systems are tools to analyse the structure of formally reducing terms to normal forms, as well as comparing the different reduction paths that lead to those normal forms. This higher structure can be captured by…

We study an alternative model of infinitary term rewriting. Instead of a metric on terms, a partial order on partial terms is employed to formalise convergence of reductions. We consider both a weak and a strong notion of convergence and…

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…

The fundamental groups of most (conjecturally, all) closed 3-manifolds with uniform geometries have finite complete rewriting systems. The fundamental groups of a large class of amalgams of circle bundles also have finite complete rewriting…

We study the computational model of polygraphs. For that, we consider polygraphic programs, a subclass of these objects, as a formal description of first-order functional programs. We explain their semantics and prove that they form a…

We show that finding rank-$R$ decompositions of a 3D tensor, for $R\le 4$, over a fixed finite field can be done in polynomial time. However, if some cells in the tensor are allowed to have arbitrary values, then rank-2 is NP-hard over the…

We generalise the termination method of higher-order polynomial interpretations to a setting with impredicative polymorphism. Instead of using weakly monotonic functionals, we interpret terms in a suitable extension of System F-omega. This…

We present a type system for strategy languages that express program transformations as compositions of rewrite rules. Our row-polymorphic type system assists compiler engineers to write correct strategies by statically rejecting non…

We present techniques to prove termination of cycle rewriting, that is, string rewriting on cycles, which are strings in which the start and end are connected. Our main technique is to transform cycle rewriting into string rewriting and…

All current investigations to analyze the derivational complexity of term rewrite systems are based on a single termination method, possibly preceded by transformations. However, the exclusive use of direct criteria is problematic due to…

We introduce layer systems for proving generalizations of the modularity of confluence for first-order rewrite systems. Layer systems specify how terms can be divided into layers. We establish structural conditions on those systems that…

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…

Polynomial interpretations are a useful technique for proving termination of term rewrite systems. They come in various flavors: polynomial interpretations with real, rational and integer coefficients. As to their relationship with respect…

We shall characterize the structure of invertible substitutions on three-letter alphabet. We show that any invertible substitution, after some cyclic operation, can be written as a finite product of permutations and Fibonacci's…

In this paper, we show how to extend the notion of reducibility introduced by Girard for proving the termination of $\beta$-reduction in the polymorphic $\lambda$-calculus, to prove the termination of various kinds of rewrite relations on…