Scalings: the semantic foundation

Unit correctness is not type safety. Kennedy makes the point sharply (WMM 2008): "What 'goes wrong' if a program contains a unit error? Nothing!" A unit error does not get a program stuck; it gets you a wrong number. So progress and preservation are vacuous here, and the semantic content of unit correctness has to be something else: invariance of program behavior under scaling.

This file builds the object that invariance is stated against.

Scalings are linear functionals

A scaling assigns a positive real factor to each base unit and each unit variable, and extends to a homomorphism UExp → (ℝ⁺, ×). Since (ℝ⁺, ×) ≅ (ℝ, +) under log, and a unit expression is an exponent vector, the extension is a dot product:

logScale ψ t = Σ_b t.base b · ψ.base b + Σ_i t.vars i · ψ.vars i

Working in log space keeps everything linear, makes positivity free (the actual factor is exp of this, so it is positive by construction), and turns the homomorphism laws into linearity.

Why the substitution lemma is easy here

Kennedy singled out the substitution lemma as the painful part of his Coq development:

"First attempt in Coq: … This doesn't even type-check! Type-checker needs to know usem τ = usem (subst ty s τ). Solution: explicit equality coercions."

That pain comes from unit expressions being syntax trees, so substitution is structural and the semantics has to be transported along it.

Here unit expressions are exponent vectors and substitution is a linear map on them, so logScale_subst is an identity between two sums: pure arithmetic, with no coercions and no transport. The representation choice made for decidability in LambdaS.Syntax pays off again, in a place it was not chosen for.

structure LambdaS.Scaling (B : Type) (k : ℕ) : Type

A scaling: a positive factor for each base unit and each unit variable, represented by its logarithm so that the group is (ℝ, +) and everything stays linear.

• base : B → ℝ
• vars : Fin k → ℝ

def LambdaS.Scaling.logScale {B : Type} [Fintype B] {k : ℕ} (ψ : Scaling B k) (t : UExp B k) : ℝ

Extend a scaling to a unit expression. In log space this is the dot product of the exponent vector with the scaling vector.

Equations

• ψ.logScale t = ∑ b : B, ↑(t.base b) * ψ.base b + ∑ i : Fin k, ↑(t.vars i) * ψ.vars i

noncomputable def LambdaS.Scaling.scale {B : Type} [Fintype B] {k : ℕ} (ψ : Scaling B k) (t : UExp B k) : ℝ

The actual scale factor. Positive by construction, which is the positivity Kennedy's Pi theorem assumes.

Equations

• ψ.scale t = Real.exp (ψ.logScale t)

theorem LambdaS.Scaling.scale_pos {B : Type} [Fintype B] {k : ℕ} (ψ : Scaling B k) (t : UExp B k) : 0 < ψ.scale t

def LambdaS.Scaling.zero {B : Type} {k : ℕ} : Scaling B k

The trivial scaling: every factor 1, every logarithm 0. The unit of composition (Scaling.comp_zero), and the scaling that fixes every value (scaleEnv_zero); holding one parameter of the twisted scaling law at zero specializes it to moving the valuation alone or the values alone.

Equations

• LambdaS.Scaling.zero = { base := fun (x : B) => 0, vars := fun (x : Fin k) => 0 }

@[simp]

theorem LambdaS.Scaling.logScale_zero {B : Type} [Fintype B] {k : ℕ} (t : UExp B k) : zero.logScale t = 0

@[simp]

theorem LambdaS.Scaling.scale_zero {B : Type} [Fintype B] {k : ℕ} (t : UExp B k) : zero.scale t = 1

The homomorphism laws

@[simp]

theorem LambdaS.Scaling.logScale_one {B : Type} [Fintype B] {k : ℕ} (ψ : Scaling B k) : ψ.logScale 1 = 0

theorem LambdaS.Scaling.logScale_mul {B : Type} [Fintype B] {k : ℕ} (ψ : Scaling B k) (u v : UExp B k) : ψ.logScale (Term.mul u v) = ψ.logScale u + ψ.logScale v

theorem LambdaS.Scaling.logScale_inv {B : Type} [Fintype B] {k : ℕ} (ψ : Scaling B k) (u : UExp B k) : ψ.logScale (Term.inv u) = -ψ.logScale u

theorem LambdaS.Scaling.logScale_div {B : Type} [Fintype B] {k : ℕ} (ψ : Scaling B k) (u v : UExp B k) : ψ.logScale (Term.div u v) = ψ.logScale u - ψ.logScale v

theorem LambdaS.Scaling.logScale_rpow {B : Type} [Fintype B] {k : ℕ} (ψ : Scaling B k) (u : UExp B k) (q : ℚ) : ψ.logScale (Term.rpow u q) = ↑q * ψ.logScale u

@[simp]

theorem LambdaS.Scaling.scale_one {B : Type} [Fintype B] {k : ℕ} (ψ : Scaling B k) : ψ.scale 1 = 1

theorem LambdaS.Scaling.scale_mul {B : Type} [Fintype B] {k : ℕ} (ψ : Scaling B k) (u v : UExp B k) : ψ.scale (Term.mul u v) = ψ.scale u * ψ.scale v

theorem LambdaS.Scaling.scale_div {B : Type} [Fintype B] {k : ℕ} (ψ : Scaling B k) (u v : UExp B k) : ψ.scale (Term.div u v) = ψ.scale u / ψ.scale v

theorem LambdaS.Scaling.scale_rpow {B : Type} [Fintype B] {k : ℕ} (ψ : Scaling B k) (u : UExp B k) (q : ℚ) : ψ.scale (Term.rpow u q) = ψ.scale u ^ ↑q

Substitution

The lemma Kennedy called out as the awkward part of mechanizing this.

def LambdaS.Scaling.cons {B : Type} {k : ℕ} (ψ : Scaling B k) (r : ℝ) : Scaling B (k + 1)

Extend a scaling with a factor for a newly bound unit variable.

Equations

• ψ.cons r = { base := ψ.base, vars := Fin.cons r ψ.vars }

theorem LambdaS.Scaling.logScale_subst {B : Type} [Fintype B] {k : ℕ} (ψ : Scaling B k) (t : UExp B (k + 1)) (σ : UExp B k) : ψ.logScale (t.subst σ) = (ψ.cons (ψ.logScale σ)).logScale t

The substitution lemma. Scaling a substituted expression is the same as scaling the original under an environment extended by the scale of the substituted expression.

Pure exponent arithmetic: no coercions, no transport.

theorem LambdaS.Scaling.scale_subst {B : Type} [Fintype B] {k : ℕ} (ψ : Scaling B k) (t : UExp B (k + 1)) (σ : UExp B k) : ψ.scale (t.subst σ) = (ψ.cons (ψ.logScale σ)).scale t

@[simp]

theorem LambdaS.Scaling.logScale_weaken {B : Type} [Fintype B] {k : ℕ} (ψ : Scaling B k) (r : ℝ) (t : UExp B k) : (ψ.cons r).logScale t.weaken = ψ.logScale t

Weakening is invisible to scaling: the fresh variable is unused, so whatever factor it is given cannot matter.

Pulling a scaling back along a substitution

logScale_subst and logScale_weaken are both instances of one fact, and the general form is what a denotation of unit-polymorphic terms needs: a scaling of the target scope induces one on the source, by scaling what each variable was substituted by.

def LambdaS.Scaling.pull {B : Type} [Fintype B] {k k₀ : ℕ} (ψ : Scaling B k₀) (η : Fin k → UExp B k₀) : Scaling B k

Pulling a scaling back along a unit substitution. Base units keep their magnitudes; a variable gets the magnitude of whatever was substituted for it.

Equations

• ψ.pull η = { base := ψ.base, vars := fun (i : Fin k) => ψ.logScale (η i) }

theorem LambdaS.Scaling.logScale_pull {B : Type} [Fintype B] {k k₀ : ℕ} (ψ : Scaling B k₀) (η : Fin k → UExp B k₀) (u : UExp B k) : (ψ.pull η).logScale u = ψ.logScale (substU η u)

The substitution lemma, in general. Scaling a substituted expression is scaling the original under the pulled-back scaling.

Pure exponent arithmetic, as before: substitution is a linear map and logScale is a linear functional, so this is a change in summation order.

theorem LambdaS.Scaling.scale_pull {B : Type} [Fintype B] {k k₀ : ℕ} (ψ : Scaling B k₀) (η : Fin k → UExp B k₀) (u : UExp B k) : (ψ.pull η).scale u = ψ.scale (substU η u)

@[simp]

theorem LambdaS.Scaling.logScale_ofVar {B : Type} [Fintype B] {k : ℕ} (ψ : Scaling B k) (i : Fin k) : ψ.logScale (Term.ofVar i) = ψ.vars i

A variable scales by exactly its own factor.

@[simp]

theorem LambdaS.Scaling.pull_weaken {B : Type} [Fintype B] {k : ℕ} (ψ : Scaling B k) (s : ℝ) : ((ψ.cons s).pull fun (i : Fin k) => Term.ofVar i.succ) = ψ

Pulling back along weakening drops the fresh variable. Whatever factor it was given cannot matter, because nothing in scope mentions it.

@[simp]

theorem LambdaS.Scaling.pull_subst {B : Type} [Fintype B] {k : ℕ} (ψ : Scaling B k) (σ : UExp B k) : ψ.pull (Fin.cons σ (idU B k)) = ψ.cons (ψ.logScale σ)

Pulling back along an instantiation extends by the instantiated unit's magnitude. This is logScale_subst read as a statement about scalings.

@[simp]

theorem LambdaS.Scaling.pull_id {B : Type} [Fintype B] {k : ℕ} (ψ : Scaling B k) : ψ.pull (idU B k) = ψ

Pulling back along the identity substitution changes nothing.

@[simp]

theorem LambdaS.Scaling.pull_nil {B : Type} [Fintype B] (ψ : Scaling B 0) : ψ.pull (nilU B) = ψ

Pulling back at the closed scope changes nothing.

@[simp]

theorem LambdaS.Scaling.pull_cons {B : Type} [Fintype B] {k k₀ : ℕ} (ψ : Scaling B k₀) (η : Fin k → UExp B k₀) (μ : UExp B k₀) : ψ.pull (Fin.cons μ η) = (ψ.pull η).cons (ψ.logScale μ)

Pulling back along an instantiation of the outermost variable.

@[simp]

theorem LambdaS.Scaling.pull_liftU {B : Type} [Fintype B] {k k₀ : ℕ} (ψ : Scaling B k₀) (η : Fin k → UExp B k₀) (s : ℝ) : (ψ.cons s).pull (liftU η) = (ψ.pull η).cons s

Pulling back under a binder. Lifting a substitution past a unit binder and pulling back is the same as pulling back and then extending.

The trivial scaling

Scaling everything by 1: the identity, and the reference point the Pi theorem collapses a polymorphic type down to.

def LambdaS.Scaling.id (B : Type) (k : ℕ) : Scaling B k

The scaling that changes nothing.

Equations

• LambdaS.Scaling.id B k = { base := fun (x : B) => 0, vars := fun (x : Fin k) => 0 }

@[simp]

theorem LambdaS.Scaling.logScale_id {B : Type} [Fintype B] {k : ℕ} (t : UExp B k) : (id B k).logScale t = 0

@[simp]

theorem LambdaS.Scaling.scale_id {B : Type} [Fintype B] {k : ℕ} (t : UExp B k) : (id B k).scale t = 1