int_ideal_cofactors : term list -> term -> term list

SYNOPSIS

Produces cofactors proving that one integer polynomial is in the ideal generated by others.

DESCRIPTION

The call int_ideal_cofactors [`p1`; ...; `pn`] `p`, where all the terms have type :int and can be considered as polynomials, will test whether p is in the ideal generated by the p1,...,pn. If so, it will return a corresponding list [`q1`; ...; `qn`] of `cofactors' such that the following is an algebraic identity provable by INT_RING or a slight elaboration of INT_POLY_CONV, for example)

  p = p1 * q1 + ... + pn * qn

hence providing an explicit certificate for the ideal membership. If ideal membership does not hold, int_ideal_cofactors fails. The test is performed using a Gr\"obner basis procedure.

FAILURE CONDITIONS

Fails if the terms are ill-typed, or if ideal membership fails. At present this is a generic version for fields, and in rare cases it may fail because cofactors are found involving non-trivial rational numbers even where there are integer cofactors. This imperfection should be fixed eventually, and is not usually a problem in practice.

EXAMPLE

In the case of a singleton list, ideal membership just amounts to polynomial divisibility, e.g.

  # prioritize_int();;
  val it : unit = ()

  # int_ideal_cofactors
     [`r * x * (&1 - x) - x`]
     `r * (r * x * (&1 - x)) * (&1 - r * x * (&1 - x)) - x`;;
  [`&1 * r pow 2 * x pow 2 +
    -- &1 * r pow 2 * x +
    -- &1 * r * x +
    &1 * r +
    &1`]

COMMENTS

When we say that terms can be `considered as polynomials', we mean that initial normalization, essentially in the style of INT_POLY_CONV, will be applied, but some complex constructs such as conditional expressions will be treated as atomic.