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

[Anthony H. <an...@an...>]

Dear Leo

> @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? 

I understand that these are all examples of why the problem of deciding what
a name refers to isn't straightforward. But that's a problem that has been
solved before, because the typechecker has already worked out what to do in
these cases. Here we are really only talking about how to record the
relevant information, not the much more difficult problem of how to work it
out. Since the type of a variable is its base type like \arithmos, not its
declared type like \nat, there is no problem in using the same id for both
cases afa the typechecker is concerned. And yes, in \forall T @ S the
declarations are all in T (or an enclosing scope) - S must be consistent
with them. 
> 
> 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 :-(.

It will be great if you can fix this! I expect I'll have to change my cross
referencer, too, but that's OK if the new scheme is better.
 
> PS:
> Another interesting possibility is to look at what ProofPowerZ does, given
it's efficient and solves similar problem?

I don't know anything about it I'm afraid but I dare say Rob would help if
asked. It's completely different, of course, being written in HOL/ML

All the best 

Anthony
> 
> 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
>