Martin Baker wrote: > > What I would like to see is the powerful capabilities in FriCAS/Axiom > for equation solving and so on in "classic mostly commutative algebra" > to be packaged in such a way that they could be adapted for other > axiomatic systems. > > Most useful to me would be the ability to write equation solvers in > matrix, quaternion, Clifford algebras where the variables represent, not > real/complex numbers, but elements of these algebras.
I think lot can be done in this direction. However, it is a big topic, so let me postpone it a bit. > Another example is that I am writing code for different types of logic > (Heyting, frames, etc.) and this includes domains for poset, lattice and > so on. > > I have documented this here: > > http://www.euclideanspace.com/prog/scratchpad/mycode/discrete/logic/ > > or, if you don't like documentation, you can go straight to the code here: > > https://github.com/martinbaker/multivector/blob/master/logic.spad > > So could you include this in any changes you are making, in particular: > > 1) Include poset, frame, lattice, etc. into the category hierarchy. > 2) Generalise equation solving capabilities to allow use for other > structures. > 3) Include axioms in category definitions. Concerning logic.spad, I think it needs some changes/corrections: 1) In Preorder the Axiom lines mention '<=' as operation name but the only exports 'implies'. Actually, in FriCAS the 'PartialOrder' category represents the same concept (unlike many expositions of orders 'PartialOrder' does not assume weak antysymmetry). 2) AFAICS usual definiton of lattice does on include top and bottom elements. If they are present we have special kind of lattice (Wikipedia calls it bounded lattice, but other names also seem to be in common use). 3) IMO FiniteLattice should be a category. Such lattice automatically has top and bottom elements. 4) I am not sure if we want to use name 'true' for top element of a lattice (and 'false' for bottom). It is natural in context of logic, but not so natural in other contexts. 5) It is not clear for me what you want to represnt by Frame. Namely, due to associativity in a lattice there is naturally defined join and meet for any finite subset. IIRC frames used in logic have a bit richer structure than what you define in Frame. 6) Once we have Lattice current Logic should inherit from Lattice. Given that we want to represnt nonclassical logics we need separate BooleanAlgebra for classical case. So I think we should have something like: MeetSemilattice JoinSemilattice | | / | | V / V | BoundedMeetSemilattice / BoundedJoinSemilattice | \ / | V \ / | Lattice <--------------X | \ \ V ---------------------- > ---> BoundedLattice \ / | \ / V \ / Logic \ / | DistributiveLattice / | \ / | BoundedDistributiveLattice | \ | \ V BooleanAlgebra -- Waldek Hebisch [email protected] -- You received this message because you are subscribed to the Google Groups "FriCAS - computer algebra system" group. To unsubscribe from this group and stop receiving emails from it, send an email to [email protected]. To post to this group, send email to [email protected]. Visit this group at http://groups.google.com/group/fricas-devel. For more options, visit https://groups.google.com/d/optout.
