pith. sign in

arxiv: 2606.20351 · v1 · pith:AJBS4QLTnew · submitted 2026-06-18 · 💻 cs.LO · cs.PL

A cubical formalisation of conditional independence, Bayesian conditioning, and Pearl's d-separation soundness

Karen Sargsyan This is my paper

Pith reviewed 2026-06-26 15:10 UTC · model grok-4.3

classification 💻 cs.LO cs.PL
keywords conditional independenced-separationBayesian conditioningdo-calculusCubical Agdahigher inductive typesMarkov categoryprobability monad
0
0 comments X

The pith

A minimal generalization of the convex interchange axiom in Cubical Agda permits verification of Pearl's d-separation soundness on arbitrary finite DAGs with no extra axioms.

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

The paper establishes that finite distributions formalized as a higher inductive type support conditional independence as cubical paths between kernels and recursive Bayesian conditioning as a total function on full-support fragments. It shows the standard interchange axiom is too weak by exhibiting a structural mismatch in the rearranged 4-leaf mixture, where the two halves carry distinct Bayesian weights linked by Bayes' formula rather than a single shared weight. The minimal generalization resolving this mismatch is then used to prove bind commutativity, the semi-graphoid axioms, intersection via structural witnesses, Pearl's do-calculus rules in kernel form, finite Bayesian conditioning, and d-separation soundness on any n-vertex DAG in both interventional and Bayesian forms. The probability monad is verified as a Markov category, all constructively above an abstract ordered-field interface. A sympathetic reader cares because this turns informal causal graphical criteria into machine-checked theorems that apply uniformly to finite graphs.

Core claim

The central claim is that defining finite distributions via a higher inductive type in Cubical Agda, expressing conditional independence as cubical paths between kernels, and adopting the minimal generalization of the interchange axiom (which reduces to the standard form precisely when the two inner weights coincide) allows constructive verification, with zero additional postulates, of bind commutativity, the four semi-graphoid axioms, intersection, Pearl's do-calculus Rules 1-3 in kernel form, finite-type Bayesian conditioning, and Pearl's d-separation theorem (soundness) on arbitrary n-vertex finite DAGs in both interventional and Bayesian forms; the probability monad is thereby verified a

What carries the argument

The higher inductive type for finite distributions together with cubical paths for conditional independence, which carries the lifting of recursive conditioning and the verification of all algebraic and graphical properties.

If this is right

  • Bind commutativity holds for the formalized kernels.
  • The four semi-graphoid axioms are provable for conditional independence.
  • Pearl's three do-calculus rules hold in kernel form.
  • d-separation implies conditional independence in both interventional and Bayesian forms for every finite n-vertex DAG.
  • The probability monad satisfies the axioms of a Markov category.

Where Pith is reading between the lines

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

  • The separation of the algebraic requirements into an abstract ordered-field interface suggests the same development could be instantiated over other models that satisfy the interface.
  • Expressing conditional independence via cubical paths may allow similar homotopy-based treatments of other probabilistic notions such as almost-sure equality.
  • The constructive character of the proofs means the formalization can serve as a library for machine-checked causal reasoning on concrete graphs.

Load-bearing premise

The abstract ordered-field interface supplies enough structure to discharge all the listed theorems without any probability-specific extra axioms.

What would settle it

An explicit four-vertex DAG together with a concrete distribution over an ordered field such that the formalized d-separation predicate fails to match the actual conditional independence relation computed from the kernels.

read the original abstract

The standard convex-algebra interchange axiom, common to probability-monad formalisations since Stone, is provably too weak to support full Bayesian conditioning. We make this precise in Cubical Agda: finite distributions as a higher inductive type, conditional independence as a cubical path between kernels, recursive Bayesian conditioning as a total function on a full-support fragment. Lifting conditioning to the full HIT exposes a structural mismatch -- the two halves of the rearranged 4-leaf mix carry distinct Bayesian weights related by Bayes' formula, not the single shared inner weight the standard axiom provides. We exhibit the minimal generalisation that resolves this and prove the standard form is the degenerate case where the two inner weights coincide. Around this observation we verify the algebraic context constructively, with zero postulates above an abstract ordered-field interface: bind commutativity, the four semi-graphoid axioms, intersection (reduced to contraction via structural $\Sigma$-witnesses, without positivity), Pearl's do-calculus Rules~1, 2, and~3 in kernel form, finite-type Bayesian conditioning, and Pearl's d-separation theorem (soundness) on arbitrary $n$-vertex finite directed acyclic graphs (DAGs) in both interventional and Bayesian forms. The probability monad is also verified as a Markov category; the abstract interface discharges at $Q$.

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

0 major / 2 minor

Summary. The manuscript presents a Cubical Agda formalization of finite distributions as a higher inductive type, conditional independence as cubical paths between kernels, and a minimal generalization of the convex-algebra interchange axiom to support full Bayesian conditioning. It constructively verifies bind commutativity, the four semi-graphoid axioms, intersection via Σ-witnesses, Pearl's do-calculus rules in kernel form, finite-type Bayesian conditioning, and Pearl's d-separation soundness (both interventional and Bayesian) on arbitrary n-vertex finite DAGs, together with the probability monad as a Markov category, all with zero additional postulates above an abstract ordered-field interface that discharges at Q.

Significance. If the machine-checked claims hold, the work supplies a constructive, axiom-minimal foundation for probabilistic and causal reasoning in homotopy type theory. The explicit identification of the structural mismatch in the standard interchange axiom (distinct Bayesian weights versus a single shared weight) and its resolution via a minimal generalization, together with the machine-checked d-separation result on arbitrary finite DAGs, constitute a substantive contribution that can serve as a verified library for further developments in formal causality and Markov categories.

minor comments (2)
  1. The abstract refers to 'the rearranged 4-leaf mix' and 'the two halves'; an explicit small example (e.g., a 4-element support with distinct weights) in the main text would make the structural mismatch concrete for readers.
  2. The claim that the development sits 'above an abstract ordered-field interface with zero postulates' is central; a short appendix or table listing the exact interface operations used by each major theorem would improve auditability.

Simulated Author's Rebuttal

0 responses · 0 unresolved

We thank the referee for their positive summary, significance assessment, and recommendation to accept the manuscript. There are no major comments requiring a point-by-point response.

Circularity Check

0 steps flagged

No significant circularity; machine-checked formalization is self-contained above the ordered-field interface.

full rationale

The paper presents a Cubical Agda development that constructs finite distributions as a HIT, defines conditional independence via cubical paths, and proves bind commutativity, semi-graphoid axioms, do-calculus, intersection, Bayesian conditioning, and d-separation soundness on arbitrary finite DAGs. All theorems are discharged directly from an abstract ordered-field interface with zero extra postulates, and the interface is shown to hold at Q. Because the proofs are machine-checked and the central results are derived constructively without reducing any theorem to a fitted parameter, self-referential definition, or unverified self-citation chain, the derivation chain is independent of its inputs. No load-bearing step matches any of the enumerated circularity patterns.

Axiom & Free-Parameter Ledger

0 free parameters · 1 axioms · 0 invented entities

The entire development rests on the abstract ordered-field interface and the cubical type theory of Agda; no free parameters or invented entities are introduced.

axioms (1)
  • domain assumption abstract ordered-field interface
    All proofs are discharged above this interface with zero additional postulates, as stated in the abstract.

pith-pipeline@v0.9.1-grok · 5765 in / 1326 out tokens · 28517 ms · 2026-06-26T15:10:52.356227+00:00 · methodology

discussion (0)

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

Reference graph

Works this paper leans on

13 extracted references · 12 canonical work pages

  1. [1]

    Formal adventures in convex and conical spaces

    [AGS20a] Reynald Affeldt, Jacques Garrigue, and Takafumi Saikawa. Formal adventures in convex and conical spaces. In Christoph Benzm¨ uller and Bruce Miller, editors,Intelligent Computer Mathe- matics: 13th International Conference (CICM 2020), volume 12236 ofLecture Notes in Computer Science, pages 23–38. Springer, 2020.doi:10.1007/978-3-030-53518-6\_2. ...

    work page doi:10.1007/978-3-030-53518-6 2020

  2. [2]

    37.3\_79

    doi:10.11309/jssst. 37.3\_79. [BCJ+19] Eli Bingham, Jonathan P. Chen, Martin Jankowiak, Fritz Obermeyer, Neeraj Pradhan, Theofanis Karaletsos, Rohit Singh, Paul Szerlip, Paul Horsfall, and Noah D. Goodman. Pyro: Deep universal probabilistic programming.Journal of Machine Learning Research, 20(28):1–6,

    work page doi:10.11309/jssst

  3. [3]

    Gordon, and Marcin Szymczak

    [BDGS16] Johannes Borgstr¨ om, Ugo Dal Lago, Andrew D. Gordon, and Marcin Szymczak. A lambda- calculus foundation for universal probabilistic programming. InProceedings of the 21st ACM SIGPLAN International Conference on Functional Programming (ICFP), pages 33–46. ACM, 2016.doi:10.1145/2951913.2951942. [CCHM18] Cyril Cohen, Thierry Coquand, Simon Huber, a...

    work page doi:10.1145/2951913.2951942 2016

  4. [4]

    [CJ19] Kenta Cho and Bart Jacobs

    doi:10.4230/LIPIcs.TYPES.2015.5. [CJ19] Kenta Cho and Bart Jacobs. Disintegration and Bayesian inversion via string diagrams.Mathe- matical Structures in Computer Science, 29(7):938–971,

    work page doi:10.4230/lipics.types.2015.5 2015

  5. [5]

    Disintegration and Bayesian inversion via string diagrams

    doi:10.1017/S0960129518000488. [Dob06] Ernst-Erich Doberkat. Eilenberg–Moore algebras for stochastic relations.Information and Com- putation, 204(12):1756–1781, 2006.doi:10.1016/j.ic.2006.09.001. [FGPR23] Tobias Fritz, Tom´ aˇ s Gonda, Paolo Perrone, and Eigil Fjeldgren Rischel. Representable Markov cat- egories and comparison of statistical experiments i...

    work page doi:10.1017/s0960129518000488 2006

  6. [6]

    doi:10.1016/j.aim.2020. 107239. 26 K. SARGSYAN [Gir82] Mich` ele Giry. A categorical approach to probability theory. InCategorical Aspects of Topology and Analysis, volume 915 ofLecture Notes in Mathematics, pages 68–85. Springer,

    work page doi:10.1016/j.aim.2020 2020

  7. [7]

    [GVP90] Dan Geiger, Thomas Verma, and Judea Pearl

    doi: 10.1007/BFb0092872. [GVP90] Dan Geiger, Thomas Verma, and Judea Pearl. Identifying independence in Bayesian networks. Networks, 20(5):507–534, 1990.doi:10.1002/net.3230200504. [H¨17] Johannes H¨ olzl. Markov processes in Isabelle/HOL. InProceedings of the 6th ACM SIGPLAN International Conference on Certified Programs and Proofs (CPP), pages 100–111. ACM,

    work page doi:10.1007/bfb0092872 1990

  8. [8]

    [HJ23] Macartan Humphreys and Alan M

    doi:10.1145/3018610.3018628. [HJ23] Macartan Humphreys and Alan M. Jacobs.Integrated Inferences: Causal Models for Qualitative and Mixed-Method Research. Cambridge University Press, 2023.doi:10.1017/9781316718636. [HKSY17] Chris Heunen, Ohad Kammar, Sam Staton, and Hongseok Yang. A convenient category for higher-order probability theory. InProceedings of ...

    work page doi:10.1145/3018610.3018628 2023

  9. [9]

    Topology Appl.158(16), 2232–2239 (2011)https://doi.org/10.1016/j.topol

    doi:10.1016/j.topol. 2008.07.002. [KW21] Donnacha Ois´ ın Kidney and Nicolas Wu. Algebras for weighted search.Proceedings of the ACM on Programming Languages, 5(ICFP):72:1–72:30, 2021.doi:10.1145/3473577. [Mah25a] Sridhar Mahadevan. Intuitionistic j-do-calculus in topos causal models.arXiv preprint arXiv:2510.17944,

    work page doi:10.1016/j.topol 2008

  10. [10]

    Universal causal inference in a topos

    [Mah25b] Sridhar Mahadevan. Universal causal inference in a topos. InAdvances in Neural Information Processing Systems 39 (NeurIPS 2025),

    2025

  11. [11]

    Modelling recursion and probabilistic choice in guarded type theory.Proc

    [SK20] Amit Sharma and Emre Kıcıman. DoWhy: An end-to-end library for causal inference.arXiv preprint arXiv:2011.04216, 2020.arXiv:2011.04216. [SMZ+25] Philipp Jan Andries Stassen, Rasmus Ejlers Møgelberg, Maaike Zwart, Alejandro Aguirre, and Lars Birkedal. Modelling recursion and probabilistic choice in guarded type theory.Proceedings of the ACM on Progr...

    work page doi:10.1145/3704884 2011

  12. [12]

    Semantics for probabilistic programming: Higher-order functions, continuous distributions, and soft constraints

    [SYW+16] Sam Staton, Hongseok Yang, Frank Wood, Chris Heunen, and Ohad Kammar. Semantics for probabilistic programming: Higher-order functions, continuous distributions, and soft constraints. InProceedings of the 31st Annual ACM/IEEE Symposium on Logic in Computer Science (LICS), pages 525–534. ACM, 2016.doi:10.1145/2933575.2935313. [VKS19] Matthijs V´ ak...

    work page doi:10.1145/2933575.2935313 2016

  13. [13]

    [VMA19] Andrea Vezzosi, Anders M¨ ortberg, and Andreas Abel

    doi:10.1145/3290349. [VMA19] Andrea Vezzosi, Anders M¨ ortberg, and Andreas Abel. Cubical Agda: A dependently typed programming language with univalence and higher inductive types. InProceedings of the ACM on Programming Languages (ICFP), volume 3, pages 87:1–87:29, 2019.doi:10.1145/3341691. This work is licensed under the Creative Commons Attribution Lic...

    work page doi:10.1145/3290349 2019