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 <[email protected]> wrote:
> On Mon, Jan 26, 2015 at 12:54 PM, Jiaqi Tan <[email protected]> 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
>> [email protected]
>> 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
[email protected]
https://lists.sourceforge.net/lists/listinfo/hol-info
