Interpreting Lambda Calculus in Domain-Valued Random Variables

Resumo Técnico: Interpretando o Cálculo Lambda em Variáveis Aleatórias de Valores de Domínio

Enunciado do Problema
O artigo aborda o desafio de fornecer uma fundação semântica para linguagens de programação probabilísticas, especificamente aquelas que envolvem tipos de ordem superior e escolha probabilística. Embora abordagens anteriores tenham utilizado espaços de coerência probabilísticos, cones e quase-espaços de Borel, os autores focam na abordagem de modelo de valor booleano iniciada por Dana Scott. Uma limitação específica identificada em trabalhos anteriores (por exemplo, [BFK+18]) é que a interpretação de conceitos da teoria dos domínios (como conjuntos direcionados e continuidade) frequentemente permanecia "externa" ou dependia de restrições artificiais ao lidar com a aleatoriedade. Além disso, o conjunto de variáveis aleatórias de valores de domínio não forma naturalmente um preorder completo direcionado contínuo (dcpo) no sentido padrão, complicando a interpretação do cálculo $\lambda$ não tipado.

Metodologia
Os autores adotam uma perspectiva "completamente de valor booleano", reconstruindo a teoria dos domínios do zero dentro de um universo de conjuntos de valor booleano ($V^A$), onde $A$ é uma álgebra booleana completa.

1. Teoria dos Conjuntos de Valor Booleano: O artigo desenvolve a maquinaria de teoria dos conjuntos necessária, interpretando igualdade e pertinência como valores na álgebra booleana $A$, em vez de valores de verdade binários. Isso envolve a definição de conjuntos $A$-valorados via uma hierarquia cumulativa e o estabelecimento de que os teoremas de ZFC são válidos com valor booleano 1 neste universo.
2. Teoria dos Domínios de Valor Booleano: Os autores definem $A$-setoids (conjuntos equipados com uma relação de equivalência $A$-valorada) e $A$-posets. Crucialmente, eles distinguem entre definições "externas" e interpretações internas. Por exemplo, um "dcpo contínuo" é definido internamente dentro de $V^A$. O artigo demonstra que, embora o conjunto de variáveis aleatórias $L^0(X; P(Y))$ não seja um dcpo contínuo no sentido clássico, ele é um dcpo contínuo quando o conceito de continuidade é interpretado internamente via lógica de valor booleano.
3. Construção de Domínio Reflexivo: O núcleo da metodologia envolve a construção de um dcpo reflexivo (um domínio $D$ isomorfo a um retrete de seu espaço de funções $[D \to D]$) dentro do universo de valor booleano. Os autores utilizam o modelo de Engeler, adaptado para $V^A$, onde o domínio é construído a partir do conjunto das partes de um conjunto enumerável $E$.
4. Isomorfismo com Variáveis Aleatórias: O artigo estabelece um isomorfismo entre o conjunto das partes de valor booleano $P_A(\check{Y})$ (onde $\check{Y}$ é o nome canônico para um conjunto $Y$) e o espaço de funções mensuráveis $L^0(X; P(Y))$ módulo um ideal nulo, vinculando efetivamente o modelo abstrato de valor booleano a variáveis aleatórias concretas de valores de domínio.

Principais Contribuições

• Reconstrução Interna da Teoria dos Domínios: A principal contribuição é o desenvolvimento de uma teoria de domínios de valor booleano onde conceitos básicos como igualdade, ordem e continuidade são interpretados internamente. Esta abordagem supera métodos anteriores "de mãos vazias" ao transferir teoremas da lógica ordinária para a lógica de valor booleano, resultando em uma teoria mais simples e robusta.
• Resolução da Questão da Continuidade: O artigo prova que, embora as variáveis aleatórias de valores de domínio não formem um dcpo contínuo no sentido clássico da teoria dos conjuntos, elas formam um quando "dcpo contínuo" é interpretado no sentido de valor booleano. Isso permite a interpretação padrão do cálculo $\lambda$ não tipado.
• Teoremas de Isomorfismo: Os autores provam que a categoria de $A$-conjuntos é equivalente à categoria de $A$-setoids e que o conjunto das partes de valor booleano $P_A(\check{Y})$ é estritamente isomorfo ao espaço de variáveis aleatórias $L^0(X; P(Y))$ (modulo um espaço de negligibilidade).
• Aplicação a Graus Incomparáveis: O artigo fornece uma aplicação concreta ao provar a existência de dois conjuntos de inteiros, nenhum dos quais pode ser mapeado para o outro por uma função $\lambda$-definível. Este resultado é derivado puramente dentro do cálculo $\lambda$ e do framework probabilístico, sem invocar a equivalência entre $\lambda$-definibilidade e recursão geral ou o teorema de Kleene-Post.

Resultos

• Construção de Modelo: Os autores constroem com sucesso um modelo do cálculo $\lambda$ não tipado no modelo de Engeler interpretado dentro de $V^A$. Eles mostram que, para qualquer dcpo reflexivo $D$ em $V^A$, existem funções de interpretação para termos $\lambda$ que respeitam equações prováveis.
• Incomparabilidade Probabilística: Usando o modelo construído, o artigo demonstra a existência de dois conjuntos de inteiros $T_1, T_2 \subseteq \mathbb{N}$ tais que $T_1 \not\leq_m T_2$ e $T_2 \not\leq_m T_1$ (onde $\leq_m$ denota redução de muitos-para-um via funções $\lambda$-definíveis). Isso é alcançado definindo conjuntos $S_1, S_2$ no universo de valor booleano que são "incomparáveis" com valor booleano 1, e então extraindo conjuntos clássicos $T_1, T_2$ de um ponto específico no espaço de probabilidade subjacente.
• Limitações da Continuidade Clássica: O artigo mostra explicitamente que $L^0(X; P(Y))$ não é um dcpo contínuo no sentido clássico se a álgebra booleana subjacente não for atômica, reforçando a necessidade da interpretação interna de valor booleano.

Significância e Alegações
O artigo afirma que sua reconstrução completamente de valor booleano oferece uma "teoria muito mais simples" que permanece fiel à visão de Dana Scott de usar modelos de teoria dos conjuntos para o cálculo $\lambda$. Ao trabalhar "internamente", os autores evitam as restrições artificiais encontradas em teorias de domínios de valor booleano anteriores.

A significância do trabalho reside em sua capacidade de lidar com processos probabilísticos de ordem superior de forma composicional. Os autores observam que seu framework permite a interpretação do cálculo $\lambda$ estendido com escolha probabilística. Além disso, o exemplo de conjuntos incomparáveis demonstra que o modelo é poderoso o suficiente para provar fatos sobre teoria da computabilidade e da recursão que não mencionam explicitamente a probabilidade, mas que dependem do raciocínio probabilístico para sua prova. O artigo conclui delineando direções futuras, como definir o condicionamento como um primitivo e explorar semânticas operacionais dentro de um framework de valor booleano, mas não afirma ter resolvido esses problemas ainda.