Open zickgraf opened 4 years ago
I extend my question further:
IsEqualForObjects( EvaluatedCell( DirectProduct( a / L, b / L ) ), DirectProduct( a, b ) )
for all objects a
and b
in C
This is probably the most important one: if it should hold true it restricts the possible optimizations which we are allowed to make in L
(e.g. the current optimization for FiberProduct
would be invalid). If it need not hold true, it means that we cannot mix computations made with LazyCategories
and computations made without LazyCategories
.
The answers are (generically): 1. false, 2. false, 3. true, 4. true
I do not see the significance of 4. as IsEqualForObjects
is called in the category underlying the lazy category.
Thanks for the quick response! Consider the following example (where I have replace DirectProduct
by FiberProduct
):
LoadPackage( "LazyCategories" );
LoadPackage( "FinSetsForCAP" );
M := FinSet( [ 1, 2 ] );
id := IdentityMorphism( M );
phi := MapOfFinSets( M, [ [ 1, 1 ], [ 2, 1 ] ], M );
L := LazyCategory( FinSets : show_evaluation := true );
IsEqualForObjects( EvaluatedCell( FiberProduct( phi / L, id / L ) ), FiberProduct( phi, id ) );
where the last line yields false
, since the object in the lazy category has changed due to the optimization.
Why is this bad?
It's not necessarily bad. It's unexpected if one thinks of LazyCategories
as a completely transparent wrapper (in the sense that once I evaluate I get exactly the same result as if I had never lazified anything), that's why I asked for the specification.
If LazyCategories
is not a completely transparent wrapper, you cannot mix computations from the lazy and the non-lazy world. And if such optimizations would be part of CompilerForCAP
, there would be some additional implications:
for
-loop the compiler cannot handle) it produces wrong results.IdentityMorphism
and a morphism which happens to be the identity by chance, exactly like LazyCategories
does). And this changed notion of equality might not be apparent in the compiled code anymore.Again, this is not necessarily bad, I'm just trying and to understand and write down my thoughts about the implications :-)
I wonder which of the following specifications should hold true for a category
C
andL := LazyCategory( C )
:IsEqualForObjects( DirectProduct( a / L, b / L ), DirectProduct( a, b ) / L )
for all objectsa
andb
inC
(of course,DirectProduct
is just an example)IsEqualForObjects( Source( morphism ), Source( EvaluatedCell( morphism ) ) / L )
for all morphismsmorphism
inL
.IsEqualForObjects( EvaluatedCell( Source( morphism ) ), Source( EvaluatedCell( morphism ) )
for all morphismsmorphism
inL
.From looking at the code I assume that 1. and 2. should not hold true, but I expect that 3. should be true.