Remodel derivation mechanism

[sebasguts]

Since several issued with the derivation mechanism popped up recently, there should be a complete remodeling of the derivation mechanism. The following topics should be adressed:

• Derivations should only happen when the category is finalized, not on the fly. A category is not guaranteed to function if not finalized anyway, so this is not a breaking change in any sense. Nevertheless, it is a change in the behaviour of categories and might need to different derivations triggered then now.

• The previous point can lead us to getting rid of the final derivations all together. Each derivation should now possibly contain a set of exclusions, in addition to a set of requirements. This leads to the fact that all derivations will be like the current final derivations.

• Derivations should be able to dependend on specific other derivations, not only on primitives. Some derivations make assumptions about how other primitives are derived. Those have to be installed in a group. It might not be flexible enough to actually group them, since some derivations in a group might work without the others in the group, and others wont.

To adress those changes, the following changes in the CAP kernel are necessary:

• [ ] Change the API for the derivations to be compatible with the one for final derivations, and remove final derivations.
• [ ] Change the method derivation graph to be able to work with the new requirements
• [ ] Change the algorithm that computes the derivations to compute a maximal tree in the derivation graph, where the term maximal might be still need discussion.

This issue is meant to track progress on this topic, and will be updated in the next few days, while I am working on implementing this feature.

[sebastianpos]

Let me explain how the final derivations are used at the moment and why they have to be enhanced.

When you take a look at the final derivations in the DerivedMethods.gi file, you will see basic operations like IsomorphismFromFiberProductToKernelOfDiagonalDifference. These are natural isomorphisms between a universal object and a concrete construction of this universal object. By the CAP's final derivation mechanism, these natural isomorphisms are set to the identity assuming the user called Finalize and did not provide his own construction of this universal object. In this way, CAP's final derivation mechanism is able to coherently deal with interdependencies of derivations. In particular, the derivation of ProjectionInFactorOfFiberProduct and UniversalMorphismIntoFiberProduct via direct products and equalizers (suggested in this pullrequest) could also be dealt with in this way by introducing a basic operation like IsomorphismFromFiberProductToEqualizerOfDirectProductDiagram and using it within the implementations of ProjectionInFactorOfFiberProduct and UniversalMorphismIntoFiberProduct.

However, a problem arises when there simply is no such natural isomorphism, e.g., in the case of weak universal objects. I can derive a weak fiber product by employing lots of different constructions, like

1. using FiberProducts,
2. using DirectSums and Kernels,
3. using DirectSums and WeakKernels,

and all of these possible constructions can yield non-isomorphic realizations of weak fiber products. There simply are no natural isomorphisms mediating between these different constructions of weak fiber products. However, I want to be able to teach CAP all of these 3 derivations. This is why an enhancement is needed.

[zickgraf]

Once https://github.com/homalg-project/CAP_project/pull/1699 is merged, I think this issue can be closed, after more than 6 years!

Changes implemented over the last years:

• Derivations only happen when the category is finalized.
• Final derivations can be grouped into bundles.
• The mechanisms for final and for ordinary derivations now both reside in Derivations.gi and share a lot of code.

Changes not implemented:

• Final and ordinary derivations are still different concepts.
• Final derivations are applied blindly in the order in which they are added to CAP.

In particular, there is no mechanism for finding a maximal tree of derivations. However, such a mechanism would come with its own drawbacks:

• The current mechanism is easy to explain: First apply as many ordinary derivations as possible, afterwards try to apply final derivations. A mechanism finding a maximal tree of derivations would be much more difficult to explain.
• The current mechanism seems to produce stable results in the sense that adding new derivations does usually not affect whether existing derivations are triggered. When finding a maximal tree of derivations however, I can imagine a situation where adding new derivations (e.g. by loading another package) suddenly leads to completely different derivations being triggered.

Summing up, I think the current state of the derivation mechanism is future-proof and covers the original problems given in this issue well enough to close this issue as completed.

[mohamed-barakat]

Wonderful, thank you very much.