Type soundness

The System F proof, with units in place of type variables.

The shape is the textbook one: a value typing relation, an environment typing relation defined mutually with it (a closure's type depends on the context its captured environment satisfies), and a preservation theorem by induction on the term with the fuel bound handled by an outer strong induction.

Where units show up

In exactly two places, and neither is structural.

EnvOkD is the semantic counterpart of the dimension context: the runtime unit environment must assign each unit variable a unit whose dimension is the one the static context declared. dimOf_substU then says grounding commutes with taking dimensions. That is the only genuinely dimensional lemma in the file, and because units are exponent vectors it is a Fubini argument rather than an induction: the same simplification Kennedy identifies as the payoff of treating units as an abelian group rather than as syntax, here strengthened by the representation being a vector rather than a normal form.

Everything else (that grounding commutes with product, quotient and rational power, that it composes, that weakening is invisible to it) is discharged in LambdaS.Syntax by linear algebra.

What is proved

If evaluation returns a value, that value has the type the checker predicted, at every type and every scope: closures, unit abstraction and dimension abstraction included. Totality is not claimed here; a fuel-bounded evaluator cannot have it without a normalization argument, and none stays ambiguous between ill-typed and out-of-fuel. LambdaS.Normalization supplies the normalization argument, and with it the "evaluation succeeds" statement at the whole language.

The dimensional side condition

def LambdaS.EnvOkD {B D : Type} [Fintype B] [UnitSys B D] {j k : ℕ} (Δ : DCtx D j k) (η : UEnv B k) (δ : DEnv D j) : Prop

The runtime environments respect the static dimension context: every unit variable is bound to a unit of the dimension its binder declared.

This is what a unit environment must satisfy to be a semantic model of Δ, and HasTy.uapp's premise dimOf Δ σ = d is exactly the syntactic check that maintains it.

Equations

• LambdaS.EnvOkD Δ η δ = ∀ (i : Fin k), LambdaS.dimOf (LambdaS.DCtx.nil D) (η i) = LambdaS.substU δ (Δ i)

theorem LambdaS.dimOf_substU {B D : Type} [Fintype B] [UnitSys B D] {j k : ℕ} {Δ : DCtx D j k} {η : UEnv B k} {δ : DEnv D j} (h : EnvOkD Δ η δ) (u : UExp B k) : dimOf (DCtx.nil D) (substU η u) = substU δ (dimOf Δ u)

Grounding commutes with taking dimensions.

The one dimensional lemma in the development. It holds because dimOf and substU are both linear maps on exponent vectors, so the content is a change in summation order rather than an induction over syntax.

theorem LambdaS.EnvOkD.cons {B D : Type} [Fintype B] [UnitSys B D] {j k : ℕ} {Δ : DCtx D j k} {η : UEnv B k} {δ : DEnv D j} (h : EnvOkD Δ η δ) {d : DExp D j} {w : UExp B 0} (hw : dimOf (DCtx.nil D) w = substU δ d) : EnvOkD (DCtx.cons d Δ) (Fin.cons w η) δ

Extending both the dimension context and the unit environment preserves the condition, provided the new unit has the declared dimension.

theorem LambdaS.EnvOkD.consDim {B D : Type} [Fintype B] [UnitSys B D] {j k : ℕ} {Δ : DCtx D j k} {η : UEnv B k} {δ : DEnv D j} (h : EnvOkD Δ η δ) (w : DExp D 0) : EnvOkD Δ.weakenDim η (Fin.cons w δ)

The dimension analogue, for a dimension abstraction.

Value and environment typing

@[reducible, inline]

abbrev LambdaS.groundCtx {B D : Type} {j k : ℕ} (η : UEnv B k) (δ : DEnv D j) (Γ : Ctx B D j k) : Ctx B D 0 0

A context grounded through the environments.

Equations

• LambdaS.groundCtx η δ Γ = List.map (LambdaS.Ty.ground η δ) Γ

inductive LambdaS.ValTy {B D R : Type} [Fintype B] [UnitSys B D] : Val R B D → Ty B D 0 0 → Prop

A runtime value has the type the checker predicts, grounded.

• scalar {B D R : Type} [Fintype B] [UnitSys B D] (m : R) (u : UExp B 0) : ValTy (Val.scalar { mag := m, unit := u }) (Ty.Q u)
• vector {B D R : Type} [Fintype B] [UnitSys B D] {xs : List R} {V : Sp B 0} : xs.length = List.length V → ValTy (Val.vector xs V) (Ty.vec V)
• matrix {B D R : Type} [Fintype B] [UnitSys B D] {M : List (List R)} {V W : Sp B 0} : M.length = List.length W → (∀ r ∈ M, r.length = List.length V) → ValTy (Val.matrix M V W) (Ty.lin V W)
• closure {B D R : Type} [Fintype B] [UnitSys B D] {j k : ℕ} {Δ : DCtx D j k} {Γ : Ctx B D j k} {σ τ : Ty B D j k} {b : Tm B D j k} {ρ : List (Val R B D)} {η : UEnv B k} {δ : DEnv D j} {T : Ty B D 0 0} : EnvTy ρ (groundCtx η δ Γ) → EnvOkD Δ η δ → ∀ (a✝ : HasTy Δ (σ :: Γ) b τ), T = Ty.ground η δ (σ.arrow τ) → ValTy (Val.closure σ b ρ η δ) T
• uclos {B D R : Type} [Fintype B] [UnitSys B D] {j k : ℕ} {Δ : DCtx D j k} {Γ : Ctx B D j k} {d : DExp D j} {τ : Ty B D j (k + 1)} {b : Tm B D j (k + 1)} {ρ : List (Val R B D)} {η : UEnv B k} {δ : DEnv D j} {T : Ty B D 0 0} : EnvTy ρ (groundCtx η δ Γ) → EnvOkD Δ η δ → ∀ (a✝ : HasTy (DCtx.cons d Δ) Γ.weaken b τ), T = Ty.ground η δ (Ty.all d τ) → ValTy (Val.uclos d b ρ η δ) T
• dclos {B D R : Type} [Fintype B] [UnitSys B D] {j k : ℕ} {Δ : DCtx D j k} {Γ : Ctx B D j k} {τ : Ty B D (j + 1) k} {b : Tm B D (j + 1) k} {ρ : List (Val R B D)} {η : UEnv B k} {δ : DEnv D j} {T : Ty B D 0 0} : EnvTy ρ (groundCtx η δ Γ) → EnvOkD Δ η δ → ∀ (a✝ : HasTy Δ.weakenDim Γ.weakenDim b τ), T = Ty.ground η δ τ.allDim → ValTy (Val.dclos b ρ η δ) T

inductive LambdaS.EnvTy {B D R : Type} [Fintype B] [UnitSys B D] : List (Val R B D) → Ctx B D 0 0 → Prop

An environment supplies a well-typed value for every entry of a context.

• nil {B D R : Type} [Fintype B] [UnitSys B D] : EnvTy [] []
• cons {B D R : Type} [Fintype B] [UnitSys B D] {v : Val R B D} {ρ : List (Val R B D)} {Γ : Ctx B D 0 0} {τ : Ty B D 0 0} : ValTy v τ → EnvTy ρ Γ → EnvTy (v :: ρ) (τ :: Γ)

theorem LambdaS.EnvTy.lookup {B D R : Type} [Fintype B] [UnitSys B D] {ρ : List (Val R B D)} {Γ : Ctx B D 0 0} {n : ℕ} {τ : Ty B D 0 0} : EnvTy ρ Γ → Γ[n]? = some τ → ∃ (v : Val R B D), ρ[n]? = some v ∧ ValTy v τ

Looking up a well-typed environment gives a well-typed value.

Inversion

A value's shape is determined by its type, which is what discharges the evaluator's | _ => none branches.

theorem LambdaS.ValTy.scalar_inv {B D R : Type} [Fintype B] [UnitSys B D] {v : Val R B D} {u : UExp B 0} (h : ValTy v (Ty.Q u)) : ∃ (m : R), v = Val.scalar { mag := m, unit := u }

theorem LambdaS.ValTy.vector_inv {B D R : Type} [Fintype B] [UnitSys B D] {v : Val R B D} {V : Sp B 0} (h : ValTy v (Ty.vec V)) : ∃ (xs : List R), v = Val.vector xs V ∧ xs.length = List.length V

theorem LambdaS.ValTy.matrix_inv {B D R : Type} [Fintype B] [UnitSys B D] {v : Val R B D} {V W : Sp B 0} (h : ValTy v (Ty.lin V W)) : ∃ (M : List (List R)), v = Val.matrix M V W ∧ M.length = List.length W ∧ ∀ r ∈ M, r.length = List.length V

The theorem

Strong induction on the fuel, then ordinary induction on the term. The fuel induction is needed only where evaluation leaves the term (entering a closure body), and the term induction handles everything else, exactly as in the System F development.

theorem LambdaS.eval_sound {B D R : Type} [Fintype B] [DecidableEq B] [Fintype D] [DecidableEq D] [UnitSys B D] [Num R] (cf : UExp B 0 → UExp B 0 → R) (n : ℕ) {j k : ℕ} (e : Tm B D j k) (η : UEnv B k) (δ : DEnv D j) (ρ : List (Val R B D)) (Δ : DCtx D j k) (Γ : Ctx B D j k) (τ : Ty B D j k) (v : Val R B D) : EnvTy ρ (groundCtx η δ Γ) → EnvOkD Δ η δ → ∀ (a✝ : HasTy Δ Γ e τ), eval cf n j k η δ ρ e = some v → ValTy v (Ty.ground η δ τ)