¿Paquetes de software simbólicos para expresiones matriciales?

Sabemos que es simétrico y positivo-definido. Sabemos que es ortogonal:$\mathbf A$$\mathbf B$

Pregunta: ¿es simétrico y positivo-definido? Respuesta: sí.$\mathbf B \cdot\mathbf A \cdot\mathbf B^\top$

Pregunta: ¿Podría una computadora habernos dicho esto? Respuesta: probablemente.

¿Existen sistemas de álgebra simbólica (como Mathematica) que manejan y propagan hechos conocidos sobre matrices?

Editar: Para ser claros, estoy haciendo esta pregunta sobre matrices definidas de forma abstracta. Es decir, no tengo entradas explícitas para y , solo sé que ambas son matrices y tienen atributos particulares como simétrico, positivo definido, etc.$A$$B$

Editar: Esto ahora está en 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

Respuesta anterior que muestra otro trabajo

Entonces, después de analizar esto por un tiempo, esto es lo que he encontrado.

La respuesta actual a mi pregunta específica es "No, no hay un sistema actual que pueda responder esta pregunta". Sin embargo, hay algunas cosas que parecen acercarse.

Primero, Matt Knepley y Lagerbaer señalaron el trabajo de Diego Fabregat y Paolo Bientinesi . Este trabajo muestra tanto la importancia potencial como la viabilidad de este problema. Es una buena lectura. Lamentablemente, no estoy seguro exactamente de cómo funciona su sistema o de lo que es capaz (si alguien sabe de otro material público sobre este tema, hágamelo saber).

En segundo lugar, hay una biblioteca de álgebra tensorial escrita para Mathematica llamada xAct que maneja las simetrías y simbólicamente. Hace algunas cosas muy bien pero no se adapta al caso especial de álgebra lineal.

Tercero, estas reglas están escritas formalmente en un par de bibliotecas para Coq , un asistente de prueba de teorema automatizado (Google busca álgebra lineal / matricial de coq para encontrar algunas). Este es un sistema poderoso que desafortunadamente parece requerir la interacción humana.

Después de hablar con algunas personas probadores de teoremas , sugieren buscar en la programación lógica (es decir, Prolog, que Lagerbaer también sugirió) para este tipo de cosas. Que yo sepa, esto aún no se ha hecho, puedo jugar con él en el futuro.

Actualización: he implementado esto usando el sistema Maude . Mi código está alojado en github

Algunos cálculos simbólicos de la matriz (p. Ej., Finalización de la matriz de bloques) se pueden hacer con el paquete NCAlgebra http://www.math.ucsd.edu/~ncalg/ (que se ejecuta en matemática).

Bergman http://servus.math.su.se/bergman/ es un paquete en Lisp con capacidades similares.

Algunos documentos relevantes:
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

Creo que la mayoría de los CASsistemas pueden mostrar esto para 2x2y 3x3matrices dada una construcción simbólica ortonormal , como las matrices de rotación. Al final, tendrá que descomponer el resultado para determinar si es positivo definitivo o no. La simetría es más fácil de mostrar.$\mathbf B$

La pregunta entonces es, ¿qué pasa con una Nmatriz dimensional? Tal vez pueda llegar a un esquema inductivo donde N-1 x N-1se supone que for es verdadero y luego construir una nueva matriz de bloques con un tamaño general N x Npara demostrar que es positiva, definida y simétrica.

Entonces, la pregunta final, sobre qué software es más adecuado para la tarea (si corresponde), mi experiencia ha sido con MATLAB/MuPady Derive(todavía lo uso) y ninguno de ellos maneja muy bien los vectores y las matrices. MATLABdivide todo en componentes y Derivepuede declarar, Non-scalarspero no les aplica ninguna regla de simplificación.

Espero que esta publicación proporcione más información sobre este tipo de "agujero" y cómo llenarlo. Para mí, quiero un software que pueda ayudarme a simplificar expresiones con múltiples puntos y productos cruzados de vectores, junto con las matrices de rotación usan identidades bien conocidas como:$\vec a \times (\vec b \times \vec c) = (\vec a \cdot \vec b)\vec c - (\vec a \cdot \vec c) \vec b$

Ha pasado un tiempo desde la última vez que usé cualquiera de estos paquetes, pero pensé que podría hacerlo en lenguajes como Mathematica mediante el uso de aserciones. Algo así como Assert [A, Symmetric] le dice a Mathematica que A es una matriz simétrica, y así sucesivamente. No tengo acceso a ninguna de las prácticas en este momento, así que esto es algo que debería verificarse.

Maple 15 no puede hacerlo. No tiene ninguna propiedad "Ortogonal" para matrices (aunque tiene Symmetric y PositiveDefinite).

En Mathematica puede al menos verificar estas propiedades para matrices específicas. Por ejemplo, la matriz Acomo la describiste:

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}

Para matriz 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

Luego:

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

Matrices de Mathematica y Documentación de Álgebra Lineal