Evidence-Tracked Tape Semantics for Probabilistic Computation

TL;DR

This paper introduces an evidence-tracked tape semantics for probabilistic computation, enabling higher-order reasoning with explicit randomness and correlation, and deriving quantitative probabilistic statements within a logical framework.

Contribution

It develops a novel higher-order logic with evidence transformers for probabilistic programs, connecting intensional tape semantics to extensional law semantics.

Findings

Enables reasoning with explicit randomness and correlation.

Derives sound inequalities for probabilities and expectations.

Relates tape-based reasoning to extensional law semantics.

Abstract

A standard intensional account of probabilistic computation represents a randomized program as a deterministic computation that consumes an explicit random tape. This yields a two-layer perspective: an intensional layer that makes reuse of randomness and correlation visible, and an extensional layer obtained by interpreting tapes under a chosen probability measure. We develop an evidence-tracked tape semantics using the monadic-core-to-evidenced-frame pipeline (and its induced realizability tripos), obtaining a higher-order logic in which entailments are witnessed by uniform evidence transformers. Quantitative statements are recovered by interpretation: once a tape measure is fixed, probabilities and expectations arise by extracting numerical summaries from tape-indexed predicates, and entailments yield sound inequalities, with an almost-sure quotient supporting probability-one reasoning. We also study intensional principles that are lost at the level of laws, including proof-relevant transport along realizable tape-rewiring maps and a canonical splitting discipline for stream tapes enforcing independent draws. Finally, we relate tape-based reasoning to an extensional law semantics via pushforward, isolating a probability-one must abstraction as a sound summary of tape-based proofs.