A Deterministic Lazy Narrowing Calculus

In this paper we study the non-determinism between the inference rules of the lazy narrowing calculusLNC(Middeldorpet al., 1996,Theoret. Comput. Sci.,167, 95–130. We show that all non-determinism can be removed without losing the important completeness property by restricting the underlying term rewriting systems to left-linear confluent constructor systems and interpreting equality as strict equality. For the subclass of orthogonal constructor systems the resulting narrowing calculus is shown to have the nice property that solutions computed by different derivations starting from the same goal are incomparable.     

A class of confluent term rewriting systems and unification

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.     

Induction for termination with local strategies

In this paper, we propose a method for specifically proving termination of rewriting with particular strategies: local strategies on operators. An inductive proof procedure is proposed, based on an explicit induction on the termination property. Given a term, the proof principle relies on alternatively applying the induction hypothesis on its subterms, by abstracting the subterms with induction variables, and narrowing the obtained terms in one step, according to the strategy. The induction relation, an F -stable ordering having the subterm property, is not given a priori, but its existence is checked along the proof, by testing satisfiability of ordering constraints.     

Proving weak properties of rewriting

In rule-based programming, properties of programs, such as termination, are in general considered in their strong acceptance, i.e., on every computation branch. But in practice, they may hold in their weak acceptance only, i.e., on at least one computation branch. Moreover, weak properties are often enough to ensure that programs give the expected result. There are very few results to handle weak properties of rewriting. We address here two of them: termination and reducibility to a constructor form, in a unified framework allowing us to prove them inductively. Proof trees are developed, which simulate rewriting trees by narrowing and abstracting subterms. Our technique is constructive in the sense that proof trees can be used to infer an evaluation strategy for any given input: the right computation branch is developed without using a costly breadth-first strategy nor backtracking.     

Counterexamples in infinitary rewriting with non-fully-extended rules

We show counterexamples exist to confluence modulo hypercollapsing subterms, fair normalisation, and the normal form property in orthogonal infinitary higher-order rewriting with non-fully-extended rules. This sets these systems apart from both fully-extended and finite systems, where no such counterexamples are possible.     

Certifying Term Rewriting Proofs in ELAN

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).     

Generalized Parsing and Term Rewriting: Semantics Driven Disambiguation

Generalized parsing technology provides the power and flexibility to attack real-world parsing applications. However, many programming languages have syntactical ambiguities that can only be solved using semantical analysis. In this paper we propose to apply the paradigm of term rewriting to filter ambiguities based on semantical information. We start with the definition of a representation of ambiguous derivations. Then we extend term rewriting with means to handle such derivations. Finally, we apply these tools to some real world examples, namely C and COBOL. The resulting architecture is simple and efficient as compared to semantic directed parsing.     

Rewrite rule systems for modal propositional logic

This paper explains new results relating modal propositional logic and rewrite rule systems. More precisely, we give complete term rewriting systems for the modal propositional systems known as K, Q, T, and S5. These systems are presented as extensions of Hsiang's system for classical propositional calculus. We have checked local confluence with the rewrite rule system K.B. (cf. the Knuth-Bendix algorithm) developed by the Formel project at INRIA. We prove that these systems are noetherian, and then infer their confluence from Newman's lemma. Therefore each term rewriting system provides a new automated decision procedure and defines a canonical form for the corresponding logic. We also show how to characterize the canonical forms thus obtained.     

Expressing combinatory reduction systems derivations in the rewriting calculus

The last few years have seen the development of the rewriting calculus (also called rho-calculus or ρ-calculus) that uniformly integrates first-order term rewriting and the λ-calculus. The combination of these two latter formalisms has been already handled either by enriching first-order rewriting with higher-order capabilities, like in the Combinatory Reduction Systems (CRS), or by adding to the λ-calculus algebraic features. The various higher-order rewriting systems and the rewriting calculus share similar concepts and have similar applications, and thus, it is important to compare these formalisms to better understand their respective strengths and differences. We show in this paper that we can express Combinatory Reduction Systems derivations in terms of rewriting calculus derivations. The approach we present is based on a translation of each possible CRS-reduction into a corresponding ρ-reduction. Since for this purpose we need to make precise the matching used when evaluating CRS, the second contribution of the paper is to present an original matching algorithm for CRS terms that uses a simple term translation and the classical matching of lambda terms.     

On modularity in infinitary term rewriting

We study modular properties in strongly convergent infinitary term rewriting. In particular, we show that:

• •Confluence is not preserved across direct sum of a finite number of systems, even when these are non-collapsing.
• •Confluence modulo equality of hypercollapsing subterms is not preserved across direct sum of a finite number of systems.
• •Normalization is not preserved across direct sum of an infinite number of left-linear systems.
• •Unique normalization with respect to reduction is not preserved across direct sum of a finite number of left-linear systems.

Together, these facts constitute a radical departure from the situation in finitary term rewriting. Positive results are:

• •Confluence is preserved under the direct sum of an infinite number of left-linear systems iff at most one system contains a collapsing rule.
• •Confluence is preserved under the direct sum of a finite number of non-collapsing systems if only terms of finite rank are considered.
• •Top-termination is preserved under the direct sum of a finite number of left-linear systems.
• •Normalization is preserved under the direct sum of a finite number of left-linear systems.

All of the negative results above hold in the setting of weakly convergent rewriting as well, as do the positive results concerning modularity of top-termination and normalization for left-linear systems.     

Minimization strategies for maximally parallel multiset rewriting systems

Maximally parallel multiset rewriting systems (MPMRS) give a convenient way to express relations between unstructured objects. The functioning of various computational devices may be expressed in terms of MPMRS (e.g., register machines and many variants of P systems). In particular, this means that MPMRS are Turing universal; however, a direct translation leads to quite a large number of rules. Like for other classes of computationally complete devices, there is a challenge to find a universal system having the smallest number of rules. In this article we present different rule minimization strategies for MPMRS based on encodings and structural transformations. We apply these strategies to the translation of a small universal register machine (Korec (1996) [9]) and we show that there exists a universal MPMRS with 23 rules. Since MPMRS are identical to a restricted variant of P systems with antiport rules, the results we obtained improve previously known results on the number of rules for those systems.     

Sufficient-completeness,ground-reducibility and their complexity

Summary The sufficient-completeness property of equational algebraic specifications has been found useful in providing guidelines for designing abstract data type specifications as well as in proving inductive properties using the induction-less-induction method. The sufficient-completeness property is known to be undecidable in general. In an earlier paper, it was shown to be decidable for constructor-preserving, complete (canonical) term rewriting systems, even when there are relations among constructor symbols. In this paper, the complexity of the sufficient-completeness property is analyzed for different classes of term rewriting systems. A number of results about the complexity of the sufficient-completeness property for complete (canonical) term rewriting systems are proved: (i) The problem is co-NP-complete for term rewriting systems with free constructors (i.e., no relations among constructors are allowed), (ii) the problem remains co-NP-complete for term rewriting systems with unary and nullary constructors, even when there are relations among constructors, (iii) the problem is provably in almost exponential time for left-linear term rewriting systems with relations among constructors, and (iv) for left-linear complete constructor-preserving rewriting systems, the problem can be decided in steps exponential innlogn wheren is the size of the rewriting system. No better lower-bound for the complexity of the sufficient-completeness property for complete (canonical) term rewriting system with nonlinear left-hand sides is known. An algorithm for left-linear complete constructor-preserving rewriting systems is also discussed. Finally, the sufficient-completeness property is shown to be undecidable for non-linear complete term rewriting systems with associative functions. These complexity results also apply to the ground-reducibility property (also called inductive-reducibility) which is known to be directly related to the sufficient-completeness property.Some of the results in this paper were reported in a paper titled Complexity of Sufficient-Completeness presented at theSixth Conf. on Foundations of Software Technology and Theoretical Computer Science, New Delhi, India, Dec. 1986. The term quasi-reducibility is replaced in this paper by ground-reducibility as the latter seems to convey a lot more about the concept than the former.Partially supported by the National Science Foundation Grant nos. CCR-8408461 and CCR-8906678Partially supported by the National Science Foundation Grant nos. CCR-8408461 and CCR-9009414Partially supported by the National Science Foundation Grant no. DCR-8603184     

The undecidability of the unification and matching problem for canonical theories

Summary The problem whether there exists a unifying substitution for two terms is considered in the class of theories which can be embedded into canonical term rewriting systems. The problem is shown to be undecidable, even if we restrict the substitutions to matching ones. This implies that the class of admissible canonical theories is a proper subset of the class of canonical theories.     

On tree automata that certify termination of left-linear term rewriting systems

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.     

Rewriting systems with limited distance permitting context

By restricting the permitting context symbols in a rewriting system to be within a specified distance from the symbol to be replaced, we strictly increase the generative power above that of rewriting systems where the context symbols can appear within arbitrary distances from the symbol to be replaced.     

Narrowing-based simulation of term rewriting systems with extra variables and its Termination Proof

Term rewriting systems (TRSs) extended by allowing to contain extra variables in their rewrite rules are called EV-TRSs. They are ill-natured since every one-step reduction by their rules with extra variables is infinitely branching and they are not terminating. To solve these problems, this paper shows that narrowing can simulate reduction sequences of EV-TRSs as narrowing sequences starting from ground terms. We prove the soundness of ground narrowing sequences for the reduction sequences. We prove the completeness for the case of right-linear systems, and also for the case that any redex reduced in the reduction sequence is not introduced by means of extra variables. Moreover, we give a method to prove the termination of the simulation, extending the dependency pair method to prove termination of TRSs, into that of narrowing on EV-TRSs starting from ground terms. We show that the method is useful for right-linear or constructor systems.     

Simple restriction in context-free rewriting

Many rewriting systems with context-free productions and with controlled derivations have been studied. On one hand, these systems preserve the simplicity of applications of context-free productions and, on the other hand, they increase the generative power to cover more aspects of natural and programming languages. However, with λ-productions, many of these systems are computationally complete. It gives rise to a natural question of what are the simplest restrictions of the derivation process of context-free grammars to obtain the universal power. In this paper, we present such a simple restriction introducing so-called restricted context-free rewriting systems. These systems are context-free grammars with a function assigning a nonterminal coupled with + or − to each nonterminal. A production is applicable if it is applicable as a context-free production and if the symbol assigned to the left-hand side of the production is coupled with +, then this symbol has to appear in the sentential form, while if coupled with −, it must not appear in the sentential form. This restriction is simpler than most of the other restrictions, since the context conditions are assigned to nonterminals, not to productions, and their type is the simplest possible – a nonterminal.     

Conditional Term Graph Rewriting with Indirect Sharing

For reasons of efficiency, term rewriting is usually implemented by term graph rewriting. In term rewriting, expressions are represented as terms, whereas in term graph rewriting these are represented as directed graphs. Unlike terms, graphs allow a sharing of common subexpressions. In previous work, we have shown that conditional term graph rewriting is a sound and complete implementation for a certain class of CTRSs with strict equality, provided that a minimal structure sharing scheme is used. In this paper, we will show that this is also true for two different extensions of normal CTRSs. In contrast to the previous work, however, a non-minimal structure sharing scheme can be used. That is, the amount of sharing is increased.     

类广义Lorenz系统的广义同步

应用广义Lorenz标准型研究了包括广义Lorenz系统、双曲型广义Lorenz系统以及Liu-Liu-Liu-Liu系统在内的类广义Lorenz系统的广义同步化问题．利用映射将一大类三阶二次混沌系统变换为广义Lorenz标准型,设计控制器使变换后的系统达到完全同步,进而使变换前的系统实现广义同步．将该方法分别用于拓扑等价和不等价的两个系统,通过数值仿真,发现结果和理论分析相符,从而表明了该方法的有效性．     

Nonterminating Rewritings with Head Boundedness

We define here the concept of head boundedness,head normal form and head confluence of term rewriting systems that allow infinite derivation.Head confluence iw weaker than confluence,but sufficient to guarantee the correctness of lazy implementations of equational logic programming languages.Then we prove several results.First,if a left-linear system is locally confluent and head-bounded.then it is head-confluent.Second,head-confluent and head-bounded systems have the heau Church-Rosser property.Last,if an orthogonal system is head-terminating,then it is head-bounded.These results can be applied to generalize equational logic programming languages.