Invariants and closures in the theory of rewrite systems

The article investigates some useful concepts of rewrite systems, especially invariants and closures. The concepts are formalised with so-called string expressions, for which an axiomatisation is given. The central operator in the theory of rewrite systems, the rewrite operator, is introduced with formulas that permit a calculational approach. The connections with distributed programming are also explained.     

Murg term rewrite systems

The union of a monadic and a right-ground term rewrite system is called a murg term rewrite system. We show that for murg TRSs the ground common ancestor problem is undecidable. We show that for a murg term rewrite system it is undecidable whether the set of descendants of a ground tree is a recognizable tree language. We show that it is undecidable whether a murg term rewrite system over Σ preserves Σ-recognizability.     

Termination of rewriting systems by polynomial interpretations and its implementation

This paper describes the actual implementation in the rewrite rule laboratory REVE of an elementary procedure that checks inequalities between polynomials and is used for proving termination of rewriting systems, especially in the more difficult case of associative-commutative rewriting systems, for which a complete characterization is given.     

A path ordering for proving termination of AC rewrite systems

We describe a method that extends the lexicographic recursive path ordering of Dershowitz and Kamin and Levy for proving termination of associative-commutative (AC) rewrite systems. Instead of comparing the arguments of an AC-operator using the multiset extension, wepartition them into disjoint subsets and use each subset only once for comparison. To preserve transitivity, we introduce two techniques —pseudocopying andelevating of arguments of an AC operator. This method imposesno restrictions at all on the underlying precedence relation on function symbols. It can therefore prove termination of a much more extensive class of AC rewrite systems than can previous methods, such as associative path ordering, that restrict AC operators to be minimal or subminimal in precedence. A number of examples illustrating the power of the approach are discussed. The method has been implemented inRRL, Rewrite Rule Laboratory, a theorem-proving environment based on rewrite techniques and completion.A preliminary version appears in Proc. of10th Conference on Foundations of Software Technology and Theoretical Computer Science, Bangalore, India (1990).Partially supported by the National Science Foundation Grant no. CCR-8906678.Partially supported by the National Science Foundation Grant no. CCR-9009755Partially supported by the National Science Foundation under Grants CCR-9202838 and CCR-9357851.     

Termination of narrowing revisited

This paper describes several classes of term rewriting systems (TRS’s), where narrowing has a finite search space and is still (strongly) complete as a mechanism for solving reachability goals. These classes do not assume confluence of the TRS. We also ascertain purely syntactic criteria that suffice to ensure the termination of narrowing, and include several subclasses of popular TRS’s such as right-linear TRS’s, almost orthogonal TRS’s, topmost TRS’s, and left-flat TRS’s. Our results improve and/or generalize previous criteria in the literature regarding narrowing termination.     

Model checking for process rewrite systems and a class of action-based regular properties

We consider the model checking problem for Process Rewrite Systems (PRS), an infinite-state formalism (non Turing-powerful) which subsumes many common models such as Pushdown Processes and Petri Nets. PRS can be adopted as a formal model for programs with dynamic creation and synchronization of concurrent processes, and with recursive procedures. The model-checking problem of PRS against action-based linear temporal logic (ALTL) is undecidable. However, decidability for some interesting fragment of ALTL remains an open question. In this paper, we state decidability results concerning generalized acceptance properties about infinite derivations (infinite term rewriting) in PRS. As a consequence, we obtain decidability of the model-checking problem (restricted to infinite runs) of PRS against a meaningful fragment of ALTL.     

分布式系统上异步算法的终止

本文论述了一种检测分布式系统上异步算法终止的有效方法．     

递归Prolog程序终止问题的探讨

本文用Ｐｒｏ图的方法讨论了递归Ｐｒｏｌｏｇ程序的终止问题。其中包括Ｐｒｏ图的概念和Ｐｒｏ图的状态序列及递归程序的终止问题。使用本文的方法可为调试程序提供足够的启示。     

阻容并联端接的研究与仿真

端接技术可以改善高速电路中的信号完整性问题。首先,介绍了多种端接技术的原理及其各自的优势与不足,然后重点研究了阻容并联端接的原理和应用,通过理论分析给出端接方案中器件的取值对电路的影响,并利用电路仿真工具进行验证,为今后进行高速电路端接设计提供了参考依据。     

Matrix Interpretations for Proving Termination of Term Rewriting

We present a new method for automatically proving termination of term rewriting. It is based on the well-known idea of interpretation of terms where every rewrite step causes a decrease, but instead of the usual natural numbers we use vectors of natural numbers, ordered by a particular nontotal well-founded ordering. Function symbols are interpreted by linear mappings represented by matrices. This method allows us to prove termination and relative termination. A modification of the latter, in which strict steps are only allowed at the top, turns out to be helpful in combination with the dependency pair transformation. By bounding the dimension and the matrix coefficients, the search problem becomes finite. Our implementation transforms it to a Boolean satisfiability problem (SAT), to be solved by a state-of-the-art SAT solver.     

两类量子游走组成的非确定型量子程序的终止验证

首先给出了C4空间中由量子游走组成的非确定型量子程序的概念,其次讨论了它们从初态运行时在不同的测量算子下的可达集合、终止集合和发散集合。研究表明:非确定型量子程序的终止、发散和可达集合、发散集合与选取的测量算子有密切的关系。程序在不同测量算子作用下从同一个初态运行时可能终止,也可能发散;并且,同一个初态的可达集合中终态和发散态共存。     

Proving termination of (conditional) rewrite systems

In this paper an important problem in the domain of term rewriting, the termination of (conditional) rewrite systems, is dealt with. We show that in many applications, well-founded orderings on terms which only make use of syntactic information of a rewrite systemR, do not suffice for proving termination ofR. Indeed sometimes semantic information is needed to orient a rewrite rule. Therefore we integrate a semantic interpretation of rewrite systems and terms into a well-founded ordering on terms: the notion ofsemantic ordering is the first main contribution of this paper. The use and usefulness of the semantic ordering in proving termination is illustrated by means of some realistic examples.Furthermore the concept of semantic information induces a novel approach for proving termination inconditional rewrite systems. The idea is to employ not only semantic information contained in the terms that are to be compared, but also extra (semantic) information contained in the premiss of the conditional equation in which the terms appear. This leads to our second contribution in the termination problem area: the notion ofcontextual ordering andcontextual semantic ordering. Thecontextual approach allows to prove termination of conditional rewrite systems where all classical partial orderings would fail.     

Termination of linear programs with nonlinear constraints

Tiwari (2004) proved that the termination problem of a class of linear programs (loops with linear loop conditions and updates) over the reals is decidable through Jordan forms and eigenvector computation. Braverman (2006) proved that it is also decidable over the integers. Following their work, we consider the termination problems of three more general classes of programs which are loops with linear updates and three kinds of polynomial loop conditions, i.e., strict constraints, non-strict constraints and both strict and non-strict constraints, respectively. First, we prove that the termination problems of such loops over the integers are all undecidable. Then, for each class we provide an algorithm to decide the termination of such programs over the reals. The algorithms are complete for those programs satisfying a property, Non-Zero Minimum.     

基于k阶秩函数的线性赋值循环程序的终止性分析

循环程序的终止性是确保循环程序完全正确的必要条件。 如果给定的线性赋值循环程序不存在传统定义的线性秩函数,那么基于传统定义的秩函数终止性证明方法将失效。基于Aⁿx的精确计算,对传统的秩函数概念进行了扩展,提出了k阶秩函数的概念。使用RegularChains软件包给出了合成k阶秩函数的具体方法。实验结果表明,相比于传统定义的线性秩函数,k阶秩函数的适应范围更广。对于 不能用传统定义的秩函数证明其终止性的部分循环程序,可以基于k阶秩函数来证明,从而体现了所提方法的优越性。     

State feedback stabilization of cascaded nonlinear systems with discontinuous connection

In practical engineering, many phenomena are described as a discontinuous function of a state variable, and the discontinuity is usually the main reason for the degradation of the control performance. For example, in the set-point control problem of mechanical systems, the static friction （described by a sgn function of velocity of the contacting faces） causes undesired positioning error. In this paper, we will investigate the stabilization problem for a class of nonlinear systems that consist of two subsystems with cascaded connection. We will show the basic idea with a special case first, and then the result will be extended to more general cases. Some interesting numerical examples will be given to demonstrate the effectiveness of the proposed design approach.     

State feedback stabilization of cascaded nonlinear systems with discontinuous connection

In practical engineering, many phenomena are described as a discontinuous function of a state variable,and the discontinuity is usually the main reason for the degradation of the control performance. For example, in the setpoint control problem of mechanical systems, the static friction (described by a sgn function of velocity of the contacting faces) causes undesired positioning error. In this paper, we will investigate the stabilization problem for a class of nonlinear systems that consist of two subsystems with cascaded connection.We will show the basic idea with a special case first, and then the result will be extended to more general cases. Some interesting numerical examples will be given to demonstrate the effectiveness of the proposed design approach.     

Distributed termination detection for dynamic systems

A symmetric algorithm for detecting the termination of a distributed computation is presented. The algorithm does not require global information concerning the system and does not assume any communication features, barring finite delays in the delivery of messages. It permits dynamic creation and destruction of processes participating in the computation, and also permits destruction of a process by external processes, such as the OS kernel. It also provides for external processes spontaneously joining an ongoing computation. Proofs of safety and liveness are provided.     

Order evaluation to new elementary operation approach for MIMO multidimensional systems

A new elementary operation approach (NEOA) for Roesser model realisation of multi-input and multi-output (MIMO) multidimensional (n-D) systems has been recently proposed, which can generate a lowest possible realisation but requires trying different processing manners for various possible realisations with different structures and orders. This paper develops two kinds of novel order evaluation methods and the corresponding algorithms for the realisation procedures A and B of the NEOA, respectively, such that the best processing manner for the lowest possible realisation can be determined with much less computational complexity. These new results enable us, for the first time, to know exactly the order of a realisation before actually conducting the realisation, and thus provide us a novel and high-efficiency way to explore the lowest possible realisation problem for MIMO n-D systems. Examples are given throughout this paper to illustrate the main idea as well as effectiveness of the proposed methods.     

Strong stable properties in distributed systems

Summary A stable property in a distributed system is a global property which once true, remains true forever. This paper refines this notion by formally introducing the concept ofstrong stable properties. A strong stable property has the nice property that it can be correctly evaluated on the consistent part of uncoordinated snapshots. Termination and deadlock are shown to be strong stable properties, whereas distributed garbage is not. We also show how to derive a simple generic algorithm for the detection of a strong stable property. The generic algorithm is illustrated by two examples: termination detection and deadlock detection. Incidentally the paper presents a very simple algorithm for termination detection. Andre Schiper has been a professor of Computer Science at EPFL (Federal Institute of Technology in Lausanne, Switzerland) since 1985, leading the Operating Systems laboratory. He graduated in Physics from the Federal Institute of technology in Zürich and received his Ph.D. in Computer Science from EPFL in 1980. In 1981–82 he spent one year at the University of Rennes, France. From 1983 to 1985, he was professor at the Engineering School in Yverdon, Switzerland. Between 1989 and 1991 André Schiper was head of the Department of Computer Science of EPFL, and during the academic year 1992–93 he was on sabbatical leave at Cornell University, Ithaca (NY). His research interests are in the areas of operating systems, distributed and fault-tolerant distributed systems, and parallelism. He is currently involved in the European Esprit project BROADCAST whose objective is the design and implementation of large scale distributed computing systems. Alain Sandoz graduated in Mathematics from the University of Neuchâtel, Switzerland, in 1984 and in Computer Science from the Federal Institute of Technology in Lausanne, Switzerland, in 1988. He received his Ph.D. in Computer Science from the Federal Institute of Technology in Lausanne in 1992. His dissertation was concerned with modelling causal relationships between transactions in distributed and replicated database systems. From 1992 to 1994 he was involved in research on fault-tolerant and large scale distributed computing systems. He is currently working on the development of information systems for the Swiss government.     

Synthesis of rewrite programs by higher-order and semantic unification

This paper presents a framework for synthesizing rewrite programs using higher-order and semantic unification. Many problems in computer science and artificial intelligence can be formalized as problems of higher-order unification. Among such problems is first-order anti-unification. In this paper, we show that first-order anti-unification can be regarded as a second-order matching problem and solved by the algorithm for higher-order unification.