#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 SimonKing):
Dear Nicolas,
it seems to me that I still don't see exactly where the theoretical model
ends
and where the implementation details start. Also, I am not sure if we talk
about the same when we both say "consistency". Therefore I try to
formulate
what I think you claim, asking you to correct where I am wrong, and also I
give you an example, asking you to explain to me how to implement it in
your
model and how your model detects the inconsistency in my example.
First, a pledge: Could you please push your latest commits providing the
latest documentation?
We agree that we have an acyclic digraph, the nodes being categories,
i.e.,
instances of category classes, the arrows being labelled with axioms that
are
being applied to the start point of the arrow and result in the end point
of
the arrow.
We agree that we should single out a spanning tree. It is useful, e.g.,
for
getting a proper inheritance of Python classes (think of parent and
element
classes).
Questions:
- Do you claim that the choice of a spanning tree doesn't matter at all?
Would any spanning tree work?
- Do you claim that all theorems about categorial identities are and will
in
future be ''asymmetric'', so that they give a natural choice of a
spanning
tree?
Now let's assume we have chosen a spanning tree, and see how that choice
can be/is implemented.
For specifying a spanning tree (or rather: forest) in an acyclic digraph,
it
is sufficient to choose one incoming arrow, for any node that has incoming
arrows. Agreed? This is done by the explicit or implicit definition of
`C._base_category_class_and_axiom`.
In addition to that (and this is where I think the implementation deviates
from the theoretical model), you say that at each node one should
additionally mark the outgoing
arrows that belong to the spanning tree: The outgoing arrows belonging to
the
spanning tree result in class attributes, the other outgoing arrows result
in
(cached) subcategory methods. Is this a correct description? And somehow
there
are these `<Axiom name>_extra_super_categories` methods, which relate
with the non-spanning-tree-outgoing-arrows as well, right?
This gives rise to a couple of questions:
- Of course, if you do specify the spanning tree both on incoming and
outgoing
arrows, then this specification should be consistent. Is this what you
mean
when you talk about a "consistent choice"? Then I agree that it is a
purely
local problem. I don't think that one needs to test it in the
`TestSuite`,
because you already test it in `__classget__`.
- ''Why'' do you think that one needs to specify the spanning tree twice
(incoming and outgoing)?
Related with the second question: I know that in your current
implementation,
one can not both define `DivisionRings.Finite = FiniteFields` and
`Fields.Finite = FiniteFields`---but it seems to me that this is ''only''
because you chose to give the same data twice. So, can you explain '''in
the
theoretical model''' why it is illegal to assign `DivisionRings.Finite =
FiniteFields` and why it is needed to use all this
`Finite_extra_supercategories` and cached subcategory methods magic?
Or is it just because of the implementation? In this case, please
elaborate (or
give a pointer to a place where you did elaborate already) why providing
the
same data twice is important and an implementation is hardly doable
without the duplication of information.
Now I come to an example.
Assume we have a category class `As`, and axioms `B, C, D, E, F` that can
all
be called on `As()`. In principle, any subset of the axioms can be
successively applied to `As()` in any order.
If I was to implement it, I would provide class attributes `As.B, As.C,
...,
As.F` whose values are category-classes-with-axiom. Each of these classes
has
`_base_category_class_and_axiom = (As, 'B'/'C'/.../'F')`. Do you agree
that
this is what one should do?
Next, there is two axioms that needs to hold for our category-with-axiom
framework: Applying axioms is commutative, and applying axioms is
idempotent. Hence, we need `As().B().C()==As().C().B()`. In other words,
`As().B().C().__class__.__base__` has two incoming arrows, and we need to
pick
one of them (say, the one labelled "C") in order to specify a tree. In
addition to that, you say that one has to do something special with
`As().C().B`: It can not be a class axiom but should be a subcategory
method
or so (I am still not buying why this is needed).
So, where are we? We have some categories, that are essentially labelled
by
subsets (not ordered!) of axioms "B",...,"F", and by specifying a spanning
tree we obtain labels that are ''ordered'' subsets of axioms "B",...,"F".
Next, William Stein proves that `As().B().C()==As().E().F()`. Now, we can
of
course change the code so that `As().B().C` becomes a subcategory method
returning `As().E().F()`, and the old class `As.B.C` is removed.
But the point I want to make: This is not enough. We still can apply
axioms
"B", "C" and "D" to `As().E().F()`. But we should have
{{{
As().E().F().D().B().C()
== As().B().C().E().F().D() # commutativity
== As().E().F().E().F().D() # William's theorem
== As().E().E().F().F().D() # commutativity
== As().E().F().D() # idempotency
== As().D().E().F() # I guess you are likely to choose the
# spanning tree by applying axioms in
# lexicographic order.
}}}
So, a fix is needed! This is what ''I'' mean when I speak about
consistency,
and this is what I think is a difficult local--global problem.
Questions:
1. Assume that a developer would simply make `As().B().C()` return
`As().E().F()`. This would be a bug, by the above reasoning. Would the
category-with-axiom framework detect this bug and raise an error on
the
attempt to create `As().E().F().D().B().C()`? Can you demonstrate it
in
the above example, and can you prove that it will always detect the
bug?
2. What does a developer need to do to fix the code?
3. How can a developer determine what needs to be done to fix the code?
In
the example above, I demonstrated one case that needed to be fixed. Do
you
really require that the developer draws the whole category digraph on
a
sheet of paper and traces (similar to the above reasoning) what has to
be
done with the chosen spanning tree after merging two of its nodes?
4. Do you provide any tool that tells the developer what needs to be
done?
For the record: I think commutative algebra can be used to detect that
there
is a bug and could make a suggestion on how to fix the bug. Ceterum
censeo: In
the long run (on a different ticket) a database of category classes can
use
commutative algebra to deal with the above local--global problem so that
developers don't need to think about it when coding. The axioms shouldn't
be
provided by coding nested classes or adding direct assignment of class
attributes into the code, since this would be the job of the database.
--
Ticket URL: <http://trac.sagemath.org/ticket/10963#comment:443>
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.
