将因果推理推广到拓扑层上的直觉主义逻辑框架,实现局部真值下的干预推断。
Intuitionistic $j$-Do-Calculus in Topos Causal Models
- 基于拓扑层上层的模态算子 $j$,用局部真值替代全局真值进行因果推断
- 提出 $j$-do 计算规则,可形式化为保持结构的同态映射,并在克里普克-乔伊尔语义中证明其保真性
- 适用于复杂系统中依赖于局部数据结构的因果建模,适合理论因果推断研究者
本文将珍珠的 do-演算推广至一个称为 $j$-稳定因果推理的直觉主义设定中,该设定位于层的范畴(topos of sheaves)内。我们的框架是近期提出的拓扑因果模型(TCMs)的扩展,其中因果干预被定义为子对象。通过拓扑上的劳弗莱-蒂埃尼拓扑(Lawvere-Tierney topology),由子对象分类器 $Ω$ 上的模态算子 $j$ 定义,我们引入了 $j$-do-演算。该演算以克里普克-乔伊尔语义中的局部真值取代全局真值,并将因果推理形式化为沿 $j$-覆盖稳定的结构保持态射。$j$-do-演算是一个保真规则系统,其前提与结论均为因果拓扑内部的直觉主义逻辑公式。我们定义了条件独立性和干预命题的 $j$-稳定性,即作为因果拓扑内部逻辑中的局部真值。给出三条推理规则,分别对应珍珠的插入/删除和行动/观测交换,并在克里普克-乔伊尔语义中证明其保真性。一篇配套论文将描述如何从数据中估计所需实体并实例化 $j$-do-演算,包括:(i) 通过制度/截面构造形成数据驱动的 $j$-覆盖,(ii) 在图手术后计算局部条件独立性,(iii) 将其拼接以验证 $j$-do 规则的前提。
原文摘要 · Abstract (English)
In this paper, we generalize Pearl's do-calculus to an Intuitionistic setting called $j$-stable causal inference inside a topos of sheaves. Our framework is an elaboration of the recently proposed framework of Topos Causal Models (TCMs), where causal interventions are defined as subobjects. We generalize the original setting of TCM using the Lawvere-Tierney topology on a topos, defined by a modal operator $j$ on the subobject classifier $Ω$. We introduce $j$-do-calculus, where we replace global truth with local truth defined by Kripke-Joyal semantics, and formalize causal reasoning as structure-preserving morphisms that are stable along $j$-covers. $j$-do-calculus is a sound rule system whose premises and conclusions are formulas of the internal Intuitionistic logic of the causal topos. We define $j$-stability for conditional independences and interventional claims as local truth in the internal logic of the causal topos. We give three inference rules that mirror Pearl's insertion/deletion and action/observation exchange, and we prove soundness in the Kripke-Joyal semantics. A companion paper in preparation will describe how to estimate the required entities from data and instantiate $j$-do with standard discovery procedures (e.g., score-based and constraint-based methods), and will include experimental results on how to (i) form data-driven $j$-covers (via regime/section constructions), (ii) compute chartwise conditional independences after graph surgeries, and (iii) glue them to certify the premises of the $j$-do rules in practice
Thank you to arXiv for use of its open access interoperability. PaperDance 不是 arXiv 官方产品;中文卡片由大模型生成,请以原文为准。