General Linear Lexicographical Lead Rewriting Systems

We used ll_red_nf_redsb/ll_red_nf_noredsb functions on rewriting systems, where the tails of the polynomials was constant and the leading term linear. They can be used in a more general setting (which allows to eliminate auxiliary variable).

Definition 2   Let $ L$ be a list of Boolean polynomials. If all elements $ p$ of $ L$ have pairwise different leading terms with respect to lexicographical ordering, then we call $ L$ a linear lexicographical lead rewriting system.

We know that such a system forms together with the complete set of field equations a Gröbner basis w.r.t. lexicographical ordering.

In particular we can use ll_red_nf_redsb to speedup substitution of a variable $ x$ by a value $ v$ also in the more general case, that the lexicographical leading term of $ x+v$ is equal to $ x$ . This can be tested most efficiently by the expression

x.set().navigation().value()>v.set().navigation().value().

In many cases, we have a bigger equation system, where many variables have a linear leading term w.r.t. lexicographical ordering (at least one can optimize the formulation of the equations to fulfill these condition). These systems can be handled by the function eliminate in the module polybori.ll. I returns three results:

  1. A maximal subset $ L$ of the equation system, which forms a linear lexicographical lexicographical rewriting system.
  2. A normal form algorithm $ f$ , s.th. $ f(p)$ forms a reduced normal form of $ p$ against the Gröbner basis consisting of $ L$ and the field equations.
  3. A list of polynomials $ R$ , which are in reduced normal form against $ L$ , s.th. $ L\cup R$ spans modulo field equations the same ideal as the original equation system.

In [1]: from polybori.ll import eliminate

In [2]: E=[x(1)+1,x(1)+x(2),x(2)+x(3)*x(4)]

In [3]: (L,f,R)=eliminate(E)

In [4]: L
Out[4]: [x(1) + 1, x(2) + x(3)*x(4)]

In [5]: R
Out[5]: [x(3)*x(4) + 1]

In [6]: f(x(1)+x(2))
Out[6]: x(3)*x(4) + 1

2011-02-25