scholarly journals Transforming Prefix-constrained or Controlled Rewrite Systems

10.29007/m335 ◽  
2018 ◽  
Author(s):  
Nirina Andrianarivelo ◽  
Vivien Pelletier ◽  
Pierre Réty
Keyword(s):  
Rewrite Systems ◽  
Rewrite System

We present two techniques for transforming any prefix-constrained and any controlled term rewrite system into an ordinary rewrite system. We prove that both transformations preserve the rewrite com- putations, and preserve termination. In this way, prefix-constrained rewriting and controlled rewriting can be run, and termination can be checked, using the usual tools for ordinary rewriting.

THE BRESSAUD NORMAL FORM OF BRAIDS THROUGH WORD REWRITE SYSTEMS

2013 ◽  
Vol 22 (01) ◽  
pp. 1250135
Author(s):  
JEREMY CHAMBOREDON
Keyword(s):  
Normal Form ◽  
Knot Theory ◽  
Rewrite Systems ◽  
Rewrite System

We introduce a nondeterministic rewrite system which is conjectured to converge to the Bressaud normal form of braids as presented in [X. Bressaud, A normal form for braids, J. Knot Theory Ramifications17(6) (2008) 697–732]. We prove the conjecture for 3-strand braids.

scholarly journals Finding small counterexamples for abstract rewriting properties

2018 ◽  
Vol 28 (8) ◽  
pp. 1485-1505
Author(s):  
HANS ZANTEMA
Keyword(s):  
Binary Relation ◽  
Normal Forms ◽  
Satisfying Assignment ◽  
Rewrite Systems ◽  
Abstract Setting ◽  
Sat Solver ◽  
Rewrite System ◽  
A Current

Rewriting notions like termination, normal forms and confluence can be described in an abstract way referring to rewriting only as a binary relation. Several theorems on rewriting, like Newman's lemma, can be proved in this abstract setting. For investigating possible generalizations of such theorems, it is fruitful to have counterexamples showing that particular generalizations do not hold. In this paper, we develop a technique to find such counterexamples fully automatically, and we describe our tool Carpa that follows this technique. The basic idea is to fix the number of objects of the abstract rewrite system, and to express the conditions and the negation of the conclusion in a satisfiability (SAT) formula, and then call a current SAT solver. In case the formula turns out to be satisfiable, the resulting satisfying assignment yields a counterexample to the encoded property. We give several examples of finite abstract rewrite systems having remarkable properties that are found in this way fully automatically.

scholarly journals Computing knowledge in equational extensions of subterm convergent theories

2020 ◽  
Vol 30 (6) ◽  
pp. 683-709
Author(s):  
Serdar Erbatur ◽  
Andrew M. Marshall ◽  
Christophe Ringeissen
Keyword(s):  
General Procedure ◽  
Security Protocols ◽  
Equational Theory ◽  
Finite Measure ◽  
Decision Procedures ◽  
Rewrite Systems ◽  
Static Equivalence ◽  
Equivalence Problems ◽  
Rewrite System

AbstractWe study decision procedures for two knowledge problems critical to the verification of security protocols, namely the intruder deduction and the static equivalence problems. These problems can be related to particular forms of context matching and context unification. Both problems are defined with respect to an equational theory and are known to be decidable when the equational theory is given by a subterm convergent term rewrite system (TRS). In this work, we extend this to consider a subterm convergent TRS defined modulo an equational theory, like Commutativity. We present two pairs of solutions for these important problems. The first solves the deduction and static equivalence problems in rewrite systems modulo shallow theories such as Commutativity. The second provides a general procedure that solves the deduction and static equivalence problems in subterm convergent systems modulo syntactic permutative theories, provided a finite measure is ensured. Several examples of such theories are also given.

scholarly journals Event structures and non-orthogonal term graph rewriting

1996 ◽  
Vol 6 (6) ◽  
pp. 545-578 ◽  
Author(s):  
David Clark ◽  
Richard Kennaway
Keyword(s):  
State Space ◽  
Garbage Collection ◽  
Event Structure ◽  
Graph Rewriting ◽  
Rewrite Systems ◽  
Event Structures ◽  
Asymmetric Conflicts ◽  
Algebraic Domain ◽  
Directed Completion ◽  
Rewrite System

We show that for every term graph in a left-linear but non-orthogonal term graph rewrite system, one can construct an event structure that represents all the possible reductions that can occur in reduction sequences starting from that term graph. Every finite reduction sequence from that graph corresponds to a configuration of the event structure, and Lévy-equivalent sequences correspond to the same configuration.Garbage collection is modelled in the event structure by an ‘erases’ relation. The asymmetric conflicts that arise in non-orthogonal rewrite systems are modelled by introducing a ‘prevents’ relation. The configurations of the event structure then form the state space of an event automaton. Taking the directed completion of this space yields a prime algebraic domain.

scholarly journals CoCo 2019: report on the eighth confluence competition

2021 ◽  
Author(s):  
Aart Middeldorp ◽  
Julian Nagele ◽  
Kiraku Shintani
Keyword(s):  
Software Tools ◽  
Rewrite Systems

AbstractWe report on the 2019 edition of the Confluence Competition, a competition of software tools that aim to prove or disprove confluence and related (undecidable) properties of rewrite systems automatically.

TERMINATION OF ABSTRACT REDUCTION SYSTEMS

2009 ◽  
Vol 20 (01) ◽  
pp. 57-82
Author(s):  
JEREMY E. DAWSON ◽  
RAJEEV GORÉ
Keyword(s):  
General Theorem ◽  
Combinatory Logic ◽  
Rewrite Systems ◽  
Path Ordering

We present a general theorem capturing conditions required for the termination of abstract reduction systems. We show that our theorem generalises another similar general theorem about termination of such systems. We apply our theorem to give interesting proofs of termination for typed combinatory logic. Thus, our method can handle most path-orderings in the literature as well as the reducibility method typically used for typed combinators. Finally we show how our theorem can be used to prove termination for incrementally defined rewrite systems, including an incremental general path ordering. All proofs have been formally machine-checked in Isabelle/HOL.

О системах переписывания процессов высокого уровня

2021 ◽  
Author(s):  
Ирина Александровна Ломазова
Keyword(s):  
Rewrite Systems

Системы переписывания процессов (Process Rewrite Systems - PRS) Ричарда Майра представляют собой систему переписывания термов специального вида и задают унифицированное представление для конечных и магазинных автоматов, сетей Петри и некоторых классов алгебр процессов. В докладе рассматривается (P,P)-подкласс систем переписывания процессов, соответствующий классическим сетям Петри, и его расширение HPRS для моделирования систем с динамической структурой. Обсуждаются вопросы выразительности и разрешимости.

Sign in / Sign up

Export Citation Format

Share Document