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:


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.


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

Reply via email to