共查询到20条相似文献,搜索用时 15 毫秒
1.
2.
Guillaume Feuillade Thomas Genet 《Electronic Notes in Theoretical Computer Science》2003,86(1):133-146
In this paper, we study the reachability problem for conditional term rewriting systems. Given two ground terms s and t, our practical aim is to prove s R* t for some join conditional term rewriting system R (possibly not terminating and not confluent). The proof method we propose relies on an over approximation of reachable terms for unrestricted join conditional term rewriting systems. This approximation is computed using an extension of the tree automata completion algorithm to the conditional case. 相似文献
3.
Guillaume Feuillade Thomas Genet Valérie Viet Triem Tong 《Journal of Automated Reasoning》2004,33(3-4):341-383
This paper surveys some techniques and tools for achieving reachability analysis over term rewriting systems. The core of those techniques is a generic tree automata completion algorithm used to compute in an exact or approximated way the set of descendants (or reachable terms). This algorithm has been implemented in the
tool. Furthermore, we show that many classes with regular sets of descendants of the literature corresponds to specific instances of the tree automata completion algorithm and can thus be efficiently computed by
. An extension of the completion algorithm to conditional term rewriting systems and some applications are also presented. 相似文献
4.
Jeroen Ketema Jan Willem Klop Vincent van Oostrom 《Electronic Notes in Theoretical Computer Science》2005,124(2):65
In this paper we first study the difference between Weak Normalization (WN) and Strong Normalization (SN), in the framework of first order orthogonal rewriting systems. With the help of the Erasure Lemma we establish a Pumping Lemma, yielding information about exceptional terms, defined as terms that are WN but not SN. A corollary is that if an orthogonal TRS is WN, there are no cyclic reductions in finite reduction graphs. This is a stepping stone towards the insight that orthogonal TRSs with the property WN, do not admit cyclic reductions at all. 相似文献
5.
A term rewriting system is called growing if each variable occurring on both the left-hand side and the right-hand side of a rewrite rule occurs at depth zero or one in the left-hand side. Jacquemard showed that the reachability and the sequentiality of linear (i.e., left-right-linear) growing term rewriting systems are decidable. In this paper we show that Jacquemard's result can be extended to left-linear growing rewriting systems that may have right-nonlinear rewrite rules. This implies that the reachability and the joinability of some class of right-linear term rewriting systems are decidable, which improves the results for right-ground term rewriting systems by Oyamaguchi. Our result extends the class of left-linear term rewriting systems having a decidable call-by-need normalizing strategy. Moreover, we prove that the termination property is decidable for almost orthogonal growing term rewriting systems. 相似文献
6.
《Journal of Symbolic Computation》1994,17(1):91-129
Often non left-linear rules in term rewriting systems can be replaced by a finite set of left-linear ones without changing the set of irreducible ground terms. Using appropriate test sets, we can always decide if this is possible and, in case it is, effectively perform such a transformation. We thus can also decide if the set of irreducible ground terms is a regular tree language. 相似文献
7.
Naoki Nishida Tomohiro Mizutani Masahiko Sakai 《Electronic Notes in Theoretical Computer Science》2007,174(10):75
Unravelings, transformations from conditional term rewriting systems (CTRSs, for short) into unconditional term rewriting systems, are valuable for analyzing properties of CTRSs. In order to completely simulate rewrite sequences of CTRSs, the restriction by a particular context-sensitive and membership condition that is determined by extra function symbols introduced due to the unravelings, must be imposed on the rewrite relations of the unraveled CTRSs. In this paper, in order to weaken the context-sensitive and membership condition, we propose a transformation applied to the unraveled CTRSs, that reduces the number of the extra symbols. In the transformation, updating the context-sensitive condition properly, we remove the extra symbols that satisfy a certain condition. If the transformation succeeds in removing all of the extra symbols, we obtain the TRSs that are computationally equivalent with the original CTRSs. 相似文献
8.
《Journal of Symbolic Computation》1994,18(4):319-352
The class of Strongly Sequential Term Rewriting Systems (SS) was defined in [Huet & Lévy (1979)]. [Strandh (1989)] defined the class of bounded TRSs (B). As a subset of B, Strandh defined the class of forward-branching TRSs (FB); FB strictly contains the class of Strongly-Left Sequential TRSs (SLS) defined by [Hoffmann & O'Donnell (1982)] for their Equational Programming System. For SLS, Hoffmann and O'Donnell found efficient algorithms to compute normal forms. Strandh showed that as efficient algorithms exist for FB.B is defined in terms of the existence of a deterministic pattern matching automaton called an index tree and FB in terms of the existence of a forward-branching index tree. Two open problems set by Strandh were to characterise FB in a simpler way and to find an algorithm to build a forward-branching index tree.This article contains three main parts. In the first part, we introduce the Strongly Sequential class and the Bounded class and we check that B = SS. This insures that FB ⊂ SS and relates Strandh's work to all the works initiated by [Huet & Lévy (1979)]. The second part contains the main result of this article: we give a very simple characterisation of FB. Our proof of the characterisation is constructive; it's then straightforward to extend it to an algorithm that builds a forward-branching index tree. In the third part we give the algorithm and show that it runs in quadratic time. 相似文献
9.
10.
11.
Zhang Xubo 《计算机科学技术学报》1991,6(3):291-295
Generally speaking,confluence property is not preserved when Term Rewriting Systems (TRSs) are combined,even if they are canonical.In this paper we give some sufficient conditions for ensuring the confluence property of combined left-linear,overlapping TRSs. 相似文献
12.
nfinite normal forms are a way of giving semantics to non-terminating rewrite systems. The notion is a generalization of the Böhm tree in the lambda calculus. It was first introduced in [Ariola, Z. M. and S. Blom, Cyclic lambda calculi, in: Abadi and Ito [Abadi, M. and T. Ito, editors, “Theoretical Aspects of Computer Software,” Lecture Notes in Computer Science 1281, Springer Verlag, 1997], pp. 77–106] to provide semantics for a lambda calculus on terms with letrec. In that paper infinite normal forms were defined directly on the graph rewrite system. In [Blom, S., “Term Graph Rewriting - syntax and semantics,” Ph.D. thesis, Vrije Universiteit Amsterdam (2001)] the framework was improved by defining the infinite normal form of a term graph using the infinite normal form on terms. This approach of lifting the definition makes the non-confluence problems introduced into term graph rewriting by substitution rules much easier to deal with. In this paper, we give a simplified presentation of the latter approach. 相似文献
13.
14.
项重写系统弱基终止性的归纳证明 总被引:3,自引:2,他引:1
1.引言项重写系统是一种受到广泛研究和应用的形式计算模型。一个项重写系统由一组称为重写规则的定向等式组成。例如,下面的R是一个由五个重写规则组成的、定义用({0,s})表示的自然数集N上的两倍函数d(x)=2×n:N→N的项重写系统: 相似文献
15.
《Information and Computation》2000,156(1-2):2-24
We present a survey of confluence properties of (acyclic) term graph rewriting. Results and counterexamples are given for different kinds of term graph rewriting; besides plain applications of rewrite rules, extensions with the operations of collapsing and copying, and both operations together are considered. Collapsing and copying together constitute bisimilarity of term graphs. We establish sufficient conditions for—and counterexamples to—confluence, confluence modulo bisimilarity, and the Church–Rosser property modulo bisimilarity. Moreover, we address rewriting modulo bisimilarity, that is, rewriting of bisimilarity classes of term graphs. 相似文献
16.
An algebraic specification of a new rewriting machine for fast rewriting of terms is considered. Theorems on the correctness of this specification are proved. A method for optimization of a strategy of iterative rewriting is proposed. 相似文献
17.
M.G.J. van den Brand P. Klint J.J. Vinju 《Electronic Notes in Theoretical Computer Science》2002,70(6):100-117
Term rewriting is an appealing technique for performing program analysis and program transformation. Tree (term) traversal is frequently used but is not supported by standard term rewriting. In this paper, many-sorted first-order term rewriting is extended with automatic tree traversal by adding two primitive tree traversal strategies and complementing them with three types of traversals. These so-called traversal functions can be either top-down or bottom-up. They can be sort preserving, mapping to a single sort, or a combination of these two. Traversal functions have a simple design, their application is type-safe in a first-order many-sorted setting and can be implemented efficiently. We describe the operational semantics of traversal functions and discuss applications. 相似文献
18.
Mechanizing Weakly Ground Termination Proving of Term Rewriting Systems by Structural and Cover-Set Inductions 下载免费PDF全文
Su Feng 《计算机科学技术学报》2005,20(4):496-513
The paper presents three formal proving methods for generalized weakly ground terminating property, i.e., weakly terminating property in a restricted domain of a term rewriting system, one with structural induction, one with cover-set induction, and the third without induction, and describes their mechanization based on a meta-computation model for term rewriting systems-dynamic term rewriting calculus. The methods can be applied to non-terminating, non-confluent and/or non-left-linear term rewriting systems. They can do "forward proving" by applying propositions in the proof, as well as "backward proving" by discovering lemmas during the proof. 相似文献
19.
Andrea Corradini Fabio Gadducci Wolfram Kahl Barbara Knig 《Electronic Notes in Theoretical Computer Science》2007,72(1):31-44
Multi-algebras allow to model nondeterminism in an algebraic framework by interpreting operators as functions from individual arguments to sets of possible results.We propose a simple inequational deduction system, based on term graphs, for inferring inclusions of derived relations in a multi-algebra, and we show that term graph rewriting provides a sound and complete implementation of it. 相似文献
20.
《Electronic Notes in Theoretical Computer Science》2001,8(4):320-340
Term rewriting has been shown to be a good environment for both programming and proving. For analysing and debugging rule-based programs, we propose in this work a formalism based on the rewriting calculus with explicit substitutions (ρσ-calculus). This formalism also allows us to build the proof terms of rewriting derivations. Therefore, term rewriting proofs can be exported to other systems by translating them into the corresponding syntaxes. That is, using a proof checker, one can certify these proofs and vice versa, this method allows us to get term rewriting in proof assistants using an external system. Our method not only works with syntactic rewriting but also with rewriting modulo a set of axioms (e.g. associativity-commutativity). 相似文献