#10963: More functorial constructions
-------------------------------------+-------------------------------------
Reporter: nthiery | Owner: stumpc5
Type: enhancement | Status: needs_review
Priority: major | Milestone: sage-6.1
Component: categories | Resolution:
Keywords: days54 | Merged in:
Authors: Nicolas M. Thiéry | Reviewers: Simon King, Frédéric
Report Upstream: N/A | Chapoton
Branch: | Work issues:
public/ticket/10963 | Commit:
Dependencies: #11224, #8327, | eb7b486c6fecac296052f980788e15e2ad1b59e4
#10193, #12895, #14516, #14722, | Stopgaps:
#13589, #14471, #15069, #15094, |
#11688, #13394, #15150, #15506 |
-------------------------------------+-------------------------------------
Comment (by nthiery):
Replying to [comment:429 SimonKing]:
> OK, but then we'd like to have 121 more implementations of
`an_instance()`...
It would be a good thing to have an_instance for all categories at
some point. Hopefully we can do that by providing just a couple
generic implementations.
Now, I am actually surprised that you get that many. Can you give a
couple examples where this fails? Have you tried the category_sample
function?
> Well, the reason for the complaint is that the axioms `Blue` and
`Unital` do not commute. But applying axioms ''has'' to commute. Hence,
the feature is not "desirable but non-implemented", but it is
"mathematically illegal".
No. See below.
> Consistency is a global property. Hence, I think there is no way around
to consider ''all'' category classes at once when testing consistency.
I am not sure. If there is some inconsistency, you can always work in
a sublattice (with bottom) that contains all the involved categories,
rather than the full lattice. And I would not be surprised if it could
be argued that one could always choose such a sublattice with a
category that is actually implemented in Sage. But anyway, let's not
pollute more this thread; we can discuss this later.
> - Create an ideal in this ring, whose generators are given by
mathematical results such as Wedderburn's. Compute the Gröbner basis. This
Gröbner basis could be computed once, stored, and then loaded at Sage
startup time. Hence, Sage startup would not suffer from an expensive
Gröbner basis computation, it only is loading a fixed result.
Right. But Sage's startup would still require being able to manipulate
such a Gröbner basis in one form or the other. And one needs to make
sure the Gröbner basis is consistent with all the code (that is Sage's
compilation might require a Gröbner basis computation). And that it
can be extended dynamically if users introduce new categories in their
own library.
I am certainly not saying it's not doable. But it introduces some
complexity which has to be well motivated.
> - When creating a category class, the Gröbner basis helps to provide
this class with the available axiomatic constructions (this is what you do
with lazy imports and with `SubcategoryMethods`), and also determines a
default construction for this class (this is the
`_base_category_class_and_axiom` attribute). Commutative algebra ensures
consistency of this local information. This would be implemented by a
meta-class for `Category`.
> This would be my approach to add more rigour to your category-with-axiom
model, and replace handmade choices of default constructions by something
that scales better.
Sorry, I can't resist; let me use the very argument that soo many
people have raised when saying that all that category stuff was just
overdesign. «Before introducing non trivial design to solve a scaling
issue, one needs to be sure there is one in practice». So far, I
haven't had a single time where I got bothered by that.
> > Since every category class is supposed to be TestSuit'ed, we should
> > cover all categories this way. Do you think we would get a global
> > enough view?
>
> No.
Can you give me a sketch of scenario where this would fail?
> > And I believe that I have no merit in that. I haven't proven it
> > formally yet, but I am pretty much convinced that as long as the two
> > following specifications (which I have now described in detail in the
> > documentation) are satisfied:
> >
> > - Tree structure on the classes
>
> Which I totally don't like!
>
> Namely, as a consequence, you need to treat `DivisionRings.Finite`
different from `Fields.Finite`: The latter is a (lazily imported) class
stored as a class attribute, the former is a cached method obtained from
Set() and will ''only'' work on instances, not on classes. This asymmetry
is unfortunate, and I think using a metaclass that works with standard
monomials corresponding to default axiomatic constructions is a nice way
to make the implementation symmetric.
>
> You see, if a developer wants to implement a new mathematical theorem on
equality of two axiomatic constructions, then your model is a bit awkward:
(S)he needs to pick one of the constructions to become a cached method on
instances, while the other stays a class attribute. But which of them?
Doing the wrong choice would mean subtle inconsistencies resulting in
difficult to find bugs.
No I don't see.
For Fields vs Division rings, the asymmetry is *very* natural. You put
the class in Fields.Finite, because it's about stuff valid for finite
fields. And you put in DivisionRings the theorem which tells you that
in the context of division rings, the "Finite" axiom implies the
"commutative" axioms.
Note also that if you would do the converse (put the class in
DivisionRings), you would see *immediately* the error: first you would
not know what to put in Fields.Finite_extra_super_categories. And
second DivisionRings().Finite() would not coincide with
Fields().Finite(); and this is the first thing you would test. Nothing
"subtle".
The same happened in every example of mathematical theorem I
implemented. And I believe this is a general feature; each time, the
theorem is telling you that, within a given category C, satisfying a
given axiom gives you more structure i.e. you land in a subcategory.
So, until I am given a concrete example where it's actually awkward to
put the mathematical theorem in one side rather than the other, I'll
consider this as a non issue.
> It seems obvious to me that we want that all axiomatic constructions can
be implemented in the same way, and that there is no danger of wrong
choices, because all choices will be made automatic by a method that is
proven to yield well-defined results (namely: Computing normal forms using
Gröbner bases).
I believe, and will work on proving formally, that the current
implementation is perfectly well-defined and gives normal forms.
> In other words: There is a tree structure in the set of standard
monomials. We shouldn't force the developer to put the same tree structure
''manually'' into the class definitions.
Maybe not. Or maybe yes. I agree there is a small inconvenient with
that tree structure because you have to make a choice between putting
stuff in C.A.B or C.B.A (it's not so bad because I believe you can
locally make whatever choice you want). And if forces to create a few
extraneous empty categories (really not that many).
But before ruling out the tree design choice, one needs to make sure
there is an alternative design choice that has:
- a syntax at least as good
- a similar performance
- a robustness at least as good
- someone willing to take the time to implement it
Anyway, I read you agree that this is all for a later ticket, right?
Can you please move the discussion to a different ticket? This ticket
is already way too cluttered for people that will try to read the
discussion later.
> I think we at least want a degree order, so that applying three axioms
will always be preferred over applying four axioms to get the same result.
I'd rather not impose any limitation if there is no good reason for
it. We should put the code wherever it's most natural mathematically
to put it.
> Well, in the case of `Blahs.Blue.Unital`, you did wrong. I don't know if
it was on purpose that you did wrong, but your example shows something
that should never happen, namely axioms that do not commute.
No I did not do wrong. It does demonstrates *on
purpose* a *missing feature*: namely that you currently can't use the
Blue_extra_super_categories mechanism in the category where the Blue
axiom is defined. You can also see it as a demonstration of a
*specified* limitation of the current specification: a category that
*defines* an axiom also has to *implement* it.
Cheers,
Nicolas
--
Ticket URL: <http://trac.sagemath.org/ticket/10963#comment:431>
Sage <http://www.sagemath.org>
Sage: Creating a Viable Open Source Alternative to Magma, Maple, Mathematica,
and MATLAB
--
You received this message because you are subscribed to the Google Groups
"sage-trac" 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/sage-trac.
For more options, visit https://groups.google.com/groups/opt_out.
