共查询到20条相似文献,搜索用时 0 毫秒
1.
We describe conditional rewriting by means of an inference system and capture termination as the absence of infinite inference: that is, all proof attempts must either successfully terminate, or they must fail in finite time. We call this notion operational termination. Our notion of operational termination is parametric on the inference system. We prove that operational termination of CTRSs is, in fact, equivalent to a very general notion proposed for 3-CTRSs, namely the notion of quasi-decreasingness, which is currently the most general one which is intended to be checked by comparing parts of the CTRS by means of term orderings. Therefore, existing methods for proving quasi-decreasingness of CTRSs immediately apply to prove operational termination of CTRSs. 相似文献
2.
《Information Processing Letters》1987,26(2):65-70
Some sufficient conditions are given for the termination of the direct sum of two term-rewriting systems: either no right-hand side of a rule is a variable, or no right-hand side contains more occurences of a variable than the corresponding left-hand side. 相似文献
3.
《The Journal of Logic and Algebraic Programming》2010,79(7):659-688
We investigate the practically crucial property of operational termination of deterministic conditional term rewriting systems (DCTRSs), an important declarative programming paradigm. We show that operational termination can be equivalently characterized by the newly introduced notion of context-sensitive quasi-reductivity. Based on this characterization and an unraveling transformation of DCTRSs into context-sensitive (unconditional) rewrite systems (CSRSs), context-sensitive quasi-reductivity of a DCTRS is shown to be equivalent to termination of the resulting CSRS on original terms (i.e., terms over the signature of the DCTRS). This result enables both proving and disproving operational termination of given DCTRSs via transformation into CSRSs. A concrete procedure for this restricted termination analysis (on original terms) is proposed and encouraging benchmarks obtained by the termination tool VMTL, that utilizes this approach, are presented. Finally, we show that the context-sensitive unraveling transformation is sound and complete for collapse-extended termination, thus solving an open problem of Duran et al. (2008) [10]. 相似文献
4.
《Information and Computation》2007,205(4):512-534
We present a new method for automatically proving termination of left-linear term rewriting systems on a given regular language of terms. It is a generalization of the match bound method for string rewriting. To prove that a term rewriting system terminates we first construct an enriched system over a new signature that simulates the original derivations. The enriched system is an infinite system over an infinite signature, but it is locally terminating: every restriction of the enriched system to a finite signature is terminating. We then construct iteratively a finite tree automaton that accepts the enriched given regular language and is closed under rewriting modulo the enriched system. If this procedure stops, then the enriched system is compact: every enriched derivation involves only a finite signature. Therefore, the original system terminates. We present two methods to construct the enrichment: roof heights for left-linear systems, and match heights for linear systems. For linear systems, the method is strengthened further by a forward closure construction. Using these methods, we give examples for automated termination proofs that cannot be obtained by standard methods. 相似文献
5.
6.
David A. Plaisted 《Information Processing Letters》1985,20(2):61-64
The self-embedding property of term rewriting systems is closely related to the uniform termination property, since a nonself-embedding term rewriting system is uniform terminating. The self-embedding property is shown to be undecidable and partially decidable. It follows that the nonself-embedding property is not partially decidable. This is true even for globally finite term rewriting systems. The same construction gives an easy alternate proof that uniform termination is undecidable in general and also for globally finite term rewriting systems. Also, the looping property is shown to be undecidable in the same way. 相似文献
7.
This work is motivated by the fact that a “compact” semantics for term rewriting systems, which is essential for the development of effective semantics-based program manipulation tools (e.g. automatic program analyzers and debuggers), does not exist. The big-step rewriting semantics that is most commonly considered in functional programming is the set of values/normal forms that the program is able to compute for any input expression. Such a big-step semantics is unnecessarily oversized, as it contains many “semantically useless” elements that can be retrieved from a smaller set of terms. Therefore, in this article, we present a compressed, goal-independent collecting fixpoint semantics that contains the smallest set of terms that are sufficient to describe, by semantic closure, all possible rewritings. We prove soundness and completeness under ascertained conditions. The compactness of the semantics makes it suitable for applications. Actually, our semantics can be finite whereas the big-step semantics is generally not, and even when both semantics are infinite, the fixpoint computation of our semantics produces fewer elements at each step. To support this claim we report several experiments performed with a prototypical implementation. 相似文献
8.
9.
Recursion can be conveniently modeled with left-linear positive/negative-conditional term rewriting systems, provided that non-termination, non-trivial critical overlaps, non-right-stability, non-normality, and extra variables are admitted. For such systems we present novel sufficient criteria for shallow confluence and arrive at the first decidable confluence criterion admitting non-trivial critical overlaps. To this end, we restrict the introduction of extra variables of right-hand sides to binding equations and require the critical pairs to have somehow complementary literals in their conditions. Shallow confluence implies [level] confluence, has applications in functional logic programming, and guarantees the object-level consistency of the underlying data types in the inductive theorem prover QuodLibet. 相似文献
10.
Using term rewriting systems to design and verify processors 总被引:2,自引:0,他引:2
11.
The limit behaviors of computations have not been fully explored. It is necessary to consider such limit behaviors when we
consider the properties of infinite objects in computer science, such as infinite logic programs, the symbolic solutions of
infinite polynomial equations. Usually, we can use finite objects to approximate infinite objects, and we should know what
kinds of infinite objects are approximable and how to approximate them effectively. A sequence {R
k
: k ε ω} of term rewriting systems has the well limit behavior if under the condition that the sequence has the set-theoretic limit
or the distance-based limit, the sequence {Th(R
k
): k ε ω} of corresponding theoretic closures of R
k
has the set-theoretic or distance-based limit, and lim
k→∞
Th(R
k
) is equal to the theoretic closure of the limit of {R
k
: k ε ω}. Two kinds of limits of term rewriting systems are considered: one is based on the set-theoretic limit, the other is on
the distance-based limit. It is proved that given a sequence {R
k
: κ ε ω} of term rewriting systems R
k
, if there is a well-founded ordering ≺ on terms such that every R
k
is ≺-well-founded, and the set-theoretic limit of {R
k
: κ ε ω} exists, then {R
k
: κ ε ω} has the well limit behavior; and if (1) there is a well-founded ordering ≺ on terms such that every R
k
is ≺-well-founded, (2) there is a distance d on terms which is closed under substitutions and contexts and (3) {R
k
: k ε ω} is Cauchy under d then {R
κ: κ ε ω} has the well limit behavior. The results are used to approximate the least Herbrand models of infinite Horn logic programs
and real Horn logic programs, and the solutions and Gr?bner bases of (infinite) sets of real polynomials by sequences of (finite)
sets of rational polynomials. 相似文献
12.
The unification problem for term rewriting systems (TRSs) is the problem of deciding, for a given TRS R and two terms M and N, whether there exists a substitution θ such that Mθ and Nθ are congruent modulo R (i.e., Mθ↔R*Nθ). In this paper, the unification problem for confluent right-ground TRSs is shown to be decidable. To show this, the notion of minimal terms is introduced and a new unification algorithm for obtaining a substitution whose range consists of minimal terms is proposed. Our result extends the decidability of unification for canonical (i.e., terminating and confluent) right-ground TRSs given by Hullot [Proceedings of the 5th Conference on Automated Deduction, LNCS, vol. 87, 1980, p. 318] in the sense that the termination condition can be omitted. 相似文献
13.
Florent Jacquemard 《Information Processing Letters》2003,87(5):265-270
Ground reachability, ground joinability and confluence are shown undecidable for flat term rewriting systems, i.e., systems in which all left and right members of rule have depth at most one. 相似文献
14.
Makoto Hamana 《Higher-Order and Symbolic Computation》2006,19(2-3):231-262
We present an extension of first-order term rewriting systems. It involves variable binding in the term language. We develop
systems called binding term rewriting systems (BTRSs) in a stepwise manner. First we present the term language, then formulate
equational logic. Finally, we define rewriting systems. This development is novel because we follow the initial algebra approach
in an extended notion of Σ-algebras in various functor categories. These are based on Fiore-Plotkin-Turi’s presheaf semantics
of variable binding and Lüth-Ghani’s monadic semantics of term rewriting systems. We characterise the terms, equational logic
and rewrite systems for BTRSs as initial algebras in suitable categories. Then, we show an important rewriting property of
BTRSs: orthogonal BTRSs are confluent. Moreover, by using the initial algebra semantics, we give a complete characterisation
of termination of BTRSs. Finally, we discuss our design choice of BTRSs from a semantic perspective.
An erlier version appeared in Proc. Fifth ACM-SIGPLAN International Conference on Principles and Practice of Declarative Programming (PPDP2003). 相似文献
15.
The narrowing mechanism and term rewriting systems are powerful tools for constructing complete and efficient unification algorithms for useful classes of equational theories. This has been shown for the case where term rewriting systems are confluent and noetherian (i.e., terminating). In this paper we show that the narrowing mechanism, combined with ordinary unification, yields a complete unification algorithm for equational theories that can be described by a closed linear term rewriting system with the non-repetition property; this class allows non-terminating rewrite systems. For some special forms of input terms, narrowing generates complete sets of E-unifiers without resorting to the non-repetition property. The key observation underlying the proof is that a reduction sequence in this class of term rewriting system can be transformed into one which possesses properties that enable a completeness proof. 相似文献
16.
Summary The decidability of the sufficient completeness property of equational specifications satisfying certain conditions is shown. In addition, the decidability of the related concept of quasi-reducibility of a term with respect to a set of rules is proved. Other results about irreducible ground terms of a term rewriting system also follow from a key technical lemma used in these decidability proofs; this technical lemma states that there is a finite bound on the substitutions of ground terms that need to be considered in order to check for a given term, whether the result obtained by any substitution of ground terms into the term is irreducible. These results are first shown for untyped systems and are subsequently extended to typed systems.Partially supported by the National Science Foundation Grant no. DCR-8408461 相似文献
17.
Antoy S. Gannon J. 《IEEE transactions on pattern analysis and machine intelligence》1994,20(4):259-274
This paper describes a uniform approach to the automation of verification tasks associated with while statements, representation functions for abstract data types, generic program units, and abstract base classes. Program units are annotated with equations containing symbols defined by algebraic axioms. An operation's axioms are developed by using strategies that guarantee crucial properties such as convergence and sufficient completeness. Sets of axioms are developed by stepwise extensions that preserve these properties. Verifications are performed with the aid of a program that incorporates term rewriting, structural induction, and heuristics based on ideas used in the Boyer-Moore prover. The program provides valuable mechanical assistance: managing inductive arguments and providing hints for necessary lemmas, without which formal proofs would be impossible. The successes and limitations of our approaches are illustrated with examples from each domain 相似文献
18.
In this paper, we propose the notion of reducibility of symbols in term rewriting systems (TRSs). For a given algebraic specification, operation symbols can be classified on the basis of their denotations: the operation symbols for functions and those for constructors. In a model, each term constructed by using only constructors should denote an element, and functions are defined on sets formed by these elements. A term rewriting system provides operational semantics to an algebraic specification. Given a TRS, a term is called reducible if some rewrite rule can be applied to it. An irreducible term can be regarded as an answer in a sense. In this paper, we define the reducibility of operation symbols as follows: an operation symbol is reducible if any term containing the operation symbol is reducible. Non-trivial properties of context-sensitive rewriting, which is a simple restriction of rewriting, can be obtained by restricting the terms on the basis of variable occurrences, its sort, etc. We confirm the usefulness of the reducibility of operation symbols by applying them to behavioral specifications for proving the behavioral coherence property. 相似文献
19.
M. R. K. Krishna Rao 《Acta Informatica》1996,33(5):595-606
Innermost-confluence is important in giving call-by-value and denotational semantics and outermost-confluence is important in giving call-by-need and lazy semantics of programs. In this paper, we give a few sets of sufficient conditions under which the properties of confluence, innermost-confluence and outermost-confluence coincide. Confluence and innermost-confluence coincide for weakly innermost normalizing overlay systems and confluence and outermost-confluence coincide for outermost normalizing left-linear overlay systems. In general, every weakly innermost (outermost) normalizingconfluent system isinnermost (outermost) confluent but the converse is not true. 相似文献
20.
《The Journal of Logic and Algebraic Programming》2014,83(1):53-63
Tail recursive functions are a special kind of recursive functions where the last action in their body is the recursive call. Tail recursion is important for a number of reasons (e.g., they are usually more efficient). In this article, we introduce an automatic transformation of first-order functions into tail recursive form. Functions are defined using a (first-order) term rewrite system. We prove the correctness of the transformation for constructor-based reduction over constructor systems (i.e., typical first-order functional programs). 相似文献