Syntax of Λs

Kennedy's Λu attaches units to scalars. Λs distributes them over an index type, so the primitive is a space and scalars are the one-point case.

Representation choices

Three, all forced by wanting a decidable checker rather than chosen for elegance.

Unit expressions are exponent vectors, not trees. A unit expression with k unit variables in scope is a Term B (Fin k): the very structure LambdaS.Unify solves systems over. Units form a free abelian group, so a normal form is an exponent vector, and equality is vector equality with no normalization pass to write or verify. m * s / m and s are literally the same object.

Scope is a type index. Ty B D j k and Tm B D j k carry the numbers of enclosing ∀δ and ∀u:d binders, so well-scopedness is a typing invariant rather than a side condition, and substitution has nowhere to go wrong.

A space is the list of units its components carry. This is LambdaS.Space at a finite index type, written structurally: a space is its unit assignment. Ordering is the indexing: [m, s] and [s, m] are isomorphic but not equal, because a linear map's entry (j,i) carries δ_W(j)/δ_V(i) and identifying them would let a matrix's columns permute silently.

Explicit typing, and why it matters here

Λu.e and e[μ] are written, not inferred, exactly as in Kennedy's Λu. So the checker needs substitution and decidable equality but never unification, types stay unique, and infer is provably complete as well as sound. The unification development in LambdaS.Unify is for a future inference engine, where let-generalization forces it; nothing here depends on it.

Unit expressions

@[reducible, inline]

abbrev LambdaS.UExp (B : Type) (k : ℕ) : Type

A unit expression with k unit variables in scope.

Equations

• LambdaS.UExp B k = LambdaS.Term B (Fin k)

theorem LambdaS.Term.ext' {B V : Type} {s t : Term B V} (hb : s.base = t.base) (hv : s.vars = t.vars) : s = t

theorem LambdaS.Term.ext'_iff {B V : Type} {s t : Term B V} : s = t ↔ s.base = t.base ∧ s.vars = t.vars

@[instance_reducible]

instance LambdaS.Term.instDecidableEqOfFintype {B V : Type} [Fintype B] [DecidableEq B] [Fintype V] [DecidableEq V] : DecidableEq (Term B V)

Equations

• s.instDecidableEqOfFintype t = decidable_of_iff (s.base = t.base ∧ s.vars = t.vars) ⋯

def LambdaS.Term.one {B V : Type} : Term B V

The trivial unit.

Equations

• LambdaS.Term.one = { base := fun (x : B) => 0, vars := fun (x : V) => 0 }

@[instance_reducible]

instance LambdaS.Term.instOne {B V : Type} : One (Term B V)

Equations

• LambdaS.Term.instOne = { one := LambdaS.Term.one }

def LambdaS.Term.mul {B V : Type} (s t : Term B V) : Term B V

Unit multiplication: exponents add.

Equations

• s.mul t = { base := fun (b : B) => s.base b + t.base b, vars := fun (v : V) => s.vars v + t.vars v }

def LambdaS.Term.inv {B V : Type} (t : Term B V) : Term B V

Unit inverse: exponents negate.

Equations

• t.inv = { base := fun (b : B) => -t.base b, vars := fun (v : V) => -t.vars v }

def LambdaS.Term.div {B V : Type} (s t : Term B V) : Term B V

Unit division.

Equations

• s.div t = { base := fun (b : B) => s.base b - t.base b, vars := fun (v : V) => s.vars v - t.vars v }

def LambdaS.Term.rpow {B V : Type} (t : Term B V) (q : ℚ) : Term B V

Rational powers. Total: every unit expression has an n-th root.

Equations

• t.rpow q = { base := fun (b : B) => q * t.base b, vars := fun (v : V) => q * t.vars v }

@[simp]

theorem LambdaS.Term.one_base {B V : Type} (b : B) : base 1 b = 0

@[simp]

theorem LambdaS.Term.one_vars {B V : Type} (v : V) : vars 1 v = 0

@[simp]

theorem LambdaS.Term.mul_base {B V : Type} (s t : Term B V) (b : B) : (s.mul t).base b = s.base b + t.base b

@[simp]

theorem LambdaS.Term.mul_vars {B V : Type} (s t : Term B V) (v : V) : (s.mul t).vars v = s.vars v + t.vars v

@[simp]

theorem LambdaS.Term.inv_base {B V : Type} (t : Term B V) (b : B) : t.inv.base b = -t.base b

@[simp]

theorem LambdaS.Term.inv_vars {B V : Type} (t : Term B V) (v : V) : t.inv.vars v = -t.vars v

@[simp]

theorem LambdaS.Term.div_base {B V : Type} (s t : Term B V) (b : B) : (s.div t).base b = s.base b - t.base b

@[simp]

theorem LambdaS.Term.div_vars {B V : Type} (s t : Term B V) (v : V) : (s.div t).vars v = s.vars v - t.vars v

@[simp]

theorem LambdaS.Term.rpow_base {B V : Type} (t : Term B V) (q : ℚ) (b : B) : (t.rpow q).base b = q * t.base b

@[simp]

theorem LambdaS.Term.rpow_vars {B V : Type} (t : Term B V) (q : ℚ) (v : V) : (t.rpow q).vars v = q * t.vars v

def LambdaS.Term.ofBase {B V : Type} [DecidableEq B] (b₀ : B) : Term B V

A base unit as a unit expression.

Equations

• LambdaS.Term.ofBase b₀ = { base := fun (b : B) => if b = b₀ then 1 else 0, vars := fun (x : V) => 0 }

def LambdaS.Term.ofVar {B V : Type} [DecidableEq V] (v₀ : V) : Term B V

A unit variable as a unit expression.

Equations

• LambdaS.Term.ofVar v₀ = { base := fun (x : B) => 0, vars := fun (v : V) => if v = v₀ then 1 else 0 }

def LambdaS.UExp.subst {B : Type} {k : ℕ} (t : UExp B (k + 1)) (σ : UExp B k) : UExp B k

Substitute σ for de Bruijn unit variable 0, discharging one binder.

Linear in the exponents, because substitution into an element of a free abelian group is a linear map.

Equations

• t.subst σ = { base := fun (b : B) => t.base b + t.vars 0 * σ.base b, vars := fun (i : Fin k) => t.vars i.succ + t.vars 0 * σ.vars i }

def LambdaS.UExp.weaken {B : Type} {k : ℕ} (t : UExp B k) : UExp B (k + 1)

Introduce a fresh unit variable, unused.

Equations

• t.weaken = { base := t.base, vars := fun (i : Fin (k + 1)) => Fin.cases 0 (fun (j : Fin k) => t.vars j) i }

@[simp]

theorem LambdaS.UExp.subst_weaken {B : Type} {k : ℕ} (t σ : UExp B k) : t.weaken.subst σ = t

Substituting into a weakened expression changes nothing: the fresh variable was unused.

Simultaneous substitution

Single-variable substitution is not closed under going beneath a binder: pushing σ into ∀u. τ must shift σ past the new variable and leave the bound one alone. The standard fix is to define everything from a simultaneous substitution, and to define single substitution and weakening as instances of it.

Λs gets that cheaply. Simultaneous substitution is a linear map on exponent vectors, so its identity, composition and homomorphism laws are Finset arithmetic rather than structural inductions. Only the walk over types is structural, and there the sole interesting case is the quantifier.

def LambdaS.substU {B : Type} {k k₀ : ℕ} (η : Fin k → UExp B k₀) (u : UExp B k) : UExp B k₀

Substitute a unit expression for every unit variable at once.

Equations

• LambdaS.substU η u = { base := fun (b : B) => u.base b + ∑ i : Fin k, u.vars i * (η i).base b, vars := fun (v : Fin k₀) => ∑ i : Fin k, u.vars i * (η i).vars v }

@[simp]

theorem LambdaS.substU_base {B : Type} {k k₀ : ℕ} (η : Fin k → UExp B k₀) (u : UExp B k) (b : B) : (substU η u).base b = u.base b + ∑ i : Fin k, u.vars i * (η i).base b

@[simp]

theorem LambdaS.substU_vars {B : Type} {k k₀ : ℕ} (η : Fin k → UExp B k₀) (u : UExp B k) (v : Fin k₀) : (substU η u).vars v = ∑ i : Fin k, u.vars i * (η i).vars v

def LambdaS.idU (B : Type) (k : ℕ) : Fin k → UExp B k

The identity substitution.

Equations

• LambdaS.idU B k i = LambdaS.Term.ofVar i

def LambdaS.liftU {B : Type} {k k₀ : ℕ} (η : Fin k → UExp B k₀) : Fin (k + 1) → UExp B (k₀ + 1)

Extend a substitution under a binder: the bound variable maps to itself and everything else is shifted past it. This clause is the whole content of the de Bruijn discipline.

Equations

• LambdaS.liftU η i = Fin.cases (LambdaS.Term.ofVar 0) (fun (i : Fin k) => (η i).weaken) i

@[simp]

theorem LambdaS.substU_ofVar {B : Type} {k k₀ : ℕ} (η : Fin k → UExp B k₀) (i : Fin k) : substU η (Term.ofVar i) = η i

@[simp]

theorem LambdaS.substU_id {B : Type} {k : ℕ} (u : UExp B k) : substU (idU B k) u = u

theorem LambdaS.weaken_ofVar {B : Type} {k : ℕ} (i : Fin k) : UExp.weaken (Term.ofVar i) = Term.ofVar i.succ

@[simp]

theorem LambdaS.liftU_id {B : Type} {k : ℕ} : liftU (idU B k) = idU B (k + 1)

def LambdaS.nilU (B : Type) : Fin 0 → UExp B 0

The empty substitution, at the closed scope.

Equations

• LambdaS.nilU B i = i.elim0

@[simp]

theorem LambdaS.substU_nil {B : Type} (u : UExp B 0) : substU (nilU B) u = u

@[simp]

theorem LambdaS.map_substU_id {B : Type} {k : ℕ} (V : List (UExp B k)) : List.map (substU (idU B k)) V = V

@[simp]

theorem LambdaS.substU_one {B : Type} {k k₀ : ℕ} (η : Fin k → UExp B k₀) : substU η 1 = 1

Substitution is a homomorphism of the unit group, which is what lets a typing rule that multiplies units survive it.

theorem LambdaS.substU_mul {B : Type} {k k₀ : ℕ} (η : Fin k → UExp B k₀) (u w : UExp B k) : substU η (Term.mul u w) = Term.mul (substU η u) (substU η w)

theorem LambdaS.substU_div {B : Type} {k k₀ : ℕ} (η : Fin k → UExp B k₀) (u w : UExp B k) : substU η (Term.div u w) = Term.div (substU η u) (substU η w)

theorem LambdaS.substU_rpow {B : Type} {k k₀ : ℕ} (η : Fin k → UExp B k₀) (u : UExp B k) (q : ℚ) : substU η (Term.rpow u q) = Term.rpow (substU η u) q

theorem LambdaS.substU_comp {B : Type} {k k₁ k₂ : ℕ} (η₂ : Fin k₁ → UExp B k₂) (η₁ : Fin k → UExp B k₁) (u : UExp B k) : substU η₂ (substU η₁ u) = substU (fun (i : Fin k) => substU η₂ (η₁ i)) u

Composition. The lemma a substitution development usually pays for with a structural induction; here both sides are linear maps.

theorem LambdaS.substU_weaken {B : Type} {k k₀ : ℕ} (η : Fin k → UExp B k₀) (u : UExp B k) : substU (liftU η) u.weaken = (substU η u).weaken

theorem LambdaS.substU_weaken_cons {B : Type} {k k₀ : ℕ} (w : UExp B k₀) (ξ : Fin k → UExp B k₀) (t : UExp B k) : substU (Fin.cons w ξ) t.weaken = substU ξ t

Substituting into a weakened expression ignores whatever was put at index zero: the weakened expression does not mention it.

theorem LambdaS.liftU_comp {B : Type} {k k₁ k₂ : ℕ} (η₂ : Fin k₁ → UExp B k₂) (η₁ : Fin k → UExp B k₁) : (liftU fun (i : Fin k) => substU η₂ (η₁ i)) = fun (i : Fin (k + 1)) => substU (liftU η₂) (liftU η₁ i)

Spaces

@[reducible, inline]

abbrev LambdaS.Sp (B : Type) (k : ℕ) : Type

A space with k unit variables in scope: the list of units carried by its components. The index type is Fin V.length, the assignment is V.get.

Equations

• LambdaS.Sp B k = List (LambdaS.UExp B k)

def LambdaS.Sp.dual {B : Type} {k : ℕ} (V : Sp B k) : Sp B k

The dual space carries reciprocal units.

Equations

• V.dual = List.map LambdaS.Term.inv V

def LambdaS.Sp.scale {B : Type} {k : ℕ} (V : Sp B k) (d : UExp B k) : Sp B k

Scaling a space by a unit.

Equations

• V.scale d = List.map (fun (x : LambdaS.Term B (Fin k)) => x.mul d) V

def LambdaS.Sp.subst {B : Type} {k : ℕ} (V : Sp B (k + 1)) (σ : UExp B k) : Sp B k

Substitute through a space.

Equations

• V.subst σ = List.map (fun (x : LambdaS.UExp B (k + 1)) => x.subst σ) V

def LambdaS.Sp.weaken {B : Type} {k : ℕ} (V : Sp B k) : Sp B (k + 1)

Weaken a space.

Equations

• V.weaken = List.map LambdaS.UExp.weaken V

@[simp]

theorem LambdaS.Sp.subst_weaken {B : Type} {k : ℕ} (V : Sp B k) (σ : UExp B k) : V.weaken.subst σ = V

The bridge to the model

Hart's classification (LambdaS.Map) is developed over units of the model, Uom B, and spaces of the model, Space B I. A closed unit expression is a unit of the model outright (the same exponent vector), a closed space is a space of the model indexed by position, and the unit the row at codomain unit w carries at component i under T-MCons is the model's entry.

def LambdaS.UExp.toUom {B : Type} (t : UExp B 0) : Uom B

A closed unit expression as a unit of the model: its exponent vector.

Equations

• t.toUom = LambdaS.Uom.ofExp t.base

@[simp]

theorem LambdaS.UExp.exp_toUom {B : Type} (t : UExp B 0) (b : B) : t.toUom.exp b = t.base b

theorem LambdaS.UExp.toUom_injective {B : Type} : Function.Injective toUom

The embedding is injective: with no unit variables in scope, a unit expression is its exponent vector.

@[simp]

theorem LambdaS.UExp.toUom_one {B : Type} : toUom 1 = 1

@[simp]

theorem LambdaS.UExp.toUom_mul {B : Type} (s t : UExp B 0) : toUom (Term.mul s t) = s.toUom * t.toUom

@[simp]

theorem LambdaS.UExp.toUom_inv {B : Type} (t : UExp B 0) : toUom (Term.inv t) = t.toUom⁻¹

@[simp]

theorem LambdaS.UExp.toUom_div {B : Type} (s t : UExp B 0) : toUom (Term.div s t) = s.toUom / t.toUom

@[simp]

theorem LambdaS.UExp.toUom_rpow {B : Type} (t : UExp B 0) (q : ℚ) : toUom (Term.rpow t q) = t.toUom ^ q

def LambdaS.Sp.toSpace {B : Type} (V : Sp B 0) : Space B (Fin (List.length V))

A closed space as a space of the model, indexed by position.

Equations

• V.toSpace i = (List.get V i).toUom

def LambdaS.linEntry {B : Type} {k : ℕ} (V W : Sp B k) (j : Fin (List.length W)) (i : Fin (List.length V)) : UExp B k

The unit of entry (j, i) of a matrix at Lin V W, read off the two spaces: W_j / V_i.

Equations

• LambdaS.linEntry V W j i = LambdaS.Term.div (List.get W j) (List.get V i)

theorem LambdaS.entry_toSpace {B : Type} (V W : Sp B 0) (j : Fin (List.length W)) (i : Fin (List.length V)) : entry V.toSpace W.toSpace j i = (linEntry V W j i).toUom

The calculus's entry units are the model's. The unit Lin V W assigns entry (j, i) is entry of LambdaS.Map at the two spaces, so Hart's classification, developed in the model, is about the matrices the calculus types.

Dimensions

A dimension expression has exactly the structure a unit expression does: the dimension group is free abelian on base dimensions, just as the unit group is free abelian on base units. So DExp is UExp at the dimension alphabet, and every operation (multiplication, division, rational powers, substitution, weakening, decidable equality) is reused rather than rebuilt.

dimension Velocity = Length/Time is therefore Term.div, an abbreviation with nothing left to check. Unit definitions are the interesting case and live in LambdaS.Declare, because unit yard = 3 foot declares a generator and an equation, and equations can conflict.

Why dimension variables

The alternative is two unit quantifiers, ∀u and ∀u:d. It does not work. An unbounded ∀u still has to say something about u's dimension, and there is no right answer: reporting the trivial dimension claims u is dimensionless, so convert x u 1 typechecks under a binder that promised nothing; reporting "unknown" makes dimOf partial and threads Option through every dimension lemma.

Abstracting the dimension is the answer, and it collapses the two quantifiers into one:

∀u. τ ≡ ∀δ. ∀u:δ. τ

Unbounded quantification is bounded quantification at a dimension variable. dimOf stays total, convert under ∀u is rejected because δ matches nothing, and there is a single quantifier rule to state and prove.

@[reducible, inline]

abbrev LambdaS.DExp (D : Type) (j : ℕ) : Type

A dimension expression with j dimension variables in scope. Literally a unit expression over base dimensions: the two are the same free abelian group construction, so UExp's whole API applies.

Equations

• LambdaS.DExp D j = LambdaS.UExp D j

class LambdaS.UnitSys (B D : Type) : Type

A unit system: the dimension each base unit measures.

dim need not be injective: meter and foot share a dimension, which is what lets Λs avoid restricting compound units to one named unit per dimension. Nor need it land on a generator: joule can be declared directly at Mass·Length²·Time⁻² rather than needing a base dimension of its own, which is what makes dimension definitions worth having.

Base units have closed dimensions: a generator's dimension cannot mention a dimension variable, since those are bound by types.

• dim : B → DExp D 0

  The dimension each base unit measures.

@[reducible, inline]

abbrev LambdaS.DCtx (D : Type) (j k : ℕ) : Type

A dimension context: the declared dimension of each unit variable in scope. ∀u:d. τ extends it by d.

Equations

• LambdaS.DCtx D j k = (Fin k → LambdaS.DExp D j)

def LambdaS.DCtx.nil (D : Type) : DCtx D 0 0

The empty context: a closed term has no unit variables in scope.

Equations

• LambdaS.DCtx.nil D i = i.elim0

def LambdaS.DCtx.cons {D : Type} {j k : ℕ} (d : DExp D j) (Δ : DCtx D j k) : DCtx D j (k + 1)

Extend under a unit binder.

Equations

• LambdaS.DCtx.cons d Δ i = Fin.cases d Δ i

def LambdaS.DCtx.weakenDim {D : Type} {j k : ℕ} (Δ : DCtx D j k) : DCtx D (j + 1) k

Extend under a dimension binder: every declared dimension is weakened into the larger dimension scope.

Equations

• Δ.weakenDim i = LambdaS.UExp.weaken (Δ i)

def LambdaS.DCtx.substDim {D : Type} {j k : ℕ} (Δ : DCtx D (j + 1) k) (σ : DExp D j) : DCtx D j k

Discharge a dimension binder.

Equations

• Δ.substDim σ i = LambdaS.UExp.subst (Δ i) σ

@[simp]

theorem LambdaS.DCtx.substDim_weakenDim {D : Type} {j k : ℕ} (Δ : DCtx D j k) (σ : DExp D j) : Δ.weakenDim.substDim σ = Δ

def LambdaS.dimOf {B D : Type} [Fintype B] [UnitSys B D] {j k : ℕ} (Δ : DCtx D j k) (u : UExp B k) : DExp D j

The dimension of a unit expression, relative to a dimension context.

Linear in the exponent vector: a matrix product, with the naive "each base unit has one base dimension" the special case where every column is a standard basis vector. Base units contribute only to base dimensions; the dimension variables of the result come entirely from the context.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem LambdaS.dimOf_ofVar {B D : Type} [Fintype B] [UnitSys B D] {j k : ℕ} (Δ : DCtx D j k) (i : Fin k) : dimOf Δ (Term.ofVar i) = Δ i

A unit variable has exactly its declared dimension.

@[simp]

theorem LambdaS.dimOf_weakenDim {B D : Type} [Fintype B] [UnitSys B D] {j k : ℕ} (Δ : DCtx D j k) (u : UExp B k) : dimOf Δ.weakenDim u = UExp.weaken (dimOf Δ u)

Weakening the dimension context weakens the dimension.

@[simp]

theorem LambdaS.dimOf_weaken_cons {B D : Type} [Fintype B] [UnitSys B D] {j k : ℕ} (Δ : DCtx D j k) (e : DExp D j) (u : UExp B k) : dimOf (DCtx.cons e Δ) u.weaken = dimOf Δ u

A weakened unit has the dimension it had before the context grew.

@[simp]

theorem LambdaS.substU_shift {B : Type} {k : ℕ} (t : UExp B k) : substU (fun (i : Fin k) => Term.ofVar i.succ) t = t.weaken

Substituting the shift is weakening.

def LambdaS.SameDim {B D : Type} [Fintype B] [UnitSys B D] {j k : ℕ} (Δ : DCtx D j k) (u v : UExp B k) : Prop

Two units are interchangeable when they have the same dimension.

Note what is not here. Before dimension contexts this also demanded u.vars = v.vars, a conservative stand-in for not knowing a unit variable's dimension. With Δ supplying it the clause is gone, and convert works under a bounded quantifier, which is what makes a dimension-typed quantity usable.

Equations

• LambdaS.SameDim Δ u v = (LambdaS.dimOf Δ u = LambdaS.dimOf Δ v)

@[instance_reducible]

instance LambdaS.instDecidableSameDimOfFintypeOfDecidableEq {B D : Type} [Fintype B] [Fintype D] [DecidableEq D] [UnitSys B D] {j k : ℕ} (Δ : DCtx D j k) (u v : UExp B k) : Decidable (SameDim Δ u v)

Equations

• LambdaS.instDecidableSameDimOfFintypeOfDecidableEq Δ u v = id inferInstance

Types

inductive LambdaS.Ty (B D : Type) : ℕ → ℕ → Type

Types of Λs, indexed by the number of dimension variables and the number of unit variables in scope.

Six formers, one unit quantifier. ∀u. τ is not primitive: it is ∀δ. ∀u:δ. τ, and the free theorems that need a genuinely unconstrained unit get one by abstracting its dimension.

• Q {B D : Type} {j k : ℕ} : UExp B k → Ty B D j k

  A scalar quantity carrying a unit. The one-point space.

• arrow {B D : Type} {j k : ℕ} : Ty B D j k → Ty B D j k → Ty B D j k
• vec {B D : Type} {j k : ℕ} : Sp B k → Ty B D j k

  A vector over a space.

• lin {B D : Type} {j k : ℕ} : Sp B k → Sp B k → Ty B D j k

  A linear map V ⊸ W. Entry (j,i) carries δ_W(j) / δ_V(i), which is Hart's rank-one condition holding by construction.

• all {B D : Type} {j k : ℕ} : DExp D j → Ty B D j (k + 1) → Ty B D j k

  Unit polymorphism bounded by a dimension, ∀u:d. τ.

• allDim {B D : Type} {j k : ℕ} : Ty B D (j + 1) k → Ty B D j k

  Dimension polymorphism, ∀δ. τ. Together with all this is unbounded unit quantification.

def LambdaS.Ty.ground {B D : Type} {j k j₀ k₀ : ℕ} : (Fin k → UExp B k₀) → (Fin j → DExp D j₀) → Ty B D j k → Ty B D j₀ k₀

Push a unit substitution and a dimension substitution through a type.

Every other substitution on types is an instance of this one. The quantifier cases are the only interesting clauses, and they are where the earlier definitions were wrong: going under ∀u:d must map the bound variable to itself and shift everything else past it, which is exactly liftU.

Equations

• LambdaS.Ty.ground x✝¹ x✝ (LambdaS.Ty.Q u) = LambdaS.Ty.Q (LambdaS.substU x✝¹ u)
• LambdaS.Ty.ground x✝¹ x✝ (a.arrow b) = (LambdaS.Ty.ground x✝¹ x✝ a).arrow (LambdaS.Ty.ground x✝¹ x✝ b)
• LambdaS.Ty.ground x✝¹ x✝ (LambdaS.Ty.vec V) = LambdaS.Ty.vec (List.map (LambdaS.substU x✝¹) V)
• LambdaS.Ty.ground x✝¹ x✝ (LambdaS.Ty.lin V W) = LambdaS.Ty.lin (List.map (LambdaS.substU x✝¹) V) (List.map (LambdaS.substU x✝¹) W)
• LambdaS.Ty.ground x✝¹ x✝ (LambdaS.Ty.all d τ) = LambdaS.Ty.all (LambdaS.substU x✝ d) (LambdaS.Ty.ground (LambdaS.liftU x✝¹) x✝ τ)
• LambdaS.Ty.ground x✝¹ x✝ τ.allDim = (LambdaS.Ty.ground x✝¹ (LambdaS.liftU x✝) τ).allDim

def LambdaS.Ty.subst {B D : Type} {j k : ℕ} (τ : Ty B D j (k + 1)) (σ : UExp B k) : Ty B D j k

Substitute a unit expression for the outermost unit variable.

Equations

• τ.subst σ = LambdaS.Ty.ground (Fin.cons σ (LambdaS.idU B k)) (LambdaS.idU D j) τ

def LambdaS.Ty.weaken {B D : Type} {j k : ℕ} (τ : Ty B D j k) : Ty B D j (k + 1)

Weaken into a larger unit-variable scope.

Equations

• τ.weaken = LambdaS.Ty.ground (fun (i : Fin k) => LambdaS.Term.ofVar i.succ) (LambdaS.idU D j) τ

def LambdaS.Ty.substDim {B D : Type} {j k : ℕ} (τ : Ty B D (j + 1) k) (σ : DExp D j) : Ty B D j k

Substitute a dimension expression for the outermost dimension variable. Units are untouched: a unit expression cannot mention a dimension variable.

Equations

• τ.substDim σ = LambdaS.Ty.ground (LambdaS.idU B k) (Fin.cons σ (LambdaS.idU D j)) τ

def LambdaS.Ty.weakenDim {B D : Type} {j k : ℕ} (τ : Ty B D j k) : Ty B D (j + 1) k

Weaken into a larger dimension-variable scope.

Equations

• τ.weakenDim = LambdaS.Ty.ground (LambdaS.idU B k) (fun (i : Fin j) => LambdaS.Term.ofVar i.succ) τ

@[simp]

theorem LambdaS.Ty.ground_id {B D : Type} {j k : ℕ} (τ : Ty B D j k) : ground (idU B k) (idU D j) τ = τ

Grounding by the identity does nothing.

theorem LambdaS.Ty.ground_comp {B D : Type} {j k j₁ k₁ j₂ k₂ : ℕ} (η₂ : Fin k₁ → UExp B k₂) (δ₂ : Fin j₁ → DExp D j₂) (η₁ : Fin k → UExp B k₁) (δ₁ : Fin j → DExp D j₁) (τ : Ty B D j k) : ground η₂ δ₂ (ground η₁ δ₁ τ) = ground (fun (i : Fin k) => substU η₂ (η₁ i)) (fun (i : Fin j) => substU δ₂ (δ₁ i)) τ

Grounding composes. Two substitutions in sequence are the substitution that maps each variable through both.

def LambdaS.Ty.decEq {B D : Type} [Fintype B] [DecidableEq B] [Fintype D] [DecidableEq D] {j k : ℕ} (a b : Ty B D j k) : Decidable (a = b)

Decidable equality, by structural recursion. Written by hand rather than derived: the deriving handler cannot carry the [Fintype B] constraint that DecidableEq (UExp B k) needs.

Equations

• (LambdaS.Ty.Q u).decEq (LambdaS.Ty.Q v) = decidable_of_iff (u = v) ⋯
• (LambdaS.Ty.vec V).decEq (LambdaS.Ty.vec W) = decidable_of_iff (V = W) ⋯
• (LambdaS.Ty.lin V W).decEq (LambdaS.Ty.lin V' W') = decidable_of_iff (V = V' ∧ W = W') ⋯
• (a.arrow b).decEq (c.arrow d) = match a.decEq c, b.decEq d with | isTrue h1, isTrue h2 => isTrue ⋯ | isFalse h1, x => isFalse ⋯ | x, isFalse h2 => isFalse ⋯
• a.allDim.decEq b.allDim = match a.decEq b with | isTrue h => isTrue ⋯ | isFalse h => isFalse ⋯
• (LambdaS.Ty.all d a).decEq (LambdaS.Ty.all e b) = if hde : d = e then match a.decEq b with | isTrue h => isTrue ⋯ | isFalse h => isFalse ⋯ else isFalse ⋯
• (LambdaS.Ty.Q a).decEq (a_1.arrow a_2) = isFalse ⋯
• (LambdaS.Ty.Q a).decEq (LambdaS.Ty.vec a_1) = isFalse ⋯
• (LambdaS.Ty.Q a).decEq (LambdaS.Ty.lin a_1 a_2) = isFalse ⋯
• (LambdaS.Ty.Q a).decEq (LambdaS.Ty.all a_1 a_2) = isFalse ⋯
• (LambdaS.Ty.Q a).decEq a_1.allDim = isFalse ⋯
• (a.arrow a_1).decEq (LambdaS.Ty.Q a_2) = isFalse ⋯
• (a.arrow a_1).decEq (LambdaS.Ty.vec a_2) = isFalse ⋯
• (a.arrow a_1).decEq (LambdaS.Ty.lin a_2 a_3) = isFalse ⋯
• (a.arrow a_1).decEq (LambdaS.Ty.all a_2 a_3) = isFalse ⋯
• (a.arrow a_1).decEq a_2.allDim = isFalse ⋯
• (LambdaS.Ty.vec a).decEq (LambdaS.Ty.Q a_1) = isFalse ⋯
• (LambdaS.Ty.vec a).decEq (a_1.arrow a_2) = isFalse ⋯
• (LambdaS.Ty.vec a).decEq (LambdaS.Ty.lin a_1 a_2) = isFalse ⋯
• (LambdaS.Ty.vec a).decEq (LambdaS.Ty.all a_1 a_2) = isFalse ⋯
• (LambdaS.Ty.vec a).decEq a_1.allDim = isFalse ⋯
• (LambdaS.Ty.lin a a_1).decEq (LambdaS.Ty.Q a_2) = isFalse ⋯
• (LambdaS.Ty.lin a a_1).decEq (a_2.arrow a_3) = isFalse ⋯
• (LambdaS.Ty.lin a a_1).decEq (LambdaS.Ty.vec a_2) = isFalse ⋯
• (LambdaS.Ty.lin a a_1).decEq (LambdaS.Ty.all a_2 a_3) = isFalse ⋯
• (LambdaS.Ty.lin a a_1).decEq a_2.allDim = isFalse ⋯
• (LambdaS.Ty.all a a_1).decEq (LambdaS.Ty.Q a_2) = isFalse ⋯
• (LambdaS.Ty.all a a_1).decEq (a_2.arrow a_3) = isFalse ⋯
• (LambdaS.Ty.all a a_1).decEq (LambdaS.Ty.vec a_2) = isFalse ⋯
• (LambdaS.Ty.all a a_1).decEq (LambdaS.Ty.lin a_2 a_3) = isFalse ⋯
• (LambdaS.Ty.all a a_1).decEq a_2.allDim = isFalse ⋯
• a.allDim.decEq (LambdaS.Ty.Q a_1) = isFalse ⋯
• a.allDim.decEq (a_1.arrow a_2) = isFalse ⋯
• a.allDim.decEq (LambdaS.Ty.vec a_1) = isFalse ⋯
• a.allDim.decEq (LambdaS.Ty.lin a_1 a_2) = isFalse ⋯
• a.allDim.decEq (LambdaS.Ty.all a_1 a_2) = isFalse ⋯

@[instance_reducible]

instance LambdaS.Ty.instDecidableEqOfFintype {B D : Type} [Fintype B] [DecidableEq B] [Fintype D] [DecidableEq D] {j k : ℕ} : DecidableEq (Ty B D j k)

Equations

• LambdaS.Ty.instDecidableEqOfFintype = LambdaS.Ty.decEq

theorem LambdaS.Ty.ground_weaken {B D : Type} {j k j₀ k₀ : ℕ} (η : Fin k → UExp B k₀) (δ : Fin j → DExp D j₀) (w : UExp B k₀) (σ : Ty B D j k) : ground (Fin.cons w η) δ σ.weaken = ground η δ σ

Weakening then grounding by an extended environment ignores the extension: the weakened type does not mention the new variable. This is what lets a context captured outside a unit binder be reused inside it.

theorem LambdaS.Ty.ground_liftU_subst {B D : Type} {j k j₀ k₀ : ℕ} (η : Fin k → UExp B k₀) (δ : Fin j → DExp D j₀) (w : UExp B k₀) (τ : Ty B D j (k + 1)) : (ground (liftU η) δ τ).subst w = ground (Fin.cons w η) δ τ

The quantifier case. Grounding under a binder and then substituting the instantiating unit is the same as grounding with the environment extended by it.

This is the lemma the uapp case of soundness turns on, and it is where the corrected liftU earns its place.

theorem LambdaS.Ty.ground_weakenDim {B D : Type} {j k j₀ k₀ : ℕ} (η : Fin k → UExp B k₀) (δ : Fin j → DExp D j₀) (w : DExp D j₀) (σ : Ty B D j k) : ground η (Fin.cons w δ) σ.weakenDim = ground η δ σ

The dimension analogue of ground_weaken.

theorem LambdaS.Ty.ground_liftD_substDim {B D : Type} {j k j₀ k₀ : ℕ} (η : Fin k → UExp B k₀) (δ : Fin j → DExp D j₀) (w : DExp D j₀) (τ : Ty B D (j + 1) k) : (ground η (liftU δ) τ).substDim w = ground η (Fin.cons w δ) τ

The dimension analogue of ground_liftU_subst.

theorem LambdaS.Ty.ground_subst {B D : Type} {j k j₀ k₀ : ℕ} (η : Fin k → UExp B k₀) (δ : Fin j → DExp D j₀) (μ : UExp B k) (τ : Ty B D j (k + 1)) : ground η δ (τ.subst μ) = ground (Fin.cons (substU η μ) η) δ τ

Grounding a single substitution: the same as grounding with the environment extended by the grounded instantiation. This is what turns uapp's result type into something the closure's own environment can produce.

theorem LambdaS.Ty.ground_substDim {B D : Type} {j k j₀ k₀ : ℕ} (η : Fin k → UExp B k₀) (δ : Fin j → DExp D j₀) (d : DExp D j) (τ : Ty B D (j + 1) k) : ground η δ (τ.substDim d) = ground η (Fin.cons (substU δ d) δ) τ

The dimension analogue.

The skeleton

Erase every unit and dimension and a type becomes a plain simple type. Nothing in the calculus's shape depends on units, which is why substituting one leaves the skeleton alone. That is what makes the normalization argument in LambdaS.Normalization Tait's rather than Girard's.

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

The size of a type's skeleton.

Equations

• (LambdaS.Ty.Q a).skel = 1
• (LambdaS.Ty.vec a).skel = 1
• (LambdaS.Ty.lin a a_1).skel = 1
• (a.arrow b).skel = a.skel + b.skel + 1
• (LambdaS.Ty.all a τ).skel = τ.skel + 1
• τ.allDim.skel = τ.skel + 1

@[simp]

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

Substitution does not change the skeleton.

@[simp]

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

@[simp]

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

@[simp]

theorem LambdaS.Ty.subst_weaken {B D : Type} {j k : ℕ} (τ : Ty B D j k) (σ : UExp B k) : τ.weaken.subst σ = τ

Substituting into a weakened type changes nothing. The type-level statement that a unit binder binds a genuinely fresh variable.

With subst and weaken both built from ground, this is composition plus the identity law rather than a structural induction of its own.

@[simp]

theorem LambdaS.Ty.substDim_weakenDim {B D : Type} {j k : ℕ} (τ : Ty B D j k) (σ : DExp D j) : τ.weakenDim.substDim σ = τ

The same for the dimension binder.

Terms

inductive LambdaS.Tm (B D : Type) : ℕ → ℕ → Type

Terms of Λs, with de Bruijn indices for value variables and type indices for the dimension- and unit-variable scopes.

• var {B D : Type} {j k : ℕ} : ℕ → Tm B D j k
• lam {B D : Type} {j k : ℕ} : Ty B D j k → Tm B D j k → Tm B D j k
• app {B D : Type} {j k : ℕ} : Tm B D j k → Tm B D j k → Tm B D j k
• lit {B D : Type} {j k : ℕ} : ℚ → Tm B D j k

  Every literal is dimensionless. There is no unitless type, only 1.

• ucon {B D : Type} {j k : ℕ} : UExp B k → Tm B D j k

  A unit constant, so m : Q m. This is what makes 1.3 m work.

• mul {B D : Type} {j k : ℕ} : Tm B D j k → Tm B D j k → Tm B D j k
• div {B D : Type} {j k : ℕ} : Tm B D j k → Tm B D j k → Tm B D j k
• add {B D : Type} {j k : ℕ} : Tm B D j k → Tm B D j k → Tm B D j k

  Addition, where unit errors are caught.

• pow {B D : Type} {j k : ℕ} : ℚ → Tm B D j k → Tm B D j k

  A constant rational power, e^q. Primitive, because it is not definable from the field operations; total, with pow 0 e : Q 1 denoting x^0 = 1. The unit grammar has had u^q all along, and this constructor makes the term grammar symmetric with it: pow (1/n) is the n-th root.

• idx {B D : Type} {j k : ℕ} : Tm B D j k → ℕ → Tm B D j k
• mrow {B D : Type} {j k : ℕ} : Tm B D j k → ℕ → Tm B D j k

  Row extraction: the elimination form for Lin, dual to mcons as idx is to vcons. Row i of a map at Lin V W is a vector over the row space w / δ_V(·) for w = δ_W(i), which is exactly the vector mcons consumes, so extraction and introduction meet on the nose.

• ifle {B D : Type} {j k : ℕ} : Tm B D j k → Tm B D j k → Tm B D j k → Tm B D j k → Tm B D j k

  Compare and branch, fused so that no Bool type is needed. The scrutinees are compared at a common unit, which is what keeps the form parametric: a rescaling multiplies both by the same positive factor and the ordering survives (Num.OrderedNum.le_scale). Comparing across units does not typecheck, so the observation that could detect a rescaling is unreachable by construction.

• mapp {B D : Type} {j k : ℕ} : Tm B D j k → Tm B D j k → Tm B D j k
• comp {B D : Type} {j k : ℕ} : Tm B D j k → Tm B D j k → Tm B D j k
• vnil {B D : Type} {j k : ℕ} : Tm B D j k

  The empty vector, at the empty space.

• vcons {B D : Type} {j k : ℕ} : Tm B D j k → Tm B D j k → Tm B D j k

  A scalar consed onto a vector: the vector introduction step. The unit of the new component is read off the scalar's type, so the constructor carries no annotation.

• mnil {B D : Type} {j k : ℕ} : Sp B k → Tm B D j k

  The zero-row matrix, carrying its column space. The annotation is the design point: a matrix with no rows still has a width, and nothing else could supply it.

• mcons {B D : Type} {j k : ℕ} : UExp B k → Tm B D j k → Tm B D j k → Tm B D j k

  A row consed onto a matrix: output unit w, a row (a vector term whose components carry w / δ_V(i)), and the rest of the matrix. The annotation w is needed because a row over an empty column space determines no output unit.

• log {B D : Type} {j k : ℕ} : Tm B D j k → Tm B D j k

  Logarithm. Requires a dimensionless argument, which is what makes the base-measure problem a type error: a probability density is not dimensionless, so log p does not typecheck.

• exp {B D : Type} {j k : ℕ} : Tm B D j k → Tm B D j k

  Exponential. Also requires a dimensionless argument.

  This is what makes exp (-i·E·t/ħ) a typed statement: the phase of a quantum time evolution must be dimensionless, and the rule enforces it.

• ulam {B D : Type} {j k : ℕ} : DExp D j → Tm B D j (k + 1) → Tm B D j k

  Unit abstraction, Λu:d. e.

• uapp {B D : Type} {j k : ℕ} : Tm B D j k → UExp B k → Tm B D j k

  Unit application, e[μ]. Checks that μ has the declared dimension.

• dlam {B D : Type} {j k : ℕ} : Tm B D (j + 1) k → Tm B D j k

  Dimension abstraction, Λδ. e.

• dapp {B D : Type} {j k : ℕ} : Tm B D j k → DExp D j → Tm B D j k

  Dimension application, e{d}.

• convert {B D : Type} {j k : ℕ} : Tm B D j k → UExp B k → UExp B k → Tm B D j k

  Conversion, e in v, written convert e u v with the source unit u carried explicitly.

  A term constructor rather than sugar for a multiplication, so that the trusted core checks the dimensions and determines the factor. Under the elaboration alternative a wrong factor would still typecheck, putting the Mars Climate Orbiter failure outside the trusted boundary.

  This is the only form that can observe a unit, and so the only form that costs parametricity: a term containing it is scale-invariant for coherent scalings rather than for all of them. See LambdaS.Conversion.

@[reducible, inline]

abbrev LambdaS.Ctx (B D : Type) (j k : ℕ) : Type

A typing context.

Equations

• LambdaS.Ctx B D j k = List (LambdaS.Ty B D j k)

def LambdaS.Ctx.weaken {B D : Type} {j k : ℕ} (Γ : Ctx B D j k) : Ctx B D j (k + 1)

Weakening under a unit binder.

Equations

• Γ.weaken = List.map LambdaS.Ty.weaken Γ

def LambdaS.Ctx.weakenDim {B D : Type} {j k : ℕ} (Γ : Ctx B D j k) : Ctx B D (j + 1) k

Weakening under a dimension binder.

Equations

• Γ.weakenDim = List.map LambdaS.Ty.weakenDim Γ