38
$\begingroup$

We know that $\mathbf A$ is symmetric and positive-definite. We know that $\mathbf B$ is orthogonal:

Question: is $\mathbf B \cdot\mathbf A \cdot\mathbf B^\top$ symmetric and positive-definite? Answer: Yes.

Question: Could a computer have told us this? Answer: Probably.

Are there any symbolic algebra systems (like Mathematica) that handle and propagate known facts about matrices?

Edit: To be clear I'm asking this question about abstractly defined matrices. I.e. I don't have explicit entries for $A$ and $B$, I just know that they are both matrices and have particular attribues like symetric, positive definite, etc....

Improve this question
$\endgroup$
7
  • 5
    $\begingroup$ What I'm missing is software that treats matrices symbolically (i.e., not as arrays). I'd want to be able to talk about some symmetric matrix $\mathbf C$ without having to fret about its entries. $\endgroup$
    – J. M.
    Nov 30, 2011 at 14:44
  • 6
    $\begingroup$ There are a few projects working on this. I happen to be familiar with the implementation in SymPy. It's buggy but slowly being built up. $\endgroup$
    – MRocklin
    Nov 30, 2011 at 14:47
  • 4
    $\begingroup$ This sounds like automated theorem proving. The trick then is to include a sufficient set of axioms in your engine so that it can then be deduced efficiently by automated reasoning (think PROLOG). If I was to design such a thing, the property you cite above is definitely something I'd encode as a fact/known relation rather than trying. On the other hand, there is Prof Paolo Bientinesi at RWTH Aachen University. In his dissertation he talks about automatic derivation of linear algebra algorithms. He uses Mathematica in a symbolic way. aices.rwth-aachen.de:8080/~pauldj $\endgroup$
    – Lagerbaer
    Nov 30, 2011 at 19:31
  • 1
    $\begingroup$ I know Paolo's stuff and the FLAME library. I don't think it can do this. $\endgroup$
    – Matt Knepley
    Nov 30, 2011 at 21:21
  • 2
    $\begingroup$ I agree that computer algebra systems for matrices would be great, but seem to be missing. I have put a bounty to increase the chance of getting an answer. $\endgroup$
    – Memming
    Mar 15, 2012 at 19:29

6 Answers 6

Reset to default
30
+50
$\begingroup$

Edit: This is now in SymPy

$ isympy
In [1]: A = MatrixSymbol('A', n, n)
In [2]: B = MatrixSymbol('B', n, n)
In [3]: context = Q.symmetric(A) & Q.positive_definite(A) & Q.orthogonal(B)
In [4]: ask(Q.symmetric(B*A*B.T) & Q.positive_definite(B*A*B.T), context)
Out[4]: True

Older answer that shows other work

So after looking into this for a while this is what I've found.

The current answer to my specific question is "No, there is no current system that can answer this question." There are however a few things that seem to come close.

First, Matt Knepley and Lagerbaer both pointed to work by Diego Fabregat and Paolo Bientinesi. This work shows both the potential importance and the feasibility of this problem. It's a good read. Unfortunately I'm not certain exactly how his system works or what it is capable of (if anyone knows of other public material on this topic do let me know).

Second, there is a tensor algebra library written for Mathematica called xAct which handles symmetries and such symbolically. It does some things very well but is not tailored to the special case of linear algebra.

Third, these rules are written down formally in a couple of libraries for Coq, an automated theorem proving assistant (Google search for coq linear/matrix algebra to find a few). This is a powerful system which unfortunately seems to require human interaction.

After talking with some theorem prover people they suggest looking into logic programming (i.e. Prolog, which Lagerbaer also suggested) for this sort of thing. To my knowledge this hasn't yet been done - I may play with it in the future.

Update: I've implemented this using the Maude system. My code is hosted on github

Improve this answer
$\endgroup$
3
  • 1
    $\begingroup$ When I found that there was no good system, my first instinct was to write a prolog program. :) $\endgroup$
    – Memming
    Mar 21, 2012 at 20:24
  • 1
    $\begingroup$ I added a link at the bottom to a side project of mine that deals with this problem. $\endgroup$
    – MRocklin
    May 17, 2012 at 15:47
  • $\begingroup$ Could SymPy infer simplification of matrix multiplication and inversion? $\endgroup$
    – Royi
    Nov 28, 2019 at 9:47
4
$\begingroup$

Some symbolic matrix computations (e.g., block matrix completion) can be done with the package NCAlgebra http://www.math.ucsd.edu/~ncalg/ (which runs under mathematica).

Bergman http://servus.math.su.se/bergman/ is a package in Lisp with similar capabilities.

Some relevant papers:
http://math.ucsd.edu/~helton/osiris/COMPALG2000/ohRevisIJC.pdf
http://math.ucsd.edu/~thesis/thesis/dkronewitter/dkronewitter.pdf
http://www.tandfonline.com/doi/abs/10.1080/00207170600882346

Improve this answer
$\endgroup$
4
$\begingroup$

I think most CAS systems can show this for 2x2 and 3x3 matrices given a symbolic orthonormal $\mathbf B$ construct, such as rotation matrices. In the end, you will have to decompose the result to figure out if it is positive definite or not. Symmetry is easier to show.

The question then becomes, what about a N dimensional matrix? Maybe you can come up with an inductive scheme where for N-1 x N-1 is assumed to be true and then construct a new block matrix with overall size N x N to prove that is positive definite and symmetric.

So the final question, of which software is better suited for the task (if any), my experience has been with MATLAB/MuPad and Derive (still use it) and neither of them handle vectors and matrices very well. MATLAB breaks everything down into components, and Derive can declare Non-scalars but it does not apply any simplification rules to them.

I hope this posting is going to provide some more insight into this kind of "hole" and how to fill it. For me, I want some software that can help me simplify expressions with multiple dot and cross products of vectors, together with rotation matrices use well known identities such as: $\vec a \times (\vec b \times \vec c) = (\vec a \cdot \vec b)\vec c - (\vec a \cdot \vec c) \vec b$

Improve this answer
$\endgroup$
3
$\begingroup$

Maple 15 cannot do it. It has no property "Orthogonal" for matrices (although it has Symmetric and PositiveDefinite).

Improve this answer
$\endgroup$
1
  • 1
    $\begingroup$ Updated to Maple 16 -> no property "Orthogonal" neither. $\endgroup$
    – GertVdE
    Apr 17, 2012 at 13:27
2
$\begingroup$

In Mathematica you can at least check these properties for specific matrices. For example, the matrix A as you described:

In[1]:= A = {{2.0,-1.0,0.0},{-1.0,2.0,-1.0},{0.0,-1.0,2.0}};
        {SymmetricMatrixQ[A],PositiveDefiniteMatrixQ[A]}
Out[2]= {True,True}

For matrix B:

In[3]:= B = {{0, -0.80, -0.60}, {0.80, -0.36, 0.48}, {0.60, 0.48, -0.64}};
        Transpose[B] == Inverse[B]
Out[4]= True

Then:

In[5]:= c = B.A.Transpose[B];
        {SymmetricMatrixQ[c],PositiveDefiniteMatrixQ[c]}
Out[6]= {True,True}

Mathematica Matrices and Linear Algebra Documentation

Improve this answer
$\endgroup$
2
  • 7
    $\begingroup$ It is my understand that the predicates above are verifying that property for a given matrix, rather than symbolically propagating these properties as Matt asks for above. $\endgroup$
    – Matt Knepley
    Nov 30, 2011 at 14:43
  • $\begingroup$ Ah yes. Sorry about that. I misunderstood. $\endgroup$
    – lynchs
    Nov 30, 2011 at 15:19
2
$\begingroup$

It's been a while since I last used either of these packages, but I thought that you could do this in languages such as Mathematica through the use of assertions. Something like Assert[A, Symmetric] tells Mathematica that A is a symmetric matrix, and so on. I don't have access to either handy at the moment, so this is something that would have to be checked.

Improve this answer
$\endgroup$
5
  • 1
    $\begingroup$ I think you mean the Mathematica command Assuming instead of Assert. Assuming will apply these assumptions when simplifying or integrating an expression, but the documentation is not clear about whether matrix properties are propagated. My guess is that such properties are not carried through symbolic computations. $\endgroup$
    – Geoff Oxberry
    Jan 12, 2012 at 1:28
  • $\begingroup$ That could be true. Like I said, this was eons ago (back in my graduate school days). But I do remember being able to do something like this once. (Perhaps it was with MuPad, as implemented in Scientific WorkPlace.) But I no longer have access to SWP to check that (Windows-only, and I don't have an emulator on my box). $\endgroup$
    – aeismail
    Jan 12, 2012 at 8:02
  • $\begingroup$ MuPAD is part of Matlab now. According to the documentation, the usage of assumptions is similar to that of Mathematica. $\endgroup$
    – Geoff Oxberry
    Jan 12, 2012 at 8:16
  • $\begingroup$ MuPAD can only deal with fixed size matrix, and doesn't take arbitrary assumptions such as positive definiteness. Also it cannot answer the question of positive definiteness of B A B' originally asked. $\endgroup$
    – Memming
    Mar 15, 2012 at 21:09
  • $\begingroup$ @Memming: Fair enough. As I said, my memory of MuPAD was substantially out of date, as I last used the program regularly around 2006 (when I switched from PC's to Macs). $\endgroup$
    – aeismail
    Mar 15, 2012 at 21:13

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge that you have read and understand our privacy policy and code of conduct.

Not the answer you're looking for? Browse other questions tagged or ask your own question.