On Contextual Distances in Randomized Programming: Amplification and Lower Bounds

on YouTube ↗10m

" summary

Proves that contextual distance trivializes (non‑equivalent programs reach distance 1) via a probabilistic construction: build copying k times and empirical mean test amplification contexts that drive one program’s observation to 1 and the other’s to 0 as k grows, using the weak law of large numbers. Uses refinements — central limit theorem, Berry–Esseen, Chernoff–Hoeffding — to give explicit lower bounds on graded and amortized distances and to quantify the convergence speed; works in terminating probabilistic lambda languages, breaks when divergence is allowed.

AI-written summary · about

" chapters (6)

1. 0:00Contextual distances intro
2. 1:48Trivialization problem
3. 3:55Alternative approaches
4. 5:00New proof with law of large numbers
5. 6:44Empirical mean testing
6. 8:50Future work