Re: [Hol-info] Question: Internal HOL4 resource usage when using prove, store_thm, and Define

[Jiaqi T. <tan...@cm...>]

Hi Ramana,

Thank you for the detailed explanation.

I only need a small number of definitions for my temporary rewrites (fewer
than 10) in proving each predicate, but I am processing a large number of
predicates (at least thousands, to the low or mid tens of thousands). For
now, I have used close to 10,000 Define calls, so I was a little concerned
about resource usage.

Thank you.

Regards,
Jiaqi



On Mon, Jan 26, 2015 at 8:30 AM, Ramana Kumar <ra...@me...> wrote:

> On Mon, Jan 26, 2015 at 12:54 PM, Jiaqi Tan <tan...@cm...> 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...@li...
>> https://lists.sourceforge.net/lists/listinfo/hol-info
>>
>>
>