Symbol different term rewrite systems
type: Item
instance of: scholarly article
title: Symbol different term rewrite systems
zbMATH Open document ID: 1332.68105
author: Sándor Vágvölgyi
published in: Journal of Logical and Algebraic Methods in Programming
publication date: 2015-08-21T00:00:00Z
review text: A term containing no variables is called a ground term. The ground reachability problem for a term rewrite system (TRS) \(R\) is the problem of deciding for any given ground terms \(s\) and \(t\) whether \(s\) can be transformed to \(t\) by \(R\) while the ground word problem asks whether \(s\) and \(t\) are equivalent with respect to the congruence defined by \(R\). Both problems are encountered in applications of term rewriting, but since they are undecidable for a general \(R\), approximating the ground reducibility relation \(\rightarrow_{R,g}^*\) or the ground equivalence relation \(\leftrightarrow_{R,g}^*\) of \(R\) by some decidable relation has been proposed as a way to settle instances of the two problems. Here the author presents three heuristics for finding ground tree transducers (GTT) (cf. [\textit{M. Dauchet} et al., Inf. Comput. 88, No. 2, 187--201 (1990; Zbl 0705.68067)]) or extended ground term rewriting systems (EGTRS) (cf. [\textit{J. Engelfriet}, Inf. Comput. 152, No. 1, 1--15 (1999; Zbl 1045.68580)]) that yield upper approximations of \(\rightarrow_{R,g}^*\) and \(\leftrightarrow_{R,g}^*\) as well as associated heuristics for using these approximations for showing that two given ground terms are not related by \(\rightarrow_{R,g}^*\) or \(\leftrightarrow_{R,g}^*\). In numerous examples the heuristics are compared with each other or with previously presented methods. The search for such approximations leads to the problem of deciding whether a given GTT is an upper approximation of a given TRS. It is not known whether the question is decidable in its general form, but the author proves its decidability for symbol-different term-rewrite systems (SDTRS), a new class of TRSs introduced here. This main result of the paper entails also the fact that it is decidable whether a given EGTRS is an upper approximation of a given SDTRS. On the other hand, it is undecidable for a linear SDTRS \(R\) and a deterministic bottom-up tree automaton \(\mathcal{A}\) …
reviewed by: Magnus Steinby
Mathematics Subject Classification ID: 68Q42
Mathematics Subject Classification ID: 03D40
Mathematics Subject Classification ID: 68Q45
zbMATH DE Number: 6474621
zbMATH Keywords: term-rewriting system
zbMATH Keywords: ground reachability
zbMATH Keywords: ground word problem
zbMATH Keywords: ground tree transducer
zbMATH Keywords: tree automaton
describes a project that uses: Timbuk
MaRDI profile type: Publication
full work available at URL: j.jlamp.2015.06.005
OpenAlex ID: W1100208954
cites work: Finer Is Better: Abstraction Refinement for Rewriting Approximations
cites work: Rewriting Approximations for Fast Prototyping of Static Analyzers
cites work: Handling Algebraic Properties in Automatic Analysis of Security Protocols
cites work: Q3259710
cites work: Decidability of the confluence of finite ground term rewrite systems and of other related term rewrite systems
cites work: Variations on the Common Subexpression Problem
cites work: Implementing term rewriting by jungle evaluation
cites work: Decidable call-by-need computations in term rewriting
cites work: Left-linear Bounded TRSs are Inverse Recognizability Preserving
cites work: Derivation trees of ground term rewriting systems.
cites work: Reachability analysis over term rewriting systems
cites work: Q4005178
cites work: Restricted ground tree transducers
cites work: Q2723425
cites work: Reachability Analysis of Term Rewriting Systems with Timbuk
cites work: On tree automata that certify termination of left-linear term rewriting systems
cites work: Q4179852
cites work: A fast algorithm for generating reduced ground rewriting systems from a set of ground equations
cites work: Q2723905
cites work: Q4799892
cites work: A fast algorithm for constructing a tree automaton recognizing a congruential tree language
cites work: Term rewriting restricted to ground terms.
cites work: Congruences Generated by Extended Ground Term Rewrite Systems
DOI: 10.1016/J.JLAMP.2015.06.005
Recommended article: Q4702599
Recommended article: Q3336738
Recommended article: Reversible Term Rewriting
Recommended article: Extended term rewriting systems
Recommended article: Q3970984
Recommended article: Q3817590
Recommended article: Q4799892
Recommended article: Murg term rewrite systems
Recommended article: Term Rewriting and Applications
description: scientific article; zbMATH DE number 6474621