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.     

Equivariant Unification

Nominal logic is a variant of first-order logic with special facilities for reasoning about names and binding based on the underlying concepts of swapping and freshness. It serves as the basis of logic programming, term rewriting, and automated theorem proving techniques that support reasoning about languages with name-binding. These applications often require nominal unification, or equational reasoning and constraint solving in nominal logic. Urban, Pitts and Gabbay developed an algorithm for a broadly applicable class of nominal unification problems. However, because of nominal logic’s equivariance property, these applications also require a different form of unification, which we call equivariant unification. In this article, we first study the complexity of the decision problem for equivariant unification and equivariant matching. We show that these problems are NP-hard in general, as is nominal unification without the ground-name restrictions employed in previous work on nominal unification. Moreover, we present an exponential-time algorithm for equivariant unification that can be used to decide satisfiability, or produce a complete finite set of solutions. We also study special cases that can be solved efficiently. In particular, we present a polynomial time algorithm for swapping-free equivariant matching, that is, for matching problems in which the swapping operation does not appear.     

Finite‐time H ∞ control for discrete‐time switched nonlinear systems with time delay

In this paper, the problem of finite‐time H _∞ control is addressed for a class of discrete‐time switched nonlinear systems with time delay. The concept of H _∞ finite‐time boundedness is first introduced for discrete‐time switched delay systems. Next, a set of switching signals are designed by using the average dwell time approach, under which some delay‐dependent sufficient conditions are derived to guarantee the H _∞ finite‐time boundedness of the closed‐loop system. Then, a finite‐time H _∞ state feedback controller is also designed by solving such conditions. Furthermore, the problem of uniform finite‐time H _∞ stabilization is also resolved. All the conditions are cast into linear matrix inequalities, which can be easily checked by using recently developed algorithms for solving linear matrix inequalities. A numerical example and a water‐quality control system are provided to demonstrate the effectiveness of the main results. Copyright © 2013 John Wiley & Sons, Ltd.     

Piece wise linear least–squares approximation of planar curves

Two algorithms for solving the piecewise linear least–squares approximation problem of plane curves are presented. The first is for the case when the L ₂ residual (error) norm in any segment is not to exceed a pre–assigned value. The second algorithm is for the case when the number of segments is given and a (balanced) L ₂ residual norm solution is required. The given curve is first digitized and either algorithm is then applied to the discrete points. For each segment, we obtain the upper triangular matrix R in the QR factorization of the (augmented) coefficient matrix of the resulting system of linear equations. The least–squares solutions are calculated in terms of the R (and Q) matrices. The algorithms then work in an iterative manner by updating the least–squares solutions for the segments via up dating the R matrices. The calculation requires as little computational effort as possible. Numerical results and comments are given. This, in a way, is a tutorial paper.     

Efficient parallel term matching and anti-unification

In this paper we present optimal processor x time parallel algorithms for term matching and anti-unification of terms represented as trees. Term matching is the special case of unification in which one of the terms is restricted to contain no variables. It has wide applicability to logic programming, term rewriting systems and symbolic pattern matching. Anti-unification is the dual problem of unification in which one computes the most specific generalization of two terms. It has application to inductive inference and theorem proving. Our algorithms run in O(log² N) time using N/log² N processors on a shared-memory model of computation that prohibits simultaneous reads or writes (EREW PRAM). These algorithms are the first polylogarithmic-time EREW algorithms with a processor x time product of the same order as that of their sequential counterparts, thereby permitting optimal speed-ups using any number of processors up to N/log² N. We also use the techniques developed in the paper to provide an N/log N-processor, O(log N)-time algorithm for a shared-memory model that allows both simultaneous reads and simultaneous writes (CRCW PRAM).Supported by NSF Grant IRI-88-09324 and NSF/DARPA Grant CCR-8908092.     

Constraint Solving for Term Orderings Compatible with Abelian Semigroups, Monoids and Groups

It is crucial for the performance of ordered resolution or paramodulation-based deduction systems that they incorporate specialized techniques to work efficiently with standard algebraic theories E. Essential ingredients for this purpose are term orderings that are E-compatible, for the given E, and algorithms deciding constraint satisfiability for such orderings.Here we introduce a uniform technique providing the first such algorithms for some orderings for abelian semigroups, abelian monoids and abelian groups, which we believe will lead to reasonably efficient techniques for practice.Our algorithms are in NP, and hence optimal, since in addition we show that, for any well-founded E-compatible ordering for these E, the constraint satisfiability problem is NP-hard even for conjunctions of inequations.     

Linear Time Algorithms for Generalized Edge Dominating Set Problems

We prove that a generalization of the edge dominating set problem, in which each edge e needs to be covered b _e times for all e∈E, admits a linear time 2-approximation for general unweighted graphs and that it can be solved optimally for weighted trees. We show how to solve it optimally in linear time for unweighted trees and for weighted trees in which b _e ∈{0,1} for all e∈E. Moreover, we show that it solves generalizations of weighted matching, vertex cover, and edge cover in trees.     

An Experimental Study of Algorithms for Weighted Completion Time Scheduling

We consider the total weighted completion time scheduling problem for parallel identical machines and precedence constraints, P| prec|\sum w _i C _i . This important and broad class of problems is known to be NP-hard, even for restricted special cases, and the best known approximation algorithms have worst-case performance that is far from optimal. However, little is known about the experimental behavior of algorithms for the general problem. This paper represents the first attempt to describe and evaluate comprehensively a range of weighted completion time scheduling algorithms. We first describe a family of combinatorial scheduling algorithms that optimally solve the single-machine problem, and show that they can be used to achieve good performance for the multiple-machine problem. These algorithms are efficient and find schedules that are on average within 1.5\percent of optimal over a large synthetic benchmark consisting of trees, chains, and instances with no precedence constraints. We then present several ways to create feasible schedules from nonintegral solutions to a new linear programming relaxation for the multiple-machine problem. The best of these linear programming-based approaches finds schedules that are within 0.2\percent of optimal over our benchmark. Finally, we describe how the scheduling phase in profile-based program compilation can be expressed as a weighted completion time scheduling problem and apply our algorithms to a set of instances extracted from the SPECint95 compiler benchmark. For these instances with arbitrary precedence constraints, the best linear programming-based approach finds optimal solutions in 78\percent of cases. Our results demonstrate that careful experimentation can help lead the way to high quality algorithms, even for difficult optimization problems. Received October 30, 1998; revised March 28, 2001.     

New results on robust H ∞ filtering design for discrete-time piecewise linear delay systems

This paper revisits the problem of robust H _∞ filtering design for a class of discrete-time piecewise linear state-delayed systems. The state delay is assumed to be time-varying and of an interval-like type, which means that both the lower and upper bounds of the time-varying delay are available. The parameter uncertainties are assumed to have a structured linear fractional form. Based on a novel delay-dependent piecewise Lyapunov–Krasovskii functional combined with Finsler's Lemma, a new delay-dependent sufficient condition for robust H _∞ performance analysis is first derived and then the filter synthesis is developed. It is shown that by using a new linearisation technique, a unified framework can be developed so that both the full-order and reduced-order filters can be obtained by solving a set of linear matrix inequalities (LMIs), which are numerically efficient with commercially available software. Finally, a numerical example is provided to illustrate the effectiveness and less conservatism of the proposed approach.     

Algorithms for unconstrained L1 simple linear regression

Many algorithms have been proposed for L₁ simple linear regression computations, and several codes implementing these algorithms are now available. Some of these algorithms are based on a linear programming formulation while others propose a descent approach.We report on a computational study comparing L₁ computer programs for solving the simple linear regression problem.     

Algorithms and reductions for rewriting problems. II

In this paper we give polynomial-time reductions between a version of joinability for rewrite systems and the word problem for rewrite systems. We prove log-space hardness or completeness for P for several problems of ground rewrite systems. We show that matching (and unification) modulo ground equations is NP-hard even when variables are restricted to at most two occurrences in the pattern and the subject is just a constant. Finally, we give the first polynomial-time algorithms for matching modulo ground equations with linear pattern and for joinability problem with ground rewrite systems. The joinability result leads to polynomial time algorithms for: local confluence of ground rewrite systems, confluence of terminating ground rewrite systems, and completeness of ground rewrite systems. The results for matching modulo ground equations are optimal with respect to occurrences of variables.     

Complexity of unification problems with associative-commutative operators

The unification problem for terms containing associative and commutative functions is of importance in theorem provers based on term rewriting and resolution methods as well as in logic programming. The complexity of determining whether two such terms are unifiable was known to be NP-hard. It is proved that the problem is NP-complete by describing a nondeterministic polynomial time algorithm for it. The case where the terms are linear and have no common variables is shown to be in P. The NP-completeness of other similar unification problems, in particular, when a function symbol is also idempotent and/or has a unit (identity), is also discussed. Finally, a table of the complexity of E-matching and E-unification problems is given.Partially supported by the National Science Foundation grant nos. DCR-8408461 and CCR-8906678. A preliminary version of this paper appeared earlier as a technical report of General Electric Corporate Research and Development, Dec. 1986.     

E-unification with Constants vs. General E-unification

We present a solution to Problem #66 from the RTA open problem list. The question is whether there exists an equational theory E such that E-unification with constants is decidable but general E-unification is undecidable. The answer is positive and we show such a theory. The problem has several equivalent formulations, therefore the solution has many consequences. Our result also shows, that there exist two theories E ₁ and E ₂ over disjoint signatures, such that E ₁-unification with constants and E ₂-unification with constants are decidable, but (E ₁ ∪ E ₂)-unification with constants is undecidable.     

Robust <Emphasis Type="Italic">H</Emphasis><Subscript>∞</Subscript> static output feedback control of discrete-time switched polytopic linear systems with average dwell-time

This paper investigates the problem of robust exponential H _∞ static output feedback controller design for a class of discrete-time switched linear systems with polytopic-type time-varying parametric uncertainties. The objective is to design a switched static output feedback controller guaranteeing the exponential stability of the resulting closed-loop system with a minimized exponential H _∞ performance under average dwell-time switching scheme. Based on a parameter-dependent discontinuous switched Lyapunov function combined with Finsler’s lemma and Dualization lemma, some novel conditions for exponential H _∞ performance analysis are first proposed and in turn the static output feedback controller designs are developed. It is shown that the controller gains can be obtained by solving a set of linear matrix inequalities (LMIs), which are numerically efficient with commercially available software. Finally, a simulation example is provided to illustrate the effectiveness of the proposed approaches.     

Permutative rewriting and unification

Permutative rewriting provides a way of analyzing deduction modulo a theory defined by leaf-permutative equations. Our analysis naturally leads to the definition of the class of unify-stable axiom sets, in order to enforce a simple reduction strategy. We then give a uniform unification algorithm modulo theories E axiomatized this way. We prove that it computes complete sets of unifiers of simply exponential cardinality, and that the E-unification decision problem belongs to NP.     

A non-recursive method for solving the general discrete-time riccati equations related to the H∞ control problem

In this paper we propose a nonrecursive method for solving the general discrete-time algebraic Riccati equation related to the H_∞ control problem (H_∞-DARE). We have achieved this by casting the problem of solving a given H_∞-DARE to the problem of solving an auxiliary continuous-time algebraic Riccati equation associated with the H_∞ control problem (H_∞-CARE) for which the well known nonrecursive methods of solving are available. The advantages of our approach are: it reduces the computation involved in the recursive algorithms while giving much more accurate solutions, and it readily provides the properties of the general H_∞-DARE.     

Large‐Scale Integer Linear Programming for Orientation Preserving 3D Shape Matching

We study an algorithmic framework for computing an elastic orientation‐preserving matching of non‐rigid 3D shapes. We outline an Integer Linear Programming formulation whose relaxed version can be minimized globally in polynomial time. Because of the high number of optimization variables, the key algorithmic challenge lies in efficiently solving the linear program. We present a performance analysis of several Linear Programming algorithms on our problem. Furthermore, we introduce a multiresolution strategy which allows the matching of higher resolution models.     

Single Versus Simultaneous Equational Unification and Equational Unification for Variable-Permuting Theories

A clear distinction is made between the (elementary) unification problem where there is only one pair of terms to be unified, and the simultaneous unification problem, where many such pairs have to be unified simultaneously – it is shown that there exists a finite, depth-reducing, linear, and confluent term-rewriting system R such that the (single) equational unification problem mod R is decidable, while the simultaneous equational unification problem mod R is undecidable. Also a finite set E of variable-permuting equations is constructed such that equational unification is undecidable mod E, thus settling an open problem. The equational matching problem for variable-permuting theories is shown to be PSPACE-complete.     

Canonization for disjoint unions of theories

If there exist efficient procedures (canonizers) for reducing terms of two first-order theories to canonical form, can one use them to construct such a procedure for terms of the disjoint union of the two theories? We prove this is possible whenever the original theories are convex. As an application, we prove that algorithms for solving equations in the two theories (solvers) can not be combined in a similar fashion. These results are relevant to the widely used Shostak’s method for combining decision procedures for theories. They provide the first rigorous answers to the questions about the possibility of directly combining canonizers and solvers.     

Finding Maximum Induced Matchings in Subclasses of Claw-Free and <Emphasis Type="Italic">P</Emphasis><Subscript>5</Subscript>-Free Graphs,and in Graphs with Matching and Induced Matching of Equal Maximum Size

In a graph G a matching is a set of edges in which no two edges have a common endpoint. An induced matching is a matching in which no two edges are linked by an edge of G. The maximum induced matching (abbreviated MIM) problem is to find the maximum size of an induced matching for a given graph G. This problem is known to be NP-hard even on bipartite graphs or on planar graphs. We present a polynomial time algorithm which given a graph G either finds a maximum induced matching in G, or claims that the size of a maximum induced matching in G is strictly less than the size of a maximum matching in G. We show that the MIM problem is NP-hard on line-graphs, claw-free graphs, chair-free graphs, Hamiltonian graphs and r-regular graphs for r \geq 5. On the other hand, we present polynomial time algorithms for the MIM problem on (P ₅,D _m )-free graphs, on (bull, chair)-free graphs and on line-graphs of Hamiltonian graphs.