Dear Ramana,
Thank you very much for your encouraging message. I will send you my files and
the documentary notes such as they are very
shortly, as soon as I add a few paragraphs to the latter.
At present I am running HOL 4 Kanasaskis-6. Having glanced at Michael's
wellorderScript.sml in examples, I think I had better not
try to hook up to it until I get Kanasaskis-8 installed here, which I have put
in to have done. My formalization of Halmos's proof of the
well-ordering theorem will do perfectly well for the time being.
As soon as I can manage, I will follow the suggestion both you and Michael
made, to try how EVAL does with a the_compset enlarged by the necessary
rewrites from my theories. I think there can be no doubt that EVAL,
unaugmented, burns up linear time for IN and quadratic time for UNION just
based on how far away the set elements mostly are in the default INSERT - {}
(that is effectively
linear list) representation for sets. Here is one data point:
val s100 = Term`{0;1;2;3;4;5;6;7;8;9;10;19;18;17;16;15;14;13;12;11;
20;22;24;26;28;30;29;27;25;23;21;39;38;37;36;35;34;33;32;31;
40;41;42;43;44;45;56;57;48;49;50;59;58;57;56;55;54;53;52;51;
60;63;66;69;61;64;67;62;65;68;79;75;71;78;74;70;77;73;76;72;
99;98;96;93;89;84;80;82;85;88;92;95;97;81;83;87;92;91;90;94}`;
val s50 = Term`{10;19;18;17;16;15;14;13;12;11;
40;41;42;43;44;45;56;57;48;49;50;59;58;57;56;55;54;53;52;51;
99;98;96;93;89;84;80;82;85;88;92;95;97;81;83;87;92;91;90;94}`;
Count.apply EVAL_CONV (Term`^s50 UNION ^s100`);
takes on my machine 33.7 seconds and 857842 inference steps (1154262 steps for
^s100 UNION ^s50).
More cumbersomely, going around through my conversions:
val t50 = make_oset numto_CONV (Term`numto`) s50; (* 14276 infs. 2.4s *)
val t100 = make_oset numto_CONV (Term`numto`) s100; (* 29374 infs. 5.6s *)
(These print out large trees you don't want to see. Most of the work so far has
gone into sorting.)
val beer1 = o_union_RULE numto_CONV t50 t100; (* 9539 inference steps, 1.25
seconds *) (another large tree)
and then
OSET_TO_SET_RULE beer1; (* 2847 inference steps, 0.4 seconds *)
produces more or less comprehensible output:
|- OSET_TO_SET
(SET_TO_OSET numto
{10; 19; 18; 17; 16; 15; 14; 13; 12; 11; 40; 41; 42; 43; 44; 45;
56; 57; 48; 49; 50; 59; 58; 57; 56; 55; 54; 53; 52; 51; 99; 98;
96; 93; 89; 84; 80; 82; 85; 88; 92; 95; 97; 81; 83; 87; 92; 91;
90; 94} o_union
SET_TO_OSET numto
{0; 1; 2; 3; 4; 5; 6; 7; 8; 9; 10; 19; 18; 17; 16; 15; 14; 13;
12; 11; 20; 22; 24; 26; 28; 30; 29; 27; 25; 23; 21; 39; 38; 37;
36; 35; 34; 33; 32; 31; 40; 41; 42; 43; 44; 45; 56; 57; 48; 49;
50; 59; 58; 57; 56; 55; 54; 53; 52; 51; 60; 63; 66; 69; 61; 64;
67; 62; 65; 68; 79; 75; 71; 78; 74; 70; 77; 73; 76; 72; 99; 98;
96; 93; 89; 84; 80; 82; 85; 88; 92; 95; 97; 81; 83; 87; 92; 91;
90; 94}) =
{0; 1; 2; 3; 4; 5; 6; 7; 8; 9; 10; 11; 12; 13; 14; 15; 16; 17; 18;
19; 20; 21; 22; 23; 24; 25; 26; 27; 28; 29; 30; 31; 32; 33; 34; 35;
36; 37; 38; 39; 40; 41; 42; 43; 44; 45; 48; 49; 50; 51; 52; 53; 54;
55; 56; 57; 58; 59; 60; 61; 62; 63; 64; 65; 66; 67; 68; 69; 70; 71;
72; 73; 74; 75; 76; 77; 78; 79; 80; 81; 82; 83; 84; 85; 87; 88; 89;
90; 91; 92; 93; 94; 95; 96; 97; 98; 99} : thm
For IN,
o_IN_RULE numto_CONV t100 (Term`35`); returns T in 246 inference steps, 0.16
seconds, whereas
EVAL (Term`35 IN ^s100`); takes a surprising 519359 inference steps, 20.7
seconds.
Best Regards,
Lockwood
|- |- |- |- |- |- |- |- |- |- |- |- |- |- |- |- |- |- |- |-
|- |- |-
Lockwood Morris [email protected] (315)443-3046 Rm. 4-125 CST
EECS Syracuse University 111 College Place Syracuse NY 13244-4100
________________________________________
From: [email protected] [[email protected]] on behalf of Ramana Kumar
[[email protected]]
Sent: Sunday, November 11, 2012 2:33 AM
To: F.Lockwood Morris
Cc: [email protected]
Subject: Re: [Hol-info] More efficient operations on finite sets and tabulated
functions.
Dear Lockwood
It was lovely to see your message.
I would be happy to look at your files, and, if they are in (or if we can get
them into) reasonable shape, to add them to HOL.
Can you put them online? Otherwise an attachment would be OK.
(Others on list interested in this feel free to help or take over.)
One comment, though, is that I suspect a lot of work on efficient computation
for explicit finite sets/lists has been put into computeLib.
Did you find that computeLib.EVAL_CONV was not appearing to do logarithmic-time
IN and linear-time UNION? (I'm not sure whether it's supposed to currently.)
It may be worth seeing whether your improvements can be formulated as theorems
and conversions that can be added to the_compset.
Regarding your first and third questions:
As I understand, a library is an ML structure and there are no further
requirements, except perhaps consistency of interface and a theme (what the
library is for).
I just had a quick look for a theorem resembling "there's a total order on
every type" (by checking relationTheory and grepping the HOL sources for
"total") and didn't see anything.
But then I thought to look for "well-ordering" and variants thereof, and found
the result in examples/set-theory/hol_sets/wellorderScript.sml, called
"allsets_wellorderable".
Cheers,
Ramana
------------------------------------------------------------------------------
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]<mailto:[email protected]>
https://lists.sourceforge.net/lists/listinfo/hol-info
------------------------------------------------------------------------------
Monitor your physical, virtual and cloud infrastructure from a single
web console. Get in-depth insight into apps, servers, databases, vmware,
SAP, cloud infrastructure, etc. Download 30-day Free Trial.
Pricing starts from $795 for 25 servers or applications!
http://p.sf.net/sfu/zoho_dev2dev_nov
_______________________________________________
hol-info mailing list
[email protected]
https://lists.sourceforge.net/lists/listinfo/hol-info
