相关论文: Polygraphs for termination of left-linear term rew…

This article is concerned with automating the decreasing diagrams technique of van Oostrom for establishing confluence of term rewrite systems. We study abstract criteria that allow to lexicographically combine labelings to show local…

Geometric modeling by constraints leads to large systems of algebraic equations. This paper studies bipartite graphs underlaid by systems of equations. It shows how these graphs make possible to polynomially decompose these systems into…

We present a translation function from nominal rewriting systems (NRSs) to combinatory reduction systems (CRSs), transforming closed nominal rules and ground nominal terms to CRSs rules and terms, respectively, while preserving the…

Dependency pairs are one of the most powerful techniques to analyze termination of term rewrite systems (TRSs) automatically. We adapt the dependency pair framework to the probabilistic setting in order to prove almost-sure innermost…

We introduce a termination method for the algebraic graph transformation framework PBPO+, in which we weigh objects by summing a class of weighted morphisms targeting them. The method is well-defined in rm-adhesive quasitoposes (which…

Conditional term rewriting is an intuitive yet complex extension of term rewriting. In order to benefit from the simpler framework of unconditional rewriting, transformations have been defined to eliminate the conditions of conditional term…

Rewriting Induction (RI) is a method to prove inductive theorems, originating from equational reasoning. By using Logically Constrained Simply-typed Term Rewriting Systems (LCSTRSs) as an intermediate language, rewriting induction becomes a…

We propose a generic termination proof method for rewriting under strategies, based on an explicit induction on the termination property. Rewriting trees on ground terms are modeled by proof trees, generated by alternatively applying…

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…

The Size-Change Termination principle was first introduced to study the termination of first-order functional programs. In this work, we show that it can also be used to study the termination of higher-order rewriting in a system of…

We report on the automation of a technique to prove the correctness of program transformations in higher-order program calculi which may permit recursive let-bindings as they occur in functional programming languages. A program…

We describe a method for proving non-looping non-termination, that is, of term rewriting systems that do not admit looping reductions. As certificates of non-termination, we employ regular (tree) automata.

We explore the Collatz conjecture and its variants through the lens of termination of string rewriting. We construct a rewriting system that simulates the iterated application of the Collatz function on strings corresponding to mixed…

We present a constructive formalization of Abstract Rewriting Systems (ARS) in the Agda proof assistant, focusing on standard results in term rewriting. We define a taxonomy of concepts related to termination and confluence and investigate…

We consider the almost-sure (a.s.) termination problem for probabilistic programs, which are a stochastic extension of classical imperative programs. Lexicographic ranking functions provide a sound and practical approach for termination of…

The theory of finite and infinitary term rewriting is extensively developed for orthogonal rewrite systems, but to a lesser degree for weakly orthogonal rewrite systems. In this note we present some contributions to the latter case of weak…

Considering patterns as sets of their instances, a difference operator over patterns computes a finite set of two given patterns, which represents the difference between the dividend pattern and the divisor pattern. A complement of a…

Term rewriting is a Turing complete model of computation. When taught to students of computer science, key properties of computation as well as techniques to analyze programs on an abstract level are conveyed. This paper gives a swift…

Orthogonality is a discipline of programming that in a syntactic manner guarantees determinism of functional specifications. Essentially, orthogonality avoids, on the one side, the inherent ambiguity of non determinism, prohibiting the…

Dependency pairs are one of the most powerful techniques for proving termination of term rewrite systems (TRSs), and they are used in almost all tools for termination analysis of TRSs. Problem #106 of the RTA List of Open Problems asks for…