Types, equations, dimensions and the Pi theorem

1. O Problema

Os autores identificam uma lacuna significativa entre as linguagens da física matemática/modelagem e as linguagens de programação funcional (FP) e de tipos dependentes.

• Falha na Abstração: As abstrações comuns das linguagens de programação falham em representar a "gramática de dimensões" inerente à física. Físicos e modeladores utilizam notações onde variáveis possuem propriedades de dimensão (ex: comprimento, tempo, massa) que são cruciais para a consistência e correção, mas que são tratadas apenas como números reais (R) nas linguagens de programação padrão.
• Barreira de Adoção: Apesar dos benefícios da programação funcional e da especificação formal para garantir a correção de modelos complexos (especialmente em áreas onde a validação empírica é impossível, como ciência do clima ou fusão nuclear), físicos e modeladores não adotaram essas tecnologias. Isso ocorre porque as linguagens atuais não capturam as diferenças fundamentais entre quantidades físicas (ex: diferenciar um comprimento de um tempo) e, ao mesmo tempo, impõem anotações de tipo que são irrelevantes para os físicos (ex: distinguir entre tipos de funções que todos consideram ser R^m -> R^n).
• Inflação de Problemas: Modelos físicos frequentemente sofrem de "problemas inflados" (demasiados parâmetros), onde a redução de dimensionalidade via Análise Dimensional (AD) poderia simplificar drasticamente a computação, mas essa redução não é automática ou verificável em linguagens de programação convencionais.

2. Metodologia

Os autores propõem o desenvolvimento e a formalização de uma Linguagem Específica de Domínio (DSL) embutida na linguagem de programação de tipos dependentes Idris.

• Abordagem Construtiva: Em vez de apenas verificar equações existentes, eles buscam formalizar os conceitos fundamentais da Análise Dimensional (AD) e do Teorema de Buckingham Pi dentro da teoria de tipos.
• Representação de Dimensões:
  • As funções de dimensão são codificadas como vetores de inteiros (ex: [1, 0, 0] para comprimento, [0, 1, 0] para tempo, [0, 0, 1] para massa no sistema LTM).
  • Quantidades físicas são representadas por um tipo Q d, onde d é a dimensão, anotando valores reais com suas dimensões físicas.
  • O princípio de covariância (a ideia de que leis físicas não dependem do sistema de unidades escolhido) é formalizado como um homomorfismo entre a álgebra das quantidades físicas e a álgebra dos números reais.
• Formalização do Teorema de Pi: O teorema é expresso em teoria de tipos, definindo tipos para provar a existência de relações entre parâmetros dimensionais e produtos adimensionais. Reconhecem que a formulação clássica do teorema é não-construtiva (existencial) e propõem uma abordagem construtiva para sua aplicação prática.

3. Principais Contribuições

O artigo apresenta várias contribuições teóricas e práticas:

1. DSL para Programação Dimensionalmente Consistente: Uma implementação em Idris que permite definir quantidades físicas, realizar operações aritméticas (soma, multiplicação, divisão) apenas quando dimensionalmente compatíveis e realizar julgamentos de dimensão em tempo de compilação.
2. Formalização do Princípio de Covariância: Demonstram que operações elementares sobre quantidades físicas preservam o princípio de covariância, provando que o sistema de medição é um homomorfismo.
3. Formalização do Teorema de Buckingham Pi:
   • Apresentam uma versão do teorema em teoria de tipos que captura a dependência e independência dimensional.
   • Discutem a natureza não-construtiva das provas clássicas do teorema (que dependem do princípio do terceiro excluído ou eliminação de dupla negação).
   • Desenvolvem uma metodologia construtiva (applyPi) que permite derivar funções físicas válidas a partir de uma "função de forma" (shape function) e de evidências de dependência dimensional, garantindo que o resultado respeite o princípio de covariância por construção.
4. Exemplos Práticos: Aplicação da DSL em modelos clássicos, como o modelo de Stommel (oceanografia) e o pêndulo simples, demonstrando como reduzir a dimensionalidade e verificar a consistência de equações diferenciais.

4. Resultados

• Verificação de Consistência: O sistema permite detectar erros de dimensionalidade (ex: somar tempo com massa) durante a compilação, algo impossível em linguagens dinâmicas ou com sistemas de tipos fracos.
• Redução de Parâmetros: A metodologia permite identificar e eliminar parâmetros redundantes em modelos físicos, reduzindo a complexidade computacional (evitando a "maldição da dimensionalidade").
• Derivação de Leis Físicas: A abordagem applyPi permite que o programador especifique apenas a estrutura funcional (baseada em dados empíricos ou princípios) e o sistema de tipos garanta que a lei resultante seja dimensionalmente correta e covariante.
• Acessibilidade: O trabalho demonstra que é possível criar pontes entre a programação funcional e a física, tornando a FP mais atraente para modeladores ao resolver problemas que eles realmente enfrentam (consistência dimensional), em vez de impor abstrações genéricas.

5. Significado e Impacto

• Ponte Interdisciplinar: O trabalho é um passo crucial para unir cientistas da computação e físicos/modeladores, oferecendo uma linguagem comum baseada em tipos dependentes que respeita a semântica física.
• Confiabilidade em Modelagem Crítica: Em áreas onde a validação experimental é impossível ou perigosa (clima, fusão nuclear), a garantia formal de consistência dimensional e covariância oferece um nível de confiança superior ao dos métodos numéricos tradicionais.
• Futuro da Programação Científica: Sugere que a próxima geração de ferramentas de modelagem científica deve incorporar análise dimensional diretamente no sistema de tipos, permitindo a derivação automática de leis físicas e a redução de complexidade de dados.
• Limitações e Extensões Futuras: Os autores reconhecem que a representação atual usa inteiros (limitando raízes quadradas exatas, por exemplo) e que a generalização para qualquer número de dimensões fundamentais requer bibliotecas de álgebra linear mais robustas em teoria de tipos. No entanto, o protótipo estabelecido prova a viabilidade do conceito.

Em resumo, o artigo propõe que a Análise Dimensional não é apenas uma ferramenta de verificação manual, mas uma estrutura algébrica que pode e deve ser integrada ao sistema de tipos de linguagens de programação, transformando a consistência física em uma propriedade verificável automaticamente pelo compilador.