Amplifying Contextual Distance in Higher-Order Languages, using the Law of Large Numbers
summary
Claim: contextual distance in a probabilistic higher-order language where every program terminates with probability 1 collapses to 0 or 1. Proof builds amplification contexts that copy an argument k times, run independent termination tests, compute the empirical mean and threshold it; the construction uses a binary probabilistic choice and requires call-by-value on base types. The new proof replaces Bernstein polynomials with the law of large numbers and uses the central limit for concrete bounds on how fast amplification converges; adding n‑out‑of‑m parallel convergence testers extends the same construction.
AI-written summary · about
chapters (9)
- 0:00Introduction
- 1:07Contextual equivalence in probabilistic languages
- 3:16Limitations of contextual equivalence
- 6:27Negative results on contextual distance
- 9:57New proof using Law of Large Numbers
- 15:52Non-terminating programs with parallel tests
- 18:41Threshold phenomena and social choice
- 20:54Perspectives on contextual distance
- 22:39Q&A
related talks
01h 02mDerandomization to Boolean Circuit Lower Bounds
01h 02mConditional Hardness for Massively Parallel Computing (MPC) Via Distributed Lower Bounds
01h 04mThe Easy Witness Lemma
25mStep-Indexed Logical Relations for Countable Nondeterminism and Probabilistic Ch...
24mVerifying Almost-Sure Termination for Randomized Distributed Algorithms
01h 07mMarrying Graph Convergence and Cascade Models
10mQuery, Communication and Discrepancy
29mOn disperser/lifting properties of the Index and Inner-Product functions