For the past year I have been engaged in developing a collection of
conversions, conversion-like functions, and supporting theories to enable
the use of one form of well-balanced binary search tree in HOL, with the
objective of bringing to computations with explicitly displayed finite
sets and functions similar speeding-up to that which the `numeral'
representation provides for numeric computations---for example,
logarithmic time IN and linear-time UNION for finite sets (if element
comparisons can be regarded as taking constant time)---but, sadly, with
no hope of imitating the invisibility of numerals. I mean to
submit a description of the package to next summer's Conference on
Automated Deduction. My hope is that it may eventually become a useful
addition to the HOL libraries.
The rest of this message consists of three more or less specific questions and
a more general plea for help.
First, I don't understand at all how libraries work, and have come across
nothing in the HOL documentation about them beyond a caution to the
effect that the addition of new ones to the system requires central approval.
Can anyone point me to relevant information on the design of, and
requirements for, HOL libraries?
Second, efficiency of derivation is of course a concern for the
conversions I have been writing, but so also to some extent is
readability. I have been modeling my style on Paulson's "A higher-order
implementation of rewriting", taking REWR_CONV (which he in that paper
called "REWRITE_CONV") as the workhorse, leaving to it the work of
matching terms and types, but avoiding searching. As an easily
grasped example of the style, here is an equivalent of the listLib's
REVERSE_CONV:
(* REVERSE_REV = |- !L. REVERSE L = REV L [] *)
val [rev_nil, rev_rec] = CONJUNCTS REV_DEF;
(* rev_nil = |- !acc. REV [ ] acc = acc
rev_rec = |- !h t acc. REV (h::t) acc = REV t (h::acc) *)
val REVERS_CONV =
let fun rev_conv t = ((REWR_CONV rev_rec THENC rev_conv) ORELSEC
REWR_CONV rev_nil) t
in REWR_CONV REVERSE_REV THENC rev_conv end;
(*- REVERS_CONV (Term`REVERSE [1; 2; 3; 4; 5]`);
> val it = |- REVERSE [1; 2; 3; 4; 5] = [5; 4; 3; 2; 1] : thm *)
Is this a reasonably efficient way to go, at least for a first version?
(Source for conversions I see in various libraries seems to feature a lot
more of INST_TYPE and SUBST in ways that I find difficult to understand.)
Third, I have been led to define a polymorphic type 'a toto of
total orders on type 'a, and this has of course entailed
showing that at least one such exists. It was a most educational
experience for me to translate the chapter of Halmos's Naive Set Theory
in which he proves the well-ordering theorem into HOL in order to make
this existence proof, but the result was a large file which I would be
very happy to suppress if, as I suppose very likely, there is already
a proof somewhere in the HOL system.
My general plea is for comments and advice from anyone who has them to offer.
I would be happy to send my files in their current state, with some rough
descriptive notes, to anyone (ideally, someone who is desperate to get
some set operatons or list searches inside a HOL proof to run faster) who
would care to look at them and give helpful criticism.
I am not exactly in a hotbed of HOL activity here at Syracuse, and I fear
that I am myself a good deal less UNIX-savvy than most hol-info
correspondents seem to be. I get on all right with HOL and emacs,
and I know to run Holmake and, when mysterious ailments appear,
Holmake cleanAll, but that is about it. Please do not withhold remarks on
grounds of obviousness.
Thanks to all,
Lockwood
|- |- |- |- |- |- |- |- |- |- |- |- |- |- |- |- |- |- |- |-
|- |- |-
Lockwood Morris [email protected] (315)443-3046 Rm. 4-125 CST
EECS Syracuse University 111 College Place Syracuse NY 13244-4100
------------------------------------------------------------------------------
Everyone hates slow websites. So do we.
Make your web apps faster with AppDynamics
Download AppDynamics Lite for free today:
http://p.sf.net/sfu/appdyn_d2d_nov
_______________________________________________
hol-info mailing list
[email protected]
https://lists.sourceforge.net/lists/listinfo/hol-info
