The notion of contextual equivalence in higher-order probabilistic programming languages captures the idea that two programs are indistinguishable when placed in any context — where contexts themselves are programs written in the same language. In a probabilistic setting, this idea can be naturally quantified, leading to the concept of contextual distance: the distance between two programs M and N is defined as the supremum of the difference that any context can observe in the behavior of M and N.
However, when copying of arguments by contexts is allowed and all programs terminate, this distance becomes trivial: any two non-equivalent programs are then always at maximal distance. In this work, we present a new proof of this trivialization phenomenon based on the weak law of large numbers, replacing purely analytic reasoning with probabilistic arguments. We then apply this approach to study amortized and graded variants of contextual distance, deriving explicit lower bounds using affine contexts and classical probabilistic tools such as the Central Limit Theorem, the Berry–Esseen theorem, and the Chernoff–Hoelding inequalities.
Simon Castellan University of Rennes; Inria; CNRS; IRISA, Tom Hirschowitz Univ. Grenoble Alpes, Univ. Savoie Mont Blanc, CNRS, LAMA, 73000 Chambéry, Hugo Paquet Inria, École Normale Supérieure