Thanks for the very thoughtful and encouraging comments. A big hurdle to starting any actual work on this has always been to see how well received the category framework would be.
Florian is also struggling with some issues of canonicity of the definitions, so your insights might be helpful to him. His issues have more to do with presentation though, while yours has to do with dynamic resolution (but it might be that a canonical presentation could be based on your resolution). In any case, I do not want to distract the thread away from the topic of Nicolas' ticket, and the fact that he has implemented something that works beyond a prototype, unlike any of us. Paul On Wed, Mar 12, 2014 at 8:28 AM, Simon King <simon.k...@uni-jena.de> wrote: > Hi Paul, hi Mark, > > On 2014-03-12, Mark Shimozono <msh...@math.vt.edu> wrote: > >> Instead, I would advocate using a declarative domain specific language > built for semi-formalizing > >> mathematics > > > > The appeal of this paradigm is evident. It addresses > > a fundamentally important issue: how to structure the development > process to > > encourage the code to reflect the mathematics in the most transparent > fashion. > > > > Alas, it appears that this is a fair distance from being implemented > > in python, and many important details need to be worked out. > > This could actually relate to another suggestion that I made on the > ticket, and like to mention here. > > A substantial part of Nicolas' approach deals with the problem > of finding the correct class which Cs().SomeAxiom() will be an instance > of. For instance, mathematical results imply that > Rings().Division().Finite() should be an instance of the FiniteFields > class (resp. Fields.Finite---actually I like nested classes and find > them rather easy to understand and transparent). > > All the logic---including the mathematical reasoning---is *implicit* in the > code, by chosing names and by setting some attributes. But in the end of > the day, we have a machinery that returns classes. Hence, what we in > fact have is (close to) a metaclass. > > This metaclass must be fairly intelligent, as it implements mathematical > results (main example: Wedderburn's theorem). Part of my criticism of > Nicolas' approach is that the mathematical reasoning somehow happens in > the cloud: There is no single spot that does the reasoning *explicitly*, > but it is a dynamical process that seemingly does the right thing, but > only *implicitly*. > > As I have demonstrated (as a proof-of-concept), the required mathematical > reasoning can be done by computations in the "boolean polynomial ring" > (which is implemented in Sage). > > Hence, one could think of implementing a metaclass for category classes, > that acts as a database and knows > - where existing category classes can be found (such as: "the FiniteFields > class is in sage.categories.finite_fields"), > - when and how the category class has to be created dynamically, > - what structure is needed to apply an axiom (for applying the > "Distributive" axiom, one needs that the category in question both is > a sub-category of multiplicative and additive magmas), > - how to find a "normalised" set of axioms that define a category. > Really, the fact that ring*division*finite is the same as > ring*division*commutative*finite boils down to normal form > computations in a boolean polynomial ring. > > And again, I have to admit that it isn't close to being implemented. > Thus, I'd prefer to have something that already works, which is Nicolas' > implementation. > > > In the meantime, we all need a version of sage to work with... > > +1 > > Best regards, > Simon > > > -- > You received this message because you are subscribed to the Google Groups > "sage-combinat-devel" group. > To unsubscribe from this group and stop receiving emails from it, send an > email to sage-combinat-devel+unsubscr...@googlegroups.com. > To post to this group, send email to sage-combinat-de...@googlegroups.com. > Visit this group at http://groups.google.com/group/sage-combinat-devel. > For more options, visit https://groups.google.com/d/optout. > -- You received this message because you are subscribed to the Google Groups "sage-devel" group. To unsubscribe from this group and stop receiving emails from it, send an email to sage-devel+unsubscr...@googlegroups.com. To post to this group, send email to sage-devel@googlegroups.com. Visit this group at http://groups.google.com/group/sage-devel. For more options, visit https://groups.google.com/d/optout.
