Relational parametricity for units

Kennedy's POPL 1997 insight: the semantic content of unit correctness is invariance of program behavior under rescaling. This file builds the relation that says so at scalar type, and proves that every operation of the arithmetic fragment preserves it.

Why the erased semantics

The relation is stated on bare magnitudes: a quantity is a real number, and the unit lives only in the relation. That is deliberate, and it is the half of Kennedy's "instrumentation is cheating" objection that survives. An instrumented semantics carries units on values, so there is nothing left to be invariant about; parametricity has content only once units are erased and something else has to carry them.

LambdaS.Erasure does the other half, where instrumentation is exactly right: eeval_erase proves the units can be dropped without moving the numbers. Neither file can state the other's theorem, and both are needed.

What is proved here

RelQ, the relation at scalar type, and (the substance) that every arithmetic operation preserves it. These are the inductive steps of the fundamental theorem, and each is an instance of a homomorphism law from LambdaS.Scaling.

Three read as design justifications rather than lemmas:

• relQ_add requires both operands at the same unit. State it at different units and it is false: the summands would scale by different factors and the sum by neither. The typing rule is forced by the semantics, not chosen.
• relQ_rpow carries no sign hypothesis on the value, and that is a theorem about Real.rpow, not a convention. For a negative base, x ^ q is the real part of the principal complex power, |x| ^ q * cos (π * q), and the cosine factor is common to both sides of (k·x)^q = k^q · x^q once the factor k is positive, which scale factors are by construction (Scaling.scale_pos); mul_rpow_of_pos_left is the identity. What remains true is that on a negative argument the primitive's value is not a root at all ((-8) ^ (1/3 : ℝ) denotes 1 under rpow; the Float carrier returns NaN there, an undefined point of the classical operation like division by zero, see LambdaS.Num), so the lemma certifies covariance of Mathlib's total extension, not root-ness.
• relQ_log holds only at the trivial unit, which is the semantic content of the base-measure problem. A dimensioned quantity has no scale-invariant logarithm, so log p for a density cannot mean anything that survives a change of units.

And eq_zero_of_relQ_self proves Kennedy's observation about zero: it is the unique scale-invariant magnitude, which is why 0.0 : ∀u. float<u> while every other literal is float<1>.

The relation at higher type

Ty.den and the full Rel are here, including the ∀u case, and free_theorem_sqr is the first result that uses them: any f related to itself at ∀u. Q u → Q (u·u) satisfies f (r + log k) (k·x) = k²·f r x for every positive k. That is the familiar f (k·x) = k²·f x, with the family index moved along by the rescaling, and it is Kennedy's "theorems for free", mechanized.

Two notes on getting Ty.den to work, since both looked like obstacles and neither was. Its type must generalize both scope indices ({j k : ℕ} → Ty B D j k → Type, not Ty B D j k → Type) because all recurses at k + 1 and allDim at j + 1. And it must be @[reducible], because instance synthesis runs at reducible transparency and otherwise HMul ℝ (Ty.Q u).den fails to resolve even though the two types are definitionally equal.

Where this leads

The fundamental theorem (every well-typed term related to itself) needs a denotation of terms, hence recursion over typing derivations. HasTy is Type-valued for exactly that reason, and LambdaS.Fundamental does the work: den interprets derivations, and fundamental and fundamental_free are the theorems. The Pi theorem is assembled in LambdaS.PiTheorem.

@[reducible]

def LambdaS.Ty.den {B D : Type} {j k : ℕ} : Ty B D j k → Type

The erased denotation of a type. Units contribute nothing: a quantity is a real number whatever unit it carries, and a dimension abstraction denotes what its body does, because dimensions have no magnitudes to carry.

A unit abstraction is different, and this is where convert shows its cost. Λu:δ. e denotes a family ℝ → Ty.den τ, indexed by the log-magnitude the instantiating unit is declared to have. It has to: Λu:Length. convert x u meter means something different depending on how big u is, and conv is what reads that. For convert-free terms the family is constant, which is Kennedy's theorem rather than our definition, and is the better place for it to live.

@[reducible] is load-bearing: instance synthesis runs at reducible transparency, so without it HMul ℝ (Ty.Q u).den fails to resolve.

Equations

• (LambdaS.Ty.Q a).den = ℝ
• (a.arrow b).den = (a.den → b.den)
• (LambdaS.Ty.vec V).den = (Fin (List.length V) → ℝ)
• (LambdaS.Ty.lin V W).den = (Fin (List.length W) → Fin (List.length V) → ℝ)
• (LambdaS.Ty.all a τ).den = (ℝ → τ.den)
• τ.allDim.den = τ.den

theorem LambdaS.Ty.den_ground {B D : Type} {j k : ℕ} (τ : Ty B D j k) {j₀ k₀ : ℕ} (η : Fin k → UExp B k₀) (δ : Fin j → DExp D j₀) : (ground η δ τ).den = τ.den

Units carry no data. Grounding a type through unit and dimension environments leaves its denotation unchanged.

This is unit erasure, stated at the level of types, and it is what makes the denotation of polymorphic terms typeable at instantiation: Λu:δ. e denotes a family, e[μ] samples it at μ's log-magnitude, and the result must land in Ty.den (τ.subst μ); this equation says that is the same type as Ty.den τ, because instantiating a unit variable moves no magnitudes. The equation is propositional rather than definitional (Ty.ground maps over a space's unit list, and (V.map f).length = V.length is a theorem), so the denotation of a unit application transports along it. That transport is not an artifact of the encoding; it is exactly the place where "units are erasable" does its work.

theorem LambdaS.Ty.den_subst {B D : Type} {j k : ℕ} (τ : Ty B D j (k + 1)) (μ : UExp B k) : (τ.subst μ).den = τ.den

Instantiating a unit variable does not change the denotation.

theorem LambdaS.Ty.den_substDim {B D : Type} {j k : ℕ} (τ : Ty B D (j + 1) k) (d : DExp D j) : (τ.substDim d).den = τ.den

Nor does instantiating a dimension variable.

theorem LambdaS.Ty.den_weaken {B D : Type} {j k : ℕ} (τ : Ty B D j k) : τ.weaken.den = τ.den

Nor does weakening.

theorem LambdaS.Ty.den_weakenDim {B D : Type} {j k : ℕ} (τ : Ty B D j k) : τ.weakenDim.den = τ.den

Nor does dimension weakening.

def LambdaS.Rel {B D : Type} [Fintype B] {j k : ℕ} (τ : Ty B D j k) : Scaling B k → τ.den → τ.den → Prop

The logical relation: "behaves the same when units are rescaled by ψ".

At a scalar the two readings differ by exactly the scale factor. At a function, related arguments must give related results. At ∀u:d. τ the two families must agree at every instantiation r and under every scaling s of the bound variable, with the rescaled reading taken at r + s because rescaling moves the instantiating unit too. The dimension bound restricts which units may instantiate, not which scalings are considered, so the free theorems keep their full strength and the Pi theorem keeps its hypothesis. At ∀δ. τ nothing changes, because dimension abstraction does not touch units.

Equations

• LambdaS.Rel (LambdaS.Ty.Q u) x✝ x_8 y = (y = x✝.scale u * x_8)
• LambdaS.Rel (a.arrow b) x✝ f g = ∀ (x y : a.den), LambdaS.Rel a x✝ x y → LambdaS.Rel b x✝ (f x) (g y)
• LambdaS.Rel (LambdaS.Ty.vec V) x✝ v w = ∀ (i : Fin (List.length V)), w i = x✝.scale (List.get V i) * v i
• LambdaS.Rel (LambdaS.Ty.lin V W) x✝ A C = ∀ (a : Fin (List.length W)) (i : Fin (List.length V)), C a i = x✝.scale (List.get W a) / x✝.scale (List.get V i) * A a i
• LambdaS.Rel (LambdaS.Ty.all a τ) x✝ F G = ∀ (r s : ℝ), LambdaS.Rel τ (x✝.cons s) (F r) (G (r + s))
• LambdaS.Rel τ.allDim x✝ F G = LambdaS.Rel τ x✝ F G

Transporting the relation along a substitution

The relation must survive instantiation, or unit abstraction has no semantics. rel_ground is that statement, and it is the semantic counterpart of Scaling.logScale_pull: relatedness under ψ at a grounded type is relatedness under the pulled-back scaling at the original.

The denotations are compared with HEq because Ty.den (Ty.ground η δ τ) and Ty.den τ are equal but not definitionally so: the same transport that appears in den at uapp and dapp.

theorem LambdaS.heq_app {α α' : Sort u_1} {β β' : Sort u_2} {f : α → β} {g : α' → β'} {x : α} {y : α'} (hα : α = α') (hβ : β = β') (hf : f ≍ g) (hx : x ≍ y) : f x ≍ g y

Applying heterogeneously equal functions to heterogeneously equal arguments.

theorem LambdaS.rel_ground {B D : Type} [Fintype B] {j k : ℕ} (τ : Ty B D j k) {j₀ k₀ : ℕ} (η : Fin k → UExp B k₀) (δ : Fin j → DExp D j₀) (ψ : Scaling B k₀) {x y : τ.den} {x' y' : (Ty.ground η δ τ).den} : x ≍ x' → y ≍ y' → (Rel (Ty.ground η δ τ) ψ x' y' ↔ Rel τ (ψ.pull η) x y)

The relation transports along grounding.

theorem LambdaS.rel_weaken {B D : Type} [Fintype B] {j k : ℕ} (τ : Ty B D j k) (ψ : Scaling B k) (s : ℝ) {x y : τ.den} {x' y' : τ.weaken.den} (hx : x ≍ x') (hy : y ≍ y') : Rel τ.weaken (ψ.cons s) x' y' ↔ Rel τ ψ x y

Weakening is invisible to the relation. The fresh unit variable is unused, so whatever factor it is given cannot matter.

theorem LambdaS.rel_subst {B D : Type} [Fintype B] {j k : ℕ} (τ : Ty B D j (k + 1)) (σ : UExp B k) (ψ : Scaling B k) {x y : τ.den} {x' y' : (τ.subst σ).den} (hx : x ≍ x') (hy : y ≍ y') : Rel (τ.subst σ) ψ x' y' ↔ Rel τ (ψ.cons (ψ.logScale σ)) x y

Instantiating a unit variable extends the scaling by that unit's magnitude. This is what makes e[μ] denote something related to itself: the relation at the instantiated type is the relation at the quantified one, read at μ's scale factor.

theorem LambdaS.rel_weakenDim {B D : Type} [Fintype B] {j k : ℕ} (τ : Ty B D j k) (ψ : Scaling B k) {x y : τ.den} {x' y' : τ.weakenDim.den} (hx : x ≍ x') (hy : y ≍ y') : Rel τ.weakenDim ψ x' y' ↔ Rel τ ψ x y

Dimension weakening is invisible. Units are untouched.

theorem LambdaS.rel_substDim {B D : Type} [Fintype B] {j k : ℕ} (τ : Ty B D (j + 1) k) (d : DExp D j) (ψ : Scaling B k) {x y : τ.den} {x' y' : (τ.substDim d).den} (hx : x ≍ x') (hy : y ≍ y') : Rel (τ.substDim d) ψ x' y' ↔ Rel τ ψ x y

Instantiating a dimension variable is invisible. Dimensions have no magnitudes, so nothing about the relation moves.

def LambdaS.RelQ {B : Type} [Fintype B] {k : ℕ} (u : UExp B k) (ψ : Scaling B k) (x y : ℝ) : Prop

The logical relation at scalar type: "the same quantity, read in unit systems that differ by ψ". The two readings differ by exactly the scale factor of the unit.

Equations

• LambdaS.RelQ u ψ x y = (y = ψ.scale u * x)

@[simp]

theorem LambdaS.relQ_id {B : Type} [Fintype B] {k : ℕ} {u : UExp B k} {x y : ℝ} : RelQ u (Scaling.id B k) x y ↔ y = x

Under the trivial scaling the relation is equality: nothing moves when nothing is rescaled.

The arithmetic operations preserve the relation

theorem LambdaS.relQ_lit {B : Type} [Fintype B] {k : ℕ} (ψ : Scaling B k) (q : ℝ) : RelQ 1 ψ q q

Dimensionless literals are invariant: the same number in every unit system. This is why lit has type Q 1, and why there is no unitless type, only the unit 1.

theorem LambdaS.relQ_mul {B : Type} [Fintype B] {k : ℕ} {u v : UExp B k} {ψ : Scaling B k} {x y x' y' : ℝ} (h : RelQ u ψ x y) (h' : RelQ v ψ x' y') : RelQ (Term.mul u v) ψ (x * x') (y * y')

Multiplication: units multiply, and so do scale factors.

theorem LambdaS.relQ_div {B : Type} [Fintype B] {k : ℕ} {u v : UExp B k} {ψ : Scaling B k} {x y x' y' : ℝ} (h : RelQ u ψ x y) (h' : RelQ v ψ x' y') : RelQ (Term.div u v) ψ (x / x') (y / y')

Division.

theorem LambdaS.relQ_add {B : Type} [Fintype B] {k : ℕ} {u : UExp B k} {ψ : Scaling B k} {x y x' y' : ℝ} (h : RelQ u ψ x y) (h' : RelQ u ψ x' y') : RelQ u ψ (x + x') (y + y')

Addition requires the same unit on both sides.

Not a convention. State it at different units and it is false: the summands would scale by different factors and the sum by neither.

theorem LambdaS.relQ_le_iff {B : Type} [Fintype B] {k : ℕ} {u : UExp B k} {ψ : Scaling B k} {x y x' y' : ℝ} (h : RelQ u ψ x y) (h' : RelQ u ψ x' y') : y ≤ y' ↔ x ≤ x'

Comparison survives a rescaling. Both sides scale by the same positive factor, so the ordering is the same in both unit systems, and a conditional takes the same branch. This is where OrderedNum.le_scale is discharged: the factor is Scaling.scale, positive by construction, and the law is read at the ℝ instance, the carrier the denotation lives over.

theorem LambdaS.mul_rpow_of_pos_left {k : ℝ} (hk : 0 < k) (x q : ℝ) : (k * x) ^ q = k ^ q * x ^ q

A positive factor distributes over real powers, for every real base.

For 0 ≤ x this is Real.mul_rpow. For x < 0 both x and k * x are negative, so both sides read through Real.rpow_def_of_neg: each is exp (q * log |·|) * cos (π * q), the real part of the principal complex power, and the cosine factor is the same on both sides, leaving the ordinary law of exponents on the positive parts. Mathlib's two-sided Real.mul_rpow asks for both factors non-negative; the one-sided statement needs only the factor to be positive.

theorem LambdaS.relQ_rpow {B : Type} [Fintype B] {k : ℕ} {u : UExp B k} {ψ : Scaling B k} {x y : ℝ} (q : ℚ) (h : RelQ u ψ x y) : RelQ (Term.rpow u q) ψ (x ^ ↑q) (y ^ ↑q)

Rational powers preserve the relation, with no sign condition.

Kennedy assumes floats are positive; the mechanization does not need to. The scale factor is positive by construction (Scaling.scale_pos), and mul_rpow_of_pos_left shows a positive factor distributes over rpow for every real base: on negatives the common cosine factor of the principal complex power cancels. The caveat lives in the primitive, not the lemma: on a negative argument rpow does not compute a root, so what is certified is covariance of that total function.

theorem LambdaS.relQ_log {B : Type} [Fintype B] {k : ℕ} {ψ : Scaling B k} {x y : ℝ} (h : RelQ 1 ψ x y) : RelQ 1 ψ (Real.log x) (Real.log y)

log is invariant only at the trivial unit: the semantic content of the base-measure problem.

theorem LambdaS.relQ_exp {B : Type} [Fintype B] {k : ℕ} {ψ : Scaling B k} {x y : ℝ} (h : RelQ 1 ψ x y) : RelQ 1 ψ (Real.exp x) (Real.exp y)

exp, likewise.

Zero is the unique scale-invariant magnitude

Kennedy's explanation of why 0.0 : ∀u. float<u> while every other literal is float<1>. Not a special case bolted on to make arithmetic work: forced. It is also what makes identity matrices and the n = 0 term of exp well-typed in LambdaS.Map, where the off-diagonal zeros must inhabit every unit.

theorem LambdaS.relQ_zero {B : Type} [Fintype B] {k : ℕ} (u : UExp B k) (ψ : Scaling B k) : RelQ u ψ 0 0

Zero relates to itself at every unit and every scaling.

theorem LambdaS.eq_zero_of_relQ_self {B : Type} [Fintype B] {x : ℝ} (h : ∀ (ψ : Scaling B 1), RelQ (Term.ofVar 0) ψ x x) : x = 0

And it is the only one. A magnitude related to itself under every scaling of a unit variable must be zero.

A theorem for free

The first result at higher type, and the shape Kennedy's Pi theorem generalizes: the type alone constrains the function's behavior, whatever its code.

theorem LambdaS.rel_Q_eq {B D : Type} [Fintype B] {j k : ℕ} (u : UExp B k) (ψ : Scaling B k) (x y : ℝ) : Rel (Ty.Q u) ψ x y ↔ RelQ u ψ x y

The relation at .Q is exactly RelQ, so every arithmetic lemma above is a lemma about Rel.

theorem LambdaS.free_theorem_sqr {B D : Type} [Fintype B] {f : ℝ → ℝ → ℝ} (h : Rel (Ty.all (Term.ofVar 0) ((Ty.Q (Term.ofVar 0)).arrow (Ty.Q ((Term.ofVar 0).mul (Term.ofVar 0))))).allDim (Scaling.id B 0) f f) (r : ℝ) {k : ℝ} (hk : 0 < k) (x : ℝ) : f (r + Real.log k) (k * x) = k ^ 2 * f r x

Theorems for free. Any f related to itself at ∀u. Q u → Q (u·u) satisfies f (k·x) = k² · f x for every positive k.

f takes the instantiating unit's log-magnitude as its first argument, and rescaling by k moves that argument by log k: the unit the term was applied to gets rescaled along with everything else. Read at a fixed r this is the familiar statement.

Note how ∀u is written: ∀δ. ∀u:δ., a unit variable bounded by a dimension variable. That is unbounded quantification, and it is where the full strength of the free theorem comes from, since nothing concrete matches δ and so convert is unavailable at u.

Nothing is known about f except its type. This is what Kennedy's parametricity buys, and it is the mechanism the Pi theorem runs on.