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.     

Paramodulation and Knuth–Bendix Completion with Nontotal and Nonmonotonic Orderings

Up to now, all existing completeness results for ordered paramodulation and Knuth–Bendix completion have required term ordering to be well founded, monotonic, and total(izable) on ground terms. For several applications, these requirements are too strong, and hence weakening them has been a well-known research challenge.Here we introduce a new completeness proof technique for ordered paramodulation where the only properties required on are well-foundedness and the subterm property. The technique is a relatively simple and elegant application of some fundamental results on the termination and confluence of ground term rewrite systems (TRS).By a careful further analysis of our technique, we obtain the first Knuth–Bendix completion procedure that finds a convergent TRS for a given set of equations E and a (possibly non-totalizable) reduction ordering whenever it exists. Note that being a reduction ordering is the minimal possible requirement on , since a TRS terminates if, and only if, it is contained in a reduction ordering.     

Infinitary Combinatory Reduction Systems

We define infinitary Combinatory Reduction Systems (iCRSs), thus providing the first notion of infinitary higher-order rewriting. The systems defined are sufficiently general that ordinary infinitary term rewriting and infinitary λ-calculus are special cases.Furthermore, we generalise a number of known results from first-order infinitary rewriting and infinitary λ-calculus to iCRSs. In particular, for fully-extended, left-linear iCRSs we prove the well-known compression property, and for orthogonal iCRSs we prove that (1) if a set of redexes U has a complete development, then all complete developments of U end in the same term and that (2) any tiling diagram involving strongly convergent reductions S and T can be completed iff at least one of S/T and T/S is strongly convergent.We also prove an ancillary result of independent interest: a set of redexes in an orthogonal iCRS has a complete development iff the set has the so-called finite jumps property.     

依赖项重写系统及其在程序设计语言中的应用

面重写系统是一种简洁通用的计算模型,在许多领域中有着重要的应用。     

Formalizing and Analyzing the Needham-Schroeder Symmetric-Key Protocol by Rewriting

This paper reports on work in progress on using rewriting techniques for the specification and the verification of communication protocols. As in Genet and Klay's approach to formalizing protocols, a rewrite system describes the steps of the protocol and an intruder's ability of decomposing and decrypting messages, and a tree automaton encodes the initial set of communication requests and an intruder's initial knowledge. In a previous work we have defined a rewriting strategy that, given a term t that represents a property of the protocol to be proved, suitably expands and reduces t using the rules in and the transitions in to derive whether or not t is recognized by an intruder. In this paper we present a formalization of the Needham-Schroeder symmetric-key protocol and use the rewriting strategy for deriving two well-known authentication attacks.     

Regular Sets of Descendants by Leftmost Strategy

For a constructor-based rewrite system R, a regular set of ground terms E, and assuming some additional restrictions, we build a finite tree automaton that recognizes the descendants of E, i.e. the terms issued from E by rewriting, according to leftmost strategy.     

General Algorithms for Permutations in Equational Inference

Mechanized systems for equational inference often produce many terms that are permutations of one another. We propose to gain efficiency by dealing with such sets of terms in a uniform manner, by the use of efficient general algorithms on permutation groups. We show how permutation groups arise naturally in equational inference problems, and study some of their properties. We also study some general algorithms for processing permutations and permutation groups, and consider their application to equational reasoning and term-rewriting systems. Finally, we show how these techniques can be incorproated into resolution theorem-proving strategies.     

Mechanizing and Improving Dependency Pairs

The dependency pair technique is a powerful method for automated termination and innermost termination proofs of term rewrite systems (TRSs). For any TRS, it generates inequality constraints that have to be satisfied by well-founded orders. We improve the dependency pair technique by considerably reducing the number of constraints produced for (innermost) termination proofs. Moreover, we extend transformation techniques to manipulate dependency pairs that simplify (innermost) termination proofs significantly. To fully mechanize the approach, we show how transformations and the search for suitable orders can be mechanized efficiently. We implemented our results in the automated termination prover AProVE and evaluated them on large collections of examples. Supported by the Deutsche Forschungsgemeinschaft DFG, grant GI 274/5-1.     

高效率重写型程序的设计

本文考虑如何设计高效率(即重写步数较少的)重写型程序。文中以计算Fibonacci数列的程序为例．比较具有相同功能的重写型程序,展示编写高效率重写型程序的可能性。介绍利用动态项重写计算编写高效率重写型程序的直观、简洁的方法。其中．动态项重写计算是项重写系统的元计算模型,其计算同样基于项重写。     

Completion for Multiple Reduction Orderings

We present a completion procedure (called MKB) that works for multiple reduction orderings. Given equations and a set of reduction orderings, the procedure simulates a computation performed by the parallel processes each of which executes the standard completion procedure (KB) with one of the given orderings. To gain efficiency, however, we develop new inference rules working on objects called nodes, which are data structures consisting of a pair s : t of terms associated with the information to show which processes contain the rule s t (or t s) and which processes contain the equation s t. The idea is based on the observation that some inferences made in different processes are often closely related, so we can design inference rules that simulate these inferences all in a single operation. Our experiments show that MKB is significantly more efficient than the naive simulation of parallel execution of KB procedures, when the number of reduction orderings is large enough. We also present an extension of this technique to the unfailing completion for multiple reduction orderings, which is useful in various areas of automated reasoning, including equational theorem proving.     

Abstract Congruence Closure

We describe the concept of an abstract congruence closure and provide equational inference rules for its construction. The length of any maximal derivation using these inference rules for constructing an abstract congruence closure is at most quadratic in the input size. The framework is used to describe the logical aspects of some well-known algorithms for congruence closure. It is also used to obtain an efficient implementation of congruence closure. We present experimental results that illustrate the relative differences in performance of the different algorithms. The notion is extended to handle associative and commutative function symbols, thus providing the concept of an associative-commutative congruence closure. Congruence closure (modulo associativity and commutativity) can be used to construct ground convergent rewrite systems corresponding to a set of ground equations (containing AC symbols). This revised version was published online in August 2006 with corrections to the Cover Date.     

Translation of Algebraic Programs into Executable Codes

An approach to the problem of translation of algebraic programs into executable codes is presented. In particular, an algorithm for translation of algebraic programs represented in the language Aplan into C codes is proposed. An algorithm of reconstruction of types in Aplan is considered that also checks the absence of features used for dynamic specification of procedures in a code. __________ Translated from Kibernetika i Sistemnyi Analiz, No. 5, pp. 168–176, September–October 2005.     

A Rewriting Machine and Optimization of Strategies of Term Rewriting

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.     

On confluence and residuals in Cauchy convergent transfinite rewriting

We show that non-collapsing orthogonal term rewriting systems do not have the transfinite Church-Rosser property in the setting of Cauchy convergence. In addition, we show that for (a transfinite version of) the Parallel Moves Lemma to hold, any definition of residual for Cauchy convergent rewriting must either part with a number of fundamental properties enjoyed by rewriting systems in the finitary and strongly convergent settings, or fail to hold for very simple rewriting systems.