Re: [sage-devel] Rigor of matrix rank over ZZ

[William Stein]

On Wed, Jul 11, 2012 at 10:19 PM, Julien Puydt <julien...@laposte.net> wrote:
> Le 12/07/2012 04:45, Fredrik Johansson a écrit :
>
>> Matrix_integer_dense.rank first tries to establish that the matrix has
>> full rank modulo a random prime. If this fails, it calls Linbox. As
>> far as I can see, the rank() function in Linbox (in matrix-rank.h)
>> also just computes the rank modulo one random prime. Am I just looking
>> at the wrong functions, or is this actually not rigorous?
>
>
> As a first remark, I find it strange that sage first tries something before
> calling something else : it should probably just call the something else
> directly!
>
> Then the code in question is more precisely in
> linbox/algorithms/matrix-rank.h (looking at version 1.3.2) ; and indeed the
> top of the file says:
> /*! @file algorithms/matrix-rank.h
> * @ingroup algorithms
> * @ingroup rank
> * @brief Computes the rank of a matrix by Gaussian Elimination, in place.
> * @details NO DOC
> */
> which implies certain results ; but most of the functions in that file (it's
> C++ template code, hence is visible in full in the header) map to a random
> modular matrix (and are documented as doing such), before calling long
> rankIn(BlasMatrix<Field>& Ap) const which does the actual elimination ; for
> example :
> /*!compute the integer matrix A by modulo a random prime,
> Monto-Carlo.
> * This is the generic method (mapping to a random modular
> matrix).
> * @param A Any matrix
> * @return the rank of A.
> */
> template<class IMatrix>
> long rank(const IMatrix& A) const
> {
>
> Field F ((unsigned long)*rp);
>
> BlasMatrix<Field> Ap(F, A.rowdim(), A.coldim());
>
> MatrixHom::map(Ap, A, F);
>
> long result;
>
> result = rankIn(Ap);
>
> return result;
> }
>
> So it's pretty clear it's Monte Carlo (not Las Vegas) and hence can give
> wrong results.
>
> Probably the top of the file should make it much more explicit that there is
> no guarantee, and the sage method which calls that code should also document
> there is no guarantee.

If that is indeed the case, then what you suggest is definitely *NOT*
what is the standard convention in Sage. All algorithms by default
are supposed to be guaranteed (modulo bugs), and assume no unproved
conjectures. Any algorithm that doesn't have this property must be
called by giving a proof=False flag or using the proofs.[tab] object
(which sets proofs= defaults for different areas of mathematics).

In this case, if what you say is true, rank should be changed to be
provably correct, and the current implementation should remain
available via proof = False.

I don't know if what you guys claim is true though. I would like a
comment from a linbox developer.

-- William

>
> Snark on #sagemath
>
>
> --
> --
> To post to this group, send an email to sage-...@googlegroups.com
> To unsubscribe from this group, send an email to
> sage-devel+...@googlegroups.com
> For more options, visit this group at
> http://groups.google.com/group/sage-devel
> URL: http://www.sagemath.org



--
William Stein
Professor of Mathematics
University of Washington
http://wstein.org

[B Saunders]

> --
> You received this message because you are subscribed to the Google Groups "linbox-devel" group.
> To post to this group, send email to linbox...@googlegroups.com.
> To unsubscribe from this group, send email to linbox-devel...@googlegroups.com.
> For more options, visit this group at http://groups.google.com/group/linbox-devel?hl=en.
>

Yes, LinBox integer matrix rank is Monte Carlo. I would say it is
rigorously Monte Carlo in that we have a published proof bounding the
probability of a wrong rank (as a function of matrix dimension and
entry sizes). The probability of error is less than the probability
that a gamma ray changes a bit in the memory during the computation --
provided you run it two or three times (depends on your altitude).

Linbox does not now provide a proof=true algorithm, but could easily do so.
However I hate to see that as default since it will be at least a
factor of n (matrix dimension) slower.

I agree that our docs could be clearer about this and will take steps.

Cheers,
-dave

--
B. David Saunders, Prof. Invité, Laboratoire de l'Informatique du Parallélisme
ENS-Lyon, France, cell: 07 6283 3041 (replace initial 0 with 01133 if
calling from USA)
Prof., CIS Department, University of Delaware, Skype: bdsaunders,
saun...@udel.edu

[William Stein]

On Thu, Jul 12, 2012 at 7:52 AM, B Saunders <saun...@udel.edu> wrote:
> Yes, LinBox integer matrix rank is Monte Carlo. I would say it is
> rigorously Monte Carlo in that we have a published proof bounding the
> probability of a wrong rank (as a function of matrix dimension and
> entry sizes). The probability of error is less than the probability
> that a gamma ray changes a bit in the memory during the computation --
> provided you run it two or three times (depends on your altitude).

Thanks for the clarification, and many thanks for sending us an email!

> Linbox does not now provide a proof=true algorithm, but could easily do so.
> However I hate to see that as default since it will be at least a
> factor of n (matrix dimension) slower.

It will be the default in Sage, but I'm of course fine with it not
being the default
in Linbox.

> I agree that our docs could be clearer about this and will take steps.

Thanks!!

William

>
> Cheers,
> -dave
>
> --
> B. David Saunders, Prof. Invité, Laboratoire de l'Informatique du Parallélisme
> ENS-Lyon, France, cell: 07 6283 3041 (replace initial 0 with 01133 if
> calling from USA)
> Prof., CIS Department, University of Delaware, Skype: bdsaunders,
> saun...@udel.edu
>