pith. machine review for the scientific record. sign in

arxiv: 2605.07259 · v1 · submitted 2026-05-08 · 💻 cs.LO

Recognition: 2 theorem links

· Lean Theorem

Evidence-Tracked Tape Semantics for Probabilistic Computation

Beer-Sheva, Israel), Liron Cohen (1), Tomer Samara (1) ((1) Ben-Gurion University of the Negev

Authors on Pith no claims yet

Pith reviewed 2026-05-11 02:05 UTC · model grok-4.3

classification 💻 cs.LO
keywords probabilistic computationtape semanticsevidence trackinghigher-order logicintensional semanticsrandomness reusequantitative reasoningprobability-one reasoning
0
0 comments X

The pith

An evidence-tracked tape semantics supplies a higher-order logic for probabilistic programs in which entailments are witnessed by evidence transformers.

A machine-rendered reading of the paper's core claim, the machinery that carries it, and where it could break.

The paper develops a way to reason about randomized programs by treating them as functions that consume explicit random tapes while tracking evidence for logical claims about those programs. This approach keeps the details of how randomness is reused and correlated visible at the intensional level. Once a probability measure on the tapes is fixed, the evidence yields sound numerical bounds on probabilities and expectations. The logic also supports certain intensional principles that disappear when reasoning only with the resulting probability laws.

Core claim

The central claim is that tape-based models of probabilistic computation can be equipped with evidence tracking to form a higher-order logic. In this logic, predicates are indexed by tapes, entailments are realized by uniform evidence transformers, and interpretation under a tape measure produces quantitative statements with sound inequalities. It further isolates intensional features such as transport along tape rewirings and a splitting rule for independent streams, and relates the whole system to extensional semantics through pushforward maps with a probability-one must abstraction.

What carries the argument

Evidence-tracked tape semantics, in which randomized programs are modeled as deterministic tape consumers and logical entailments are witnessed by uniform transformers that manipulate the evidence attached to tape predicates.

If this is right

  • Fixing a tape measure turns entailments into sound inequalities between probabilities and expectations.
  • The almost-sure quotient permits reasoning that holds with probability one.
  • Proof-relevant transport along tape-rewiring maps becomes available as an intensional principle.
  • Stream tapes admit a canonical splitting discipline that enforces independent random draws.
  • Pushforward maps provide a sound summary relating tape proofs to extensional laws of probability.

Where Pith is reading between the lines

These are editorial extensions of the paper, not claims the author makes directly.

  • Verification tools might benefit from explicit tracking of randomness dependencies in probabilistic programs.
  • The separation of intensional and extensional views could inform analysis of other computational models.
  • Concrete tests on algorithms like randomized sorting would check if evidence transformers remain manageable.

Load-bearing premise

The evidence-tracking construction can be applied to tape models of probabilistic computation without losing the intensional principles or the soundness of the quantitative interpretation.

What would settle it

A counterexample would be a simple probabilistic program, such as repeated coin flips, for which the derived entailments produce probability bounds that fail to match the actual values computed from the tape measure, or for which the claimed intensional transport principles do not hold.

read the original 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.

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, simulated authors' rebuttal, and a circularity audit. Tearing a paper down is the easy half of reading it; the pith above is the substance, this is the friction.

Referee Report

1 major / 3 minor

Summary. The paper develops an evidence-tracked tape semantics for probabilistic computation by applying the monadic-core-to-evidenced-frame pipeline and its induced realizability tripos. This yields a higher-order logic in which entailments are witnessed by uniform evidence transformers. Quantitative statements are recovered by fixing a tape measure and extracting numerical summaries from tape-indexed predicates, with entailments producing sound inequalities; an almost-sure quotient supports probability-one reasoning. The work studies preserved intensional principles (proof-relevant transport along realizable tape-rewiring maps and canonical stream splitting for independent draws) and relates the tape semantics to extensional law semantics via pushforward, isolating a probability-one must abstraction.

Significance. If the central construction is verified, the result supplies a logical bridge between intensional tape models (making randomness reuse and correlation explicit) and extensional probabilistic laws. The evidence-tracking mechanism provides witnessed entailments that translate directly to sound quantitative inequalities, while the preservation of specific intensional features (absent from law-based semantics) and the use of an established pipeline for uniformity are clear strengths. The approach supports higher-order reasoning about probabilistic programs with explicit randomness management and could facilitate formal verification tasks.

major comments (1)
  1. [§3] §3 (application of the pipeline): the claim that the monadic-core-to-evidenced-frame pipeline applies directly to tape-based models while preserving intensional principles requires an explicit check that the tape-indexed predicates and stream-splitting discipline commute with the induced realizability tripos; without this verification the preservation of proof-relevant transport is not load-bearing for the central claim.
minor comments (3)
  1. [Introduction] The definition of 'uniform evidence transformers' is introduced late; an early dedicated paragraph with the precise uniformity condition would improve readability for readers unfamiliar with the pipeline.
  2. Notation for the almost-sure quotient and the pushforward map should be introduced with a small diagram or table relating the intensional and extensional layers.
  3. [§4] A few sentences on how the tape measure is chosen (or left parametric) would clarify the quantitative recovery step.

Simulated Author's Rebuttal

1 responses · 0 unresolved

We thank the referee for the positive assessment and the constructive suggestion regarding §3. We address the major comment below.

read point-by-point responses

  1. Referee: [§3] §3 (application of the pipeline): the claim that the monadic-core-to-evidenced-frame pipeline applies directly to tape-based models while preserving intensional principles requires an explicit check that the tape-indexed predicates and stream-splitting discipline commute with the induced realizability tripos; without this verification the preservation of proof-relevant transport is not load-bearing for the central claim.

    Authors: We agree that an explicit verification of commutation would make the preservation of intensional principles more robust and directly load-bearing for the central claim. Although the monadic-core-to-evidenced-frame pipeline is functorial and our tape model is defined to satisfy the required monadic structure (ensuring direct applicability by construction), we will add a dedicated paragraph in the revised §3. This will explicitly confirm that tape-indexed predicates and the canonical stream-splitting discipline commute with the induced realizability tripos, verifying uniformity of the evidence transformers for rewiring maps and independent draws. The addition will not alter any theorems but will clarify the interaction. revision: yes

Circularity Check

0 steps flagged

No significant circularity

full rationale

The paper applies an existing monadic-core-to-evidenced-frame pipeline and its induced realizability tripos to tape-based probabilistic models. The resulting higher-order logic, evidence transformers, quantitative recovery via tape measures, and pushforward to extensional laws are presented as direct consequences of this application. No equations reduce the new semantics to a fitted parameter, self-definition, or prior result by the same authors. The intensional principles (proof-relevant transport, stream splitting) are isolated as preserved features rather than derived by construction from the inputs. The construction is self-contained against the external pipeline benchmark.

Axiom & Free-Parameter Ledger

0 free parameters · 1 axioms · 2 invented entities

The central claim rests on the applicability of the monadic-core-to-evidenced-frame pipeline to probabilistic tape models and on the existence of uniform evidence transformers and an almost-sure quotient; these are treated as given by the pipeline rather than derived from more elementary principles.

axioms (1)
  • domain assumption The monadic-core-to-evidenced-frame pipeline induces a realizability tripos suitable for tape semantics
    Invoked to obtain the higher-order logic with uniform evidence transformers.
invented entities (2)
  • Uniform evidence transformers no independent evidence
    purpose: Witness entailments in the higher-order logic for tape-indexed predicates
    Introduced as part of the semantics construction; no independent falsifiable handle supplied in the abstract.
  • Almost-sure quotient no independent evidence
    purpose: Support probability-one reasoning over tape-based proofs
    New construct for the framework; no external evidence given.

pith-pipeline@v0.9.0 · 5508 in / 1589 out tokens · 51870 ms · 2026-05-11T02:05:54.815905+00:00 · methodology

discussion (0)

Sign in with ORCID, Apple, or X to comment. Anyone can read and Pith papers without signing in.

Lean theorems connected to this paper

Citations machine-checked in the Pith Canon. Every link opens the source theorem in the public Lean library.

Reference graph

Works this paper leans on

37 extracted references · 37 canonical work pages

  1. [1]

    Di Gianantonio, Pietro and Edalat, Abbas , year =. A. doi:10.1145/3661814.3662126 , booktitle =

    work page doi:10.1145/3661814.3662126

  2. [2]

    1991 , organization=

    Pitts, Andrew M , booktitle=. 1991 , organization=. doi:10.1007/978-1-4471-3182-3_11

    work page doi:10.1007/978-1-4471-3182-3_11 1991

  3. [3]

    Staton, Sam , title =. Programming Languages and Systems: 26th European Symposium on Programming, ESOP 2017, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2017, Uppsala, Sweden, April 22–29, 2017, Proceedings , pages =. 2017 , isbn =. doi:10.1007/978-3-662-54434-1_32 , abstract =

    work page doi:10.1007/978-3-662-54434-1_32 2017

  4. [5]

    2020 , publisher=

    Aguirre, Alejandro and Katsumata, Shin-ya , journal=. 2020 , publisher=

    work page 2020

  5. [6]

    Probabilistic

    Barthe, Gilles and K\". Probabilistic. ACM Transactions on Programming Languages and Systems , publisher =. 2013 , month = nov, pages =. doi:10.1145/2492061 , number =

    work page doi:10.1145/2492061 2013

  6. [7]

    Giry, Michèle , year =. A. doi:10.1007/bfb0092872 , booktitle =

    work page doi:10.1007/bfb0092872

  7. [8]

    Heunen, Chris and Kammar, Ohad and Staton, Sam and Yang, Hongseok , year =. A. doi:10.1109/lics.2017.8005137 , booktitle =

    work page doi:10.1109/lics.2017.8005137 2017

  8. [9]

    POPL , year =

    Barthe, Gilles and Gr"un, Benjamin and others , title =. POPL , year =

    work page

  9. [10]

    Mathematics of Program Construction , year =

    McIver, Annabelle and Morgan, Carroll , title =. Mathematics of Program Construction , year =

    work page

  10. [11]

    Borel S tructures for F unction S paces

    Aumann, Robert J. Borel S tructures for F unction S paces. Illinois Journal of Mathematics. 1961. doi:10.1215/ijm/1255631584

    work page doi:10.1215/ijm/1255631584 1961

  11. [12]

    Measurable

    Ehrhard, Thomas and Pagani, Michele and Tasson, Christine , year =. Measurable. Proceedings of the ACM on Programming Languages , publisher =. doi:10.1145/3158147 , number =

    work page doi:10.1145/3158147

  12. [13]

    , year =

    Chaitin, Gregory J. , year =. A. Journal of the ACM , publisher =. doi:10.1145/321892.321894 , number =

    work page doi:10.1145/321892.321894

  13. [14]

    A Demonic

    Zilberstein, Noam and Kozen, Dexter and Silva, Alexandra and Tassarotti, Joseph , year =. A Demonic. Proceedings of the ACM on Programming Languages , publisher =. doi:10.1145/3704855 , number =

    work page doi:10.1145/3704855

  14. [15]

    Barthe, Gilles and Hsu, Justin and Liao, Kevin , year =. A. Proceedings of the ACM on Programming Languages , publisher =. doi:10.1145/3371123 , number =

    work page doi:10.1145/3371123

  15. [16]

    LIPIcs, Volume 131, FSCD 2019 , volume =

    Differentials and. LIPIcs, Volume 131, FSCD 2019 , volume =. 2019 , copyright =. doi:10.4230/LIPICS.FSCD.2019.17 , author =

    work page doi:10.4230/lipics.fscd.2019.17 2019

  16. [17]

    , year =

    Gill, John T. , year =. Computational. doi:10.1145/800119.803889 , booktitle =

    work page doi:10.1145/800119.803889

  17. [18]

    Semantics for

    Staton, Sam and Yang, Hongseok and Wood, Frank and Heunen, Chris and Kammar, Ohad , year =. Semantics for. doi:10.1145/2933575.2935313 , booktitle =

    work page doi:10.1145/2933575.2935313

  18. [19]

    Semantics of

    Kozen, Dexter , year =. Semantics of. Journal of Computer and System Sciences , publisher =. doi:10.1016/0022-0000(81)90036-2 , number =

    work page doi:10.1016/0022-0000(81)90036-2

  19. [20]

    10175691

    Dahlqvist, Fredrik and Silva, Alexandra and Smith, William , year =. Deterministic. doi:10.1109/lics56636.2023.10175773 , booktitle =

    work page doi:10.1109/lics56636.2023.10175773 2023

  20. [21]

    and Henzinger, Thomas A

    Gordon, Andrew D. and Henzinger, Thomas A. and Nori, Aditya V. and Rajamani, Sriram K. , year =. Probabilistic. doi:10.1145/2593882.2593900 , booktitle =

    work page doi:10.1145/2593882.2593900

  21. [22]

    2018 , copyright =

    An Introduction to Probabilistic Programming , publisher =. 2018 , copyright =. doi:10.48550/ARXIV.1809.10756 , author =

    work page doi:10.48550/arxiv.1809.10756 2018

  22. [23]

    Boneh, Dan and Shoup, Victor , description =

    work page

  23. [24]

    Saini, Anish and Tsokanos, Athanasios and Kirner, Raimund , year =. Quantum. Information , publisher =. doi:10.3390/info13080358 , number =

    work page doi:10.3390/info13080358

  24. [25]

    Corin, Ricardo and den Hartog, Jerry , year =. A. doi:10.1007/11787006_22 , booktitle =

    work page doi:10.1007/11787006_22

  25. [26]

    Kaminski, Benjamin Lucien and Katoen, Joost-Pieter and Matheja, Christoph and Olmedo, Federico , year =. Weakest. doi:10.1007/978-3-662-49498-1_15 , booktitle =

    work page doi:10.1007/978-3-662-49498-1_15

  26. [27]

    Relational Reasoning via Probabilistic Coupling , ISBN =

    Barthe, Gilles and Espitau, Thomas and Grégoire, Benjamin and Hsu, Justin and Stefanesco, Léo and Strub, Pierre-Yves , year =. Relational Reasoning via Probabilistic Coupling , ISBN =. doi:10.1007/978-3-662-48899-7_27 , booktitle =

    work page doi:10.1007/978-3-662-48899-7_27

  27. [28]

    36th Annual

    Cohen, Liron and Miquey, Etienne and Tate, Ross , year =. Evidenced. doi:10.1109/lics52264.2021.9470514 , booktitle =

    work page doi:10.1109/lics52264.2021.9470514 2021

  28. [29]

    Hyland, J. M. E. and Johnstone, P. T. and Pitts, A. M. , year =. Tripos. Mathematical Proceedings of the Cambridge Philosophical Society , publisher =. doi:10.1017/s0305004100057534 , number =

    work page doi:10.1017/s0305004100057534

  29. [30]

    , year =

    Pitts, Andrew M. , year =. Tripos. Mathematical Structures in Computer Science , publisher =. doi:10.1017/s096012950200364x , number =

    work page doi:10.1017/s096012950200364x

  30. [31]

    Notions of

    Moggi, Eugenio , year =. Notions of. Information and Computation , publisher =. doi:10.1016/0890-5401(91)90052-4 , number =

    work page doi:10.1016/0890-5401(91)90052-4

  31. [32]

    Zilberstein, Noam and Dreyer, Derek and Silva, Alexandra , year =. Outcome. Proceedings of the ACM on Programming Languages , publisher =. doi:10.1145/3586045 , number =

    work page doi:10.1145/3586045

  32. [33]

    Notes by G

    John von Neumann , title =. Notes by G. E. Forsythe, in National Bureau of Standards, Applied Mathematics Series , volume =. 1951 , publisher =

    work page 1951

  33. [34]

    Alternating Nominal Automata with Name Allocation , booktitle =

    Cohen, Liron and Grunfeld, Ariel and Kirst, Dominik and Miquey,. 40th Annual ACM/IEEE Symposium on Logic in Computer Science (LICS) , year=. doi:10.1109/lics65433.2025.00009 , volume=

    work page doi:10.1109/lics65433.2025.00009 2025

  34. [35]

    10th International Conference on Formal Structures for Computation and Deduction (FSCD 2025) , pages =

    Cohen, Liron and Grunfeld, Ariel and Kirst, Dominik and Miquey, \'. 10th International Conference on Formal Structures for Computation and Deduction (FSCD 2025) , pages =. 2025 , volume =. doi:10.4230/LIPIcs.FSCD.2025.14 , annote =

    work page doi:10.4230/lipics.fscd.2025.14 2025

  35. [36]

    Abstraction, R efinement and P roof for P robabilistic S ystems

    Annabelle McIver and Carroll Morgan. Abstraction, R efinement and P roof for P robabilistic S ystems. 2005. doi:10.1007/b138392

    work page doi:10.1007/b138392 2005

  36. [37]

    Noam Zilberstein and Alexandra Silva and Joseph Tassarotti , year = 2026, month =. Proc. ACM Program. Lang. , publisher =. doi:10.1145/3776651 , issue_date =

    work page doi:10.1145/3776651 2026

  37. [38]

    doi:10.48550/ARXIV.2404.01256 , author =

    2024 , copyright =. doi:10.48550/ARXIV.2404.01256 , author =

    work page doi:10.48550/arxiv.2404.01256 2024