The F5 criterion revised

The purpose of this work is to generalize part of the theory behind Faugère’s “F5” algorithm. This is one of the fastest known algorithms to compute a Gröbner basis of a polynomial ideal I generated by polynomials f₁,…,f_m. A major reason for this is what Faugère called the algorithm’s “new” criterion, and we call “the F5 criterion”; it provides a sufficient condition for a set of polynomials G to be a Gröbner basis. However, the F5 algorithm is difficult to grasp, and there are unresolved questions regarding its termination.This paper introduces some new concepts that place the criterion in a more general setting: S-Gröbner bases and primitive S-irreducible polynomials. We use these to propose a new, simple algorithm based on a revised F5 criterion. The new concepts also enable us to remove various restrictions, such as proving termination without the requirement that f₁,…,f_m be a regular sequence.     

F5C: A variant of Faugère’s F5 algorithm with reduced Gröbner bases

The F5 algorithm for computing Gröbner bases achieves a high level of efficiency through the careful analysis of signatures assigned to each computed polynomial. However, it computes and uses many polynomials that turn out to be redundant. Eliminating these redundant polynomials is a non-trivial task, because they correspond to signatures required for reduction. This paper revisits the theory underlying F5 and describes F5C, a new variant that prunes redundant polynomials, then re-computes signatures to preserve correctness. This strategy successfully reduces both overhead and execution time.     

Universal characteristic decomposition of radical differential ideals

We call a differential ideal universally characterizable, if it is characterizable w.r.t. any ranking on partial derivatives. We propose a factorization-free algorithm that represents a radical differential ideal as a finite intersection of universally characterizable ideals. The algorithm also constructs a universal characteristic set for each universally characterizable component, i.e., a finite set of differential polynomials that contains a characterizing set of the ideal w.r.t. any ranking. As a part of the proposed algorithm, the following problem of satisfiability by a ranking is efficiently solved: given a finite set of differential polynomials with a derivative selected in each polynomial, determine whether there exists a ranking w.r.t. which the selected derivatives are leading derivatives and, if so, construct such a ranking.     

Generating priority rewrite systems for OSOS process languages

We propose an algorithm for generating a Priority Rewrite System (PRS) for an arbitrary process language in the OSOS format such that rewriting of process terms is sound for bisimulation and head normalising. The algorithm is inspired by a procedure which was developed by Aceto, Bloom and Vaandrager and presented in Turning SOS rules into equations [L. Aceto, B. Bloom, F.W. Vaandrager, Turning SOS rules into equations, Information and Computation 111 (1994) 1–52].For a subclass of OSOS process languages representing finite behaviours the PRSs that are generated by our algorithm are strongly normalising (terminating) and confluent, where termination is proved using the dependency pair and dependency graph techniques. Additionally, such PRSs are complete for bisimulation on closed process terms modulo associativity and commutativity of the choice operator of CCS. We illustrate the usefulness of our results, and the benefits of rewriting with priorities in general, with several examples.     

Complexity measures and hierarchies for the evaluation of integers and polynomials

The complexity of evaluating integers and polynomials is studied. A new model is proposed for studying such complexities. This model differs from previous models by requiring the construction of constant to be used in the computation. This construction is given a cost which is dependent upon the size of the constant. Previous models used a uniform cost, of either 0 or 1, for operations involving constants. Using this model, proper hierarchies are shown to exist for both integers and polynomials with respect to evaluation cost. Furthmore, it is shown that almost all integers (polynomials) are as difficult to evaluate as the hardest integer (polynomial). These results remain true even if the underlying basis of binary operations which the algorithm performs are varied.     

An alternative proof of Kharitonov's theorem

An alternative proof is presented of Kharitonov's theorem for real polynomials. The proof shows that if an unstable root exists in the interval family, then another unstable root must also show up in what is called the Kharitonov plane, which is delimited by the four Kharitonov polynomials. This fact is proved by using a simple lemma dealing with convex combinations of polynomials. Then a well-known result is utilized to prove that when the four Kharitonov polynomials are stable, the Kharitonov plane must also be stable, and this contradiction proves the theorem     

Necessary conditions for Hadamard factorizations of Hurwitz polynomials

A property of Hurwitz polynomials is related with the Hadamard product. Garloff and Wagner proved that Hadamard products of Hurwitz polynomials are Hurwitz polynomials, and Garloff and Shrinivasan shown that there are Hurwitz polynomials of degree 4 which do not have a Hadamard factorization into two Hurwitz polynomials of the same degree 4. In this paper, we give necessary conditions for an even-degree Hurwitz polynomial to have a Hadamard factorization into two even-degree Hurwitz polynomials; such conditions are given in terms of the coefficients of the given polynomial alone. Furthermore, we show that if an odd-degree Hurwitz polynomial has a Hadamard factorization then a system of nonlinear inequalities has at least one solution.     

A stochastic estimation algorithm with observation averaging

An algorithm for the constrained problem of estimating the regression coefficients is presented. The algorithm is based on the idea of direct averaging of the observations in order to estimate the search direction. It is shown that if the true parameter belongs to the permitted set, then the algorithm delivers asymptotically optimal estimates of the parameter. Finite convergence of the method is proved when the true parameter lies outside the permitted set     

Gröbner fan and universal characteristic sets of prime differential ideals

The concepts of Gröbner cone, Gröbner fan, and universal Gröbner basis are generalized to the case of characteristic sets of prime differential ideals. It is shown that for each cone there exists a set of polynomials which is characteristic for every ranking from this cone; this set is called a strong characteristic set, and an algorithm for its construction is given. Next, it is shown that the set of all differential Gröbner cones is finite for any differential ideal. A subset of the ideal is called its universal characteristic set, if it contains a characteristic set of the ideal w.r.t. any ranking. It is shown that every prime differential ideal has a finite universal characteristic set, and an algorithm for its construction is given. The question of minimality of this set is addressed in an example. The example also suggests that construction of a universal characteristic set can help in solving a system of nonlinear PDE’s, as well as maybe providing a means for more efficient parallel computation of characteristic sets.     

Formalisation of the computation of the echelon form of a matrix in Isabelle/HOL

In this contribution we present a formalised algorithm in the Isabelle/HOL proof assistant to compute echelon forms, and, as a consequence, characteristic polynomials of matrices. We have proved its correctness over Bézout domains, but its executability is only guaranteed over Euclidean domains, such as the integer ring and the univariate polynomials over a field. This is possible since the algorithm has been parameterised by a (possibly non-computable) operation that returns the Bézout coefficients of a pair of elements of a ring. The echelon form is also used to compute determinants and inverses of matrices. As a by-product, some algebraic structures have been implemented (principal ideal domains, Bézout domains, etc.). In order to improve performance, the algorithm has been refined to immutable arrays inside of Isabelle and code can be generated to functional languages as well.     

张量积de Casteljau算法的效率分析

在几何造型中，张量积Bernstein多项式具有非常重要的地位。在几何系统中主要应用de Casteljau算法逐个方向地计算张量积Bernstein多项式上的点，例如首先计算u-方向、然后是v-方向、w-方向等。分析了张量积形式的de Casteljau算法的效率，证明了对于不同的参数方向的计算顺序会导致不同的计算效率，并且当按照参数方向的次数递增的顺序应用de Casteljau算法时，计算量是最小的，除了理论分析之外，我们还给出了实验结果，并且实验结果与理论分析是一致的。     

Algebraic characterization of arbitrary pole assignability by static output feedback”“

Based on the explicit algebraic dependences p — g(F) between the vector p of the closed-loop characteristic-polynomial coefficients and the static output feedback matrix F, the well-known problem of arbitrary pole assignability by static output feedback is considered: local pole assignability is possible if and only if the differential g_* has full rank. Taking advantage of the known analytical dependences of g_*FF on F, new sufficient criteria for global pole assignability are derived. An explicit formula to compute the algebraic submanifold of feedback matrices F for which g_*F does not have full rank is also obtained. If the property of local pole assignability holds, then there exists a smooth submanifold of matrices F each point of which ensures the desired pole assignment. An algorithm by which this smooth submanifold can be computed is outlined. Illustrative examples are discussed in some detail.     

Increasing interpretations

The article at hand introduces a refinement of interpretation-based termination criteria for term rewrite systems in the dependency pair setting. Traditional methods share the property that—in order to be successful—all rewrite rules must (weakly) decrease with respect to some measure. One novelty of our approach is that we allow some rules to increase the interpreted value. These rules are found by simultaneously searching for adequate polynomial interpretations while considering the information of the dependency graph. We prove that our method extends the termination proving power of linear interpretations. Furthermore, this generalization perfectly fits the dependency pair framework which is implemented in virtually every termination prover dealing with term rewrite systems. We present two dependency pair processors for increasing interpretations. The novelty of the second one is that it can be used to eliminate single edges from the dependency graph.     

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.     

Ring models for delay-differential systems

This paper studies the algebraic structure of linear systems defined over R[λ], the ring of polynomials in λ with real coefficients. Natural definitions of controllability and observability are introduced and properties of R[λ]-transfer matrix realizations are discussed. It is shown that (A_n×n,D_n×m) is a controllable R[λ]-matrix pair if and only if for each set of polynomialsβ₁,β₂,…,β_n, in R[λ] there exists an R[λ] feedback matrixF such that detsI?A?BF]=∏i=1n(s+β_i). By regarding λ as a suitably defined delay operator, it is explained how this result might be applied to delay-differential systems in order to control dynamic response.     

F[x]-lattice basis reduction algorithm and multisequence synthesis

By means of F[x]-lattice basis reduction algorithm, a new algorithm is presented for synthesizing minimum length linear feedback shift registers (or minimal polynomials) for the given mul-tiple sequences over a field F. Its computational complexity is O(N2) operations in F where N is the length of each sequence. A necessary and sufficient condition for the uniqueness of minimal polynomi-als is given. The set and exact number of all minimal polynomials are also described when F is a finite field.     

The symmetric all-furthest- neighbor problem

Given a set of n points on the plane, a symmetric furthest-neighbor (SFN) pair of points p, q is one such that both p and q are furthest from each other among the points in . A pair of points is antipodal if it admits parallel lines of support. In this paper it is shown that a SFN pair of is both a set of extreme points of and an antipodal pair of . It is also shown that an asymmetric furthest-neighbor (ASFN) pair is not necessarily antipodal. Furthermore, if is such that no two distances are equal, it is shown that as many as, and no more than, n/2 pairs of points are SFN pairs. A polygon is unimodal if for each vertex p_k, k = 1,…,n the distance function defined by the euclidean distance between p_k and the remaining vertices (traversed in order) contains only one local maximum. The fastest existing algorithms for computing all the ASFN or SFN pairs of either a set of points, a simple polygon, or a convex polygon, require 0(n log n) running time. It is shown that the above results lead to an 0(n) algorithm for computing all the SFN pairs of vertices of a unimodal polygon.     

A DESCRIPTION OF A SET OF HYPOTHESES FOR SYSTEM IDENTIFICATION PROBLEM*

This paper concerns the system identification process which is a specific form of the hypothetico-deductive process. More specifically, this paper deals with the inductive inference, i.e., with the process of generating a set of hypotheses σ(E) that explain a given finite set of input-output experiments performed on a finite sequential system being identified. It is shown that Sεσ(E) if and only if there exists a homomorphism of a basic hypothesis explaining E, into S. Next, a set of hypotheses σ¹(E). defined as follows: Sεσ¹(E) if E is structure-complete w.r.t. S, is considered. Then it is proved that Sεσ¹(E) if and only if there exists a full homomorphism of a basic hypothesis onto S. Some important methodological consequences of obtained results are derived. Finally, relationship linking the properties of a system identification algorithm is investigated.     

Fast parallel polynomial division via reduction to triangular toeplitz matrix inversion and to polynomial inversion modulo a power

It is known that division with a remainder of two polynomials of degree at most s can be performed over an arbitrary field F of constants using uniform arithmetic and Boolean circuits of depth O(log s log log s) and polynomial size. A new algorithm is presented that yields those bounds via reduction to triangular Toeplitz matrix inversion and to polynomial inversion modulo a power. (If|F| > (s?1)² or if P-uniform computation is allowed, then the depth can be reduced to O(log s).) This approach is new and makes the result conceptually simpler.