Interpreting Lambda Calculus in Domain-Valued Random Variables

Sintesi Tecnica: Interpretazione del Lambda Calcolo in Variabili Casuali a Valore di Dominio

Enunciato del Problema
Il saggio affronta la sfida di fornire una fondazione semantica per i linguaggi di programmazione probabilistica, in particolare quelli che coinvolgono tipi di ordine superiore e scelta probabilistica. Mentre approcci precedenti hanno utilizzato spazi di coerenza probabilistici, coni e spazi quasi-Borel, gli autori si concentrano sull'approccio del modello a valori booleani avviato da Dana Scott. Una specifica limitazione identificata nel lavoro precedente (ad es. [BFK+18]) è che l'interpretazione dei concetti della teoria dei domini (come gli insiemi diretti e la continuità) rimaneva spesso "esterna" o dipendeva da restrizioni artificiali nel gestire la casualità. Inoltre, l'insieme delle variabili casuali a valore di dominio non forma naturalmente un ordine parziale completo diretto (dcpo) continuo nel senso standard, complicando l'interpretazione del lambda calcolo non tipizzato.

Metodologia
Gli autori adottano una prospettiva "completamente booleana", ricostruendo la teoria dei domini partendo dalle fondamenta all'interno di un universo di insiemi a valori booleani ($V^A$), dove $A$ è un'algebra booleana completa.

1. Teoria degli Insiemi a Valori Booleani: Il saggio sviluppa la necessaria strumentazione teoria degli insiemi, interpretando l'uguaglianza e l'appartenenza come valori nell'algebra booleana $A$ piuttosto che come valori di verità binari. Ciò comporta la definizione di insiemi $A$-valori tramite una gerarchia cumulativa e l'instaurazione del fatto che i teoremi di ZFC valgono con valore booleano 1 in questo universo.
2. Teoria dei Domini a Valori Booleani: Gli autori definiscono $A$-setoid (insiemi dotati di una relazione di equivalenza a valori $A$) e $A$-poset. Fondamentalmente, distinguono tra definizioni "esterne" e interpretazioni interne. Ad esempio, un "dcpo continuo" è definito internamente all'interno di $V^A$. Il saggio dimostra che, sebbene l'insieme delle variabili casuali $L^0(X; P(Y))$ non sia un dcpo continuo nel senso classico, esso è un dcpo continuo quando il concetto di continuità è interpretato internamente tramite la logica a valori booleani.
3. Costruzione di un Dominio Riflessivo: Il nucleo della metodologia consiste nella costruzione di un dcpo riflessivo (un dominio $D$ isomorfo a un ritratto del suo spazio di funzioni $[D \to D]$) all'interno dell'universo a valori booleani. Gli autori utilizzano il modello di Engeler, adattato a $V^A$, dove il dominio è costruito dal parte dell'insieme enumerabile $E$.
4. Isomorfismo con le Variabili Casuali: Il saggio stabilisce un isomorfismo tra l'insieme delle parti a valori booleani $P_A(\check{Y})$ (dove $\check{Y}$ è il nome canonico per un insieme $Y$) e lo spazio delle funzioni misurabili $L^0(X; P(Y))$ modulo un ideale nullo, collegando efficacemente l'astratto modello a valori booleani alle concrete variabili casuali a valore di dominio.

Contributi Chiave

• Ricostruzione Interna della Teoria dei Domini: Il contributo primario è lo sviluppo di una teoria dei domini a valori booleani in cui i concetti base come uguaglianza, ordine e continuità sono interpretati internamente. Questo approccio supera i precedenti metodi "a mani nude" trasferendo i teoremi dalla logica ordinaria alla logica a valori booleani, risultando in una teoria più semplice e robusta.
• Risoluzione del Problema della Continuità: Il saggio prova che, sebbene le variabili casuali a valore di dominio non formino un dcpo continuo nel senso set-teoretico standard, esse formano un tale struttura quando "dcpo continuo" è interpretato nel senso a valori booleani. Ciò consente l'interpretazione standard del lambda calcolo non tipizzato.
• Teoremi di Isomorfismo: Gli autori dimostrano che la categoria degli $A$-insiemi è equivalente alla categoria degli $A$-setoid e che l'insieme delle parti a valori booleani $P_A(\check{Y})$ è strettamente isomorfo allo spazio delle variabili casuali $L^0(X; P(Y))$ (modulo uno spazio di negligenza).
• Applicazione a Gradi Incomparabili: Il saggio fornisce un'applicazione concreta provando l'esistenza di due insiemi di interi, nessuno dei quali può essere mappato all'altro da una funzione $\lambda$-definibile. Questo risultato è derivato puramente all'interno del lambda calcolo e del framework probabilistico, senza invocare l'equivalenza tra $\lambda$-definibilità e ricorsione generale o il teorema di Kleene-Post.

Risultati

• Costruzione del Modello: Gli autori costruiscono con successo un modello del lambda calcolo non tipizzato nel modello di Engeler interpretato all'interno di $V^A$. Dimostrano che per ogni dcpo riflessivo $D$ in $V^A$, esistono funzioni di interpretazione per i termini $\lambda$ che rispettano le equazioni provabili.
• Incomparabilità Probabilistica: Utilizzando il modello costruito, il saggio dimostra l'esistenza di due insiemi di interi $T_1, T_2 \subseteq \mathbb{N}$ tali che $T_1 \not\leq_m T_2$ e $T_2 \not\leq_m T_1$ (dove $\leq_m$ denota la riducibilità many-one tramite funzioni $\lambda$-definibili). Ciò viene ottenuto definendo gli insiemi $S_1, S_2$ nell'universo a valori booleani che sono "incomparabili" con valore booleano 1, ed estraendo poi gli insiemi classici $T_1, T_2$ da un punto specifico dello spazio probabilistico sottostante.
• Limiti della Continuità Classica: Il saggio mostra esplicitamente che $L^0(X; P(Y))$ non è un dcpo continuo nel senso classico se l'algebra booleana sottostante non è atomica, rinforzando la necessità dell'interpretazione interna a valori booleani.

Significatività e Rivendicazioni
Il saggio sostiene che la sua ricostruzione completamente a valori booleani offre una "teoria molto più semplice" che rimane fedele alla visione di Dana Scott di utilizzare modelli set-teoretici per il lambda calcolo. Lavorando "internamente", gli autori evitano le restrizioni artificiali presenti nelle precedenti teorie dei domini a valori booleani.

La significatività del lavoro risiede nella sua capacità di gestire processi di ordine superiore in modo composizionale. Gli autori osservano che il loro framework permette l'interpretazione del lambda calcolo esteso con la scelta probabilistica. Inoltre, l'esempio degli insiemi incomparabili dimostra che il modello è abbastanza potente da provare fatti sulla computabilità e la teoria della ricorsione che non menzionano esplicitamente la probabilità, pur facendo affidamento sul ragionamento probabilistico per la loro dimostrazione. Il saggio conclude delineando direzioni future, come la definizione del condizionamento come primitiva ed esplorazione della semantica operativa all'interno di un framework a valori booleani, ma non rivendica di aver risolto ancora questi problemi.