Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

Types, equations, dimensions and the Pi theorem

Nicola Botta, Patrik Jansson

TL;DR

The paper targets the gap between mathematical physics and dependently typed programming by proposing a minimal Idris-embedded DSL that encodes a grammar of dimensions, physical quantities, and units. It integrates covariance principles and Buckingham's Pi theorem into a type-theoretic framework, highlighting both constructive and non-constructive aspects and offering a pathway for DA-driven program derivation. Key contributions include a concrete DSL for dimensions, a type-theoretic formulation of the Pi theorem, and a constructive methodology (applyPi) to generate covariant functions, demonstrated on pendulum-like relations. The work advances interdisciplinary dialogue by providing verifiable, dimensionally aware programming tools that can assist model specification, analysis, and data-driven formulation in climate and physics contexts.

Abstract

The languages of mathematical physics and modelling are endowed with a rich ``grammar of dimensions'' that common abstractions of programming languages fail to represent. We propose a dependently typed domain-specific language (embedded in Idris) that captures this grammar. We apply it to explain basic notions of dimensional analysis and Buckingham's Pi theorem. We hope that the language makes mathematical physics more accessible to computer scientists and functional programming more palatable to modellers and physicists.

Types, equations, dimensions and the Pi theorem

TL;DR

The paper targets the gap between mathematical physics and dependently typed programming by proposing a minimal Idris-embedded DSL that encodes a grammar of dimensions, physical quantities, and units. It integrates covariance principles and Buckingham's Pi theorem into a type-theoretic framework, highlighting both constructive and non-constructive aspects and offering a pathway for DA-driven program derivation. Key contributions include a concrete DSL for dimensions, a type-theoretic formulation of the Pi theorem, and a constructive methodology (applyPi) to generate covariant functions, demonstrated on pendulum-like relations. The work advances interdisciplinary dialogue by providing verifiable, dimensionally aware programming tools that can assist model specification, analysis, and data-driven formulation in climate and physics contexts.

Abstract

The languages of mathematical physics and modelling are endowed with a rich ``grammar of dimensions'' that common abstractions of programming languages fail to represent. We propose a dependently typed domain-specific language (embedded in Idris) that captures this grammar. We apply it to explain basic notions of dimensional analysis and Buckingham's Pi theorem. We hope that the language makes mathematical physics more accessible to computer scientists and functional programming more palatable to modellers and physicists.
Paper Structure (24 sections, 1 theorem, 26 equations, 1 figure)

This paper contains 24 sections, 1 theorem, 26 equations, 1 figure.

Table of Contents

  1. Introduction
  2. Equations, physical laws and types
  3. Generic differential equations
  4. Physical laws, specific models
  5. Dimensions, physical quantities, units of measurement
  6. Similarity theory and the Pi theorem
  7. Buckingham's Pi theorem
  8. A minimal DSL for dimensionally consistent programming
  9. Dimension function
  10. Physical Quantities and Homorphic Measurement
  11. Dimensional judgments, dimensional consistent programming
  12. Units of measurement
  13. Dimensional (in)dependence
  14. The Pi theorem in Type Theory
  15. The covariance principle and the Pi theorem in Type Theory
  16. ...and 9 more sections

Key Result

Lemma 1

Let $as = a_1,\dots,a_k$ have independent dimensions. Then for any system of units $u$, any positive real number $r$ and any $1 \leqslant j \leqslant k$ there exists a system of units $u_j$ such that $\mu \ u_j \ a_j = r \cdot \mu \ u \ a_j$ and $\mu \ u_j \ a_i = \mu \ u \ a_i$ for all $1 \leqslant

Figures (1)

  • Figure 1: The covariance principle (or principle of relativity of measurements) for a function between physical quantities.

Theorems & Definitions (1)

  • Lemma 1