CAP_project
CAP_project copied to clipboard
Compile AdelmanCategory( ... ) as Wrapper( Op( Freyd( Op( Freyd( ... ) ) ) ) )
I would also suggest the other order Wrapper( Freyd( Op( Freyd( Op( ... ) ) ) ) ).
Does this issue mean: Make a compilation of Wrapper( Op( Freyd( Op( Freyd( ... ) ) ) ) work?
My point is that the equivalence of Adel( A ) and Freyd( Freyd( A^op)^op ) is mathematically non-trivial. Thus, I would not regard a compiled version of Wrapper( Op( Freyd( Op( Freyd( ... ) ) ) ) as "being the Adelman category".
My naive idea was: The wrapper category should use this non-trivial equivalence to translate between the data structures of AdelmanCategory( ... ) and Op( Freyd( Op( Freyd( ... ) ) ) ), so that Wrapper( Op( Freyd( Op( Freyd( ... ) ) ) ) ) actually behaves like and compiles to AdelmanCategory( ... ). Do you think this is feasible?
I think I'm simply not aware of the capabilities of Wrapper categories. My naive thoughts on this project were the following: your compiler gets as an input
- the code of
Op( Freyd( Op( Freyd( ... ) ) - the code that implements the non-trivial equivalence (in both directions) with the data structures of Adelman objects and Adelman morphisms
and outputs a compiled category whose algorithms somehow look like a compiled version the Adelman category.
But maybe the Wrapper categories somehow merge 1) and 2) into a single category, and you are going to simply compile that category?
In any case, I would suspect that during this process, several identites and zero morphisms are going to blow up the objects, and the only way to get rid of them would be applying simplifications that somehow need to be aware of the big picture (e.g., just looking at the underlying matrix code and applying equalities of matrices could never get rid of stuff that blows up the representation of an object).
But maybe the
Wrappercategories somehow merge 1) and 2) into a single category, and you are going to simply compile that category?
Exactly, WrapperCategory gets the code from your point 2) and thus CompilerForCAP does not have to do anything special :-)
In any case, I would suspect that during this process, several identites and zero morphisms are going to blow up the objects, and the only way to get rid of them would be applying simplifications that somehow need to be aware of the big picture (e.g., just looking at the underlying matrix code and applying equalities of matrices could never get rid of stuff that blows up the representation of an object).
I (naively?) hope that this big picture optimizations could be encoded as rewrite rules for the compiler. So this sound like a promising example for testing the limits of the current approach.
Do you have a reference (or maybe even an implementation) of the non-trivial equivalence? If not, I would try to construct it from the universal property of the Adelman category. Or is there a better approach?
I (naively?) hope that this big picture optimizations could be encoded as rewrite rules for the compiler. So this sound like a promising example for testing the limits of the current approach.
That would be nice. In particular, we could learn from that example about possible simplifications of the objects in an Adelman category.
Do you have a reference (or maybe even an implementation) of the non-trivial equivalence? If not, I would try to construct it from the universal property of the Adelman category. Or is there a better approach?
No, I don't have it explicitly spelled out in a reference. The point is that Adelman( A ) has enough projectives, and the subcategory of projectives is equivalent to Freyd( A^op )^op. From this, the claim follows.
There is an implementation of the universal property of Adelman categories: AdelmanCategoryFunctorInducedByUniversalProperty
You could apply it on Adelman( A ) for A given by QuiverRows( Q ) for the quiver consisting of two consecutive arrows. This can be seen as an abelian category containing a generic object in an Adelman category. From this, you can read off all formal manipulations with that object.
By the way, Freyd( A^op )^op should somehow have a name, like CoFreyd, and maybe even an own implementation, since it is the universal way of attaching kernels to A. Is it possible with your framework to reduce the work of an implementation to a declaration of appropriate functions (just like you derived CategoryOfColumns from CategoryOfRows)?
Do you have a reference (or maybe even an implementation) of the non-trivial equivalence? If not, I would try to construct it from the universal property of the Adelman category. Or is there a better approach?
No, I don't have it explicitly spelled out in a reference. The point is that Adelman( A ) has enough projectives, and the subcategory of projectives is equivalent to Freyd( A^op )^op. From this, the claim follows.
There is an implementation of the universal property of Adelman categories:
AdelmanCategoryFunctorInducedByUniversalPropertyYou could apply it on Adelman( A ) for A given by QuiverRows( Q ) for the quiver consisting of two consecutive arrows. This can be seen as an abelian category containing a generic object in an Adelman category. From this, you can read off all formal manipulations with that object.
That sounds perfect, I will report once I find the time to try this (hopefully soon :D ).
By the way, Freyd( A^op )^op should somehow have a name, like CoFreyd, and maybe even an own implementation, since it is the universal way of attaching kernels to A. Is it possible with your framework to reduce the work of an implementation to a declaration of appropriate functions (just like you derived
CategoryOfColumnsfromCategoryOfRows)?
That's certainly possible! With WrapperCategory( Freyd( A^op )^op ) one can easily change the data structure of Freyd( A^op )^op visible to the outside world (while the internal data structure and algorithms stay the same). This introduces even more wrapping and unwrapping than Freyd( A^op )^op alone. If performance is an issue, we can then compile WrapperCategory( Freyd( A^op )^op ) and should get what I assume you mean by an "own implementation".
In case this is hard to grasp: I have to write down the ideas behind the combination of WrapperCategory and CompilerForCAP somewhere, then things should get clear :-)
I assume that CoFreyd should have similar data structures as Freyd, i.e.
- Objects are given by morphisms in A.
- A morphism
phiis given by a morphism in A with source and range matching the source of the morphisms definingSource( phi )andRange( phi ).
Is this correct?
In case this is hard to grasp: I have to write down the ideas behind the combination of WrapperCategory and CompilerForCAP somewhere, then things should get clear :-)
That would be very helpful. Let me know once you have some draft available.
Is this correct?
Exactly. It is like imposing "co-relations" on the source object. Whatever that means :-)