The Pi theorem: linear-algebra core #
Kennedy's Pi Theorem for programming (POPL 1997; restated in the 2009 lecture notes as Theorem 4) says that a first-order unit-polymorphic type
∀α₁…αₘ. float<u₁> → ⋯ → float<uₙ> → float<u₀>
is isomorphic to one with n − r dimensionless arguments, where r is the
rank of the matrix of unit-variable exponents.
He mechanized the extensional semantics in Coq (WMM 2008) but listed the Pi theorem's proof as work in progress, along with the non-definability results and the higher-order generalization. No completion appears in the eighteen years since. This file is progress on that, and it is important to be precise about how much.
What is proved here #
The linear-algebra core: the dimensionless power-products of the arguments
form the kernel of the exponent matrix, its dimension is n − r by
rank-nullity, and (the pedagogically important part) a unit variable occurring
in exactly one argument forces that argument out of every dimensionless group
and out of the answer.
That last theorem is the pendulum, mechanized. Mass appears only in the mass, so it has nothing to cancel against.
What is not proved here #
Kennedy's syntactic route to the isomorphism (applying primitive
isomorphisms corresponding to row and column operations until the matrix is in
normal form) is not taken, because its witnesses need positivity of the values
they raise to rational powers (Tm.pow exists; a sign does not) to make them
meaningful.
LambdaS.PiTheorem proves the isomorphism (piEquiv) by the semantic route
instead: the scaling law plus the exponent-matrix linear algebra of this file.
So the computational content is mechanized here, and the isomorphism there.
Why ℚ helps #
Kennedy's proof reduces the exponent matrix to Smith Normal Form, which is
what ℤ forces. Over ℚ the matrix is over a field, so the same reduction is
Gaussian elimination and the rank theory is Mathlib's off the shelf. The
rational-exponent decision, taken in LambdaS.Uom for volatility and
wavefunctions, pays off again here for reasons unrelated to either.
The exponent matrix of a first-order signature: A v i is the
exponent, in the unit of argument i, of the v-th rescalable unit symbol.
In Kennedy's statement the rows are the quantified unit variables; the bridge
in LambdaS.PiTheorem (den_mulScaleLaw) instantiates the row index with
B ⊕ Fin k, one row per base unit and per unit variable in scope, so the
matrix sees every rescaling the fundamental theorem provides.
Instances For
A dimensionless power-product of the arguments: exponents x such that
x₁·u₁ + ⋯ + xₙ·uₙ cancels every unit variable.
These are the Π groups of Buckingham's theorem.
Equations
Instances For
The Pi count. The dimensionless groups form a space of dimension
n − r, where r is the rank of the exponent matrix.
Stated as an addition to avoid truncated subtraction. This is Buckingham's
theorem's arithmetic, and it is exactly what a :pi command would report.
A unit variable occurring in exactly one argument forces that argument out of every dimensionless group.
This is the pendulum. The mass dimension M appears only in the mass, so it has
nothing to cancel against, and the M row of the exponent matrix reduces to the
single equation x_mass = 0, with no physics involved.
It is also the precise sense in which the Pi theorem does not claim mass is
irrelevant to pendulums. It claims that given this list of variables, mass
cannot appear. Add a second mass-carrying quantity, such as a fluid density, and
the hypothesis hrow fails, the mass ratio becomes a legitimate group, and the
conclusion evaporates.
The same argument applied to the solution, not just the kernel.
If unit variable v occurs only in argument j, and the result unit does
not mention v, then every solution of A X = B has X j = 0. So argument j
does not appear in the answer at all, which is the pendulum's conclusion, that
the period is independent of the mass.
The pendulum, concretely #
Variables M, L, T; arguments m, l, g, θ.
Exponents of M, L, T in the units of m, l, g = L/T², θ = 1.
Equations
- LambdaS.Pi.pendulum = !![1, 0, 0, 0; 0, 1, 1, 0; 0, 0, -2, 0]
Instances For
Mass cannot appear in any dimensionless group of the pendulum, derived rather than observed.
The witness the pendulum system admits: the exponent vector
(0, 1/2, -1/2, 0), which is T = √(l / g), solves
pendulum.mulVec X = ![0, 0, 1]; rational exponents are why the unit group is
over ℚ. This exhibits a solution of the linear system, so the hypothesis of
pendulum_period_independent_of_mass (the first half of pendulum_mass_absent
in LambdaS.PiTheorem) is satisfied by an actual vector rather than assumed.