In graduate school I used Mathematica all day every day. I've not had the luxury of that kind of immersion in Sage (yet). But I've searched the documentation and the forums and I see others struggling with the same issue I'm having so I don't think it's just me.
I am working on mathematical algorithms over arbitrary finite real data. The dimensions are known to be finite but are not fixed with respect to the executable representation of the algorithm. In many important cases, the largest of the dimensions is not even known during the early stages of execution, e.g. reading variable-length records from a file or network connection. Typically I'm given a "canonical form" of the algorithm to start with, and typically it is pretty straightforward stuff. Matrix Matrix vector, sum of sums of sums of something. I need to transform the algorithm so that it can be implemented more efficiently, compared to the canonical form, and still get the right answer. I used Mathematica to attack this kind of task a few years ago (a decade out of school) and found it very difficult to do well. I could express the canonical and transformed algorithms easily enough as finite sums over an indefinite range but the system could only prove equivalence if I fixed the ranges to some specific values. I could hack around with enough distinct combinations of dimensions to satisfy myself that the transformation was right but that wasn't entirely satisfactory. Now I'm working with a family of algorithms expressed in terms of standard linear algebra (and matrix calculus) operators. The matrices have a lot of structure, eg a lot of them are block diagonal symmetric with repeated blocks, but the number of blocks and their size are both arbitrary. I found a partial implementation https://groups.google.com/forum/#!topic/sage-devel/yvtIbHmi6zw/discussion but it doesn't accept scalar factors, doesn't know that a 1x1 matrix expression evaluates to a scalar, knows nothing about symmetry, block structure, trace, det, etc. I played around with Isabel/HOL and looked at other proof-checking systems in school as well but they are a bear to use. Or were back then. In an ideal world I'd get a sabbatical to implement a Prolog-equivalent subsystem in Python and a proof checking subsystem in Sage. Yeah, right. I'd like to be able to start out saying Let m, n, p be positive integers such that p divides n, Let X be a real n*m matrix Let Mb be a real p*p symmetric matrix Let M be the block diagonal n*n matrix with n/p copies of Mb on the diagonal Then X^T * M * X == Sum over blocks Xi of X, Xi^T Mb Xi ==> "True" And if I botched something the answer would be "Error" or "False" or a partially simplified form of the predicate. I know that's asking a lot, but hey if you don't ask you won't get it, right? Oh, and then I want to be able to emit the transformed expressions in a form I can directly paste into my code as well as typesetting my proof as part of the program documentation. For the specific kind of work I'm doing now transforming all the matrix algebra into equivalent nested summations and then attacking the summation equivalence problem might be a simplification of the problem space but it's not a very elegant way to proceed. I welcome any suggestions here. Am I barking up the wrong tree entirely? Am I missing some existing functionality? -- You received this message because you are subscribed to the Google Groups "sage-support" group. To unsubscribe from this group and stop receiving emails from it, send an email to sage-support+unsubscr...@googlegroups.com. To post to this group, send email to sage-support@googlegroups.com. Visit this group at http://groups.google.com/group/sage-support?hl=en. For more options, visit https://groups.google.com/groups/opt_out.
