(β_{s}) ((λ_{u} t_{1}) t_{2})_{v} → [[t_{1}, 1, 0, (t_{2}, 0) :: nil]]_{v} (β′_{s}) ((λ_{u} [[t_{1}, ol + 1, nl + 1, @nl :: e]]_{o}) t_{2})_{v} → [[t_{1}, ol + 1, nl, (t_{2}, nl) :: e]]_{v} (r1) [[c, ol, nl, e]]_{u} → c

provided c is a constant (r2) [[x, ol, nl, e]]_{u} → x

provided x is an instantiatable variable (r3) [[#i, ol, nl, e]]_{u} → #j

provided i > ol and j = i − ol + nl. (r4) [[#i, ol, nl, e]]_{u} → #j

provided i ≤ ol and e[i] = @l and j = nl − l. (r5) [[#i, ol, nl, e]]_{u} → [[t, 0, j, nil]]_{u}

provided i ≤ ol and e[i] = (t, l) and j = nl − l. (r6) [[(t_{1} t_{2})_{u}, ol, nl, e]]_{v} → ([[t_{1}, ol, nl, e]]_{v} [[t_{2}, ol, nl, e]]_{v})_{v}. (r7) [[(λ_{u} t), ol, nl, e]]_{v} → (λ_{v} [[t, ol + 1, nl + 1, @nl :: e]]_{o}). (r8) [[(t_{1} t_{2})_{c}, ol, nl, e]]_{u} → (t_{1} t_{2})_{c}. (r9) [[(λ_{c} t), ol, nl, e]]_{u} → (λ_{c} t). (r10) [[[[t, ol, nl, e]]_{c}, ol′, nl′, e′]]_{u} → [[t, ol, nl, e]]_{c}. (r11) [[[[t, ol, nl, e]]_{o}, 0, nl′, nil]]_{o} → [[t, ol, nl + nl′, e]]_{o}. (r12) [[t, 0, 0, nil]]_{u} → t

Figure 1: Rule schemata for rewriting annotated terms

With Merging  Without Merging
Program  Heap  Traversal Time  Heap  Traversal Time
Terms  Count (sec.)  Terms  Count  (sec.)

SKI

lazy  76,779 367,944 0.40  135,691  431,750 0.46
enhanced  98,319 459,198 0.40  137,720  504,125 0.46

Church

lazy  37,162 169,192 0.17  627,048  782,972 0.58
enhanced  37,161 213,095 0.22  626,582  826,124 0.65

Compiler

lazy  134,316 2,390,346 3.17 2,417,025 5,226,479 5.03
enhanced 109,589 2,452,932 3.13 1,475,457 4,018,991 4.20

Typeinf

lazy  1,722,696 4,314,569 3.64 15,695,839 18,936,333 13.06
enhanced 1,588,648 4,936,116 3.49 13,072,813 16,484,357 11.05

Hilbert

lazy  5,642 446,715 0.26  25,074  464,505 0.28
enhanced  12,908 461,851 0.27  58,565  503,727 0.30

Funtrans

lazy  24,404 665,773 0.40  55,290  701,188 0.45
enhanced  19,734 676,067 0.41  48,548  708,866 0.43

Table 1: Impact of Merging Rules

Eager Substitution  Lazy Substitution
Program  Heap  Traversal Time  Heap  Traversal Time
Terms  Count (sec.) Terms  Count (sec.)
SKI  98,319 449,917 0.41  76,779 367,944 0.40
Church  44,797 175,301 0.18  37,162 169,192 0.17
Compiler 2,640,909 4,276,004 4.30  134,316 2,390,346 3.17
Typeinf 7,142,880 8,724,726 5.70 1,722,696 4,314,569 3.64
Hilbert  170,123 574,705 0.38  5,642 446,715 0.26
Funtrans  28,027 679,757 0.40  24,404 665,773 0.40

Table 2: Comparison of Head-Normalization Strategies

Head Normalization  Full Normalization
Program  Heap  Traversal Time  Heap  Traversal Time
Terms  Count (sec.) Terms  Count  (sec.)
SKI  76,779 367,944 0.40  98,319  1,535,208  0.76
Church  37,162 169,192 0.17  37,161 418,755,708 370.98
Compiler 134,316 2,390,346 3.17  150,625 32,317,036 12.68
Typeinf 1,722,696 4,314,569 3.64 1,629,028 10,590,519  4.87
Hilbert  5,642 446,715 0.26  13,142  1,736,602  0.68
Funtrans  24,404 665,773 0.40  20,414  1,273,737  0.53

Table 3: Comparison of Laziness and Eagerness in Reduction

Lazy Substitution  Enhanced Head Normalization
Program  Heap  Traversal Time  Heap Traversal Time
Terms  Count (sec.) Terms  Count  (sec.)
SKI  76,779 367,944 0.40  98,319 459,198 0.40
Church  37,162 169,192 0.17  37,161 213,095 0.22
Compiler 134,316 2,390,346 3.17  109,589 2,452,932 3.13
Typeinf 1,722,696 4,314,569 3.64 1,588,648 4,936,116 3.49
Hilbert  5,642 446,715 0.26  12,908 461,851 0.27
Funtrans  24,404 665,773 0.40  19,734 676,067 0.41

Table 4: Performance Under an Enhanced Form of Head Normalization

Number  Number  Eager Substitution Lazy Substitution
of  of  Heap Traversal Heap Traversal
Abstractions Applications Terms Count  Terms Count
3  3  52  175  24  113
3  12  124  538  60  320
12  3  532  1,085  74  511
12  12  840  2,269  114  1,053

Table 5: copy A A (reduction only)

Number  Number  Eager Substitution Lazy Substitution
of  of  Heap Traversal Heap Traversal
Abstractions Applications Terms Count  Terms Count
3  3  429  986  169  684
3  12  2,670  4,097  520  2,070
12  3  5,880  6,865 1,094  2,956
12  12  20,629  20,896 2,983  7,162

Table 6: copy A U, copy U V (impact of embedded redices)

Lazy Substitution  Enhanced Head Normalization
Program Total Renumbering Total Renumbering
Substitutions Substitutions Substitutions Substitutions
SKI  16,749  643  16,749  1005
Church  35,824  200  35,824  200
Compiler  93,766  0  60,677  0
Typeinf  780,745  0  656,950  0
Hilbert  1,718  412  5,977  1,773
Funtrans  8,367  96  7,866  96

Table 7: The Frequency of Renumbering with the de Bruijn Representation

Lazy Substitution  Enhanced Head Normalization
Program Separate Merged Separate Merged
Renumbering Renumbering Renumbering Renumbering
SKI  23,884  23,884  23,884  23,884
Church  13,063  13,063  13,063  13,063
Compiler  102,592  102,592  70,062  70,062
Typeinf  1,441,489  1,441,489  1,314,324  1,319,901
Hilbert  3,188  3,188  4,860  4,860
Funtrans  9,508  9,508  9,422  9,462

Table 8: The Effect of Separating Contraction and Renumbering Walks