55 lines
1.7 KiB
Python
55 lines
1.7 KiB
Python
#!/usr/bin/env python3
|
|
# bench-lean4-0003.py
|
|
# lean4-0003: fresh name generation while loop
|
|
#
|
|
# Models the Lean4 Name.mkFresh / getUnusedName defect where the while
|
|
# loop calls List.contains (O(N)) to check for collisions with N existing
|
|
# names. For each of M candidates checked, cost is O(M*N). Fixed version
|
|
# builds a HashSet once and checks O(1) per candidate.
|
|
|
|
import sys
|
|
import time
|
|
|
|
def bench_defective(n):
|
|
"""Model while loop with list membership check: O(N) per iteration."""
|
|
existing = list(range(n))
|
|
t0 = time.perf_counter()
|
|
candidate = n # will not be found -- simulates worst-case scan
|
|
for _ in range(n):
|
|
_ = candidate in existing # O(N) each time
|
|
return time.perf_counter() - t0
|
|
|
|
def bench_fixed(n):
|
|
"""Model while loop with set membership check: O(1) per iteration."""
|
|
existing = list(range(n))
|
|
existing_set = set(existing) # O(N) build once
|
|
t0 = time.perf_counter()
|
|
candidate = n
|
|
for _ in range(n):
|
|
_ = candidate in existing_set # O(1)
|
|
return time.perf_counter() - t0
|
|
|
|
TRIALS = 3
|
|
SIZES = [100, 500, 1000]
|
|
|
|
def run():
|
|
lines = []
|
|
header = "=== lean4-0003: fresh name generation ==="
|
|
print(header)
|
|
lines.append(header)
|
|
|
|
for n in SIZES:
|
|
def_times = [bench_defective(n) for _ in range(TRIALS)]
|
|
fix_times = [bench_fixed(n) for _ in range(TRIALS)]
|
|
d_ms = min(def_times) * 1000
|
|
f_ms = min(fix_times) * 1000
|
|
speedup = d_ms / f_ms if f_ms > 0 else float('inf')
|
|
line = f"N={n:<5}: defective={d_ms:.3f}ms fixed={f_ms:.3f}ms speedup={speedup:.1f}x"
|
|
print(line)
|
|
lines.append(line)
|
|
sys.stdout.flush()
|
|
|
|
return lines
|
|
|
|
if __name__ == "__main__":
|
|
run()
|