Sheet1
Comparison of Reduction Strategies
Explanations:
The data is arranged by examples: Llambda (compiler, typeinf), reduction (church, IKS combinators), and higher order unification (hilbert, funtrans).
Each line represents a variation depending on use of annotations, merging (betas-prime), eager or explicit suspensions (substitution), means of
Reduction (lambda is true or "naive" full normalization, "full" means the intermediate method), and method of commiting rewriting steps.
Data is tabulated for each variation in terms of number of heap terms created, number of bytes, and the "traversals" measure indicates
The ammount of work done in traversing terms. Time is clock time for the entire teyjus process - all other figures are only for the reduction routines.
In the "renumbering costs" set of tests, the versions of head- and full norm indicated by the properties of no annotations, with merging, and lazy
rewriting are used to count the number of beta redexes, substitutions, and non-trivial renumbering substitutions (r.n. Substs). They are contrasted
against versions where a term being substituted in is head-contracted first before a renumbering walk (where nl>0).
No merge data for annotated versions not adjusted!
Compiler
Annotation Merging Substitution Reduction Rewriting Heap Terms Heap Bytes Traversals Time teyjus file name Notes
no yes eager full lazy 109,589 1,476,804 2,452,932 3.13 full_hnorm 41.6
no no eager full lazy 1,475,457 16,199,084 4,018,991 4.20 full_nomerge
no yes eager full eager 493,643 4,885,764 2,693,513 3.16 exp_fnorm 44.19
no yes lazy head lazy 134,316 1,764,172 2,390,346 3.17 comb_hnorm
no yes eager head lazy 2,640,909 19,703,580 4,276,004 4.30 imp_hnorm
no no eager head lazy 13,252,785 91,051,408 16,527,263 11.31 imp_head_nomerge added 8/18
no no lazy head lazy 2,417,025 27,487,728 5,226,479 5.03 comb_head_nomerge 100.25
no yes lazy head eager 635,851 6,372,836 2,656,330 3.15 exp_hnorm 43.49
no yes eager lambda lazy 150,625 1,974,116 32,317,036 12.68 lam_norm
yes yes eager full lazy 109,447 1,474,852 2,452,690 3.33 full_an_hnorm
yes no eager full lazy 1,612,687 16,977,836 3,783,235 4.13 full_an_nomerge
yes yes lazy head lazy 134,316 1,764,172 2,390,346 3.26 comb_an_hnorm
yes yes eager head lazy 133,730 1,982,756 2,501,384 3.29 imp_an_hnorm
yes no lazy head lazy 2,485,417 27,309,472 4,802,224 5.01 comb_head_an_nomerge 93.57
yes yes eager lambda lazy 150,483 1,972,164 32,317,036 13.59 lam_an_norm 105-church
yes no eager head lazy 1,691,312 16,035,364 4,034,042 4.04 imp_head_an_nomerge added 8/19
yes yes lazy head eager 594,941 5,922,184 2,611,259 3.03 exp_an_hnorm added 8/22
Renumbering costs substs r.n. substs redexes traversals
same as file comb_hnorm 93766 0 102592 2390346 comb_sc_hnorm.c
same as file full_hnorm 60677 0 70062 2452932 full_sc_hnorm.c
headnorm, eager contraction afer subst 93380 0 102592 2412429 comb_ea_hnorm.c
fullnorm, eager contraction after subst 57922 0 70062 2584330 full_ea_hnorm.c
typeinf
Annotation Merging Substitution Reduction Rewriting Heap Terms Heap Bytes Traversals Time teyjus file name Notes
no yes eager full lazy 1,588,648 20,388,452 4,936,116 3.49 full_hnorm
no no eager full lazy 13,072,813 119,685,572 16,484,357 11.05 full_nomerge
no yes eager full eager 7,234,409 75,934,096 8,144,674 4.35 exp_fnorm
no yes lazy head lazy 1,722,696 22,012,896 4,314,569 3.64 comb_hnorm
no yes eager head lazy 7,142,880 61,045,064 8,724,726 5.70 imp_hnorm
no no eager head lazy 50,272,482 351,634,500 56,399,791 31.11 imp_head_nomerge added 8/18
no no lazy head lazy 15,695,839 146,337,820 18,936,333 13.06 comb_head_nomerge
no yes lazy head eager 7,691,000 80,893,824 7,647,293 4.37 exp_hnorm
no yes eager lambda lazy 1,629,028 20,789,368 10,590,519 4.87 lam_norm
yes yes eager full lazy 1,588,576 20,387,792 4,936,080 3.66 full_an_hnorm
yes no eager full lazy 16,782,819 152,161,460 14,943,761 10.48 full_an_nomerge
yes yes lazy head lazy 1,722,694 22,012,860 4,314,569 3.95 comb_an_hnorm
yes yes eager head lazy 1,654,245 21,736,256 4,808,113 3.71 imp_an_hnorm
yes no lazy head lazy 19,154,339 176,307,392 16,704,153 12.16 comb_head_an_nomerge
yes yes eager lambda lazy 1,628,956 20,788,708 10,590,519 5.23 lam_an_norm
yes no eager head lazy 15,759,776 138,189,040 15,386,892 9.35 imp_head_an_nomerge added 8/19
yes yes lazy head eager 7,291,185 76,484,808 7,236,379 3.92 exp_an_hnorm added 8/22
Renumbering costs substs r.n. substs redexes traversals
same as file comb_hnorm 780745 0 1441489 4314569 comb_sc_hnorm.c
same as file full_hnorm 656950 0 1319901 4936116 full_sc_hnorm.c
headnorm, eager contraction afer subst 789700 0 1441489 4593170 comb_ea_hnorm.c
fullnorm, eager contraction after subst 670568 0 1314324 5765474 full_ea_hnorm.c
church
Annotation Merging Substitution Reduction Rewriting Heap Terms Heap Bytes Traversals Time teyjus file name Notes
no yes eager full lazy 37,161 531,880 213,095 0.22 full_hnorm
no no eager full lazy 626,581 6,453,764 826,397 0.65 full_nomerge
no yes eager full eager 137,936 1,342,076 308,896 0.16 exp_fnorm
no yes lazy head lazy 37,162 531,892 169,192 0.17 comb_hnorm
no yes eager head lazy 44,797 610,528 175,301 0.18 imp_hnorm
no no eager head lazy 972,184 8,993,080 1,126,578 0.68 imp_head_nomerge added 8/18
no no lazy head lazy 627,048 6,459,368 786,259 0.58 comb_head_nomerge
no yes lazy head eager 137,936 1,342,076 265,004 0.14 exp_hnorm
no yes eager lambda lazy 37,161 531,880 418,755,708 370.98 lam_norm
yes yes eager full lazy 37,161 531,880 213,095 0.24 full_an_hnorm
yes no eager full lazy 462,116 4,775,464 629,871 0.54 full_an_nomerge
yes yes lazy head lazy 37,162 531,892 169,192 0.18 comb_an_hnorm
yes yes eager head lazy 37,596 543,656 171,133 0.18 imp_an_hnorm
yes no lazy head lazy 462,583 4,781,068 586,446 0.50 comb_head_an_nomerge
yes yes eager lambda lazy 37,161 531,880 418,755,708 428.35 lam_an_norm
yes no eager head lazy 169,365 1,907,752 282,973 0.16 imp_head_an_nomerge added 8/19
yes yes lazy head eager 127,693 1,236,740 262,098 0.14 exp_an_hnorm added 8/22
Renumbering costs substs r.n. substs redexes traversals
same as file comb_hnorm 35824 200 13063 169192 comb_sc_hnorm.c
same as file full_hnorm 35824 200 13063 213095 full_sc_hnorm.c
headnorm, eager contraction afer subst 59932 3912 13063 385009 comb_ea_hnorm.c
fullnorm, eager contraction after subst 59932 3912 13063 428482 full_ea_hnorm.c
SKI (combos2, object-level hnorm)
Annotation Merging Substitution Reduction Rewriting Heap Terms Heap Bytes Traversals Time teyjus file name Notes
no yes eager full lazy 98,319 1,164,656 459,198 0.40 full_hnorm nothing changed
no no eager full lazy 137,720 1,424,476 504,125 0.46 full_nomerge
no yes eager full eager 235,576 2,290,084 660,768 0.41 exp_fnorm
no yes lazy head lazy 76,779 939,104 367,944 0.40 comb_hnorm
no yes eager head lazy 98,319 1,164,656 449,917 0.41 imp_hnorm nothing chnaged
no no eager head lazy 132,193 1,358,152 519,769 0.46 imp_head_nomerge added 8/18
no no lazy head lazy 135,691 1,407,024 431,750 0.46 comb_head_nomerge
no yes lazy head eager 180,777 1,800,160 491,688 0.37 exp_hnorm
no yes eager lambda lazy 98,319 1,164,656 1,535,208 0.76 lam_norm
yes yes eager full lazy 45,884 595,148 402,271 0.40 full_an_hnorm
yes no eager full lazy 150,545 1,472,584 447,198 0.44 full_an_nomerge
yes yes lazy head lazy 46,362 605,368 360,327 0.41 comb_an_hnorm
yes yes eager head lazy 45,884 595,148 391,004 0.39 imp_an_hnorm
yes no lazy head lazy 159,113 1,575,400 417,416 0.46 comb_head_an_nomerge
yes yes eager lambda lazy 45,884 595,148 1,535,208 0.78 lam_an_norm
yes no eager head lazy 145,018 1,406,260 460,856 0.45 imp_head_an_nomerge added 8/19
yes yes lazy head eager 123,659 1,252,724 417,818 0.33 exp_an_hnorm added 8/22
Renumbering costs substs r.n. substs redexes traversals
same as file comb_hnorm 16749 643 23884 367944 comb_sc_hnorm.c
same as file full_hnorm 16749 1005 23884 459198 full_sc_hnorm.c
headnorm, eager contraction afer subst 16749 643 23884 415583 comb_ea_hnorm.c
fullnorm, eager contraction after subst 16749 1005 23884 563895 full_ea_hnorm.c
Hilbert
Annotation Merging Substitution Reduction Rewriting Heap Terms Heap Bytes Traversals Time teyjus file name Notes
no yes eager full lazy 12,908 135,380 461,851 0.27 full_hnorm
no no eager full lazy 58,565 554,416 503,727 0.30 full_nomerge
no yes eager full eager 35,610 354,700 522,236 0.17 exp_fnorm
no yes lazy head lazy 5,642 75,020 446,715 0.26 comb_hnorm
no yes eager head lazy 170,123 1,387,192 574,705 0.38 imp_hnorm
no no eager head lazy 320,821 2,619,816 771,638 0.51 imp_head_nomerge added 8/18
no no lazy head lazy 25,074 284,064 464,505 0.28 comb_head_nomerge
no yes lazy head eager 18,894 196,596 455,327 0.14 exp_hnorm
no yes eager lambda lazy 13,142 138,028 1,736,602 0.68 lam_norm
yes yes eager full lazy 12,908 135,380 461,851 0.29 full_an_hnorm
yes no eager full lazy 69,926 658,468 499,594 0.31 full_an_nomerge
yes yes lazy head lazy 5,642 75,020 446,715 0.28 comb_an_hnorm
yes yes eager head lazy 169,748 1,384,100 574,419 0.39 imp_an_hnorm
yes no lazy head lazy 29,758 329,684 461,565 0.29 comb_head_an_nomerge
yes yes eager lambda lazy 13,142 138,028 1,736,602 0.73 lam_an_norm
yes no eager head lazy 412,920 3,366,812 760,940 0.53 imp_head_an_nomerge added 8/19
yes yes lazy head eager 18,606 193,336 454,937 0.12 exp_an_hnorm added 8/22
Renumbering costs substs r.n. substs redexes traversals
same as file comb_hnorm 1718 412 3188 446715 comb_sc_hnorm.c
same as file full_hnorm 5977 1773 4860 461851 full_sc_hnorm.c
headnorm, eager contraction afer subst 1718 412 3188 448465 comb_ea_hnorm.c
fullnorm, eager contraction after subst 5977 1773 4860 474152 full_ea_hnorm.c
funtrans
Annotation Merging Substitution Reduction Rewriting Heap Terms Heap Bytes Traversals Time teyjus file name Notes
no yes eager full lazy 19,734 249,412 676,067 0.41 full_hnorm
no no eager full lazy 48,548 498,340 708,866 0.43 full_nomerge
no yes eager full eager 62,277 620,632 720,390 0.38 exp_fnorm
no yes lazy head lazy 24,404 313,744 665,773 0.40 comb_hnorm
no yes eager head lazy 28,027 319,740 679,757 0.40 imp_hnorm
no no eager head lazy 73,267 637,492 740,320 0.45 imp_head_nomerge added 8/18
no no lazy head lazy 55,290 584,340 701,188 0.45 comb_head_nomerge
no yes lazy head eager 66,622 659,384 710,615 0.36 exp_hnorm
no yes eager lambda lazy 20,414 259,096 1,273,737 0.53 lam_norm
yes yes eager full lazy 18,749 236,788 674,751 0.41 full_an_hnorm
yes no eager full lazy 51,316 520,624 692,821 0.44 full_an_nomerge
yes yes lazy head lazy 23,762 304,688 665,098 0.46 comb_an_hnorm
yes yes eager head lazy 19,165 243,816 671,751 0.43 imp_an_hnorm
yes no lazy head lazy 59,089 619,904 686,782 0.46 comb_head_an_nomerge
yes yes eager lambda lazy 19,433 246,512 1,273,728 0.57 lam_an_norm
yes no eager head lazy 46,745 468,904 692,152 0.44 imp_head_an_nomerge added 8/19
yes yes lazy head eager 53,747 518,184 692,546 0.31 exp_an_hnorm added 8/22
Renumbering costs substs r.n. substs redexes traversals
same as file comb_hnorm 8367 96 9508 665773 comb_sc_hnorm.c
same as file full_hnorm 7866 96 9462 676067 full_sc_hnorm.c
headnorm, eager contraction afer subst 8212 90 9508 672448 comb_ea_hnorm.c
fullnorm, eager contraction after subst 7678 90 9422 685420 full_ea_hnorm.c