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.

翻译：概率计算的标准内涵描述将随机程序表示为消耗显式随机磁带的确定性计算。这产生了双层视角：内涵层使得随机性的重用和相关性可见，而外延层则通过选定的概率测度解释磁带获得。我们利用单子核到证据框架的管道（及其诱导的可实现性三元组），发展了基于证据磁带的语义，得到了一个高阶逻辑，其中蕴含关系由统一的证据变换器见证。定量陈述通过解释恢复：一旦固定磁带测度，概率和期望通过从磁带索引谓词中提取数值摘要而出现，蕴含关系产生合理的非等式，而几乎必然商支持概率为1的推理。我们还研究了在法则层面丢失的内涵原则，包括沿着可实现磁带重连映射的证明相关传输，以及强制独立抽取的流磁带的规范分裂规则。最后，通过前推将基于磁带的推理与外延法则语义联系起来，将概率为1的必须抽象隔离为基于磁带证明的合理摘要。