Hi Heiko, | suppose I want to evaluate the definition | | let factorial = define `(fact (0) = 1) | /\ (fact (SUC n) = SUC n * fact (n))`;; | | in the term | | `fact 10` | | in HOL-Light. | | Do I need to use Conversions to do this or is there a simpler way like | Coq's "Eval compute" or HOL4's "EVAL"?
There is currently no automated evaluation mechanism of this kind in HOL Light. (Of course for the actual core arithmetic operations including the usual factorial there is NUM_REDUCE_CONV, but I assume the factorial was just an example.) I would indeed quite like to have such a thing, an example I'm particularly interested in being the graph enumeration program used in the Flyspeck project. It would not be that difficult to write a simple version --- there is a toy example in the Tutorial, sec 21.4 starting on p177: https://www.cl.cam.ac.uk/~jrh13/hol-light/tutorial_220.pdf But making it really robust and efficient without any changes to the kernel is a bit more work. | As a context, I have constructed a function that computes a boolean | result by structural recursion in HOL-Light that can be used as a | certificate checker for a static analysis. | | The problem is that currently the certificate checking is very slow | since I am using only rewrite conversions. Ultimately you are constrained by the very simple and minimal kernel in HOL Light, so some things like arithmetic just will be slow. Nevertheless, even without some faster evaluation mechanism you may be able to get a significant speedup with sufficiently careful coding. (Alexey Solovyev's inequality prover in "Formal_ineqs" is a striking example of what can be achieved.) There may also be scope for exploiting some kind of separate certificate-checking for some of the sub-problems. If you are really struggling to get acceptable performance, I'd be interested to hear some more details and I or someone else might have more concrete suggestions. John. ------------------------------------------------------------------------------ Check out the vibrant tech community on one of the world's most engaging tech sites, SlashDot.org! http://sdm.link/slashdot _______________________________________________ hol-info mailing list hol-info@lists.sourceforge.net https://lists.sourceforge.net/lists/listinfo/hol-info
