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

Sintesi Tecnica: Una Formalizzazione Cubica dell'Indipendenza Condizionata, del Condizionamento Bayesiano e della Correttezza della D-Separazione di Pearl

Enunciato del Problema
Il saggio affronta una lacuna fondamentale nella verifica formale del ragionamento probabilistico: l'assoma di scambio algebrico convesso standard, comune alle formalizzazioni del monade della probabilità sin da Stone, è dimostrabilmente troppo debole per supportare il pieno condizionamento bayesiano. Mentre le formalizzazioni classiche (ad esempio in Coq) trattano l'indipendenza condizionata (CI) come un'uguaglianza proposizionale tra probabilità a valori reali, esse si affidano alla logica classica e all'estensionalità, richiedendo spesso ipotesi di positività e la divisione per probabilità non nulle per derivare risultati strutturali come l'assioma di intersezione. Inoltre, elevare il condizionamento bayesiano ricorsivo a una rappresentazione tramite Tipi Induttivi Superiori (HIT) di distribuzioni rivela un disallineamento strutturale: l'assoma di scambio standard assume un singolo peso interno condiviso per le miscele riorganizzate, mentre il condizionamento bayesiano produce naturalmente miscele con pesi distinti correlati dalla formula di Bayes.

Metodologia
L'autore sviluppa una formalizzazione costruttiva in Cubical Agda, utilizzando la Teoria dei Tipi Cubici e i Tipi Induttivi Superiori (HIT). La metodologia si basa su tre spostamenti strutturali rispetto agli approcci classici:

1. Monade della Probabilità come HIT: Le distribuzioni finite (FDist) sono definite come un HIT generato da masse puntuali e un'operazione di miscelazione pesata binaria. Le leggi dell'algebra convessa standard (idempotenza, skew-commutatività, casi limite, scambio e skew-associatività) sono imposte come costruttori di cammini (path constructors). Ciò consente di trattare le uguaglianze distribuzionali come trasformazioni eseguibili (cammini) piuttosto che come uguaglianze proposizionali opache.
2. Indipendenza Condizionata Strutturale: La CI è definita come un cammino tra kernel di distribuzione (kXY z ≡ kX z ⊗D kY z) piuttosto che come un'uguaglianza punto a punto di numeri reali. Ciò consente un ragionamento composizionale in cui i testimoni di CI possono essere trasportati attraverso operazioni monadiche.
3. Gestione Costruttiva dei Pesi: Lo sviluppo è polimorfico rispetto a una firma di Peso astratta (un campo ordinato con ordine decidibile), istanziata concretamente sui razionali ($\mathbb{Q}$). Ciò evita l'indecidibilità dell'uguaglianza nei reali costruttivi e permette la gestione esplicita di positività e divisione.

Contributi Chiave e Risultati

• Il Disallineamento dello Scambio e la Generalizzazione: Il risultato tecnico centrale è che l'assoma di scambio standard (legge mediale) è insufficiente per il pieno condizionamento bayesiano. Il condizionamento di una miscela a 4 foglie crea due metà interne con pesi distinti ($q_1$ e $q_2$) correlati dalla formula di Bayes, mentre l'assoma standard richiede che siano identici ($q_1 = q_2$). L'autore introduce un assoma di scambio generalizzato (mix-bayes-interchange) che permette pesi interni distinti. Si dimostra che la forma standard è il caso degenere in cui questi pesi coincidono.
• Assioma di Intersezione Costruttivo: Il saggio fornisce una prova costruttiva dell'assioma di intersezione (che classicamente richiede la positività) riducendolo alla contrazione. Inve no di estrazione bayesiana tramite divisione, la prova utilizza testimoni strutturali di tipo $\Sigma$ di fattorizzazione e ipotesi di inabitazione per le variabili di condizionamento. Ciò recupera il contenuto completo dell'intersezione per qualsiasi modello di distribuzione positiva concreta senza postulati.
• Verifica del Do-Calculus di Pearl: Tutti e tre i regole del do-calculus di Pearl sono verificati a livello di kernel su piccoli modelli causali strutturali (SCM):
  • Regole 1 e 3: Verificate come corollari delle leggi del monade e del lemma constBind (l'intervento su variabili indipendenti lascia invariate le marginali).
  • Regola 2: Verificata su SCM confondenti usando un testimone di CI strutturale secondo cui il prior congiunto si fattorizza. Ciò stabilisce l'equivalenza tra intervento e condizionamento sotto indipendenza.
• Condizionamento Bayesiano Ricorsivo: Una funzione totale per il condizionamento bayesiano ricorsivo è definita su un frammento a supporto completo dell'HIT. L'autore soddisfa tutti i sei obblighi di coerenza richiesti per elevare questa funzione al pieno HIT. La quinta coerenza (scambio) richiede il l'assoma generalizzato menzionato sopra.
• Allineamento con le Categorie di Markov: Il monade FDist è verificato come un'istanza concreta di una categoria di Markov (nel senso di Fritz e Cho–Jacobs). L'assoma non banale di delete-naturality (preservazione della massa totale) è dimostrato tramite induzione HIT, confermando che i costruttori di cammino catturano correttamente la normalizzazione stocastica.
• Correttezza della D-Separazione: La correttezza del teorema di d-separazione di Pearl è verificata costruttivamente per arbitrari Grafi Aciclici Diretti (DAG) finiti. Ciò copre sia le forme interventive (per insiemi multi-elemento $X, Y, Z$) che le forme bayesiane (per pattern elementari), derivate tramite fattorizzazione ancestrale senza riduzione per percorso.

Significatività e Rivendicazioni
Il saggio rivendica di fornire la prima formalizzazione verificata da macchina della direzione di correttezza del teorema di d-separazione di Pearl a questo livello di generalità, interamente all'interno di un framework di teoria dei tipi.

• Contenuto Computazionale: A differenza delle formalizzazioni classiche dove la CI è un'asserzione, l'approccio cubico produce contenuto computazionale. I testimoni di CI sono trasformazioni eseguibili; le distribuzioni a posteriori sono termini eseguibili calcolati dal normalizzatore di Agda.
• Correzione Fondamentale: Il lavoro identifica che la base algebrica standard per le monadi della probabilità è "troppo debole" per il condizionamento bayesiano. La generalizzazione proposta dell'assoma di scambio è presentata come un raffinamento strutturale necessario per qualsiasi framework che miri a supportare il pieno inferenza bayesiana in un contesto monadico.
• Verifica dello Stack di Mahadevan: Il saggio verifica lo "strato inferiore" del framework Topos Causal Model (TCM) di Mahadevan. Conferma che le identità di kernel del do-calculus e la monade della distribuzione commutativa valgono costruttivamente, fungendo da substrato verificato su cui la macchina topos-teorica (fogli, semantica di forcing) può essere costruita.
• Zero Postulati: L'intero sviluppo, inclusi la correttezza della d-separazione e il condizionamento bayesiano, è verificato con zero postulati sopra l'interfaccia astratta del campo ordinato (istanziata in $\mathbb{Q}$). Ciò include la rimozione dei precedenti limiti non corretti e la sostitazione della divisione classica con operazioni costruttive protette dalla positività.

Il saggio conclude che il contenuto costruttivo dell'indipendenza condizionata e del condizionamento è meglio catturato non dalla logica classica più l'estensionalità, ma dal ragionamento strutturale e basato sui cammini della teoria dei tipi cubici, dove le leggi algebriche della probabilità sono intrinseche alla definizione del tipo.