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!" Under an erased semantics a unit error yields a wrong number, not a stuck program, so progress and preservation there say nothing about units; the semantic content of unit correctness is 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."

Kennedy also represents units by exponent vectors. The equality coercions arise when object-language types are interpreted as Coq types, so unit substitution changes the type indexing a denotation (Kennedy, WMM 2008).

Here logScale_subst is an identity between two sums because substitution on exponent vectors is linear. Type interpretation still requires transport; the family-indexed denotation in Fundamental handles that separately.

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 scaling at which free_theorem_sqr reads a closed polymorphic type.

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

The scaling that changes nothing: Scaling.zero with B and k explicit.

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