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 HOLLight.

 Do I need to use Conversions to do this or is there a simpler way like
 Coq's "Eval compute" or HOL4's "EVAL"?
Advertising
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/hollight/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 HOLLight 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
certificatechecking for some of the subproblems. 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
_______________________________________________
holinfo mailing list
holinfo@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/holinfo