Maude-help mailing list

[Marc Boyer <Marc.Boyer AT onera.fr>]

Le 20/04/2012 20:05, Matthew Rocklin a écrit :
> Hi Everyone,
>
> I'm trying to simplify expressions in matrix algebra using known facts
> about the matrices in the expression.
>
> I.e. supplied with the following
>
> expression: transpose(B*Q*transpose(B*Q) )
> facts: Q is orthogonal, B is symmetric
>
> can we simplify to the following expression
> B*B
>
> by going through the following states
> transpose(B*Q*transpose(Q)*transpose(B))    *** because transpose(XY) ==
> transpose(X)*transpose(Y)
> transpose(B*transpose(B))    *** because X*transpose(X) == identity if X
> is orthogonal and Q is orthogonal
> B*transpose(B)   *** because transpose(X) == X if X is symmetric and
> X*transpose(X) is symmetric for any X
> B * B   *** because transpose(X) == X if X is symmetric and B is symmetric
>
> I know/can write down all of the equations and rules that appear on the
> right. I need to organize a system that handles both the known facts and
> the expression at once.

I am not a Maude expert, but I have written some Maude code.

You could try something like:

fmod MATRIX is
  sort Matrix .
  op symetric : Matrix -> Bool .
  op transpose : Matrix -> Matrix .
  op _ * _ : Matrix Matrix -> Matrix .

  var M M' : Matrix .

  eq symetric( M * transpose(M ) ) = true .
  eq transpose( M * M' ) = transpose( M ) * transpose( M' ) .
  ceq transpose( M ) = M if symetric( M ) .
endfm

fmod System is
 protecting MATRIX .

 ops A B : -> Matrix .

 eq symetric( A ) = true .

endfm

red transpose( A * B ) .
red transpose( A * A ) .
--
Marc Boyer, Ingenieur de recherche                              ONERA
Tel: (33)  5.62.25.26.36                                         DTIM
Fax: (33)  5.62.25.26.93                          2, av Edouard Belin
http://www.onera.fr/staff/marc-boyer/          31055 TOULOUSE Cedex 4