조건부 독립, 베이지안 조건화(Bayesian conditioning), 그리고 Pearl의 d-separation 건전성에 대한 입방체

Stone 이후 확률 모나드 (probability-monad) 형식화에서 흔히 사용되는 표준적인 볼록 대수 교환 공리 (convex-algebra interchange axiom)는 완전한 베이지안 조건화 (Bayesian conditioning)를 지원하기에는 증명 가능할 정도로 너무 약합니다. 우리는 이를 Cubical Agda에서 정밀하게 구현합니다: 고차 귀납적 타입 (higher inductive type, HIT)으로서의 유한 분포, 커널 (kernels) 사이의 입방체 경로 (cubical path)로서의 조건부 독립 (conditional independence), 그리고 전체 지원 파편 (full-support fragment) 상의 전함수 (total function)로서의 재귀적 베이지안 조건화. 조건화를 전체 HIT로 들어 올리면 구조적 불일치가 드러납니다. 즉, 재배열된 4-잎 혼합 (4-leaf mix)의 두 절반은 표준 공리가 제공하는 단일한 공유 내부 가중치가 아니라, 베이즈 정리 (Bayes' formula)에 의해 서로 연결된 별개의 베이지안 가중치를 가집니다. 우리는 이를 해결하는 최소한의 일반화를 제시하며, 표준 형태가 두 내부 가중치가 일치하는 퇴화된 사례 (degenerate case)임을 증명합니다. 이 관찰을 바탕으로, 우리는 추상적인 순서체 (ordered-field) 인터페이스 이상의 어떠한 공리도 없이 대수적 맥락을 구성적으로 검증합니다: 결합 교환성 (bind commutativity), 4가지 세미-그래포이드 공리 (four semi-graphoid axioms), 교집합 (intersection, 양의 조건 없이 구조적 $Σ$-증거 (structural $Σ$-witnesses)를 통해 수축 (contraction)으로 축소됨), 커널 형태의 Pearl의 do-calculus 규칙 1, 2, 3, 유한 타입 베이지안 조건화, 그리고 개입적 (interventional) 및 베이지안 형태 모두에서 임의의 $n$-정점 유한 유향 비순환 그래프 (directed acyclic graphs, DAGs)에 대한 Pearl의 d-separation 정리 (건전성). 또한 확률 모나드가 마르코프 범주 (Markov category)임을 검증하며, 추상 인터페이스는 $Q$에서 해소됩니다.