Types, equations, dimensions and the Pi theorem

1. El Problema

Los autores identifican una brecha fundamental entre el lenguaje de la física matemática y el modelado por un lado, y las abstracciones de los lenguajes de programación funcional (FP) y la programación dependiente por otro.

• Falta de "Gramática de Dimensiones": Los lenguajes de programación estándar y las abstracciones comunes de FP (como Haskell o Idris) carecen de una representación adecuada de la "gramática de dimensiones" inherente a la física. En física, no todas las funciones son simplemente de tipo $\mathbb{R}^m \to \mathbb{R}^n$; tienen propiedades semánticas críticas (longitud, tiempo, masa, temperatura) que determinan la consistencia de las ecuaciones.
• Inconsistencia en la Validación: En áreas como la ciencia del clima o la física de plasmas, donde la validación empírica es imposible o demasiado costosa, los modelos computacionales deben ser correctos por construcción. Sin embargo, los físicos y modeladores no adoptan lenguajes de tipos dependientes porque las anotaciones de tipo actuales no capturan las diferencias que importan (ej. longitud vs. tiempo) y, a menudo, complican derivaciones que son intuitivas en papel (como la adimensionalización de ecuaciones).
• El Teorema de Pi de Buckingham: Este teorema fundamental del análisis dimensional permite reducir la complejidad de los problemas físicos al identificar parámetros adimensionales. Sin embargo, su formulación clásica es no constructiva y difícil de formalizar en sistemas de tipos, lo que impide su aplicación automatizada en la derivación de programas.

2. Metodología

Los autores proponen el desarrollo de un Lenguaje Específico de Dominio (DSL) incrustado en Idris, un lenguaje de programación funcional con tipos dependientes. La metodología se basa en los siguientes pilares:

• Formalización de Dimensiones como Tipos: En lugar de tratar las unidades como metadatos o cadenas de texto, las dimensiones se codifican como tipos. Utilizan vectores de enteros para representar funciones de dimensión (ej. en mecánica, un vector de longitud 3 para Longitud, Tiempo y Masa).
• Tipos Dependientes para Cantidades Físicas: Definen un tipo de dato Q d (Cantidad Física) indexado por su dimensión d. Esto permite que el verificador de tipos rechace operaciones inválidas (como sumar una longitud con un tiempo) en tiempo de compilación.
• Principio de Covarianza: Formalizan el principio de que las leyes físicas no dependen del sistema de unidades elegido. Esto se modela como un homomorfismo entre el álgebra de cantidades físicas y el álgebra de números reales. Es decir, medir una cantidad y luego operar es equivalente a operar y luego medir.
• Abordaje Constructivo del Teorema de Pi: Reconocen que la formulación clásica del Teorema de Pi es no constructiva (existencial). En su lugar, proponen una metodología para "aplicar" el teorema de manera verificada, construyendo funciones que satisfacen las restricciones dimensionales por construcción, en lugar de intentar probar la existencia de la función física desconocida.

3. Contribuciones Clave

El artículo presenta varias contribuciones técnicas significativas:

1. DSL Minimalista en Idris:

   • Implementación de funciones de dimensión usando vectores de enteros (Vec 3 Z para mecánica).
   • Definición de cantidades físicas (Q d) que anotan valores reales con dimensiones y sistemas de unidades.
   • Operadores combinadores (Times, Over, Pow) que permiten derivar dimensiones compuestas (velocidad, fuerza, energía) de manera tipada.

2. Formalización del Principio de Covarianza:

   • Demuestran que las operaciones elementales (+, -, *, /) sobre cantidades físicas preservan la covarianza.
   • Proban que la función de medición $\mu_u$ es un homomorfismo, garantizando que los resultados son independientes del sistema de unidades utilizado.

3. Formulación del Teorema de Pi en Teoría de Tipos:

   • Definen tipos que representan las premisas del teorema: independencia dimensional de parámetros y dependencia de otros.
   • Reconocen la naturaleza no constructiva de la prueba clásica (que requiere eliminación de doble negación) y, por tanto, no implementan el teorema como una función que "descubre" leyes físicas automáticamente.

4. Método Constructivo para Derivación de Programas (applyPi):

   • Introducen una función applyPi que toma una "función de forma" (una función sobre números reales obtenida de datos o primeros principios) y la transforma en una función de cantidades físicas que garantiza cumplir con el Teorema de Pi y el principio de covarianza.
   • Esto permite a los programadores definir la estructura dimensional de una ley física y dejar que el sistema de tipos verifique la consistencia, mientras la forma funcional específica se determina empíricamente.

5. Análisis de Dependencia e Independencia Dimensional:

   • Implementan procedimientos decidibles para verificar si un conjunto de dimensiones es linealmente independiente (crucial para aplicar el teorema) y para encontrar los exponentes que hacen que una cantidad sea adimensional.

4. Resultados

• Verificación de Consistencia: El DSL permite detectar errores de dimensionalidad (ej. sumar masa y tiempo) en tiempo de compilación, algo que los lenguajes imperativos tradicionales (C, Python, Fortran) no hacen.
• Reducción de Parámetros: El enfoque permite formalizar cómo reducir un problema con múltiples parámetros dimensionales a uno con menos parámetros adimensionales, replicando el poder del Teorema de Pi en un entorno de programación.
• Ejemplo del Péndulo: Los autores demuestran la utilidad del sistema aplicándolo al péndulo simple. Logran deducir que el cuadrado del periodo ($\tau^2$) es proporcional a la longitud dividida por la gravedad ($l/g$), independientemente de la masa, y construyen una función verificada que respeta esta relación.
• Idoneidad para FP: El trabajo demuestra que los lenguajes de tipos dependientes pueden manejar la complejidad de la física sin ser excesivamente verbosos, siempre que se diseñen las abstracciones correctas (como el uso de vectores de enteros en lugar de números racionales para mantener la decidibilidad).

5. Significancia

• Puente entre Disciplinas: El trabajo actúa como un puente crucial entre la ciencia de la computación (específicamente la programación funcional y los tipos dependientes) y la física/modelado. Hace que la FP sea más "palatable" para físicos al abordar sus preocupaciones reales (dimensiones, unidades) en lugar de imponer abstracciones ajenas.
• Seguridad en Modelado Crítico: Ofrece una metodología para garantizar la corrección de modelos computacionales en dominios donde la experimentación es imposible (cambio climático, fusión nuclear), reduciendo el riesgo de errores conceptuales en las ecuaciones.
• Nueva Perspectiva en el Teorema de Pi: Cambia la visión del Teorema de Pi de ser una herramienta puramente analítica a una herramienta de derivación de programas. Permite construir leyes físicas verificadas que respetan las restricciones de similitud física.
• Futuro de la Ciencia Computacional: Sugiere que la formalización de principios de relatividad (como la independencia de las unidades) mediante teoría de tipos podría extenderse a otras ciencias (biología, economía), donde los principios de similitud son menos claros pero potencialmente aplicables.

En resumen, Botta y Jansson no solo han creado una herramienta técnica para verificar dimensiones, sino que han propuesto un nuevo paradigma para la interacción entre la programación y la física, donde la consistencia dimensional es una propiedad intrínseca y verificable del código, facilitando la colaboración interdisciplinaria y la creación de modelos más robustos.