Pacotes de software simbólicos para expressões Matrix?

36

Sabemos que é simétrico e positivo-definido. Sabemos que é ortogonal:BAB

Pergunta: simétrico e positivo-definido? Resposta: Sim.BAB

Pergunta: Um computador poderia ter nos dito isso? Resposta: Provavelmente.

Existem sistemas de álgebra simbólica (como o Mathematica) que manipulam e propagam fatos conhecidos sobre matrizes?

Edit: Para ser claro, eu estou fazendo esta pergunta sobre matrizes definidas abstratamente. Ou seja, eu não tenho entradas explícitas para e , só sei que elas são matrizes e têm atributos particulares como simétrico, definido positivo, etc.BAB

MRocklin
fonte
5
O que estou perdendo é um software que trata matrizes simbolicamente (ou seja, não como matrizes). Eu gostaria de poder falar sobre alguma matriz simétrica sem ter que se preocupar com suas entradas. C
JM
6
Existem alguns projetos trabalhando nisso. Por acaso, estou familiarizado com a implementação no SymPy. É de buggy, mas lentamente sendo construído.
30911 MRocklin
4
Isso soa como prova automatizada de teoremas. O truque é incluir um conjunto suficiente de axiomas em seu mecanismo para que ele possa ser deduzido com eficiência pelo raciocínio automatizado (pense em PROLOG). Se eu fosse projetar algo assim, a propriedade que você cita acima é definitivamente algo que eu codificaria como uma relação fato / conhecida, em vez de tentar. Por outro lado, há o Prof Paolo Bientinesi na Universidade RWTH Aachen. Em sua dissertação, ele fala sobre derivação automática de algoritmos de álgebra linear. Ele usa o Mathematica de forma simbólica. aices.rwth-aachen.de:8080/~pauldj #
30511 Lagerbaer
11
Conheço as coisas de Paolo e a biblioteca FLAME. Eu não acho que pode fazer isso.
Matt Knepley
2
Concordo que os sistemas de álgebra computacional para matrizes seriam ótimos, mas parecem estar faltando. Eu coloquei uma recompensa para aumentar a chance de obter uma resposta.
Memming 15/03/12

Respostas:

27

Edit: Agora está no 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

Resposta mais antiga que mostra outro trabalho

Então, depois de analisar isso por um tempo, foi o que eu encontrei.

A resposta atual para minha pergunta específica é "Não, não existe um sistema atual que possa responder a essa pergunta". No entanto, existem algumas coisas que parecem se aproximar.

Primeiro, Matt Knepley e Lagerbaer apontaram para o trabalho de Diego Fabregat e Paolo Bientinesi . Este trabalho mostra a importância potencial e a viabilidade desse problema. É uma boa leitura. Infelizmente, não sei exatamente como o sistema dele funciona ou do que ele é capaz (se alguém souber de outro material público sobre esse assunto, me avise).

Segundo, há uma biblioteca de álgebra tensorial escrita para o Mathematica chamada xAct, que lida com simetrias e simbolicamente. Ele faz algumas coisas muito bem, mas não é adaptado ao caso especial da álgebra linear.

Terceiro, essas regras são formalmente escritas em algumas bibliotecas para o Coq , um assistente automatizado de prova de teoremas (o Google pesquisa a álgebra linear / matricial coq para encontrar algumas). Este é um sistema poderoso que infelizmente parece exigir interação humana.

Depois de conversar com algumas pessoas que provam o teorema, elas sugerem procurar na programação lógica (ou seja, Prolog, que Lagerbaer também sugeriu) esse tipo de coisa. Que eu saiba, isso ainda não foi feito - eu posso brincar com isso no futuro.

Atualização: eu implementei isso usando o sistema Maude . Meu código está hospedado no github

MRocklin
fonte
11
Quando descobri que não havia um bom sistema, meu primeiro instinto foi escrever um programa de prólogo. :)
Memming 21/03
11
Adicionei um link na parte inferior de um projeto paralelo que lida com esse problema.
MRocklin
Poderia SymPyinferir a simplificação da multiplicação e inversão de matrizes?
Royi
4

Alguns cálculos de matriz simbólica (por exemplo, conclusão da matriz de bloco) podem ser feitos com o pacote NCAlgebra http://www.math.ucsd.edu/~ncalg/ (que é executado no mathematica).

Bergman http://servus.math.su.se/bergman/ é um pacote no Lisp com recursos semelhantes.

Alguns artigos 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

Arnold Neumaier
fonte
3

CAS2x23x3B

A questão então se torna: o que dizer de uma Nmatriz dimensional? Talvez você possa criar um esquema indutivo no qual N-1 x N-1for assumido verdadeiro e, em seguida, construir uma nova matriz de blocos com tamanho geral N x Npara provar que é positivo e definitivo e simétrico.

Portanto, a pergunta final, de qual software é mais adequado para a tarefa (se houver), minha experiência foi com ( MATLAB/MuPade Deriveainda o uso) e nenhum deles lida com vetores e matrizes muito bem. MATLABdivide tudo em componentes e Derivepode declarar, Non-scalarsmas não lhes aplica nenhuma regra de simplificação.

a×(b×c)=(ab)c(ac)b

ja72
fonte
2

Já faz um tempo desde a última vez que usei um desses pacotes, mas pensei que você poderia fazer isso em idiomas como o Mathematica através do uso de asserções. Algo como Assert [A, Symmetric] diz ao Mathematica que A é uma matriz simétrica, e assim por diante. No momento, não tenho acesso a nenhum desses itens úteis, portanto, isso deve ser verificado.

aeismail
fonte
11
Eu acho que você quer dizer o comando Mathematica em Assumingvez de Assert. Assumingaplicará essas suposições ao simplificar ou integrar uma expressão, mas a documentação não está clara sobre se as propriedades da matriz são propagadas. Meu palpite é que essas propriedades não são realizadas através de cálculos simbólicos.
Geoff Oxberry
Isso pode ser verdade. Como eu disse, isso foi há eras (nos meus dias de pós-graduação). Mas eu me lembro de poder fazer algo assim uma vez. (Talvez tenha sido com o MuPad, conforme implementado no Scientific WorkPlace.) Mas não tenho mais acesso ao SWP para verificar isso (somente Windows, e não tenho um emulador na minha caixa).
Aeismail
O MuPAD agora faz parte do Matlab. De acordo com a documentação , o uso de suposições é semelhante ao do Mathematica.
Geoff Oxberry
O MuPAD só pode lidar com matrizes de tamanho fixo e não assume premissas arbitrárias, como definição positiva. Também não pode responder à questão da definição positiva do BAB 'originalmente feita.
Memming 15/03/12
@ Memming: justo o suficiente. Como eu disse, minha memória do MuPAD estava substancialmente desatualizada, quando usei o programa pela última vez regularmente por volta de 2006 (quando mudei de PC para Mac).
aeismail
2

Maple 15 não pode fazê-lo. Não possui propriedade "Ortogonal" para matrizes (embora tenha Simétrico e PositivoDefinido).

GertVdE
fonte
11
Atualizado para Maple 16 -> nenhuma propriedade "Ortogonal" também.
precisa saber é o seguinte
1

No Mathematica, você pode pelo menos verificar essas propriedades para matrizes específicas. Por exemplo, a matriz Acomo você descreveu:

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

Então:

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

Matrizes Mathematica e documentação de álgebra linear

linchamentos
fonte
7
Entendo que os predicados acima estão verificando essa propriedade para uma determinada matriz, em vez de propagar simbolicamente essas propriedades, como Matt pede acima.
Matt Knepley
Ah sim. Me desculpe por isso. Eu entendi errado.
Lynchs