Re: [CZT-Devel] Reducing memory usage: Signatures are the biggest culprit?

[Leo F. <leo...@ne...>]

Hi Tim / Anthony,

@Tim do you remember the discussions when we moved from ZDEclName/RefName to ZName? When was it?
There could lie some important clues for what to (not) do. 

@Anthony one case that is tricky is when you have name collusion as in  S == [ x: \nat ]; T == [x : \num]; R == S \land T,
where declared/unified types are different, here the two references ought to get / have the same ID. Other weird cases
appear when you have schema quantification i.e.  \forall T @ S, in which case the first is the declaring name? 

Andrius and I have been discussing potential solutions that take memory and functionality preservation into account,
if with some need to change practices / code in various projects. Will look at this as soon as I free myself from an Isabelle 
proof that is taking longer than I wanted it to :-(…

PS:
Another interesting possibility is to look at what ProofPowerZ does, given it's efficient and solves similar problem?

Best,
Leo

On 15 Apr 2013, at 11:22, Anthony Hall <an...@an...> wrote:

> Tim
> 
> Can I ask a question about ids? I had understood that the id was necessary
> for distinguishing truly different instances of a name - for example x
> declared globally and x within a schema. If that's true we can't presumably
> drop ids altogether? Certainly I use them in my cross reference (as you may
> remember, we had extensive discussions about this) and I've just been
> looking at the "Go To Declaration" tool in the Eclipse IDE, which I think
> uses the word + id as the unique identifier of a name.
> 
> So I wonder whether we do need to keep the id, but not to create a new id
> for every schema inclusion? If I declare x in S and then include S in T, I
> don't think we should need a new id for the x in T, for example. Of course
> if I declare x in S1 and S2 and then include both in T, there would have to
> be an arbitrary choice of which id to use for references in T, but that's
> really no different from the arbitrary choice of location that has to be
> made at present if I ask where x in T is defined.
> 
> Also, there the special id deltaxi, which presumably needs to be kept or
> replaced with a different mechanism?
> 
> At the moment it also seems to be true that there are many instances of a
> ZName with the same id - that too could presumably be avoided?
> 
> Please do say if I've misunderstood this!
> 
> Thanks
> 
> Anthony
> 
> -----Original Message-----
> From: Tim Miller [mailto:tm...@un...] 
> Sent: 15 April 2013 00:49
> To: CZT-Devel
> Subject: Re: [CZT-Devel] Reducing memory usage: Signatures are the biggest
> culprit?
> 
> Hi everyone,
> 
> You wrote:
>> This lead me to thinking - do signatures really need to be duplicated 
>> everywhere? I imagine that the signature of schema A would be the same 
>> everywhere? Can we reuse the signature, or is it important to 
>> duplicate and assign new IDs to the name?
>> 
> It was, at some point, very important to create new signatures, because
> referenced schema names declare new variables into the name space of a
> specification, and we can't have 2 variables with the same IDs if they refer
> to different declarations. The IDs were a CZT-specific thing (i.e. 
> not part of the standard), and were used by other tools (the typechecker
> does not require them because it keeps track of references in the type
> environments itself).
> 
> Now, I'm not sure whether they are still important in CZT. Other tools may
> still rely on them. I'm pretty sure the rules package used them at some
> point.
> 
> Andrius, have you tried running all CZT tests to see what happens when you
> don't create new signatures? If some of the rules tests fail, then the
> dependency there means that we can't just switch these off in the
> typechecker. If not, then there is a chance these aren't used any more.
> 
> If I do a grep -r for "getId" and "setId" in the rules package, there are a
> number of references, but most look to be just ensuring that they are passed
> around.
> 
> If it was decided that IDs are no longer necessary (I know at one point
> there was talk of dropping them), then they should be removed from the ZName
> class all together, along with any reference to them in all of the other
> packages. Anything else would be too confusing. If they don't play an
> important role, then the memory saving may be worth removing them, but I'd
> wager the change would be tedious.
> 
>> The massive space saving becomes quite obvious when you think about it.
>> If we have schema references, every RefExpr would duplicate the whole 
>> schema definition when typechecked, hence creating a lot of new ZName 
>> instances and consuming all this memory.
>> 
> It wouldn't duplicate the whole schema definition -- it would only create a
> new Signature instance, and new ZName instances for all names inside the
> signature. The existing type instances are used.
> 
> This alone will certainly account for a large chunk of memory in a
> state-machine, because every schema inclusion (including Xi/Delta) will
> create a new ZName for every name in that inclusion (two for Delta
> inclusions).
> 
> Cheers,
> Tim
> 
> ----------------------------------------------------------------------------
> --
> Precog is a next-generation analytics platform capable of advanced analytics
> on semi-structured data. The platform includes APIs for building apps and a
> phenomenal toolset for data science. Developers can use our toolset for easy
> data analysis & visualization. Get a free account!
> http://www2.precog.com/precogplatform/slashdotnewsletter
> _______________________________________________
> CZT-Devel mailing list
> CZT...@li...
> https://lists.sourceforge.net/lists/listinfo/czt-devel
> 
> 
> ------------------------------------------------------------------------------
> Precog is a next-generation analytics platform capable of advanced
> analytics on semi-structured data. The platform includes APIs for building
> apps and a phenomenal toolset for data science. Developers can use
> our toolset for easy data analysis & visualization. Get a free account!
> http://www2.precog.com/precogplatform/slashdotnewsletter
> _______________________________________________
> CZT-Devel mailing list
> CZT...@li...
> https://lists.sourceforge.net/lists/listinfo/czt-devel