Categorical Models of Amortized Cost: An Adjoint Relationship between Cost and Potential

Problema
Sistemas de tipos foram desenvolvidos para rastrear o custo computacional $\kappa$ de programas, tipicamente utilizando monadas de rastreamento de custo $M_\kappa \tau$ para fornecer garantias de pior caso. No entanto, a análise de pior caso é frequentemente insuficiente para estruturas de dados funcionais, onde a complexidade amortizada é a métrica relevante. A análise amortizada baseia-se no método de potenciais, onde operações baratas armazenam potencial (créditos) para pagar por operações caras posteriormente. Embora sistemas como o $\lambda$-amor [Rajani et al. 2021] rastreiem com sucesso tanto o custo quanto o potencial no sistema de tipos, eles carecem de um modelo categórico geral. Os modelos existentes, como o modelo de relações lógicas de Kripke indexado por passos no artigo original do $\lambda$-amor, são altamente concretos e difíceis de compor com outras características de linguagem (ex: recursão, efeitos probabilísticos). Há uma necessidade de um framework categórico abstrato e composicional que explique a relação estrutural entre custo e potencial, facilitando a combinação da análise amortizada com outros efeitos computacionais.

Metodologia
Os autores abordam o problema identificando as propriedades matemáticas abstratas necessárias para modelos denotacionais de teorias de tipos envolvendo custo e potencial.

1. Generalização do Domínio de Custo: O artigo generaliza o domínio de custo de números reais positivos ($\mathbb{R}^+$) para um monóide comutativo ordenado $\mathcal{C}$ arbitrário.
2. Refinamento do Cálculo: Os autores introduzem o $\lambda$-amor Core, um cálculo refinado derivado do $\lambda$-amor. Este núcleo remove a primitiva complexa release e a substitui por três construtos mais primitivos: pay (usar potencial para pagar por custo), plet (ação functorial para potencial) e split (divisão de custo). Esta decomposição é motivada pela necessidade de alinhar a sintaxe com as estruturas categóricas subjacentes.
3. Modelagem Categórica: Os autores propõem que o custo e o potencial devem ser modelados por uma relação de adjunção. Especificamente:
   • Custo é modelado por uma monada graduada $M$ (para sequenciamento de custos) que também é uma comonada graduada (para divisão de custos).
   • Potencial é modelado por um functor graduado $P$.
   • Interação: Para cada grau de custo $p$, existe uma adjunção $P_p \dashv M_p$. A unidade da adjunção corresponde a armazenar potencial (store), e a counidade corresponde a usar potencial para pagar por custo (pay/release).
4. Formalização: Os autores mecanizam o sistema de tipos e a verificação das leis do modelo no assistente de prova Lean.

Principais Contribuições
O artigo apresenta três contribuições primárias:

1. Modelo Adjunto Abstrato: Os autores descrevem um modelo abstrato geral onde custo e potencial estão relacionados por uma família de adjunções entre uma monada graduada forte (modelando custo) e um functor graduado forte (modelando potencial). Eles provam a correção deste modelo em relação à teoria equacional do $\lambda$-amor Core.
2. Mecanização e Instância de Kripke: Eles fornecem uma mecanização do sistema de tipos em Lean e verificam que o modelo de relações lógicas de Kripke do artigo original do $\lambda$-amor [Rajani et al. 2021] é uma instância específica de seu modelo categórico geral. Esta conexão não foi observada anteriormente e exigiu detalhes técnicos não triviais para ser provada.
3. Novo Modelo de Copresheaf: Eles apresentam um novo modelo baseado em copresheaves sobre uma categoria monoidal de custos. Neste modelo, pares e funções são modelados usando a convolução de Day e seu adjunto à direita. Isso fornece uma construção canônica para modelos de custo amortizado que difere do modelo de Kripke, particularmente na forma como interpreta a monada graduada de custo.

Resultos

• Correção (Soundness): O artigo prova que toda derivação de tipagem no $\lambda$-amor Core pode ser interpretada no modelo adjunto proposto.
• Equivalência: O modelo de relações lógicas de Kripke mostra satisfazer as leis do modelo categórico geral, confirmando que a estrutura abstrata captura a semântica concreta do sistema original.
• Decomposição: O artigo demonstra que a operação release no $\lambda$-amor original pode ser decomposta em pay, plet e split, e que estas primitivas podem ser reconstruídas a partir de release.
• Comparação de Modelos: O modelo de copresheaf mostra-se coincidente com o modelo de Kripke para tipos de potencial, mas oferece uma interpretação distinta para a monada graduada de custo, evitando a relação de força (forcing relation) explícita usada no modelo de Kripke.

Significância
O artigo afirma fornecer a peça "composicional" faltante para a compreensão da análise de custo amortizado em teoria de tipos. Ao estabelecer que custo e potencial estão relacionados via adjunções, os autores oferecem uma explicação estrutural de como a análise amortizada funciona, indo além de modelos concretos e ad-hoc. Este framework permite a potencial combinação do rastreamento de custo amortizado com outros efeitos determinísticos ou probabilísticos de maneira composicional. Além disso, o refinamento da sintaxe para o $\lambda$-amor Core, impulsionado por insights categóricos, simplifica a teoria equacional e clarifica a interação entre custo e potencial. Os autores posicionam este trabalho como uma fundação para construir teorias de tipos mais expressivas para análise quantitativa e para integrar modelos de custo amortizado com outros modelos categóricos de computação.