Types, equations, dimensions and the Pi theorem

1. Il Problema

Gli autori identificano un divario significativo tra le lingue della fisica matematica e della modellazione e quelle della programmazione funzionale (FP) e della specifica formale.

• Fallimento dell'adozione: Nonostante oltre un decennio di promozione della FP e dei linguaggi a tipi dipendenti (come Haskell, Agda, Idris) nella ricerca climatica e nella scienza dei sistemi globali, i fisici e i modellatori non li hanno adottati.
• Causa radice: I linguaggi di programmazione standard e le loro astrazioni falliscono nel rappresentare la "grammatica delle dimensioni" intrinseca alla fisica. Mentre i fisici lavorano con grandezze fisiche (forza, massa, tempo) che hanno proprietà dimensionali specifiche, i linguaggi di programmazione trattano spesso questi valori come semplici numeri reali ($\mathbb{R}$), perdendo informazioni cruciali sulla consistenza dimensionale.
• Limiti attuali: Le astrazioni FP esistenti si concentrano su annotazioni di tipo che sono irrilevanti per i fisici (es. $R^m \to R^n$), ma ignorano le differenze fondamentali tra grandezze fisiche (es. lunghezza vs. tempo). Inoltre, la mancanza di trasparenza referenziale e di informazioni sui tipi espliciti nei linguaggi di modellazione tradizionali rende difficile l'analisi formale e la verifica di correttezza, specialmente in domini dove la validazione empirica è impossibile (es. fisica del plasma, cambiamenti climatici).

2. Metodologia

Per colmare questo divario, gli autori propongono un approccio basato sui tipi dipendenti per formalizzare i concetti fondamentali dell'analisi dimensionale.

• Linguaggio Target: Utilizzano Idris, un linguaggio di programmazione funzionale a tipi dipendenti, per creare un Linguaggio Specifico di Dominio (DSL) incorporato.
• Formalizzazione Teorica:
  • Funzione di Dimensione: Definiscono formalmente la funzione di dimensione $[x]$ come una funzione che mappa un sistema di unità di misura in un fattore di scala. Dimostrano che queste funzioni sono monomi di potenza (es. $L^a T^b M^c$).
  • Grandezze Fisiche: Modellano le grandezze fisiche come tipi dipendenti che annotano i valori numerici con le loro dimensioni e il sistema di unità di misura.
  • Misura Omomorfa: Formalizzano il principio di covarianza (o relatività delle misure) come un omomorfismo tra le operazioni sulle grandezze fisiche e le operazioni sui numeri reali.
  • Teorema di Buckingham $\Pi$: Tentano di formalizzare il teorema di Buckingham, che afferma che una relazione fisica tra grandezze dimensionali può essere riscritta come una relazione tra parametri adimensionali.
• Approccio Costruttivo vs Non-Costruttivo: Riconoscono che la formulazione classica del Teorema di $\Pi$ è non-costruttiva (esiste una funzione $\Phi$ ma non è data esplicitamente). Pertanto, sviluppano una metodologia alternativa per "applicare" il teorema in modo costruttivo, permettendo la generazione di funzioni che rispettano il principio di covarianza per costruzione.

3. Contributi Chiave

Il lavoro presenta diversi contributi tecnici originali:

1. DSL per la Coerenza Dimensionale in Idris:
   • Implementazione di un tipo Q d (Quantità) che associa un valore reale a una dimensione d (rappresentata come vettore di interi, es. $[1, 0, 0]$ per la lunghezza).
   • Definizione di operatori aritmetici (+, *, /) che sono tipizzati per garantire che operazioni come l'addizione siano possibili solo tra grandezze della stessa dimensione, prevenendo errori concettuali (es. "aggiungere mele e arance").
   • Supporto per il calcolo automatico delle dimensioni di espressioni composte.
2. Formalizzazione del Principio di Covarianza:
   • Dimostrazione che le operazioni elementari sulle grandezze fisiche preservano il principio di covarianza (l'invarianza rispetto alla scelta delle unità di misura).
   • Formalizzazione del principio come un omomorfismo tra l'algebra delle grandezze fisiche e quella dei numeri reali.
3. Applicazione Costruttiva del Teorema di Buckingham $\Pi$:
   • Poiché la formulazione classica del teorema non è implementabile direttamente (richiede l'eliminazione della doppia negazione), gli autori introducono un tipo PhysFunType che codifica le condizioni di indipendenza e dipendenza dimensionale.
   • Sviluppo della funzione applyPi, che costruisce funzioni fisiche verificate combinando una "funzione di forma" (da determinare empiricamente o teoricamente) con termini di potenza dimensionale. Questo permette di generare funzioni che soddisfano il principio di covarianza per costruzione.
4. Esempi Pratici:
   • Applicazione del DSL al modello di Stommel (clima) e al pendolo semplice, dimostrando come ridurre la dimensionalità dei problemi e verificare la corretteza delle equazioni differenziali.

4. Risultati

• Verifica della Correttezza: Il sistema è in grado di verificare staticamente la coerenza dimensionale di espressioni complesse, rifiutando definizioni che violano le leggi fisiche fondamentali.
• Riduzione della Complessità: La metodologia permette di identificare automaticamente i gruppi adimensionali ($\Pi$), riducendo il numero di parametri necessari per descrivere un sistema fisico (es. riducendo da $N^{k+m}$ a $N^m$ nel costo computazionale per l'analisi dei dati).
• Dimostrazione di Fattibilità: È stato dimostrato che è possibile formalizzare concetti avanzati di fisica (come il teorema di $\Pi$ e il principio di relatività delle misure) all'interno di un sistema di tipi dipendenti, trasformando concetti matematici astratti in codice eseguibile e verificabile.
• Limiti Riconosciuti: La rappresentazione attuale utilizza esponenti interi (vettori di Z), il che limita l'uso di radici quadrate o esponenti razionali diretti senza estensioni future (es. numeri razionali). Inoltre, la formalizzazione completa dell'algebra lineare necessaria per determinare l'indipendenza dimensionale in domini generici richiede librerie esterne non ancora integrate completamente.

5. Significato e Impatto

Questo lavoro è significativo per diverse ragioni:

• Ponte Interdisciplinare: Offre un linguaggio comune che rende la programmazione funzionale più accessibile ai fisici e i concetti di modellazione fisica più comprensibili agli informatici.
• Affidabilità nella Modellazione: In campi critici come la scienza del clima o la fusione nucleare, dove la validazione empirica è costosa o impossibile, l'uso di tipi dipendenti per garantire la coerenza dimensionale offre un livello di sicurezza e fiducia nei modelli computazionali che i linguaggi tradizionali non possono fornire.
• Nuova Prospettiva sul Teorema di $\Pi$: Trasforma il Teorema di Buckingham da un risultato puramente teorico e non-costruttivo in uno strumento pratico per la derivazione di programmi verificati.
• Fondamento per Principi di Relatività: Suggerisce che i principi di relatività (invarianza rispetto a trasformazioni di scala o unità) possono essere formalizzati in teoria dei tipi, aprendo la strada a applicazioni in scienze economiche o biologiche dove tali principi sono meno definiti.

In sintesi, Botta e Jansson dimostrano che l'analisi dimensionale non è solo un controllo di consistenza manuale, ma può essere integrata nel cuore del sistema di tipi di un linguaggio di programmazione, trasformando le leggi fisiche in vincoli di compilazione che guidano lo sviluppo di software scientificamente rigoroso.