Conversion ratios as syntax

Concretely, convert x m ft contributes the ratio m/ft, and the round trip convert (convert x m ft) ft m accumulates (m/ft) · (ft/m) = 1; this file gives ratios like these a first-order syntax.

An earlier design, since deleted, carried a term's accumulated conversion ratio as a semantic object: at arrow type the ratio was a Lean function space. That works at first order and stops working at a unit binder, and the reason is worth stating, because it is a familiar one.

A function space is higher-order abstract syntax for the ratio map, and HOAS cannot be traversed or substituted into. Instantiating a unit variable is a substitution, so e[μ] has nowhere to send the ratio of e; and the map is contravariant at arrow type, so no covariant transport exists either. A ratio analysis built on function spaces has nothing to say at a quantifier: not a choice, an obstruction.

This file makes ratios first-order instead. Two things fall out beyond covering the quantifiers.

Substitution disappears rather than becoming structural: Tw.uapp records the instantiating unit instead of performing it, and the interpretation does the work. So there is no ratio-substitution lemma at all, and no transport.

And a first-order ratio is inspectable. With a function space you can define a term's ratio but never decide whether it is trivial; with syntax you can, which turns Twist.invariant_iff from a characterization into an algorithm: the compiler diagnostic "this program's conversions do not cancel, so its result depends on the declared magnitudes".

Shapes

Ratios are indexed by a Shape (the type's skeleton) rather than by the type. That is not a simplification but an observation: the deleted semantic ratios never inspected a type's units, only its structure, so type-indexing was buying nothing. A shape records where the ratio is a unit (scalar), where it is a map (arrow), where it is a family of scalars (vec and mat, for spaces and linear maps: the drift of a vector is a vector of drifts, and the drift of a matrix is a matrix of drifts, indexed by component counts, which are unit-blind), and where a unit binder was crossed (bind).

inductive LambdaS.Shape : Type

The skeleton of a type, as far as conversion ratios can see.

• scalar : Shape

  A quantity: the ratio is a unit expression.

• arrow : Shape → Shape → Shape

  A function: the ratio maps ratios to ratios.

• vec : ℕ → Shape

  A space of the given length: one scalar ratio per component.

• mat : ℕ → ℕ → Shape

  A linear map, by domain and codomain lengths: one scalar ratio per entry.

• bind : Shape → Shape

  Under a unit binder: the ratio lives one unit scope out.

def LambdaS.instDecidableEqShape.decEq (x✝ x✝¹ : Shape) : Decidable (x✝ = x✝¹)

Equations

• One or more equations did not get rendered due to their size.
• LambdaS.instDecidableEqShape.decEq LambdaS.Shape.scalar LambdaS.Shape.scalar = isTrue ⋯
• LambdaS.instDecidableEqShape.decEq LambdaS.Shape.scalar (a.arrow a_1) = isFalse ⋯
• LambdaS.instDecidableEqShape.decEq LambdaS.Shape.scalar (LambdaS.Shape.vec a) = isFalse ⋯
• LambdaS.instDecidableEqShape.decEq LambdaS.Shape.scalar (LambdaS.Shape.mat a a_1) = isFalse ⋯
• LambdaS.instDecidableEqShape.decEq LambdaS.Shape.scalar a.bind = isFalse ⋯
• LambdaS.instDecidableEqShape.decEq (a.arrow a_1) LambdaS.Shape.scalar = isFalse ⋯
• LambdaS.instDecidableEqShape.decEq (a.arrow a_1) (LambdaS.Shape.vec a_2) = isFalse ⋯
• LambdaS.instDecidableEqShape.decEq (a.arrow a_1) (LambdaS.Shape.mat a_2 a_3) = isFalse ⋯
• LambdaS.instDecidableEqShape.decEq (a.arrow a_1) a_2.bind = isFalse ⋯
• LambdaS.instDecidableEqShape.decEq (LambdaS.Shape.vec a) LambdaS.Shape.scalar = isFalse ⋯
• LambdaS.instDecidableEqShape.decEq (LambdaS.Shape.vec a) (a_1.arrow a_2) = isFalse ⋯
• LambdaS.instDecidableEqShape.decEq (LambdaS.Shape.vec a) (LambdaS.Shape.vec b) = if h : a = b then h ▸ isTrue ⋯ else isFalse ⋯
• LambdaS.instDecidableEqShape.decEq (LambdaS.Shape.vec a) (LambdaS.Shape.mat a_1 a_2) = isFalse ⋯
• LambdaS.instDecidableEqShape.decEq (LambdaS.Shape.vec a) a_1.bind = isFalse ⋯
• LambdaS.instDecidableEqShape.decEq (LambdaS.Shape.mat a a_1) LambdaS.Shape.scalar = isFalse ⋯
• LambdaS.instDecidableEqShape.decEq (LambdaS.Shape.mat a a_1) (a_2.arrow a_3) = isFalse ⋯
• LambdaS.instDecidableEqShape.decEq (LambdaS.Shape.mat a a_1) (LambdaS.Shape.vec a_2) = isFalse ⋯
• LambdaS.instDecidableEqShape.decEq (LambdaS.Shape.mat a a_1) (LambdaS.Shape.mat b b_1) = if h : a = b then h ▸ if h : a_1 = b_1 then h ▸ isTrue ⋯ else isFalse ⋯ else isFalse ⋯
• LambdaS.instDecidableEqShape.decEq (LambdaS.Shape.mat a a_1) a_2.bind = isFalse ⋯
• LambdaS.instDecidableEqShape.decEq a.bind LambdaS.Shape.scalar = isFalse ⋯
• LambdaS.instDecidableEqShape.decEq a.bind (a_1.arrow a_2) = isFalse ⋯
• LambdaS.instDecidableEqShape.decEq a.bind (LambdaS.Shape.vec a_1) = isFalse ⋯
• LambdaS.instDecidableEqShape.decEq a.bind (LambdaS.Shape.mat a_1 a_2) = isFalse ⋯
• LambdaS.instDecidableEqShape.decEq a.bind b.bind = if h : a = b then h ▸ have inst := LambdaS.instDecidableEqShape.decEq a a; isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance LambdaS.instDecidableEqShape : DecidableEq Shape

Equations

• LambdaS.instDecidableEqShape = LambdaS.instDecidableEqShape.decEq

@[instance_reducible]

instance LambdaS.instReprShape : Repr Shape

Equations

• LambdaS.instReprShape = { reprPrec := LambdaS.instReprShape.repr }

def LambdaS.instReprShape.repr : Shape → ℕ → Std.Format

Equations

• One or more equations did not get rendered due to their size.
• LambdaS.instReprShape.repr LambdaS.Shape.scalar prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "LambdaS.Shape.scalar")).group prec✝

@[reducible]

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

The shape of a type. Units are ignored; only the structure survives.

@[reducible] for the same reason Ty.den is: instance synthesis runs at reducible transparency, and SemTw (Ty.shape (.Q u)) has to resolve to the positive-real carrier.

Equations

• (LambdaS.Ty.Q a).shape = LambdaS.Shape.scalar
• (a.arrow b).shape = a.shape.arrow b.shape
• (LambdaS.Ty.vec V).shape = LambdaS.Shape.vec (List.length V)
• (LambdaS.Ty.lin V W).shape = LambdaS.Shape.mat (List.length V) (List.length W)
• (LambdaS.Ty.all a τ).shape = τ.shape.bind
• τ.allDim.shape = τ.shape

def LambdaS.Ctx.shapes {B D : Type} {j k : ℕ} (Γ : Ctx B D j k) : List Shape

The shapes of a context, one ratio variable per term variable.

Equations

• Γ.shapes = List.map LambdaS.Ty.shape Γ

@[simp]

theorem LambdaS.Ctx.shapes_nil {B D : Type} {j k : ℕ} : shapes [] = []

@[simp]

theorem LambdaS.Ctx.shapes_cons {B D : Type} {j k : ℕ} (τ : Ty B D j k) (Γ : Ctx B D j k) : shapes (τ :: Γ) = τ.shape :: Γ.shapes

theorem LambdaS.Ctx.shapes_getElem? {B D : Type} {j k : ℕ} {Γ : Ctx B D j k} {n : ℕ} {τ : Ty B D j k} (h : Γ[n]? = some τ) : Γ.shapes[n]? = some τ.shape

A context lookup, read at the shapes.

@[simp]

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

Shape is blind to units. Grounding a type through unit and dimension environments leaves its shape alone, which is why ratios need no transport: the Tw indexed by a type is equally an index for every instantiation of it. The space cases are List.length_map: lengths are unit-blind.

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

theorem LambdaS.Ctx.shapes_weaken {B D : Type} {j k : ℕ} (Γ : Ctx B D j k) : Γ.weaken.shapes = Γ.shapes

@[simp]

theorem LambdaS.Ctx.shapes_weakenDim {B D : Type} {j k : ℕ} (Γ : Ctx B D j k) : Γ.weakenDim.shapes = Γ.shapes

The syntax of ratios

A ratio is an open term over a context of ratio variables (one for each free term variable) in the free abelian group generated by unit expressions, closed under abstraction and application so that the analysis passes first order.

uapp records its instantiating unit rather than substituting it. That is what makes the whole construction transport-free.

inductive LambdaS.Tw (B : Type) : ℕ → List Shape → Shape → Type

Conversion-ratio expressions.

• var {B : Type} {k : ℕ} {Θ : List Shape} {s : Shape} (n : ℕ) : Θ[n]? = some s → Tw B k Θ s

  The ratio of a free variable.

• unit {B : Type} {k : ℕ} {Θ : List Shape} : UExp B k → Tw B k Θ Shape.scalar

  A constant ratio: a unit expression. 1 is the trivial ratio.

• mul {B : Type} {k : ℕ} {Θ : List Shape} : Tw B k Θ Shape.scalar → Tw B k Θ Shape.scalar → Tw B k Θ Shape.scalar

  Multiplication multiplies ratios.

• div {B : Type} {k : ℕ} {Θ : List Shape} : Tw B k Θ Shape.scalar → Tw B k Θ Shape.scalar → Tw B k Θ Shape.scalar

  Division divides them.

• qpow {B : Type} {k : ℕ} {Θ : List Shape} : Tw B k Θ Shape.scalar → ℚ → Tw B k Θ Shape.scalar

  A constant rational power lifts a ratio to that power. This is what carries the analysis through pow: the scale factor of e ^ q is ψ(u) ^ q, so its drift is the drift of e to the q.

• lam {B : Type} {k : ℕ} {Θ : List Shape} {s t : Shape} : Tw B k (s :: Θ) t → Tw B k Θ (s.arrow t)

  Abstraction binds a ratio variable. This is the first-order replacement for the function space, and the whole point of the file.

• app {B : Type} {k : ℕ} {Θ : List Shape} {s t : Shape} : Tw B k Θ (s.arrow t) → Tw B k Θ s → Tw B k Θ t

  Application.

• vecnil {B : Type} {k : ℕ} {Θ : List Shape} : Tw B k Θ (Shape.vec 0)

  The empty drift vector.

• veccons {B : Type} {k : ℕ} {Θ : List Shape} {n : ℕ} : Tw B k Θ Shape.scalar → Tw B k Θ (Shape.vec n) → Tw B k Θ (Shape.vec (n + 1))

  Consing a scalar drift onto a drift vector.

• proj {B : Type} {k : ℕ} {Θ : List Shape} {n : ℕ} : Tw B k Θ (Shape.vec n) → Fin n → Tw B k Θ Shape.scalar

  Projecting a component out of a drift vector.

• matnil {B : Type} {k : ℕ} {Θ : List Shape} {n : ℕ} : Tw B k Θ (Shape.mat n 0)

  The zero-row drift matrix, at any domain length.

• matcons {B : Type} {k : ℕ} {Θ : List Shape} {n m : ℕ} : Tw B k Θ (Shape.vec n) → Tw B k Θ (Shape.mat n m) → Tw B k Θ (Shape.mat n (m + 1))

  Consing a row-drift vector onto a drift matrix.

• row {B : Type} {k : ℕ} {Θ : List Shape} {n m : ℕ} : Tw B k Θ (Shape.mat n m) → Fin m → Tw B k Θ (Shape.vec n)

  Reading a row-drift vector out of a drift matrix.

• ulam {B : Type} {k : ℕ} {Θ : List Shape} {s : Shape} : Tw B (k + 1) Θ s → Tw B k Θ s.bind

  Under a unit binder the ratio lives at the larger unit scope.

• uapp {B : Type} {k : ℕ} {Θ : List Shape} {s : Shape} : Tw B k Θ s.bind → UExp B k → Tw B k Θ s

  Unit instantiation is recorded, not performed.

def LambdaS.Tw.castShape {B : Type} {k : ℕ} {Θ : List Shape} {s s' : Shape} (h : s = s') : Tw B k Θ s → Tw B k Θ s'

Retyping a ratio along an equality of shapes. Needed only at uapp and dapp, where the result type is τ.subst σ and Ty.shape_subst is a theorem rather than a definitional equality, and at a matrix row, whose space is a map over the column space with List.length_map likewise a theorem.

Equations

• LambdaS.Tw.castShape h t = h ▸ t

@[simp]

theorem LambdaS.Tw.castShape_rfl {B : Type} {k : ℕ} {Θ : List Shape} {s : Shape} (t : Tw B k Θ s) : castShape ⋯ t = t

Renaming and substitution

uapp records unit instantiation, so no unit-substitution is ever forced; but a recorded β-redex (app (lam t) s, or uapp (ulam t) μ) is opaque to the flat-form comparison, which costs completeness at the agreement checks. These operations let the redexes that arise at construction be reduced on the spot: a ratio-context renaming (for weakening a substituend under lam), a unit-scope pullback (for carrying a substituend under ulam, and for performing a recorded instantiation), and simultaneous substitution built from the two. Each preserves evaluation, which is proved below the interpreter.

def LambdaS.Tw.liftR (f : ℕ → ℕ) : ℕ → ℕ

Lifting a ratio-context renaming under a binder.

Equations

• LambdaS.Tw.liftR f 0 = 0
• LambdaS.Tw.liftR f n.succ = f n + 1

theorem LambdaS.Tw.liftR_ok {Θ Θ' : List Shape} {s₀ : Shape} (f : ℕ → ℕ) (hf : ∀ (n : ℕ) (s : Shape), Θ[n]? = some s → Θ'[f n]? = some s) (n : ℕ) (s : Shape) : (s₀ :: Θ)[n]? = some s → (s₀ :: Θ')[liftR f n]? = some s

A lifted renaming stays coherent with the shape contexts.

def LambdaS.Tw.rename {B : Type} {k : ℕ} {Θ Θ' : List Shape} (f : ℕ → ℕ) : (∀ (n : ℕ) (s : Shape), Θ[n]? = some s → Θ'[f n]? = some s) → {s : Shape} → Tw B k Θ s → Tw B k Θ' s

Renaming the ratio context along a coherent index map.

Equations

• LambdaS.Tw.rename x✝² x✝¹ (LambdaS.Tw.var n h) = LambdaS.Tw.var (x✝² n) ⋯
• LambdaS.Tw.rename x✝¹ x✝ (LambdaS.Tw.unit u) = LambdaS.Tw.unit u
• LambdaS.Tw.rename x✝¹ x✝ (a.mul b) = (LambdaS.Tw.rename x✝¹ x✝ a).mul (LambdaS.Tw.rename x✝¹ x✝ b)
• LambdaS.Tw.rename x✝¹ x✝ (a.div b) = (LambdaS.Tw.rename x✝¹ x✝ a).div (LambdaS.Tw.rename x✝¹ x✝ b)
• LambdaS.Tw.rename x✝¹ x✝ (t.qpow q) = (LambdaS.Tw.rename x✝¹ x✝ t).qpow q
• LambdaS.Tw.rename x✝¹ x✝ t_1.lam = (LambdaS.Tw.rename (LambdaS.Tw.liftR x✝¹) ⋯ t_1).lam
• LambdaS.Tw.rename x✝² x✝¹ (g.app a) = (LambdaS.Tw.rename x✝² x✝¹ g).app (LambdaS.Tw.rename x✝² x✝¹ a)
• LambdaS.Tw.rename x✝¹ x✝ LambdaS.Tw.vecnil = LambdaS.Tw.vecnil
• LambdaS.Tw.rename x✝¹ x✝ (a.veccons v) = (LambdaS.Tw.rename x✝¹ x✝ a).veccons (LambdaS.Tw.rename x✝¹ x✝ v)
• LambdaS.Tw.rename x✝¹ x✝ (v.proj i) = (LambdaS.Tw.rename x✝¹ x✝ v).proj i
• LambdaS.Tw.rename x✝¹ x✝ LambdaS.Tw.matnil = LambdaS.Tw.matnil
• LambdaS.Tw.rename x✝¹ x✝ (r.matcons M) = (LambdaS.Tw.rename x✝¹ x✝ r).matcons (LambdaS.Tw.rename x✝¹ x✝ M)
• LambdaS.Tw.rename x✝¹ x✝ (M.row j) = (LambdaS.Tw.rename x✝¹ x✝ M).row j
• LambdaS.Tw.rename x✝¹ x✝ t.ulam = (LambdaS.Tw.rename x✝¹ x✝ t).ulam
• LambdaS.Tw.rename x✝² x✝¹ (t.uapp μ) = (LambdaS.Tw.rename x✝² x✝¹ t).uapp μ

def LambdaS.Tw.weakenR {B : Type} {k : ℕ} {Θ : List Shape} {s₀ s : Shape} (t : Tw B k Θ s) : Tw B k (s₀ :: Θ) s

Weakening by a fresh ratio variable at position 0.

Equations

• t.weakenR = LambdaS.Tw.rename (fun (x : ℕ) => x + 1) ⋯ t

def LambdaS.Tw.pullU {B : Type} {k k' : ℕ} (η : Fin k → UExp B k') {Θ : List Shape} {s : Shape} : Tw B k Θ s → Tw B k' Θ s

Pulling a ratio back along a unit substitution: every unit constant is substituted, and a recorded instantiation records the substituted unit. The syntactic face of Scaling.pull.

Equations

• LambdaS.Tw.pullU x✝² (LambdaS.Tw.var n h) = LambdaS.Tw.var n h
• LambdaS.Tw.pullU x✝¹ (LambdaS.Tw.unit u) = LambdaS.Tw.unit (LambdaS.substU x✝¹ u)
• LambdaS.Tw.pullU x✝¹ (a.mul b) = (LambdaS.Tw.pullU x✝¹ a).mul (LambdaS.Tw.pullU x✝¹ b)
• LambdaS.Tw.pullU x✝¹ (a.div b) = (LambdaS.Tw.pullU x✝¹ a).div (LambdaS.Tw.pullU x✝¹ b)
• LambdaS.Tw.pullU x✝¹ (t.qpow q) = (LambdaS.Tw.pullU x✝¹ t).qpow q
• LambdaS.Tw.pullU x✝¹ t_1.lam = (LambdaS.Tw.pullU x✝¹ t_1).lam
• LambdaS.Tw.pullU x✝² (g.app a) = (LambdaS.Tw.pullU x✝² g).app (LambdaS.Tw.pullU x✝² a)
• LambdaS.Tw.pullU x✝¹ LambdaS.Tw.vecnil = LambdaS.Tw.vecnil
• LambdaS.Tw.pullU x✝¹ (a.veccons v) = (LambdaS.Tw.pullU x✝¹ a).veccons (LambdaS.Tw.pullU x✝¹ v)
• LambdaS.Tw.pullU x✝¹ (v.proj i) = (LambdaS.Tw.pullU x✝¹ v).proj i
• LambdaS.Tw.pullU x✝¹ LambdaS.Tw.matnil = LambdaS.Tw.matnil
• LambdaS.Tw.pullU x✝¹ (r.matcons M) = (LambdaS.Tw.pullU x✝¹ r).matcons (LambdaS.Tw.pullU x✝¹ M)
• LambdaS.Tw.pullU x✝¹ (M.row j) = (LambdaS.Tw.pullU x✝¹ M).row j
• LambdaS.Tw.pullU x✝¹ t.ulam = (LambdaS.Tw.pullU (LambdaS.liftU x✝¹) t).ulam
• LambdaS.Tw.pullU x✝² (t.uapp μ) = (LambdaS.Tw.pullU x✝² t).uapp (LambdaS.substU x✝² μ)

def LambdaS.Tw.uweaken {B : Type} {k : ℕ} {Θ : List Shape} {s : Shape} (t : Tw B k Θ s) : Tw B (k + 1) Θ s

Weakening the unit scope by a fresh unit variable.

Equations

• t.uweaken = LambdaS.Tw.pullU (fun (i : Fin k) => LambdaS.Term.ofVar i.succ) t

def LambdaS.Tw.liftS {B : Type} {k : ℕ} {Θ Θ' : List Shape} {s₀ : Shape} (σ : (n : ℕ) → (s : Shape) → Θ[n]? = some s → Tw B k Θ' s) (n : ℕ) (s : Shape) : (s₀ :: Θ)[n]? = some s → Tw B k (s₀ :: Θ') s

Lifting a simultaneous substitution under a binder: the bound variable maps to itself and everything else is weakened past it.

Equations

• LambdaS.Tw.liftS σ 0 x x_1 = LambdaS.Tw.var 0 ⋯
• LambdaS.Tw.liftS σ n.succ x x_1 = (σ n x x_1).weakenR

def LambdaS.Tw.subst {B : Type} {k : ℕ} {Θ Θ' : List Shape} (σ : (n : ℕ) → (s : Shape) → Θ[n]? = some s → Tw B k Θ' s) {s : Shape} : Tw B k Θ s → Tw B k Θ' s

Simultaneous substitution of ratios for ratio variables. Crossing lam lifts the substitution; crossing ulam weakens every substituend's unit scope.

Equations

• LambdaS.Tw.subst x✝¹ (LambdaS.Tw.var n h) = x✝¹ n x✝ h
• LambdaS.Tw.subst x✝ (LambdaS.Tw.unit u) = LambdaS.Tw.unit u
• LambdaS.Tw.subst x✝ (a.mul b) = (LambdaS.Tw.subst x✝ a).mul (LambdaS.Tw.subst x✝ b)
• LambdaS.Tw.subst x✝ (a.div b) = (LambdaS.Tw.subst x✝ a).div (LambdaS.Tw.subst x✝ b)
• LambdaS.Tw.subst x✝ (t.qpow q) = (LambdaS.Tw.subst x✝ t).qpow q
• LambdaS.Tw.subst x✝ t_1.lam = (LambdaS.Tw.subst (LambdaS.Tw.liftS x✝) t_1).lam
• LambdaS.Tw.subst x✝¹ (g.app a) = (LambdaS.Tw.subst x✝¹ g).app (LambdaS.Tw.subst x✝¹ a)
• LambdaS.Tw.subst x✝ LambdaS.Tw.vecnil = LambdaS.Tw.vecnil
• LambdaS.Tw.subst x✝ (a.veccons v) = (LambdaS.Tw.subst x✝ a).veccons (LambdaS.Tw.subst x✝ v)
• LambdaS.Tw.subst x✝ (v.proj i) = (LambdaS.Tw.subst x✝ v).proj i
• LambdaS.Tw.subst x✝ LambdaS.Tw.matnil = LambdaS.Tw.matnil
• LambdaS.Tw.subst x✝ (r.matcons M) = (LambdaS.Tw.subst x✝ r).matcons (LambdaS.Tw.subst x✝ M)
• LambdaS.Tw.subst x✝ (M.row j) = (LambdaS.Tw.subst x✝ M).row j
• LambdaS.Tw.subst x✝ t.ulam = (LambdaS.Tw.subst (fun (n : ℕ) (s : LambdaS.Shape) (h : x✝²[n]? = some s) => (x✝ n s h).uweaken) t).ulam
• LambdaS.Tw.subst x✝¹ (t.uapp μ) = (LambdaS.Tw.subst x✝¹ t).uapp μ

def LambdaS.Tw.subst0 {B : Type} {k : ℕ} {Θ : List Shape} {s₀ s : Shape} (t : Tw B k (s₀ :: Θ) s) (a : Tw B k Θ s₀) : Tw B k Θ s

Substituting for the most recently bound ratio variable.

Equations

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

def LambdaS.Tw.appE {B : Type} {k : ℕ} {Θ : List Shape} {s t : Shape} : Tw B k Θ (s.arrow t) → Tw B k Θ s → Tw B k Θ t

Application that β-reduces when the head is a literal abstraction, so that a redex formed at construction is not left for the flat form to treat as an opaque atom.

Equations

• b.lam.appE x✝ = b.subst0 x✝
• x✝¹.appE x✝ = x✝¹.app x✝

def LambdaS.Tw.uappE {B : Type} {k : ℕ} {Θ : List Shape} {s : Shape} : Tw B k Θ s.bind → UExp B k → Tw B k Θ s

Unit instantiation that reduces when the head is a literal unit abstraction, by performing the recorded substitution through pullU.

Equations

• t.ulam.uappE x✝ = LambdaS.Tw.pullU (Fin.cons x✝ (LambdaS.idU B k)) t
• x✝¹.uappE x✝ = x✝¹.uapp x✝

What a ratio means

@[reducible]

def LambdaS.SemScalar : Type

The semantic ratio at scalar shape: a positive real. A definition of its own so that the space shapes can be compositional in the scalar meaning: change the scalar carrier and every shape follows.

Positivity is carried by the type rather than by a side relation: a ratio's value is built from scale factors (positive) by multiplication, division and rational powers (positivity-preserving), and the rational-power former is sound only on positives, so the carrier says so. This is the semantic face of the unit group having no zero.

Equations

• LambdaS.SemScalar = { x : ℝ // 0 < x }

noncomputable def LambdaS.SemScalar.rpow (x : SemScalar) (q : ℝ) : SemScalar

Rational powers on positive scalars, via Real.rpow.

Equations

• x.rpow q = ⟨↑x ^ q, ⋯⟩

@[simp]

theorem LambdaS.SemScalar.val_rpow (x : SemScalar) (q : ℝ) : ↑(x.rpow q) = ↑x ^ q

@[simp]

theorem LambdaS.SemScalar.val_div (x y : SemScalar) : ↑(x / y) = ↑x / ↑y

@[reducible]

def LambdaS.SemTw : Shape → Type

The semantic ratio at each shape: a scale factor at a quantity, a map at a function, a scale factor per component at a space, a scale factor per entry at a linear map (entry (j, i) is row j, column i), a family at a unit binder.

Equations

• LambdaS.SemTw LambdaS.Shape.scalar = LambdaS.SemScalar
• LambdaS.SemTw (a.arrow a_1) = (LambdaS.SemTw a → LambdaS.SemTw a_1)
• LambdaS.SemTw (LambdaS.Shape.vec a) = (Fin a → LambdaS.SemScalar)
• LambdaS.SemTw (LambdaS.Shape.mat a a_1) = (Fin a_1 → Fin a → LambdaS.SemScalar)
• LambdaS.SemTw a.bind = (ℝ → LambdaS.SemTw a)

@[reducible]

def LambdaS.TwEnv : List Shape → Type

Semantic ratios for a ratio context.

Equations

• LambdaS.TwEnv [] = PUnit.{1}
• LambdaS.TwEnv (s :: Θ) = (LambdaS.SemTw s × LambdaS.TwEnv Θ)

def LambdaS.TwEnv.lookup {Θ : List Shape} {s : Shape} (n : ℕ) : Θ[n]? = some s → TwEnv Θ → SemTw s

Looking a ratio variable up.

Equations

• LambdaS.TwEnv.lookup x✝¹ x✝ x_7 = absurd x✝ ⋯
• LambdaS.TwEnv.lookup 0 h ρ = ⋯ ▸ ρ.1
• LambdaS.TwEnv.lookup n.succ h ρ = LambdaS.TwEnv.lookup n h ρ.2

noncomputable def LambdaS.Tw.eval {B : Type} [Fintype B] {k : ℕ} : Scaling B k → {Θ : List Shape} → {s : Shape} → Tw B k Θ s → TwEnv Θ → SemTw s

The meaning of a ratio, under a declared scaling. uapp is where the recorded instantiation is finally performed: semantically, by reading the family at the instantiating unit's magnitude.

Equations

• LambdaS.Tw.eval x✝³ (LambdaS.Tw.var n h) x✝ = LambdaS.TwEnv.lookup n h x✝
• LambdaS.Tw.eval x✝² (LambdaS.Tw.unit u) x✝ = ⟨x✝².scale u, ⋯⟩
• LambdaS.Tw.eval x✝² (a.mul b) x✝ = LambdaS.Tw.eval x✝² a x✝ * LambdaS.Tw.eval x✝² b x✝
• LambdaS.Tw.eval x✝² (a.div b) x✝ = LambdaS.Tw.eval x✝² a x✝ / LambdaS.Tw.eval x✝² b x✝
• LambdaS.Tw.eval x✝² (t.qpow q) x✝ = LambdaS.SemScalar.rpow (LambdaS.Tw.eval x✝² t x✝) ↑q
• LambdaS.Tw.eval x✝² t_1.lam x✝ = fun (r : LambdaS.SemTw s) => LambdaS.Tw.eval x✝² t_1 (r, x✝)
• LambdaS.Tw.eval x✝³ (f.app a) x✝ = LambdaS.Tw.eval x✝³ f x✝ (LambdaS.Tw.eval x✝³ a x✝)
• LambdaS.Tw.eval x✝² LambdaS.Tw.vecnil x✝ = fun (i : Fin 0) => i.elim0
• LambdaS.Tw.eval x✝² (a.veccons v) x✝ = Fin.cons (LambdaS.Tw.eval x✝² a x✝) (LambdaS.Tw.eval x✝² v x✝)
• LambdaS.Tw.eval x✝² (v.proj i) x✝ = LambdaS.Tw.eval x✝² v x✝ i
• LambdaS.Tw.eval x✝² LambdaS.Tw.matnil x✝ = fun (j : Fin 0) => j.elim0
• LambdaS.Tw.eval x✝² (r.matcons M) x✝ = Fin.cons (LambdaS.Tw.eval x✝² r x✝) (LambdaS.Tw.eval x✝² M x✝)
• LambdaS.Tw.eval x✝² (M.row j) x✝ = LambdaS.Tw.eval x✝² M x✝ j
• LambdaS.Tw.eval x✝² t.ulam x✝ = fun (r : ℝ) => LambdaS.Tw.eval (x✝².cons r) t x✝
• LambdaS.Tw.eval x✝³ (t.uapp μ) x✝ = LambdaS.Tw.eval x✝³ t x✝ (x✝³.logScale μ)

@[simp]

theorem LambdaS.Tw.eval_castShape {B : Type} [Fintype B] {k : ℕ} (ψ : Scaling B k) {Θ : List Shape} {s s' : Shape} (h : s = s') (t : Tw B k Θ s) (ρ : TwEnv Θ) : eval ψ (castShape h t) ρ = h ▸ eval ψ t ρ

Evaluation commutes with retyping.

theorem LambdaS.Tw.eval_castShape_vec {B : Type} [Fintype B] {k : ℕ} (ψ : Scaling B k) {Θ : List Shape} {n n' : ℕ} (h : Shape.vec n = Shape.vec n') (t : Tw B k Θ (Shape.vec n)) (ρ : TwEnv Θ) (i : Fin n') : eval ψ (castShape h t) ρ i = eval ψ t ρ (Fin.cast ⋯ i)

Retyping along an equality of vector shapes reindexes the components and changes nothing else. The equality in play is List.length_map at a matrix row, where the row space is a map over the column space.

Derived vector and matrix combinators

vecOfFn and matOfFn build literal drift vectors and matrices from component functions. projE and rowE are proj and row that reduce on literals, so that the syntactic comparison in the drift computation sees a literal's components rather than an opaque projection; on anything that is not a literal they fall back to the formers.

def LambdaS.Tw.vecOfFn {B : Type} {k : ℕ} {Θ : List Shape} {n : ℕ} : (Fin n → Tw B k Θ Shape.scalar) → Tw B k Θ (Shape.vec n)

A literal drift vector from a component function.

Equations

• LambdaS.Tw.vecOfFn x_2 = LambdaS.Tw.vecnil
• LambdaS.Tw.vecOfFn f = (f 0).veccons (LambdaS.Tw.vecOfFn fun (i : Fin n) => f i.succ)

def LambdaS.Tw.matOfFn {B : Type} {k : ℕ} {Θ : List Shape} {n m : ℕ} : (Fin m → Tw B k Θ (Shape.vec n)) → Tw B k Θ (Shape.mat n m)

A literal drift matrix from a row function.

Equations

• LambdaS.Tw.matOfFn x_2 = LambdaS.Tw.matnil
• LambdaS.Tw.matOfFn g = (g 0).matcons (LambdaS.Tw.matOfFn fun (j : Fin n_1) => g j.succ)

def LambdaS.Tw.projE {B : Type} {k : ℕ} {Θ : List Shape} {n : ℕ} : Tw B k Θ (Shape.vec n) → Fin n → Tw B k Θ Shape.scalar

Projection that reduces on vector literals.

Equations

• (a.veccons v).projE i = Fin.cases a (fun (i' : Fin n) => v.projE i') i
• x✝¹.projE x✝ = x✝¹.proj x✝

def LambdaS.Tw.rowE {B : Type} {k : ℕ} {Θ : List Shape} {n m : ℕ} : Tw B k Θ (Shape.mat n m) → Fin m → Tw B k Θ (Shape.vec n)

Row extraction that reduces on matrix literals.

Equations

• (r.matcons M).rowE j = Fin.cases r (fun (j' : Fin m) => M.rowE j') j
• x✝¹.rowE x✝ = x✝¹.row x✝

Normalization

appE and uappE reduce the redex at hand, but substitution can create another: a lam-bound variable in head position, instantiated by an abstraction, becomes a redex the construction site never sees. The flat-form comparison treats any surviving app as an atom, so a residue of this kind costs an agreement check its completeness. Tw.norm reduces every redex, under binders included, before a ratio is compared. It runs on fuel, one unit per reduction at a root; the ratio calculus is simply typed, so a normal form exists, and the fuel is a bound the normalizer never exhausts on the ratios twistOf builds, which nest applications no deeper than the program does. Exhausting it leaves a redex in place, which the comparison then declines: fuel costs completeness, never soundness (Tw.eval_norm).

def LambdaS.Tw.size {B : Type} {k : ℕ} {Θ : List Shape} {s : Shape} : Tw B k Θ s → ℕ

Node count of a ratio, the fuel Tw.norm runs on.

Equations

• (LambdaS.Tw.var n a).size = 1
• (LambdaS.Tw.unit a).size = 1
• (a.mul b).size = a.size + b.size + 1
• (a.div b).size = a.size + b.size + 1
• (t.qpow a).size = t.size + 1
• t_1.lam.size = t_1.size + 1
• (f.app a).size = f.size + a.size + 1
• LambdaS.Tw.vecnil.size = 1
• (a.veccons v).size = a.size + v.size + 1
• (v.proj a).size = v.size + 1
• LambdaS.Tw.matnil.size = 1
• (r.matcons M).size = r.size + M.size + 1
• (M.row a).size = M.size + 1
• t.ulam.size = t.size + 1
• (t.uapp a).size = t.size + 1

@[irreducible]

def LambdaS.Tw.normN {B : Type} (n : ℕ) {k : ℕ} {Θ : List Shape} {s : Shape} : Tw B k Θ s → Tw B k Θ s

Full β-normalization on fuel: reduces app of a literal lam and uapp of a literal ulam wherever they occur, projections and rows of literals included, and leaves everything else in place.

Equations

• LambdaS.Tw.normN 0 x✝ = x✝
• LambdaS.Tw.normN n.succ (f.app a) = match LambdaS.Tw.normN (n + 1) f, LambdaS.Tw.normN (n + 1) a with | b.lam, a' => LambdaS.Tw.normN n (b.subst0 a') | f', a' => f'.app a'
• LambdaS.Tw.normN n.succ (t.uapp μ) = match LambdaS.Tw.normN (n + 1) t with | b.ulam => LambdaS.Tw.normN n (LambdaS.Tw.pullU (Fin.cons μ (LambdaS.idU B x✝²)) b) | t' => t'.uapp μ
• LambdaS.Tw.normN n.succ (a.mul b) = (LambdaS.Tw.normN (n + 1) a).mul (LambdaS.Tw.normN (n + 1) b)
• LambdaS.Tw.normN n.succ (a.div b) = (LambdaS.Tw.normN (n + 1) a).div (LambdaS.Tw.normN (n + 1) b)
• LambdaS.Tw.normN n.succ (t.qpow q) = (LambdaS.Tw.normN (n + 1) t).qpow q
• LambdaS.Tw.normN n.succ t_1.lam = (LambdaS.Tw.normN (n + 1) t_1).lam
• LambdaS.Tw.normN n.succ (a.veccons v) = (LambdaS.Tw.normN (n + 1) a).veccons (LambdaS.Tw.normN (n + 1) v)
• LambdaS.Tw.normN n.succ (v.proj i) = (LambdaS.Tw.normN (n + 1) v).projE i
• LambdaS.Tw.normN n.succ (r.matcons M) = (LambdaS.Tw.normN (n + 1) r).matcons (LambdaS.Tw.normN (n + 1) M)
• LambdaS.Tw.normN n.succ (M.row j) = (LambdaS.Tw.normN (n + 1) M).rowE j
• LambdaS.Tw.normN n.succ t.ulam = (LambdaS.Tw.normN (n + 1) t).ulam
• LambdaS.Tw.normN n.succ (LambdaS.Tw.var n_1 h) = LambdaS.Tw.var n_1 h
• LambdaS.Tw.normN n.succ (LambdaS.Tw.unit u) = LambdaS.Tw.unit u
• LambdaS.Tw.normN n.succ LambdaS.Tw.vecnil = LambdaS.Tw.vecnil
• LambdaS.Tw.normN n.succ LambdaS.Tw.matnil = LambdaS.Tw.matnil

def LambdaS.Tw.norm {B : Type} {k : ℕ} {Θ : List Shape} {s : Shape} (t : Tw B k Θ s) : Tw B k Θ s

Normalization at the fuel a ratio's own size supplies.

Equations

• t.norm = LambdaS.Tw.normN t.size t

def LambdaS.Tw.one {B : Type} {k : ℕ} {Θ : List Shape} (s : Shape) : Tw B k Θ s

The trivial ratio, as syntax, at every shape: the unit 1 at a scalar, 1 in every component at a space, the constant trivial family at an arrow and under a unit binder. This is the ratio the frees-at-one assignment gives every context variable of a program: an input is a measurement, and a measurement rescales ideally, so its ratio is 1. Atoms are reserved for lam-bound variables, whose future arguments may genuinely drift.

Equations

• LambdaS.Tw.one LambdaS.Shape.scalar = LambdaS.Tw.unit 1
• LambdaS.Tw.one (a.arrow t) = (LambdaS.Tw.one t).lam
• LambdaS.Tw.one (LambdaS.Shape.vec a) = LambdaS.Tw.vecOfFn fun (x : Fin a) => LambdaS.Tw.unit 1
• LambdaS.Tw.one (LambdaS.Shape.mat a a_1) = LambdaS.Tw.matOfFn fun (x : Fin a_1) => LambdaS.Tw.vecOfFn fun (x : Fin a) => LambdaS.Tw.unit 1
• LambdaS.Tw.one s.bind = (LambdaS.Tw.one s).ulam

@[simp]

theorem LambdaS.Tw.eval_vecOfFn {B : Type} [Fintype B] {k : ℕ} (ψ : Scaling B k) {Θ : List Shape} {n : ℕ} (f : Fin n → Tw B k Θ Shape.scalar) (ρ : TwEnv Θ) (i : Fin n) : eval ψ (vecOfFn f) ρ i = eval ψ (f i) ρ

@[simp]

theorem LambdaS.Tw.eval_matOfFn {B : Type} [Fintype B] {k : ℕ} (ψ : Scaling B k) {Θ : List Shape} {n m : ℕ} (g : Fin m → Tw B k Θ (Shape.vec n)) (ρ : TwEnv Θ) (a : Fin m) : eval ψ (matOfFn g) ρ a = eval ψ (g a) ρ

@[simp]

theorem LambdaS.Tw.eval_projE {B : Type} [Fintype B] {k : ℕ} (ψ : Scaling B k) {Θ : List Shape} {n : ℕ} (t : Tw B k Θ (Shape.vec n)) (i : Fin n) (ρ : TwEnv Θ) : eval ψ (t.projE i) ρ = eval ψ t ρ i

@[simp]

theorem LambdaS.Tw.eval_rowE {B : Type} [Fintype B] {k : ℕ} (ψ : Scaling B k) {Θ : List Shape} {n m : ℕ} (t : Tw B k Θ (Shape.mat n m)) (j : Fin m) (ρ : TwEnv Θ) : eval ψ (t.rowE j) ρ = eval ψ t ρ j

Renaming and substitution preserve evaluation

theorem LambdaS.Tw.eval_rename {B : Type} [Fintype B] {k : ℕ} (ψ : Scaling B k) {Θ Θ' : List Shape} (f : ℕ → ℕ) (hf : ∀ (n : ℕ) (s : Shape), Θ[n]? = some s → Θ'[f n]? = some s) {s : Shape} (t : Tw B k Θ s) (ρ : TwEnv Θ) (ρ' : TwEnv Θ') : (∀ (n : ℕ) (sh : Shape) (h : Θ[n]? = some sh), TwEnv.lookup (f n) ⋯ ρ' = TwEnv.lookup n h ρ) → eval ψ (rename f hf t) ρ' = eval ψ t ρ

Renaming preserves evaluation, at environments that agree along the renaming.

theorem LambdaS.Tw.eval_weakenR {B : Type} [Fintype B] {k : ℕ} (ψ : Scaling B k) {Θ : List Shape} {s₀ s : Shape} (t : Tw B k Θ s) (r : SemTw s₀) (ρ : TwEnv Θ) : eval ψ t.weakenR (r, ρ) = eval ψ t ρ

Weakening by a fresh ratio variable is invisible to evaluation.

theorem LambdaS.Tw.eval_pullU {B : Type} [Fintype B] {k k' : ℕ} (ψ : Scaling B k') (η : Fin k → UExp B k') {Θ : List Shape} {s : Shape} (t : Tw B k Θ s) (ρ : TwEnv Θ) : eval ψ (pullU η t) ρ = eval (ψ.pull η) t ρ

The unit-scope pullback is the syntactic face of Scaling.pull.

theorem LambdaS.Tw.eval_uweaken {B : Type} [Fintype B] {k : ℕ} (ψ : Scaling B k) (r : ℝ) {Θ : List Shape} {s : Shape} (t : Tw B k Θ s) (ρ : TwEnv Θ) : eval (ψ.cons r) t.uweaken ρ = eval ψ t ρ

Weakening the unit scope is invisible to evaluation.

theorem LambdaS.Tw.eval_subst {B : Type} [Fintype B] {k : ℕ} (ψ : Scaling B k) {Θ Θ' : List Shape} (σ : (n : ℕ) → (s : Shape) → Θ[n]? = some s → Tw B k Θ' s) {s : Shape} (t : Tw B k Θ s) (ρ : TwEnv Θ) (ρ' : TwEnv Θ') : (∀ (n : ℕ) (sh : Shape) (h : Θ[n]? = some sh), eval ψ (σ n sh h) ρ' = TwEnv.lookup n h ρ) → eval ψ (subst σ t) ρ' = eval ψ t ρ

Substitution preserves evaluation, at environments where each substituend evaluates to the value it replaces.

theorem LambdaS.Tw.eval_subst0 {B : Type} [Fintype B] {k : ℕ} (ψ : Scaling B k) {Θ : List Shape} {s₀ s : Shape} (t : Tw B k (s₀ :: Θ) s) (a : Tw B k Θ s₀) (ρ : TwEnv Θ) : eval ψ (t.subst0 a) ρ = eval ψ t (eval ψ a ρ, ρ)

β: substituting for the most recent ratio variable evaluates the body at the substituend's value.

@[simp]

theorem LambdaS.Tw.eval_appE {B : Type} [Fintype B] {k : ℕ} (ψ : Scaling B k) {Θ : List Shape} {s t : Shape} (f : Tw B k Θ (s.arrow t)) (a : Tw B k Θ s) (ρ : TwEnv Θ) : eval ψ (f.appE a) ρ = eval ψ f ρ (eval ψ a ρ)

The reducing application evaluates as app does.

@[simp]

theorem LambdaS.Tw.eval_uappE {B : Type} [Fintype B] {k : ℕ} (ψ : Scaling B k) {Θ : List Shape} {s : Shape} (t : Tw B k Θ s.bind) (μ : UExp B k) (ρ : TwEnv Θ) : eval ψ (t.uappE μ) ρ = eval ψ t ρ (ψ.logScale μ)

The reducing unit instantiation evaluates as uapp does: performing the recorded substitution syntactically agrees with reading the family at the instantiating unit's magnitude, which is Scaling.pull_subst.

theorem LambdaS.Tw.eval_normN {B : Type} [Fintype B] {k : ℕ} (ψ : Scaling B k) (n : ℕ) {Θ : List Shape} {s : Shape} (t : Tw B k Θ s) (ρ : TwEnv Θ) : eval ψ (normN n t) ρ = eval ψ t ρ

Normalization preserves evaluation, at every fuel.

@[simp]

theorem LambdaS.Tw.eval_norm {B : Type} [Fintype B] {k : ℕ} (ψ : Scaling B k) {Θ : List Shape} {s : Shape} (t : Tw B k Θ s) (ρ : TwEnv Θ) : eval ψ t.norm ρ = eval ψ t ρ

Normalization preserves evaluation.

def LambdaS.oneSem (s : Shape) : SemTw s

The trivial semantic ratio at each shape: 1 at a quantity, 1 in every component at a space, and "maps trivial to trivial" at a function.

Equations

• LambdaS.oneSem LambdaS.Shape.scalar = 1
• LambdaS.oneSem (a.arrow a_1) = fun (x : LambdaS.SemTw a) => LambdaS.oneSem a_1
• LambdaS.oneSem (LambdaS.Shape.vec a) = fun (x : Fin a) => 1
• LambdaS.oneSem (LambdaS.Shape.mat a a_1) = fun (x : Fin a_1) (x_1 : Fin a) => 1
• LambdaS.oneSem a.bind = fun (x : ℝ) => LambdaS.oneSem a

theorem LambdaS.Tw.eval_one {B : Type} [Fintype B] {k : ℕ} (ψ : Scaling B k) {Θ : List Shape} (s : Shape) (θρ : TwEnv Θ) : eval ψ (one s) θρ = oneSem s

The trivial syntactic ratio evaluates to the trivial semantic one, in every scaling and every environment.

The twisted logical relation

Rel says a term is scale-invariant. TwRel says it is invariant up to a ratio, and it separates the two things a rescaling can move. The valuation the conversion factors are drawn from is rescaled by φ; the values themselves are rescaled by ψ. A conversion pays once for each: its factor V(u)/V(v) moves with φ, and the converted value moves with ψ at its source unit where its type promises the target. So the relation carries two readings of the ratio, s under φ and s' under ψ, and at a quantity the rescaled value is ψ(u) · s · s' times the original. At φ = ψ the ratio appears squared, the law of the paper's opening example; at ψ = 0 (values fixed, valuation moved) it appears once and the type's factor not at all, which is what makes a drift-free program declaration-independent; at φ = 0 (valuation fixed, values moved) it appears once beside the type's factor, which is the scaling law the Pi theorem consumes. At ratio 1 all three are Rel.

At a unit binder the ratio is a family indexed by the bound unit's scaling, one family per reading, while the denotation is a family indexed by its magnitude. Those are different things, which is why all three indices appear; the rescaled denotation is read at r + s, the magnitude moved by the valuation's extension.

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

The logical relation, twisted by a ratio, read once under the valuation rescaling φ and once under the value rescaling ψ.

Equations

• One or more equations did not get rendered due to their size.
• LambdaS.TwRel (LambdaS.Ty.Q u) s s' x✝¹ x✝ x_12 y = (y = x✝.scale u * (↑s * ↑s') * x_12)
• LambdaS.TwRel (a.arrow b) F F' x✝¹ x✝ f g = ∀ (r r' : LambdaS.SemTw a.shape) (x y : a.den), LambdaS.TwRel a r r' x✝¹ x✝ x y → LambdaS.TwRel b (F r) (F' r') x✝¹ x✝ (f x) (g y)
• LambdaS.TwRel (LambdaS.Ty.vec V) r r' x✝¹ x✝ v w = ∀ (i : Fin (List.length V)), w i = x✝.scale (List.get V i) * (↑(r i) * ↑(r' i)) * v i
• LambdaS.TwRel (LambdaS.Ty.all a τ) F F' x✝¹ x✝ X Y = ∀ (r s s' : ℝ), LambdaS.TwRel τ (F s) (F' s') (x✝¹.cons s) (x✝.cons s') (X r) (Y (r + s))
• LambdaS.TwRel τ.allDim F F' x✝¹ x✝ X Y = LambdaS.TwRel τ F F' x✝¹ x✝ X Y

def LambdaS.IsOneSem (s : Shape) : SemTw s → Prop

Having a trivial ratio, at every shape: 1 at a quantity, and at a function "maps trivial to trivial". The arrow clause is what a convert-free function satisfies (λx. x·x sends ratio 1 to 1 even though it squares others), and it is a predicate rather than a value for exactly that reason.

Equations

• LambdaS.IsOneSem LambdaS.Shape.scalar r = (r = 1)
• LambdaS.IsOneSem (s.arrow t) φ = ∀ (r : LambdaS.SemTw s), LambdaS.IsOneSem s r → LambdaS.IsOneSem t (φ r)
• LambdaS.IsOneSem (LambdaS.Shape.vec a) v = ∀ (i : Fin a), v i = 1
• LambdaS.IsOneSem (LambdaS.Shape.mat a a_1) A = ∀ (a_2 : Fin a_1) (i : Fin a), A a_2 i = 1
• LambdaS.IsOneSem s.bind F = ∀ (r : ℝ), LambdaS.IsOneSem s (F r)

theorem LambdaS.isOneSem_oneSem (s : Shape) : IsOneSem s (oneSem s)

The canonical trivial ratio is trivial.

@[simp]

theorem LambdaS.trel_Q_one {B D : Type} [Fintype B] {k : ℕ} {u : UExp B k} (φ ψ : Scaling B k) (x y : ℝ) : TwRel (Ty.Q u) 1 1 φ ψ x y ↔ Rel (Ty.Q u) ψ x y

At the trivial ratio and at scalar type, TwRel is Rel. So Kennedy's theorem is the s = 1 case of the twisted one rather than a separate result. The valuation rescaling φ is invisible at scalar type: only conversion reads the valuation, and a trivial ratio says the conversions canceled.

Stated at scalar type, and that is not a limitation to apologize for: at arrow type TwRel quantifies over every argument ratio, so it is strictly stronger than Rel there rather than equivalent to it. The scalar case is where the characterization is used, and where the two genuinely coincide.

Positivity of ratios lives in the carrier itself, SemScalar, where the rational-power former needs it, rather than in a separate logical relation over shapes. A scalar ratio's value is positive by type, which is what lets the characterization divide by it, and it is the semantic face of the group having no zero.

Transporting the twisted relation

The same shape as rel_ground and relCo_ground, carrying the two ratio readings as well. The ratios' transport is along an equality of shapes, which is why it costs nothing: Ty.shape_ground says grounding leaves the shape alone.

theorem LambdaS.twRel_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₀) {w v : SemTw τ.shape} {w' v' : SemTw (Ty.ground η δ τ).shape} {x y : τ.den} {x' y' : (Ty.ground η δ τ).den} : w ≍ w' → v ≍ v' → x ≍ x' → y ≍ y' → (TwRel (Ty.ground η δ τ) w' v' φ ψ x' y' ↔ TwRel τ w v (φ.pull η) (ψ.pull η) x y)

TwRel transports along grounding.

theorem LambdaS.twRel_subst {B D : Type} [Fintype B] {j k : ℕ} (τ : Ty B D j (k + 1)) (σ : UExp B k) (φ ψ : Scaling B k) {w v : SemTw τ.shape} {w' v' : SemTw (τ.subst σ).shape} {x y : τ.den} {x' y' : (τ.subst σ).den} (hw : w ≍ w') (hv : v ≍ v') (hx : x ≍ x') (hy : y ≍ y') : TwRel (τ.subst σ) w' v' φ ψ x' y' ↔ TwRel τ w v (φ.cons (φ.logScale σ)) (ψ.cons (ψ.logScale σ)) x y

Instantiating a unit variable, for TwRel.

theorem LambdaS.twRel_substDim {B D : Type} [Fintype B] {j k : ℕ} (τ : Ty B D (j + 1) k) (d : DExp D j) (φ ψ : Scaling B k) {w v : SemTw τ.shape} {w' v' : SemTw (τ.substDim d).shape} {x y : τ.den} {x' y' : (τ.substDim d).den} (hw : w ≍ w') (hv : v ≍ v') (hx : x ≍ x') (hy : y ≍ y') : TwRel (τ.substDim d) w' v' φ ψ x' y' ↔ TwRel τ w v φ ψ x y

Instantiating a dimension variable, for TwRel.

theorem LambdaS.twRel_weaken {B D : Type} [Fintype B] {j k : ℕ} (τ : Ty B D j k) (φ ψ : Scaling B k) (s s' : ℝ) {w v : SemTw τ.shape} {w' v' : SemTw τ.weaken.shape} {x y : τ.den} {x' y' : τ.weaken.den} (hw : w ≍ w') (hv : v ≍ v') (hx : x ≍ x') (hy : y ≍ y') : TwRel τ.weaken w' v' (φ.cons s) (ψ.cons s') x' y' ↔ TwRel τ w v φ ψ x y

Weakening under a unit binder, for TwRel.

def LambdaS.oneTwEnv (Θ : List Shape) : TwEnv Θ

Every argument enters with trivial ratio: a TwEnv of ones.

Equations

• LambdaS.oneTwEnv [] = PUnit.unit
• LambdaS.oneTwEnv (s :: Θ) = (LambdaS.oneSem s, LambdaS.oneTwEnv Θ)

theorem LambdaS.TwEnv.lookup_oneTwEnv {Θ : List Shape} {s : Shape} (n : ℕ) (h : Θ[n]? = some s) : lookup n h (oneTwEnv Θ) = oneSem s

Looking up the all-ones environment gives the trivial ratio.

def LambdaS.TwEnv.OnesFrom (p : ℕ) {Θ : List Shape} (θρ : TwEnv Θ) : Prop

The pinned region of a ratio environment. A ratio environment is trivial from position p on: positions below p are the genuine atoms, introduced by lam binders, and positions at p and beyond are the program's own context variables, whose ratio the frees-at-one assignment fixes at 1.

Equations

• LambdaS.TwEnv.OnesFrom p θρ = ∀ (n : ℕ) (s : LambdaS.Shape) (h : Θ[n]? = some s), p ≤ n → LambdaS.TwEnv.lookup n h θρ = LambdaS.oneSem s

theorem LambdaS.TwEnv.OnesFrom.cons {p : ℕ} {Θ : List Shape} {θρ : TwEnv Θ} {s : Shape} (r : SemTw s) (hθ : OnesFrom p θρ) : OnesFrom (p + 1) (r, θρ)

Extending the environment at a fresh atom moves the pinned region one position out: the lam case of the scaling law.

theorem LambdaS.TwEnv.onesFrom_oneTwEnv (p : ℕ) {Θ : List Shape} : OnesFrom p (oneTwEnv Θ)

The all-ones environment is trivial from every position on.

The symbolic normalizer

A ratio's value under ψ at the trivial environment is ψ.scale of a single unit expression, and that expression is computable. This is what makes the triviality of a ratio decidable, which is the point of ratios being syntax.

The normalizer is environment-passing in the unit scope: rather than moving values between scopes (which would force a Kripke model, since the function space at arrow shape cannot be weakened), every value lives at one global scope k₀, and a term's own unit variables are interpreted through υ. Crossing a ulam extends υ; nothing is ever weakened. bind is interpreted as a function from unit expressions, not from reals: the semantic family is read only at magnitudes of expressible units (uapp records a UExp), so agreement there is agreement everywhere it is consulted.

@[reducible]

def LambdaS.SynTw (B : Type) (k₀ : ℕ) : Shape → Type

The symbolic model, at a fixed global unit scope.

Equations

• LambdaS.SynTw B k₀ LambdaS.Shape.scalar = LambdaS.UExp B k₀
• LambdaS.SynTw B k₀ (a.arrow a_1) = (LambdaS.SynTw B k₀ a → LambdaS.SynTw B k₀ a_1)
• LambdaS.SynTw B k₀ (LambdaS.Shape.vec a) = (Fin a → LambdaS.UExp B k₀)
• LambdaS.SynTw B k₀ (LambdaS.Shape.mat a a_1) = (Fin a_1 → Fin a → LambdaS.UExp B k₀)
• LambdaS.SynTw B k₀ a.bind = (LambdaS.UExp B k₀ → LambdaS.SynTw B k₀ a)

def LambdaS.SynTw.one {B : Type} {k₀ : ℕ} (s : Shape) : SynTw B k₀ s

Trivial values, at every shape.

Equations

• LambdaS.SynTw.one LambdaS.Shape.scalar = 1
• LambdaS.SynTw.one (a.arrow t) = fun (x : LambdaS.SynTw B x✝ a) => LambdaS.SynTw.one t
• LambdaS.SynTw.one (LambdaS.Shape.vec a) = fun (x : Fin a) => 1
• LambdaS.SynTw.one (LambdaS.Shape.mat a a_1) = fun (x : Fin a_1) (x_1 : Fin a) => 1
• LambdaS.SynTw.one s.bind = fun (x : LambdaS.UExp B x✝) => LambdaS.SynTw.one s

@[reducible]

def LambdaS.SynEnv (B : Type) (k₀ : ℕ) : List Shape → Type

Symbolic environments.

Equations

• LambdaS.SynEnv B k₀ [] = PUnit.{1}
• LambdaS.SynEnv B k₀ (s :: Θ) = (LambdaS.SynTw B k₀ s × LambdaS.SynEnv B k₀ Θ)

def LambdaS.SynEnv.lookup {B : Type} {k₀ : ℕ} {Θ : List Shape} {s : Shape} (n : ℕ) : Θ[n]? = some s → SynEnv B k₀ Θ → SynTw B k₀ s

Looking a symbolic value up.

Equations

• LambdaS.SynEnv.lookup x✝¹ x✝ x_7 = absurd x✝ ⋯
• LambdaS.SynEnv.lookup 0 h ρ = ⋯ ▸ ρ.1
• LambdaS.SynEnv.lookup n.succ h ρ = LambdaS.SynEnv.lookup n h ρ.2

def LambdaS.SynEnv.ones {B : Type} {k₀ : ℕ} (Θ : List Shape) : SynEnv B k₀ Θ

The all-ones symbolic environment.

Equations

• LambdaS.SynEnv.ones [] = PUnit.unit
• LambdaS.SynEnv.ones (s :: Θ) = (LambdaS.SynTw.one s, LambdaS.SynEnv.ones Θ)

def LambdaS.Tw.nf {B : Type} {k₀ k : ℕ} (υ : Fin k → UExp B k₀) {Θ : List Shape} {s : Shape} : Tw B k Θ s → SynEnv B k₀ Θ → SynTw B k₀ s

The normalizer. Computes the symbolic value of a ratio.

Equations

• LambdaS.Tw.nf x✝³ (LambdaS.Tw.var n h) x✝ = LambdaS.SynEnv.lookup n h x✝
• LambdaS.Tw.nf x✝² (LambdaS.Tw.unit u) x✝ = LambdaS.substU x✝² u
• LambdaS.Tw.nf x✝² (a.mul b) x✝ = LambdaS.Term.mul (LambdaS.Tw.nf x✝² a x✝) (LambdaS.Tw.nf x✝² b x✝)
• LambdaS.Tw.nf x✝² (a.div b) x✝ = LambdaS.Term.div (LambdaS.Tw.nf x✝² a x✝) (LambdaS.Tw.nf x✝² b x✝)
• LambdaS.Tw.nf x✝² (t.qpow q) x✝ = LambdaS.Term.rpow (LambdaS.Tw.nf x✝² t x✝) q
• LambdaS.Tw.nf x✝² t_1.lam x✝ = fun (x : LambdaS.SynTw B k₀ s) => LambdaS.Tw.nf x✝² t_1 (x, x✝)
• LambdaS.Tw.nf x✝³ (f.app a) x✝ = LambdaS.Tw.nf x✝³ f x✝ (LambdaS.Tw.nf x✝³ a x✝)
• LambdaS.Tw.nf x✝² LambdaS.Tw.vecnil x✝ = fun (i : Fin 0) => i.elim0
• LambdaS.Tw.nf x✝² (a.veccons v) x✝ = Fin.cons (LambdaS.Tw.nf x✝² a x✝) (LambdaS.Tw.nf x✝² v x✝)
• LambdaS.Tw.nf x✝² (v.proj i) x✝ = LambdaS.Tw.nf x✝² v x✝ i
• LambdaS.Tw.nf x✝² LambdaS.Tw.matnil x✝ = fun (j : Fin 0) => j.elim0
• LambdaS.Tw.nf x✝² (r.matcons M) x✝ = Fin.cons (LambdaS.Tw.nf x✝² r x✝) (LambdaS.Tw.nf x✝² M x✝)
• LambdaS.Tw.nf x✝² (M.row j) x✝ = LambdaS.Tw.nf x✝² M x✝ j
• LambdaS.Tw.nf x✝² t.ulam x✝ = fun (μ : LambdaS.UExp B k₀) => LambdaS.Tw.nf (Fin.cons μ x✝²) t x✝
• LambdaS.Tw.nf x✝³ (t.uapp μ) x✝ = LambdaS.Tw.nf x✝³ t x✝ (LambdaS.substU x✝³ μ)

Correctness

def LambdaS.SRel {B : Type} [Fintype B] {k₀ : ℕ} (ψ : Scaling B k₀) (s : Shape) : SynTw B k₀ s → SemTw s → Prop

The relation between symbolic and semantic values. At bind the two families need only agree at magnitudes of expressible units: those are the only points uapp ever reads.

Equations

• LambdaS.SRel ψ LambdaS.Shape.scalar m v = (↑v = ψ.scale m)
• LambdaS.SRel ψ (s.arrow t) F G = ∀ (m : LambdaS.SynTw B k₀ s) (v : LambdaS.SemTw s), LambdaS.SRel ψ s m v → LambdaS.SRel ψ t (F m) (G v)
• LambdaS.SRel ψ (LambdaS.Shape.vec a) mV vV = ∀ (i : Fin a), ↑(vV i) = ψ.scale (mV i)
• LambdaS.SRel ψ (LambdaS.Shape.mat a a_1) mA vA = ∀ (a_2 : Fin a_1) (i : Fin a), ↑(vA a_2 i) = ψ.scale (mA a_2 i)
• LambdaS.SRel ψ s.bind F G = ∀ (μ : LambdaS.UExp B k₀), LambdaS.SRel ψ s (F μ) (G (ψ.logScale μ))

def LambdaS.SRelEnv {B : Type} [Fintype B] {k₀ : ℕ} (ψ : Scaling B k₀) (Θ : List Shape) : SynEnv B k₀ Θ → TwEnv Θ → Prop

Environments related pointwise.

Equations

• LambdaS.SRelEnv ψ [] x_3 x_4 = True
• LambdaS.SRelEnv ψ (s :: Θ) mρ θρ = (LambdaS.SRel ψ s mρ.1 θρ.1 ∧ LambdaS.SRelEnv ψ Θ mρ.2 θρ.2)

theorem LambdaS.SRelEnv.lookup {B : Type} [Fintype B] {k₀ : ℕ} {ψ : Scaling B k₀} {Θ : List Shape} {s : Shape} (n : ℕ) (h : Θ[n]? = some s) {mρ : SynEnv B k₀ Θ} {θρ : TwEnv Θ} : SRelEnv ψ Θ mρ θρ → SRel ψ s (SynEnv.lookup n h mρ) (TwEnv.lookup n h θρ)

theorem LambdaS.srel_one {B : Type} [Fintype B] {k₀ : ℕ} (ψ : Scaling B k₀) (s : Shape) : SRel ψ s (SynTw.one s) (oneSem s)

The trivial symbolic value relates to the trivial semantic one.

theorem LambdaS.srelEnv_ones {B : Type} [Fintype B] {k₀ : ℕ} (ψ : Scaling B k₀) (Θ : List Shape) : SRelEnv ψ Θ (SynEnv.ones Θ) (oneTwEnv Θ)

The all-ones environments are related.

theorem LambdaS.Tw.nf_correct {B : Type} [Fintype B] {k₀ : ℕ} (ψ : Scaling B k₀) {k : ℕ} (υ : Fin k → UExp B k₀) {Θ : List Shape} {s : Shape} (t : Tw B k Θ s) (mρ : SynEnv B k₀ Θ) (θρ : TwEnv Θ) : SRelEnv ψ Θ mρ θρ → SRel ψ s (nf υ t mρ) (eval (ψ.pull υ) t θρ)

The normalizer is correct. Its output, under SRel, matches the ratio's value (the ratio's unit scope read through υ, its scaling therefore the pullback). The ulam case is pull_cons and the uapp case is logScale_pull: the environment-passing design paying off, with no weakening, no Kripke structure, and no transport.