On Mon, Jan 26, 2015 at 12:54 PM, Jiaqi Tan <tanji...@cmu.edu> wrote:
> Hi,
>
> I have some questions regarding the internals of HOL4, and whether there
> are any internal resources (memory/storage) used when certain functions are
> used.
>
There are at least two kinds of resources that are relevant when
considering where and how theorems and definitions are stored. The first is
HOL4's database, which includes the hierarchy of theories, defined
constants, and saved theorems. The second is values available in the ML
runtime, which consume memory until they are garbage collected.
>
> 1. If I use prove or TAC_PROOF, and a theorem is successfully proved, is
> the theorem automatically saved in internal HOL4 storage? I would believe
> it is not stored, unless I assigned it to a variable with val my_thm =
> prove(...). In this case, if I just use prove() (or TAC_PROOF) without
> saving the result to a variable, does this mean that one command later on
> the interactive shell, the prove theorem will no longer use any resources?
> (i.e. after val it has been overwritten).
>
Theorems proved using prove or TAC_PROOF do not affect the HOL4 database.
If you bind them to ML variables (using val my_thm = prove(...)) then they
stay in memory as long as they are in scope (e.g. until shadowed).
> 2. If I use store_thm instead, then this would consume resources in HOL4's
> internal memory? After I call store_thm, suppose I don't need the theorem
> any more, is there any way to reclaim the internal storage used?
>
store_thm affects HOL4's database, by adding the theorem to the database.
To remove it, you can use Theory.delete_binding. (With regards to the ML
runtime, however, store_thm is the same as prove.)
>
> 3. Similarly for Define, are the theorems which described the Define-d
> function stored internally in HOL4 storage? Suppose I do "Define ``MY_FUNC
> = 1``", and I do not store the definition theorem in a variable, does the
> definition still get stored internally in HOL4? And is there any way to
> clear/remove the definition later to reclaim space if so?
>
Definitions (including those made by Define) are always stored in the HOL4
database. To remove them you can use Theory.delete_const (or
delete_binding).
>
> In general, if I am Define-ing a large number of functions for temporary
> use (e.g. rewriting away a large expression), but I do not need them after
> a certain point in the code, are there any internal HOL4 memory/resources
> used, and is there any way to reclaim these resources later?
>
How large is your "large number"? The HOL4 database probably won't suffer
much from having lots of definitions stored in it. But it's certainly much
cleaner and logically nicer to delete temporary definitions with
delete_const when they are no longer useful. For temporary theorems, you
can simply not store them in the database to begin with (i.e. use prove
rather than store_thm).
>
> Thank you in advance!
>
> Regards,
> Jiaqi
>
>
>
> ------------------------------------------------------------------------------
> Dive into the World of Parallel Programming. The Go Parallel Website,
> sponsored by Intel and developed in partnership with Slashdot Media, is
> your
> hub for all things parallel software development, from weekly thought
> leadership blogs to news, videos, case studies, tutorials and more. Take a
> look and join the conversation now. http://goparallel.sourceforge.net/
> _______________________________________________
> hol-info mailing list
> hol-info@lists.sourceforge.net
> https://lists.sourceforge.net/lists/listinfo/hol-info
>
>
------------------------------------------------------------------------------
Dive into the World of Parallel Programming. The Go Parallel Website,
sponsored by Intel and developed in partnership with Slashdot Media, is your
hub for all things parallel software development, from weekly thought
leadership blogs to news, videos, case studies, tutorials and more. Take a
look and join the conversation now. http://goparallel.sourceforge.net/
_______________________________________________
hol-info mailing list
hol-info@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info
