Des progiciels symboliques pour les expressions Matrix?

Nous savons que est symétrique et positif-défini. Nous savons que est orthogonal:$\mathbf A$$\mathbf B$

Question: symétrique et positif-défini? Réponse: oui$\mathbf B \cdot\mathbf A \cdot\mathbf B^\top$

Question: Un ordinateur aurait-il pu nous le dire? Réponse: probablement.

Existe-t-il des systèmes algébriques symboliques (comme Mathematica) qui gèrent et propagent des faits connus sur les matrices?

Edit: Pour être clair, je pose cette question sur les matrices définies de manière abstraite. C'est-à-dire que je n'ai pas d'entrées explicites pour et , je sais juste qu'elles sont toutes les deux matrices et ont des attributs particuliers comme symétrique, positif défini, etc.$A$$B$

Edit: Ceci est maintenant dans 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

Réponse plus ancienne qui montre un autre travail

Donc, après avoir examiné cela pendant un moment, voici ce que j'ai trouvé.

La réponse actuelle à ma question spécifique est "Non, aucun système actuel ne peut répondre à cette question". Il y a cependant quelques petites choses qui semblent se rapprocher.

Matt Knepley et Lagerbaer ont tout d’abord évoqué les travaux de Diego Fabregat et Paolo Bientinesi . Ce travail montre à la fois l’importance potentielle et la faisabilité de ce problème. C'est une bonne lecture. Malheureusement, je ne sais pas exactement comment son système fonctionne ni de quoi il est capable (si quelqu'un connaît d'autres documents publics sur ce sujet, faites-le-moi savoir).

Deuxièmement, il existe une bibliothèque d'algèbre de tenseurs écrite pour Mathematica appelée xAct, qui traite les symétries et symboliquement. Il fait certaines choses très bien mais n'est pas adapté au cas particulier de l'algèbre linéaire.

Troisièmement, ces règles sont formellement écrites dans quelques bibliothèques pour Coq , un assistant de démonstration de théorèmes automatisé (recherche Google pour l’algèbre matricielle linéaire / matricielle pour en trouver quelques-unes). C'est un système puissant qui semble malheureusement nécessiter une interaction humaine.

Après avoir discuté avec des gens qui ont prouvé leur théorie, ils suggèrent de se pencher sur la programmation logique (c'est-à-dire Prolog, que Lagerbaer a également suggéré) pour ce genre de chose. À ma connaissance, cela n’a pas encore été fait - il est possible que je joue avec dans le futur.

Mise à jour: j'ai implémenté cela en utilisant le système Maude . Mon code est hébergé sur github

Certains calculs de matrice symbolique (par exemple, l'achèvement de la matrice de blocs) peuvent être effectués avec le package NCAlgebra http://www.math.ucsd.edu/~ncalg/ (qui fonctionne sous mathematica).

Bergman http://servus.math.su.se/bergman/ est un paquet dans Lisp avec des capacités similaires.

Quelques articles pertinents:
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

Je pense que la plupart des CASsystèmes peuvent montrer cela pour 2x2et les 3x3matrices étant donné une construction symbolique orthonormale , telle que les matrices de rotation. En fin de compte, vous devrez décomposer le résultat pour déterminer s'il est positif défini ou non. La symétrie est plus facile à montrer.$\mathbf B$

La question devient alors, qu'en est-il d'une Nmatrice dimensionnelle? Vous pouvez peut-être imaginer un schéma inductif dans lequel for N-1 x N-1est supposé être vrai, puis construire une nouvelle matrice de blocs avec une taille globale N x Npour prouver que cela est positif et symétrique.

Donc, la dernière question, de savoir quel logiciel convient le mieux à la tâche (le cas échéant), mon expérience a été avec MATLAB/MuPadet Derive(continue de l’utiliser) et aucun d’eux ne gère très bien les vecteurs et les matrices. MATLABdécompose tout en composants et Derivepeut déclarer Non-scalarsmais il ne leur applique aucune règle de simplification.

$\vec a \times (\vec b \times \vec c) = (\vec a \cdot \vec b)\vec c - (\vec a \cdot \vec c) \vec b$

Cela fait longtemps que je n'ai utilisé aucun de ces packages, mais je pensais que vous pouviez le faire dans des langages tels que Mathematica en utilisant des assertions. Quelque chose comme Assert [A, Symétrique] indique à Mathematica que A est une matrice symétrique, etc. Je n'ai accès à aucun des deux pour le moment, c'est donc quelque chose qui devrait être vérifié.

Maple 15 ne peut pas le faire. Il n'a pas de propriété "Orthogonal" pour les matrices (bien qu'il ait Symmetric et PositiveDefinite).

Dans Mathematica, vous pouvez au moins vérifier ces propriétés pour des matrices spécifiques. Par exemple, la matrice Atelle que vous l'avez décrite:

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}

Pour la matrice 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

Ensuite:

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

Documentation sur les matrices Mathematica et l'algèbre linéaire