Re: [Axiom-mail] A question about Axiom capabilities
We did not get time to convert all the comments into code as is done for some the new categories and domains in the trunk repository. For example, from http://sourceforge.net/p/open-axiom/code/2800/tree/trunk/src/algebra/catdef.spad.pamphlet Is there a way I could help in a pan-Axiom sort of way? For instance, would it be any help if I went through these categories and drew a diagram of their relationships? I realise diagrams like: http://www.axiom-developer.org/axiom-website/bookvol10.2full.html tend to quickly become unwieldy. But if the diagram was limited to pure algebras and split into operator and algebra categories, perhaps it might be more manageable? Or, would it be more practical to model it in one of the formal methods tools around, such as? * Formal specification program, * Formal development program, * Formal verification program, * Theorem provers I have no experience in using any of these programs but, when they came up in this thread I did some searches and they appear to be very powerful (I guess their limitations only become clear with experience)? At first glance CASL appears very powerful for axioms. quote from wiki page here. http://en.wikipedia.org/wiki/Specification_language In the property-oriented approach to specification (taken e.g. by CASL), specifications of programs consist mainly of logical axioms, usually in a logical system in which equality has a prominent role, describing the properties that the functions are required to satisfy - often just by their interrelationship. This is in contrast to so-called model-oriented specification in frameworks like VDM and Z, which consist of a simple realization of the required behaviour. So, if I understand correctly: CASL is good at theories (axiom categories). ACL2 is good at models of those theories (axiom domains). (or by Curry–Howard: proofs) I have not yet seen a program that is good at both. I get the impression that ACL2, after a very quick search on the web (so I may be wrong), does term rewriting and proofs but its input is not axioms but some sort of state machine defined in LISP? (I have not seen the light regarding LISP, but let not have that debate!). So I just wondered if anyone has had experience with any of these 'formal methods tools' and would there be any benefit in my attempting to learn one? (to experiment with specifying axioms or to experiment with term rewriting systems). Or would it be best to wait (hopefully not for the full 30 years) until you guys implement more of this stuff? Martin ___ Axiom-mail mailing list Axiom-mail@nongnu.org https://lists.nongnu.org/mailman/listinfo/axiom-mail
Re: [Axiom-mail] A question about Axiom capabilities
Is there a way I could help in a pan-Axiom sort of way? For instance, would it be any help if I went through these categories and drew a diagram of their relationships? I realise diagrams like: http://www.axiom-developer.org/axiom-website/bookvol10.2full.html tend to quickly become unwieldy. But if the diagram was limited to pure algebras and split into operator and algebra categories, perhaps it might be more manageable? The graph is very large. All of the information to create the graph exists in static files (the algebra Makefile and the bookvol10* files). It would be useful to be able to create portions of the graph dynamically. Some of the functionality exists in the API domain (ApplicationProgramInterface), such as getAncestors and getDomains. Any other functionality is just as easy to add. I'd be happy to help. In addition, it would be useful to be able to graph some information related to functions. Where are all of the integrate functions and how are they related? Or to know about a domain by showing the locally defined functions and the tree of parents whose functions it inherits. From a given domain it would be useful to create portions of the graph of a given distance around the domain. So you could ask for a small graph of categories and make the limit distance of 3. If the output was in some standard format (e.g. dot files, html, etc.) it could be used as input to graph drawing programs. This is a reasonably straightforward problem and would get you more familiar with Axiom's hierarchy as well as writing code. Some of this functionality can be embedded into latex documents which would make them much more useful. Currently the big graph contains links to the source code in the books. There are mini-graphs in the books but the links are not (yet) part of the graphs. It would be useful to click on the pictures in the book and move to, say, a parent category's source code. Tim Daly ___ Axiom-mail mailing list Axiom-mail@nongnu.org https://lists.nongnu.org/mailman/listinfo/axiom-mail
Re: [Axiom-mail] A question about Axiom capabilities, Fwd: [fricas-devel] Abstract Vector Algebra
On 05/04/13 01:07, Ralf Hemmecke wrote: I don't quite understand. If you assume myOp1 to be commutative, then solving equations is quite a different task from when it is non-commutative. Where would you store all these axioms? Yes that's an interesting question. For an Axiom category to correspond to a 'category' in category theory or a 'theory' in universal algebra then it should define both the function signatures and the axioms. I get the impression that Axiom(the program) attempts to include axioms in categories to a limited extent by say: inheriting commutative but this would not be complete enough to drive a general equation solver? (and, of course, it cannot enforce commutative axiom in domain instances). It seems a sight irony that Axiom(the program) does not do much about axioms. Given that there is no resources (or desire, as far as I can see) to change the structure of Axiom then I was wondering, just for specific domains where we want a specific equation solver, could we encode the axioms in a set of rules in a domain or package? I guess I'm looking for a compromise between building this into the Lisp code and writing a seperate equation solver in every domain. Looks like you aim at a general term rewriting system. Yes, but again I recognise that there are no resources, so I was wondering if it would be possible to start with a very simple domain (not a field, something really simple, which is what I was trying to indicate in the psudocode in my last message). Then abstract out a rule engine. Then gradually build it up over time so that it could cope with more complex domains. This is probably not very practical, but I was just trying to do a thought experiment to investigate what would be required to have variables that range over domains that are not numbers. Martin ___ Axiom-mail mailing list Axiom-mail@nongnu.org https://lists.nongnu.org/mailman/listinfo/axiom-mail
Re: [Axiom-mail] A question about Axiom capabilities, Fwd: [fricas-devel] Abstract Vector Algebra
On 04/05/2013 10:51 AM, Martin Baker wrote: It seems a sight irony that Axiom(the program) does not do much about axioms. Of course, AXIOM can deal with axioms, but the SPAD language does not include any way to specify axiom (not even Aldor can do this). Looks like you aim at a general term rewriting system. Yes, but again I recognise that there are no resources, so I was wondering if it would be possible to start with a very simple domain For a term rewriting system you basically have to start with the implementation of a term algebra. The signature would basically tell, what symbols are allowed. Since LISP is so fitting for a representation of such a term algebra, it is no surprise that quite a lot of computer algebra systems were written in LISP. Then you can add equations (axioms) and a mechanism to reduce a given term modulo such equations. But there is no general algorithm to transform a given term modulo such equation into a canonical form. A canonical form does not even exist for every given term rewriting system. The non-existence of the eierlegende Wollmilchsau (http://de.wikipedia.org/wiki/Eierlegende_Wollmilchsau http://en.wiktionary.org/wiki/eierlegende_Wollmilchsau) is the reason why people work on specialized solvers and use special representations of the respective term algebra to make things fast. Ralf ___ Axiom-mail mailing list Axiom-mail@nongnu.org https://lists.nongnu.org/mailman/listinfo/axiom-mail
Re: [Axiom-mail] A question about Axiom capabilities, Fwd: [fricas-devel] Abstract Vector Algebra
On 05/04/13 10:20, Ralf Hemmecke wrote: On 04/05/2013 10:51 AM, Martin Baker wrote: It seems a sight irony that Axiom(the program) does not do much about axioms. Of course, AXIOM can deal with axioms, but the SPAD language does not include any way to specify axiom (not even Aldor can do this). I was thinking of something like CASL: http://www.informatik.uni-bremen.de/cofi/wiki/index.php/CASL I realise that its purpose is different to a category in Axiom but it does at least show how the semantics as well as the syntax of a category could be encoded in a well defined language. Even if it were not possible to use this 'semantic' information for enforcing axioms or equation solvers it would be good to have it for documentation and automatically generating test scripts. Looks like you aim at a general term rewriting system. Yes, but again I recognise that there are no resources, so I was wondering if it would be possible to start with a very simple domain For a term rewriting system you basically have to start with the implementation of a term algebra. The signature would basically tell, what symbols are allowed. Since LISP is so fitting for a representation of such a term algebra, it is no surprise that quite a lot of computer algebra systems were written in LISP. Then you can add equations (axioms) and a mechanism to reduce a given term modulo such equations. But there is no general algorithm to transform a given term modulo such equation into a canonical form. A canonical form does not even exist for every given term rewriting system. The non-existence of the eierlegende Wollmilchsau (http://de.wikipedia.org/wiki/Eierlegende_Wollmilchsau http://en.wiktionary.org/wiki/eierlegende_Wollmilchsau) is the reason why people work on specialized solvers and use special representations of the respective term algebra to make things fast. So are you saying that, for practical purposes, it is not even worth trying to write an equation solver for a given category/domain in SPAD, even for a very simple category? I realise there is no general algorithm to do this, but I was hoping there might have been the possibility of a common 'toolkit' so at least every category/domain writer was not totally on their own. Martin ___ Axiom-mail mailing list Axiom-mail@nongnu.org https://lists.nongnu.org/mailman/listinfo/axiom-mail
Re: [Axiom-mail] A question about Axiom capabilities
On Fri, Apr 5, 2013 at 3:51 AM, Martin Baker ax87...@martinb.com wrote: Given that there is no resources (or desire, as far as I can see) to change the structure of Axiom then I was wondering, just for specific domains where we want a specific equation solver, could we encode the axioms in a set of rules in a domain or package? I guess I'm looking for a compromise between building this into the Lisp code and writing a seperate equation solver in every domain. Your probably know that OpenAxiom started putting the axioms in AXIOM. See for example: http://sourceforge.net/p/open-axiom/code/2800/tree/trunk/src/algebra/catdef.spad.pamphlet In fact, a couple of years ago, a student of mine did experiments on exploiting these axioms to help code generation and automatic parallelization. The results were very encouraging (see the yli-sandbox for example.) OpenAxiom is very much committed to get the axioms integrated to the entire type checking and elaboration process. -- Gaby ___ Axiom-mail mailing list Axiom-mail@nongnu.org https://lists.nongnu.org/mailman/listinfo/axiom-mail
Re: [Axiom-mail] A question about Axiom capabilities
On 05/04/13 12:11, Gabriel Dos Reis wrote:
Your probably know that OpenAxiom started putting the axioms in AXIOM.
See for example:
http://sourceforge.net/p/open-axiom/code/2800/tree/trunk/src/algebra/catdef.spad.pamphlet
In fact, a couple of years ago, a student of mine did experiments on
exploiting these axioms to help code generation and automatic
parallelization. The results were very encouraging (see the
yli-sandbox for example.)
OpenAxiom is very much committed to get the axioms integrated to the
entire type checking and elaboration process.
Gaby,
Thanks, I find this stuff interesting, Its not that I expect it to
appear in any flavour of Axiom soon (feel free to correct my
assumptions), its just that I like to know how things work, what can and
what can't be done.
AFSICS axioms are currently embedded in the inline documentation for the
category like this:
snippet from:
http://sourceforge.net/p/open-axiom/code/2800/tree/trunk/src/algebra/catdef.spad.pamphlet
++ Axioms:
++ \spad{associative(+:(%,%)-%)}\tab{30}\spad{ (x+y)+z = x+(y+z) }
++ \spad{commutative(+:(%,%)-%)}\tab{30}\spad{ x+y = y+x }
AbelianSemiGroup(): Category == SetCategory with
I had a rummage about in the sandbox you mentioned (written by Yueli
about 3 years ago) and I did not come across any overall tutorial file
(what I would think of as top level documentation) I may have missed it.
Did Yueli write any thesis or anything like that?
At first glance it does look encouraging as the code to analyse the code
does seems to be written in SPAD, which hopefully shows that it can be
done. When I look at the code (such as snippet below) it looks like the
axioms are coded differently, that is on a per operator basis?
snippet from:
http://sourceforge.net/apps/trac/open-axiom/browser/yli-sandbox/contrib/redec/operatorcats.spad?rev=2776
)abbrev category ASSOCOP AssociativeOperator
++ Axiom: associativity: rule op(a, op(b, c)) == op(op(a,b), c)
AssociativeOperator(T: SetCategory, op: Mapping(T, T, T)):Category
== MagmaOperator(T, op)
Any further clues for understanding the code appreciated, thanks,
Martin
___
Axiom-mail mailing list
Axiom-mail@nongnu.org
https://lists.nongnu.org/mailman/listinfo/axiom-mail
Re: [Axiom-mail] A question about Axiom capabilities
On Fri, Apr 5, 2013 at 11:05 AM, Martin Baker ax87...@martinb.com wrote:
On 05/04/13 12:11, Gabriel Dos Reis wrote:
Your probably know that OpenAxiom started putting the axioms in AXIOM.
See for example:
http://sourceforge.net/p/open-axiom/code/2800/tree/trunk/src/algebra/catdef.spad.pamphlet
In fact, a couple of years ago, a student of mine did experiments on
exploiting these axioms to help code generation and automatic
parallelization. The results were very encouraging (see the
yli-sandbox for example.)
OpenAxiom is very much committed to get the axioms integrated to the
entire type checking and elaboration process.
Gaby,
Thanks, I find this stuff interesting, Its not that I expect it to appear in
any flavour of Axiom soon (feel free to correct my assumptions), its just
that I like to know how things work, what can and what can't be done.
AFSICS axioms are currently embedded in the inline documentation for the
category like this:
snippet from:
http://sourceforge.net/p/open-axiom/code/2800/tree/trunk/src/algebra/catdef.spad.pamphlet
++ Axioms:
++ \spad{associative(+:(%,%)-%)}\tab{30}\spad{ (x+y)+z = x+(y+z) }
++ \spad{commutative(+:(%,%)-%)}\tab{30}\spad{ x+y = y+x }
AbelianSemiGroup(): Category == SetCategory with
We did not get time to convert all the comments into code as is done
for some the new categories and domains in the trunk repository.
For example, from
http://sourceforge.net/p/open-axiom/code/2800/tree/trunk/src/algebra/catdef.spad.pamphlet
you see:
SemiGroupOperatorCategory(T: BasicType): Category ==
BinaryOperatorCategory T with
assume associativity ==
forall(f: %, x: T, y:T, z: T) . f(f(x,y),z) = f(x,f(y,z))
and
MonoidOperatorCategory(T: BasicType): Category ==
SemiGroupOperatorCategory T with
neutralValue: % - T
++ \spad{neutralValue f} returns the neutral value of the
++ monoid operation \spad{f}.
assume neutrality ==
forall(f: %, x: T) .
f(x, neutralValue f) = x
f(neutralValue f, x) = x
The general idea is that most of the axioms and properties are
with the operations, not the carrier sets of structures (as currently
done for old domains.) That entails some redesign of the
category and domain hierarchies. We didn't get around to finish
the conversion; plus Yue is no longer working in this area.
I had a rummage about in the sandbox you mentioned (written by Yueli about 3
years ago) and I did not come across any overall tutorial file (what I would
think of as top level documentation) I may have missed it. Did Yueli write
any thesis or anything like that?
unfortunately, no. What I have are internal reports we didn't to put
in shape that is publishable, even as technical reports.
At first glance it does look encouraging as the code to analyse the code
does seems to be written in SPAD, which hopefully shows that it can be done.
Yes, most of the code was written in Spad; some hooks into the parser was
needed, but the elaboration, and the whole static analysis is written in Spad.
(By the way, I used OpenAxiom in 2006 and 2008 for static analysis and
compiler courses so, there was precedent for writing the compiler stuff in
Spad. Some improvements were needed to make the whole experience palatable
though -- for example, that is why we have a Syntax domain, some form of
pattern matching, user-defined case operator, existential type, etc.)
When I look at the code (such as snippet below) it looks like the axioms are
coded differently, that is on a per operator basis?
Yes, I explained above many properties are with the operators, not the
carrier set -- Integer can be the carrier set for many monoidal structures.
snippet from:
http://sourceforge.net/apps/trac/open-axiom/browser/yli-sandbox/contrib/redec/operatorcats.spad?rev=2776
)abbrev category ASSOCOP AssociativeOperator
++ Axiom: associativity: rule op(a, op(b, c)) == op(op(a,b), c)
AssociativeOperator(T: SetCategory, op: Mapping(T, T, T)):Category
== MagmaOperator(T, op)
Any further clues for understanding the code appreciated, thanks,
The main trunk has the axioms integrated in codes. One of the reasons why
Yue used the old commentary style to write some of the axioms is that he
needed to analyse the entire algebra set (which he did), but he did
not have the time
to redesign the entire algebra hierarchy. After the positive
preliminary reports,
we headed for getting some results out (see the ISSAC 2011 paper); and
after that
he changed fields of studies.
-- Gaby
___
Axiom-mail mailing list
Axiom-mail@nongnu.org
https://lists.nongnu.org/mailman/listinfo/axiom-mail
Re: [Axiom-mail] A question about Axiom capabilities, Fwd: [fricas-devel] Abstract Vector Algebra
Given that there is no resources (or desire, as far as I can see) to change the structure of Axiom There is the desire. Axiom has a long term goal of introducing program-proof technology (either COQ or ACL2). ACL2 runs on the same lisp as Axiom. The plan is to load it into the Axiom image and make it support program proofs for spad code. I do not have the resources to attack this problem yet. I am still rewriting Axiom into literate form. However, I assure you that it is in Axiom's long-term goals, somewhere in the 30 year horizon. Look at http://axiom-developer.org (the Axiom home page) and see item (f), that's the program-proof goal. Tim Daly ___ Axiom-mail mailing list Axiom-mail@nongnu.org https://lists.nongnu.org/mailman/listinfo/axiom-mail
Re: [Axiom-mail] A question about Axiom capabilities, Fwd: [fricas-devel] Abstract Vector Algebra
This is probably not very practical, but I was just trying to do a thought experiment to investigate what would be required to have variables that range over domains that are not numbers. Actually, I wrote an NSF proposal to introduce indeterminate integers. This would be a first example of a special symbolic domain that would create arbitrary integers rather than actual integers. This is my approach to the Maple assume facility. I want to say that the uderlying domain is an indeterminate integer rather than assume x is an integer. This idea seems more in-line with Axiom's approach to computational mathematics. I'm working on creating a sort-of indeterminate matrix domain based on a prior question on this list so you can perform operations like (A B)^T = B^T A^T where A and B are indeterminate matrices. I will note that the NSF will not fund open source projects. Science can only occur if you are at a University. Sigh. Tim Daly ___ Axiom-mail mailing list Axiom-mail@nongnu.org https://lists.nongnu.org/mailman/listinfo/axiom-mail
Re: [Axiom-mail] A question about Axiom capabilities, Fwd: [fricas-devel] Abstract Vector Algebra
On 03/30/2013 06:25 PM, Martin Baker wrote: On 30/03/13 12:01, Ralf Hemmecke wrote: Unless you specify what solver you intend to write, it's probably an unsolvable task to write a general solver that works for all types of algebras. Agreed, but I was thinking more about doing it on a per-domain basis and building up gradually. So we start with a very simple algebra that we want to create a equation solver for, for example we might want to create an algebra domain based on this category: MyAlgebra() : Category with myOp1 : ($,$) - $ myOp2 : ($) - $ I don't quite understand. If you assume myOp1 to be commutative, then solving equations is quite a different task from when it is non-commutative. Where would you store all these axioms? If you mean equations solver then that includes also solving for (x,y) in x + y = 0. Or suppose your algebra is a ring. Do you want to write a solver for 7*x^5+y^3*x^4+2 = 0 i.e. finding all pairs (x,y) that fulfil this equation? Looks like you aim at a general term rewriting system. Ralf ___ Axiom-mail mailing list Axiom-mail@nongnu.org https://lists.nongnu.org/mailman/listinfo/axiom-mail
Re: [Axiom-mail] A question about Axiom capabilities, Fwd: [fricas-devel] Abstract Vector Algebra
Would anyone object if I ask a slightly wider question on this topic? It would be really nice if one could write an equation solver for a given algebra, I have often wanted to do that and I wonder if there is any general advise on this topic for Axiom? I guess what I am looking for is a way to have variables that represent a given algebra element. If I understand correctly variables are built in to an Axiom Expression but they are hard coded to be some form of number only. So I'm guessing that, to do this, one would not only need to define an algebra but a specific expression (coalgebra) domain to go with it and then some sort of rule solving logic? Martin Baker ___ Axiom-mail mailing list Axiom-mail@nongnu.org https://lists.nongnu.org/mailman/listinfo/axiom-mail
Re: [Axiom-mail] A question about Axiom capabilities, Fwd: [fricas-devel] Abstract Vector Algebra
It would be really nice if one could write an equation solver for a given algebra, I have often wanted to do that and I wonder if there is any general advise on this topic for Axiom? Well, would be nice, but think about the following. An algebra, which is a field. Depending on which equations you want to solve, there is need for completely different algorithms. Solve (ax+by=c,dx+ey=f) for x and y or ax^2+bx+c=0 for x. Add a new operation (diferentiation) making the algebra into a differential field, there are even more ways to come up with equations. Unless you specify what solver you intend to write, it's probably an unsolvable task to write a general solver that works for all types of algebras. Ralf ___ Axiom-mail mailing list Axiom-mail@nongnu.org https://lists.nongnu.org/mailman/listinfo/axiom-mail
Re: [Axiom-mail] A question about Axiom capabilities, Fwd: [fricas-devel] Abstract Vector Algebra
On 30/03/13 12:01, Ralf Hemmecke wrote: Unless you specify what solver you intend to write, it's probably an unsolvable task to write a general solver that works for all types of algebras. Ralf Agreed, but I was thinking more about doing it on a per-domain basis and building up gradually. So we start with a very simple algebra that we want to create a equation solver for, for example we might want to create an algebra domain based on this category: MyAlgebra() : Category with myOp1 : ($,$) - $ myOp2 : ($) - $ Then create an expression holder that is specific to that algebra: MyAlgebraExpression() : Exports == Implementation where Implementation == add Rep := Union(_ literalTerm : MyAlgebra, _ variableTerm : Symbol, _ myOp1Term : Record(left: $, right: $), _ myOp2Term : $_ ) bind : (Symbol,MyAlgebra,$) - $ canonicalForm : $ - $ decomposeMyOp1 : $ - ($,$) decomposeMyOp2 : $ - ($) Then create an equation solver that is also specific to that algebra: MyAlgebraEquation() : Exports == Implementation where Implementation == add Rep := Record(left: MyAlgebraExpression, right: MyAlgebraExpression) solveFor : (Symbol,$) - MyAlgebraExpression This would require 3 domains for every algebra that we wanted to be able to solve but why not have some separate common rule interpreter code. So MyAlgebraEquation domain would consist mostly of a set of substitution rules for that particular algebra? Martin ___ Axiom-mail mailing list Axiom-mail@nongnu.org https://lists.nongnu.org/mailman/listinfo/axiom-mail
Re: [Axiom-mail] A question about Axiom capabilities
Dear Tim, If you look at the matrixcookbook that Mike mentioned, the first 10 equations are: (A*B)^-1 = B^-1 * A^-1 (A*B*C...)^-1 = ...C^-1 * B^-1 * A^-1 (A^T)^-1 = (A^-1)^T (A+B)^T = A^T + B^T (A*B)^T = B^T * A^T (A*B*C...)^T = C^T * B^T *A^T (A^H)^-1 = (A^-1)^H (A+B)^H = A^H + B^H (A*B)^H = B^H * A^H (A*B*C...)^H = ...C^H * B^H * A^H Yes, I know this book very well. It would be indeed nice if Axiom could do such things in an abstract fashion. It seems like we could create a SymbolicMatrix algebra that could perform these manipulations with uninterpreted matrix symbols A, B, C with a special recognized symbol 'T'. I think it would be possible, however I expect representation of abstract matrix algebra to be much more complicated than the vector algebra stuff. There are transposes, conjugates, inverses, traces, determinants and much more. One would need to have a way to encode all these operation unevaluated. These matrices could have actual values which, for certain operations are ignored, so that (A*B)^-1 = B^-1 * A^-1 but for other operations would be evaluated as in: eval(B^-1 * A^-1) giving the actual matrix result shown element by element. Yes, of course this should play together with usual (dense or sparse) matrices nicely. Doesn't make the task easier though. And do we want define abstract matrices with or without shape information? An additional enhancement would be to make a SymbolicMatrixCategory so that there could be specific domains such as GeneralSymbolicMatrix, SymmetricSymbolicMatrix, UpperTriangularSymbolicMatrix, DiagonalSymbolicMatrix, etc which could exploit certain matrix-level properties at the symbolic level. Maybe someone should indeed try. I don't think I find the time to try this soon. It occurred to me that component-free geometric algebra might be easier to start with anyway. There is a nice book on the topic: https://sites.google.com/site/grassmannalgebra/ https://sites.google.com/site/grassmannalgebra/thegrassmannalgebrabook which is accompanied by a Mathematica Package (that I never tried so far): https://sites.google.com/site/grassmannalgebra/thegrassmannalgebrapackage The algebra in there is as far as I remember not done in an abstract way, but with explicit bases. -- Raoul ___ Axiom-mail mailing list Axiom-mail@nongnu.org https://lists.nongnu.org/mailman/listinfo/axiom-mail
Re: [Axiom-mail] A question about Axiom capabilities, Fwd: [fricas-devel] Abstract Vector Algebra
See: https://www.researchgate.net/publication/220915895_Rule-Based_Simplification_in_Vector-Product_Spaces There has been some work done on this subject in one of the Axiom forks: -- Forwarded message -- From: someone someb...@bluewin.ch Date: 27 October 2012 21:07 Subject: Re: [fricas-devel] Abstract Vector Algebra To: fricas-de...@googlegroups.com I started making a small package for component-free vector algebra. It is based on the work Rule-Based Simplification in Vector-Product Spaces written by Songxin Liang and David J. Jeffrey. I made some real progress with the code. In the most up to date version it can do many non-trivial problems. For example: (122) - simplify( (va-vd)^(vb-vc) + (vb-vd)^(vc-va) + (vc-vd)^(va-vb) - 2*(va^vb + vb^vc + vc^va) ) (122) 00 Type: VectorAlgebra(Integer) I attached the code as well as the examples and some other tests. You can find the most recent versions of all files in the github repo at: https://github.com/raoulb/fricas_code/blob/vectoralg/vecalg/ -- You received this message because you are subscribed to the Google Groups FriCAS - computer algebra system group. To post to this group, send email to fricas-de...@googlegroups.com. To unsubscribe from this group, send email to fricas-devel+unsubscr...@googlegroups.com. For more options, visit this group at http://groups.google.com/group/fricas-devel?hl=en. -- Forwarded message -- From: Raoul rao...@bluewin.ch Date: 29 March 2013 19:42 Subject: Re: [Axiom-mail] A question about Axiom capabilities To: u1204 d...@axiom-developer.org, axiom-mail@nongnu.org Dear Tim, If you look at the matrixcookbook that Mike mentioned, the first 10 equations are: (A*B)^-1 = B^-1 * A^-1 (A*B*C...)^-1 = ...C^-1 * B^-1 * A^-1 (A^T)^-1 = (A^-1)^T (A+B)^T = A^T + B^T (A*B)^T = B^T * A^T (A*B*C...)^T = C^T * B^T *A^T (A^H)^-1 = (A^-1)^H (A+B)^H = A^H + B^H (A*B)^H = B^H * A^H (A*B*C...)^H = ...C^H * B^H * A^H Yes, I know this book very well. It would be indeed nice if Axiom could do such things in an abstract fashion. It seems like we could create a SymbolicMatrix algebra that could perform these manipulations with uninterpreted matrix symbols A, B, C with a special recognized symbol 'T'. I think it would be possible, however I expect representation of abstract matrix algebra to be much more complicated than the vector algebra stuff. There are transposes, conjugates, inverses, traces, determinants and much more. One would need to have a way to encode all these operation unevaluated. These matrices could have actual values which, for certain operations are ignored, so that (A*B)^-1 = B^-1 * A^-1 but for other operations would be evaluated as in: eval(B^-1 * A^-1) giving the actual matrix result shown element by element. Yes, of course this should play together with usual (dense or sparse) matrices nicely. Doesn't make the task easier though. And do we want define abstract matrices with or without shape information? An additional enhancement would be to make a SymbolicMatrixCategory so that there could be specific domains such as GeneralSymbolicMatrix, SymmetricSymbolicMatrix, UpperTriangularSymbolicMatrix, DiagonalSymbolicMatrix, etc which could exploit certain matrix-level properties at the symbolic level. Maybe someone should indeed try. I don't think I find the time to try this soon. It occurred to me that component-free geometric algebra might be easier to start with anyway. There is a nice book on the topic: https://sites.google.com/site/grassmannalgebra/ https://sites.google.com/site/grassmannalgebra/thegrassmannalgebrabook which is accompanied by a Mathematica Package (that I never tried so far): https://sites.google.com/site/grassmannalgebra/thegrassmannalgebrapackage The algebra in there is as far as I remember not done in an abstract way, but with explicit bases. -- Raoul ___ Axiom-mail mailing list Axiom-mail@nongnu.org https://lists.nongnu.org/mailman/listinfo/axiom-mail examples.input Description: Binary data tests.input Description: Binary data VA.spad Description: Binary data ___ Axiom-mail mailing list Axiom-mail@nongnu.org https://lists.nongnu.org/mailman/listinfo/axiom-mail
Re: [Axiom-mail] A question about Axiom capabilities
I've been looking for some CAS that provided significant symbolic matrix manipulations, including matrix calculus. Maybe you should look at SymPy. They have some (although limited) support for symbolic matrix expressions and computations. SymPy documentation: http://docs.sympy.org/0.7.2/modules/matrices/expressions.html http://docs.sympy.org/0.7.2/modules/matrices/immutablematrices.html And various Blog posts: http://planet.sympy.org/ http://matthewrocklin.com/blog/ Hope this helps. ___ Axiom-mail mailing list Axiom-mail@nongnu.org https://lists.nongnu.org/mailman/listinfo/axiom-mail
Re: [Axiom-mail] A question about Axiom capabilities
Mike, It would be possible to build a Domain (e.g. SymbolicMatrix) that had elements which were symbolic, e.g. the symbol A from the Domain would be considered an uninterpreted SymbolicMatrix. So you could write something like: (A*B)^-1 and get the result B^1 * A^-1 Indeed, the SymbolicMatrix could be a matrix of symbols such as A := [[a[1,1],a[1,2]],[a[2,1],a[2,2]]] +- -+ | a a| | 1,11,2 | | | | a a| | 2,12,2 | +- -+ but some operations would be only on an uninterpreted A matrix and some operations would be applied elementwise. The 'sum' question you sent could be handled in a similar way. I will look at what this would take for equations 1-10 in the cookbook you sent. Tim Daly ___ Axiom-mail mailing list Axiom-mail@nongnu.org https://lists.nongnu.org/mailman/listinfo/axiom-mail
Re: [Axiom-mail] A question about Axiom capabilities
Raoul, I will look at your code. Thanks. Tim Daly d...@axiom-developer.org ___ Axiom-mail mailing list Axiom-mail@nongnu.org https://lists.nongnu.org/mailman/listinfo/axiom-mail
Re: [Axiom-mail] A question about Axiom capabilities
Raoul, If you look at the matrixcookbook that Mike mentioned, the first 10 equations are: (A*B)^-1 = B^-1 * A^-1 (A*B*C...)^-1 = ...C^-1 * B^-1 * A^-1 (A^T)^-1 = (A^-1)^T (A+B)^T = A^T + B^T (A*B)^T = B^T * A^T (A*B*C...)^T = C^T * B^T *A^T (A^H)^-1 = (A^-1)^H (A+B)^H = A^H + B^H (A*B)^H = B^H * A^H (A*B*C...)^H = ...C^H * B^H * A^H It seems like we could create a SymbolicMatrix algebra that could perform these manipulations with uninterpreted matrix symbols A, B, C with a special recognized symbol 'T'. These matrices could have actual values which, for certain operations are ignored, so that (A*B)^-1 = B^-1 * A^-1 but for other operations would be evaluated as in: eval(B^-1 * A^-1) giving the actual matrix result shown element by element. An additional enhancement would be to make a SymbolicMatrixCategory so that there could be specific domains such as GeneralSymbolicMatrix, SymmetricSymbolicMatrix, UpperTriangularSymbolicMatrix, DiagonalSymbolicMatrix, etc which could exploit certain matrix-level properties at the symbolic level. This isn't exactly what Mike was originally asking but I think that Axiom ought to be able to symbolically compute the equations in the handbook. Tim Daly ___ Axiom-mail mailing list Axiom-mail@nongnu.org https://lists.nongnu.org/mailman/listinfo/axiom-mail
Re: [Axiom-mail] A question about Axiom capabilities
I can send you a copy I have downloaded, but I will send that email just to you as I don't feel like spamming the mailing list On Wed, Feb 27, 2013 at 7:58 PM, u1204 d...@axiom-developer.org wrote: I tried the cookbook link you posted http://orion.uwaterloo.ca/~hwolkowi/matrixcookbook.pdf which fails due to access rights. I looked at the home page for http://orion.uwaterloo.ca/~hwolkowi which has a link to an offsite copy of the cookbook but the page refuses to load. Tim Daly ___ Axiom-mail mailing list Axiom-mail@nongnu.org https://lists.nongnu.org/mailman/listinfo/axiom-mail
Re: [Axiom-mail] A question about Axiom capabilities
Mike, These are interesting ideas but I don't know how to do what you want in the current version of Axiom. Where is this Matrix Cookbook you mention? Tim Daly ___ Axiom-mail mailing list Axiom-mail@nongnu.org https://lists.nongnu.org/mailman/listinfo/axiom-mail
Re: [Axiom-mail] A question about Axiom capabilities
The Matrix Cookbook is available online at: http://orion.uwaterloo.ca/~hwolkowi/matrixcookbook.pdf It is simply a collection of matrix properties which are proved elsewhere. I have done enough matrix calculus to know a basic approach (very similar to the derivatives for indexed tensors in Maxima) if it has to be implemented. The single entry matrix is sort of a generalization of the Kronecker delta function used in matrix calculus. On Tue, Feb 26, 2013 at 6:25 PM, u1204 d...@axiom-developer.org wrote: Mike, These are interesting ideas but I don't know how to do what you want in the current version of Axiom. Where is this Matrix Cookbook you mention? Tim Daly ___ Axiom-mail mailing list Axiom-mail@nongnu.org https://lists.nongnu.org/mailman/listinfo/axiom-mail
Re: [Axiom-mail] A question about Axiom capabilities
One other note - I forgot a logarithm in my example: D( ln( sum(p[k]*multivariate_normal(mu[k], Sigma), k) ) -- ... On Tue, Feb 26, 2013 at 8:39 PM, Mike Valenzuela mickle.mo...@gmail.comwrote: The Matrix Cookbook is available online at: http://orion.uwaterloo.ca/~hwolkowi/matrixcookbook.pdf It is simply a collection of matrix properties which are proved elsewhere. I have done enough matrix calculus to know a basic approach (very similar to the derivatives for indexed tensors in Maxima) if it has to be implemented. The single entry matrix is sort of a generalization of the Kronecker delta function used in matrix calculus. On Tue, Feb 26, 2013 at 6:25 PM, u1204 d...@axiom-developer.org wrote: Mike, These are interesting ideas but I don't know how to do what you want in the current version of Axiom. Where is this Matrix Cookbook you mention? Tim Daly ___ Axiom-mail mailing list Axiom-mail@nongnu.org https://lists.nongnu.org/mailman/listinfo/axiom-mail
