图操作与do算子：非循环结构因果模型的精确对应关系

中文摘要 AI 辅助

do算子在图层面的描述是删除指向其目标变量的箭头，在函数层面的描述是用常数替换这些目标变量的机制。称这些操作等价目前还不是一个数学命题：前者返回一个图且仅保留目标变量，而后者返回机制且还保留施加的数值。我们针对具有有限个内生变量的确定性非循环结构因果模型，在依赖层面进行了精确比较。若Graph(F)提取机制族F的依赖关系，我们的主定理为Graph(F^ι)=Surg(Graph(F),T_ι)，即替换目标机制恰好移除图操作所移除的依赖关系。对于图中可能存在未使用箭头的模型M=(G,F)，我们刻画了用G替代Graph(F)时等式成立的条件：当且仅当G精确记录了F的依赖关系时，该等式对所有干预均成立。随后我们定义了干预后的模型，刻画其运行过程，说明序列干预如何结合，并证明结果仅依赖于其实际依赖祖先处的干预。

英文摘要

The $\operatorname{do}$-operator is described graphically by deleting arrows into its targets and functionally by replacing their mechanisms with constants. To call these operations equivalent is not yet a mathematical statement: one returns a graph and remembers only the targets, whereas the other returns mechanisms and also remembers the imposed values. We make a dependency-level comparison precise for deterministic acyclic structural causal models with finitely many endogenous variables. If $\operatorname{Graph}(F)$ extracts the dependencies of a mechanism family $F$, our main theorem is $\operatorname{Graph}(F^ι)=\operatorname{Surg}(\operatorname{Graph}(F),T_ι)$. Thus replacing target mechanisms removes exactly the dependencies removed by graph surgery. For a model $M=(G,F)$ whose graph may contain unused arrows, we characterize when the same equality holds with $G$ in place of $\operatorname{Graph}(F)$; it holds for every intervention exactly when $G$ records the dependencies of $F$ exactly. We then define the intervened model, characterize its run, show how sequential interventions combine, and prove that an outcome depends only on interventions at its actual dependency ancestors. All principal results are machine-checked in an accompanying Lean 4 development.

发表机构

• Ashoka University（阿育王大学）

机构由 AI 辅助整理，请以论文原文为准。