Hi,
Just for reference. The Patricia tree library works well for simple
dictionary-style lookups (IN) but itβs not so suited to computing UNIONS.
For example, you can define constants as follows:
val s100_def = patriciaLib.Define_mk_ptree "s100"
(patriciaLib.ptree_of_ints
[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_def = patriciaLib.Define_mk_ptree "s50"
(patriciaLib.ptree_of_ints
[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])
The operation KEYS converts this to a list:
val thm1 = Count.apply (DEPTH_CONV patriciaLib.PTREE_DEFN_CONV THENC EVAL)
``KEYS s100`;
runtime: 0.071s, gctime: 0.000s, systime: 0.003s.
Axioms: 0, Defs: 0, Disk: 0, Orcl: 0, Prims: 95675; Total: 95675
val thm1 =
|- KEYS s100 =
[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
Lookup is fairly fast:
val thm2 = Count.apply EVAL ``35 IN_PTREE s100`;
runtime: 0.001s, gctime: 0.000s, systime: 0.000s.
Axioms: 0, Defs: 0, Disk: 0, Orcl: 0, Prims: 1170; Total: 1170
val thm2 = |- 35 IN_PTREE s100 β T: thm
This scales reasonably well to trees with thousands of elements.
UNION is more complicated but with effort lookup can be fast:
val union_s50_s100_CONV =
REWRITE_CONV
[MATCH_MP patriciaTheory.IN_PTREE_UNION_PTREE
(CONJ (DB.theorem "s50_is_ptree_thm")
(DB.theorem "s100_is_ptree_thm"))];
val thm3 = Count.apply (union_s50_s100_CONV THENC EVAL)
``35 IN_PTREE (s50 UNION_PTREE s100)``;
runtime: 0.003s, gctime: 0.000s, systime: 0.001s.
Axioms: 0, Defs: 0, Disk: 0, Orcl: 0, Prims: 2052; Total: 2052
val thm3 = |- 35 IN_PTREE s50 UNION_PTREE s100 β T: thm
Of course, it will be a bit quicker if the element is in the first tree:
val thm4 = Count.apply (union_s50_s100_CONV THENC EVAL)
``11 IN_PTREE (s50 UNION_PTREE s100)``;
runtime: 0.001s, gctime: 0.000s, systime: 0.001s.
Axioms: 0, Defs: 0, Disk: 0, Orcl: 0, Prims: 884; Total: 884
val thm4 = |- 11 IN_PTREE s50 UNION_PTREE s100 β T: thm
Cheers,
Anthony
On 13 Nov 2012, at 17:42, F.Lockwood Morris <[email protected]> wrote:
> 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
------------------------------------------------------------------------------
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
