Multi types and reasonable space

Título: Multi types and reasonable space

Autores: Beniamino Accattoli, Ugo Dal Lago, Gabriele Vanoni
Contexto: Artigo estendido da versão apresentada na ICFP 2022.

1. O Problema

O cálculo $\lambda$ (lambda calculus) é o fundamento teórico das linguagens de programação funcionais. Um desafio central na teoria da complexidade computacional é definir modelos de custo razoáveis (reasonable cost models) para o cálculo $\lambda$. Um modelo é considerado "razoável" se simular máquinas de Turing com um sobrecarga polinomial no tempo e linear no espaço (Tese de Invariância de Slot e van Emde Boas).

• Tempo: Já foi estabelecido que o número de passos de redução $\beta$ (ou passos da Máquina Abstrata de Krivine - KAM) constitui um modelo de tempo razoável para avaliação forte e fraca.
• Espaço: O problema do espaço permaneceu em aberto por muito tempo. Medidas naturais de espaço (como o tamanho máximo dos termos durante a avaliação) não conseguem capturar a classe LOGSPACE (espaço logarítmico), pois não separam adequadamente o espaço de entrada do espaço de trabalho.
• Solução Parcial Recente: Recentemente, Accattoli, Dal Lago e Vanoni demonstraram que o Space KAM (uma variante otimizada da KAM) fornece um modelo de custo de espaço razoável, capaz de capturar LOGSPACE. No entanto, faltava uma caracterização estática (via sistemas de tipos) que extraísse esses limites de espaço diretamente dos termos $\lambda$, sem precisar simular a execução da máquina.

2. Metodologia

Os autores desenvolvem um novo sistema de tipos baseado em tipos múltiplos (uma variante não-idempotente dos tipos de interseção), adaptado especificamente para medir o consumo de espaço do Space KAM.

Conceitos Fundamentais:

• Tipos Múltiplos (Multi-types): Ao contrário dos tipos de interseção clássicos onde $A \cap A = A$, nos tipos múltiplos as interseções são tratadas como multiconjuntos. Isso permite rastrear quantas vezes um termo é copiado ou usado durante a redução.
• Space KAM: Uma máquina abstrata otimizada para espaço que implementa duas técnicas cruciais:
  1. Unchaining (Desencadeamento): Evita a criação de cadeias de renomeações em ambientes, prevenindo vazamentos de espaço.
  2. Coleta de Lixo Eager (Eager GC): Remove fechaduras (closures) mortas imediatamente.
  3. Sem Compartilhamento de Ponteiros: Para garantir razoabilidade de espaço, a máquina não usa ponteiros para estruturar ambientes e pilhas (usando strings não estruturadas), exceto ponteiros para o código inicial imutável.

O Sistema de Tipos Proposto (Closure Types):

Os autores introduzem o sistema Closure Types, que estende os tipos múltiplos tradicionais com as seguintes inovações:

1. Índices em Multiconjuntos: Cada multiconjunto de tipos associado a um argumento carrega um índice natural ($k$). Este índice representa o tamanho da fechadura (closure) que será construída para aquele argumento na máquina.
2. Ambientes de Tipos "Secos" (Dry Contexts): O sistema força que o domínio do ambiente de tipos corresponda exatamente às variáveis livres do termo ($dom(\Gamma) = fv(t)$). Isso é necessário porque, no Space KAM, variáveis não utilizadas ainda ocupam espaço no ambiente se não forem coletadas corretamente. O sistema usa um tratamento especial de enfraquecimento (weakening) para lidar com variáveis que existem no termo mas não são usadas (tipadas com multiconjuntos vazios mas com índice positivo).
3. Pesos (Weights): As derivações de tipos são decoradas com pesos que capturam o custo máximo de espaço atingido durante a execução.
   • O peso de um estado da máquina é calculado como a soma dos tamanhos dos ambientes e das fechaduras na pilha.
   • O peso final de uma derivação de tipo corresponde ao espaço máximo consumido pela execução completa da Space KAM.

3. Contribuições Chave

1. Correspondência de de Carvalho para Espaço: Estendem a famosa correspondência entre tipos múltiplos e a execução da KAM (originalmente para tempo) para o Space KAM, extraindo limites de espaço.
2. Caracterização Exata de Espaço: O sistema de tipos caracteriza e fornece o consumo exato de espaço para todos os termos $\lambda$ que terminam (em relação à avaliação call-by-name fraca).
3. Unificação de Tempo e Espaço: Demonstram que o mesmo sistema de tipos subjacente pode medir tanto o tempo quanto o espaço, dependendo apenas de como os pesos são atribuídos:
   • Para Espaço: Os pesos usam a operação de máximo ($\max$) sobre os estados alcançados.
   • Para Tempo de Baixo Nível: Os pesos usam a soma ($\sum$) dos tamanhos dos estados, capturando o tempo real de implementação da máquina (que é razoável, embora exponencial em relação aos passos $\beta$ puros).
4. Prova de Razoabilidade via Tipos: O sistema valida a razoabilidade do Space KAM de forma estática, mostrando que o espaço consumido é linearmente relacionado ao espaço de Turing (considerando o logaritmo do tamanho do código).
5. Modelos Denotacionais: Mostram que, devido ao uso não padrão de enfraquecimento (necessário para o controle de lixo), este sistema de tipos não induz um modelo denotacional (como os modelos relacionais tradicionais), pois a equivalência $\beta$ não é preservada na semântica dos tipos para termos abertos.

4. Resultados Principais

• Teorema de Correção (Espaço): Existe uma execução completa do Space KAM para um termo $t$ com consumo de espaço $w$ se e somente se existe uma derivação de tipos múltiplos para $t$ com peso $w$.
• Teorema de Correção (Tempo de Baixo Nível): Uma variante do sistema de pesos captura o tempo de execução real da implementação do Space KAM, confirmando que este é um modelo de tempo razoável.
• Extensão para Ponteiros de Tamanhos Diferentes: O sistema é refinado na Seção 9 para distinguir entre ponteiros de diferentes tamanhos (ex: ponteiros para o código da máquina vs. ponteiros para a entrada), utilizando um sistema de "split types" (tipos divididos em pares de contadores). Isso é essencial para provar a razoabilidade estrita (LOGSPACE) em simulações de máquinas de Turing.

5. Significância

• Resolução de um Problema Aberto: O trabalho fornece a primeira caracterização estática (via tipos) de um modelo de custo de espaço razoável para o cálculo $\lambda$, resolvendo um problema aberto de longa data.
• Ponte entre Semântica e Complexidade: Demonstra como sistemas de tipos avançados (tipos múltiplos) podem ser usados não apenas para provar terminação, mas para extrair métricas de complexidade operacionais precisas (tempo e espaço) de forma composicional.
• Fundamentos para Análise Estática: Abre caminho para a criação de analisadores estáticos que possam prever o uso de memória de programas funcionais com garantias teóricas rigorosas, baseadas na estrutura do código e não apenas em testes empíricos.
• Refinamento de Modelos de Custo: Clarifica a distinção entre modelos de custo de alto nível (passos $\beta$) e baixo nível (implementação da máquina), mostrando como ambos podem ser capturados pelo mesmo arcabouço teórico.

Em resumo, o artigo estabelece que a complexidade espacial de programas funcionais pode ser analisada e limitada rigorosamente através de um sistema de tipos sofisticado, alinhando a teoria dos tipos com a teoria da complexidade computacional moderna.