Adequacy: the evaluator computes the denotation, at the declared factors

Two halves of the conversion story have been proved separately and never joined.

LambdaS.Declare says when a set of unit declarations determines a valuation, and rejects the sets that do not. LambdaS.Conversion says a valuation makes conversion path-independent. LambdaS.Fundamental gives the denotational semantics, in which convert reads that valuation for its factor. (Unit application also consults it, but only to pick the index at which a family is sampled.) LambdaS.Dynamics gives the evaluator, which takes the conversion factor from an abstract oracle cf, constrained by nothing at all.

So the declarations determine a number, and the evaluator multiplies by a number, and nothing but eval_adeq says they are the same number. Every worked example elsewhere passes fun _ _ => 1.0; this file is where the conversion oracle is finally pinned.

eval_adeq is the join. Take the oracle to be conv V (the conversion the valuation determines, hence the one the declarations determine), and evaluation of a well-typed term agrees with its denotation, unit and magnitude both. The convert case is where the content is: the evaluator's factor is conv V (substU η u) (substU η v) and the denotation's is conv (V.pull η) u v, and Scaling.scale_pull says those are equal.

Why the relation carries the environments

Adeq is indexed by the runtime unit and dimension environments rather than stated at grounded types. That is what keeps it free of transports: at ∀u:δ. τ the relation recurses at Fin.cons μ η and at τ itself, so the denotation stays in Ty.den τ and never has to be cast along Ty.den_subst. The scaling follows the environments by Scaling.pull, and pull_cons is the lemma that says instantiating a unit variable and extending the scaling agree.

Function, unit-polymorphic and dimension-polymorphic values are related behaviorally, as in LambdaS.Normalization: a closure is adequate when applying it to adequate arguments yields adequate results. Nothing is said about the closure's captured scope, which is what lets the relation live at a single type while the evaluator works at many.

def LambdaS.Adeq {B D : Type} [Fintype B] [DecidableEq B] [Fintype D] [DecidableEq D] [UnitSys B D] (V : Scaling B 0) {j k : ℕ} : UEnv B k → DEnv D j → (τ : Ty B D j k) → Val ℝ B D → τ.den → Prop

Adequacy at a type: a runtime value carries exactly the magnitude the denotation predicts, at exactly the unit the type predicts.

Equations

• One or more equations did not get rendered due to their size.
• LambdaS.Adeq V x✝² x✝¹ (LambdaS.Ty.Q u) x✝ x_10 = (x✝ = LambdaS.Val.scalar { mag := x_10, unit := LambdaS.substU x✝² u })
• LambdaS.Adeq V x✝² x✝¹ (LambdaS.Ty.vec Vs) x✝ f = (x✝ = LambdaS.Val.vector (List.ofFn f) (List.map (LambdaS.substU x✝²) Vs))

inductive LambdaS.EnvAdeq {B D : Type} [Fintype B] [DecidableEq B] [Fintype D] [DecidableEq D] [UnitSys B D] (V : Scaling B 0) {j k : ℕ} (η : UEnv B k) (δ : DEnv D j) (Γ : Ctx B D j k) : List (Val ℝ B D) → Env Γ → Prop

Adequacy of an environment, pointwise. An inductive rather than a recursive definition so that its indices unify up to definitional equality: the binder cases present the context as Γ.weaken, not as a literal list.

• nil {B D : Type} [Fintype B] [DecidableEq B] [Fintype D] [DecidableEq D] [UnitSys B D] {V : Scaling B 0} {j k : ℕ} {η : UEnv B k} {δ : DEnv D j} {ρ : List (Val ℝ B D)} {ρd : Env []} : EnvAdeq V η δ [] ρ ρd
• cons {B D : Type} [Fintype B] [DecidableEq B] [Fintype D] [DecidableEq D] [UnitSys B D] {V : Scaling B 0} {j k : ℕ} {η : UEnv B k} {δ : DEnv D j} {τ : Ty B D j k} {Γ : Ctx B D j k} {w : Val ℝ B D} {ρ : List (Val ℝ B D)} {ρd : Env (τ :: Γ)} : Adeq V η δ τ w ρd.1 → EnvAdeq V η δ Γ ρ ρd.2 → EnvAdeq V η δ (τ :: Γ) (w :: ρ) ρd

Transporting adequacy along a substitution

Grounding the type corresponds to composing the environments, which is what lets the binder cases of eval_adeq appeal to the induction hypothesis. It is the same shape as rel_ground, and for the same reason: Adeq is a type-indexed family, so a change of type has to be matched by a transport of the denotation.

theorem LambdaS.ofFn_heq {m n : ℕ} (h : m = n) {f : Fin m → ℝ} {g : Fin n → ℝ} (hfg : f ≍ g) : List.ofFn f = List.ofFn g

List.ofFn respects heterogeneous equality of index-shifted functions.

theorem LambdaS.ofFn₂_heq {m n m' n' : ℕ} (h1 : m = m') (h2 : n = n') {A : Fin m → Fin n → ℝ} {C : Fin m' → Fin n' → ℝ} (hAC : A ≍ C) : (List.ofFn fun (a : Fin m) => List.ofFn fun (i : Fin n) => A a i) = List.ofFn fun (a : Fin m') => List.ofFn fun (i : Fin n') => C a i

The two-index version, for linear maps.

theorem LambdaS.adeq_ground {B D : Type} [Fintype B] [DecidableEq B] [Fintype D] [DecidableEq D] [UnitSys B D] (V : Scaling B 0) {j k : ℕ} (τ : Ty B D j k) {j₀ k₀ : ℕ} (η : UEnv B k₀) (δ : DEnv D j₀) (ηs : Fin k → UExp B k₀) (δs : Fin j → DExp D j₀) (v : Val ℝ B D) {x : τ.den} {x' : (Ty.ground ηs δs τ).den} : x ≍ x' → (Adeq V η δ (Ty.ground ηs δs τ) v x' ↔ Adeq V (fun (i : Fin k) => substU η (ηs i)) (fun (i : Fin j) => substU δ (δs i)) τ v x)

Adequacy transports along grounding.

theorem LambdaS.adeq_weaken {B D : Type} [Fintype B] [DecidableEq B] [Fintype D] [DecidableEq D] [UnitSys B D] (V : Scaling B 0) {j k : ℕ} (τ : Ty B D j k) (η : UEnv B k) (δ : DEnv D j) (μ : UExp B 0) (v : Val ℝ B D) {x : τ.den} {x' : τ.weaken.den} (hx : x ≍ x') : Adeq V (Fin.cons μ η) δ τ.weaken v x' ↔ Adeq V η δ τ v x

Weakening under a unit binder.

theorem LambdaS.adeq_subst {B D : Type} [Fintype B] [DecidableEq B] [Fintype D] [DecidableEq D] [UnitSys B D] (V : Scaling B 0) {j k : ℕ} (τ : Ty B D j (k + 1)) (σ : UExp B k) (η : UEnv B k) (δ : DEnv D j) (v : Val ℝ B D) {x : τ.den} {x' : (τ.subst σ).den} (hx : x ≍ x') : Adeq V η δ (τ.subst σ) v x' ↔ Adeq V (Fin.cons (substU η σ) η) δ τ v x

Instantiating a unit variable.

theorem LambdaS.adeq_weakenDim {B D : Type} [Fintype B] [DecidableEq B] [Fintype D] [DecidableEq D] [UnitSys B D] (V : Scaling B 0) {j k : ℕ} (τ : Ty B D j k) (η : UEnv B k) (δ : DEnv D j) (dd : DExp D 0) (v : Val ℝ B D) {x : τ.den} {x' : τ.weakenDim.den} (hx : x ≍ x') : Adeq V η (Fin.cons dd δ) τ.weakenDim v x' ↔ Adeq V η δ τ v x

Weakening under a dimension binder.

theorem LambdaS.adeq_substDim {B D : Type} [Fintype B] [DecidableEq B] [Fintype D] [DecidableEq D] [UnitSys B D] (V : Scaling B 0) {j k : ℕ} (τ : Ty B D (j + 1) k) (dd : DExp D j) (η : UEnv B k) (δ : DEnv D j) (v : Val ℝ B D) {x : τ.den} {x' : (τ.substDim dd).den} (hx : x ≍ x') : Adeq V η δ (τ.substDim dd) v x' ↔ Adeq V η (Fin.cons (substU δ dd) δ) τ v x

Instantiating a dimension variable.

theorem LambdaS.envAdeq_weaken {B D : Type} [Fintype B] [DecidableEq B] [Fintype D] [DecidableEq D] [UnitSys B D] (V : Scaling B 0) {j k : ℕ} {η : UEnv B k} {δ : DEnv D j} (μ : UExp B 0) {Γ : Ctx B D j k} {ρ : List (Val ℝ B D)} {ρd : Env Γ} : EnvAdeq V η δ Γ ρ ρd → EnvAdeq V (Fin.cons μ η) δ Γ.weaken ρ ρd.weaken

Environment weakening under a unit binder.

theorem LambdaS.envAdeq_weakenDim {B D : Type} [Fintype B] [DecidableEq B] [Fintype D] [DecidableEq D] [UnitSys B D] (V : Scaling B 0) {j k : ℕ} {η : UEnv B k} {δ : DEnv D j} (dd : DExp D 0) {Γ : Ctx B D j k} {ρ : List (Val ℝ B D)} {ρd : Env Γ} : EnvAdeq V η δ Γ ρ ρd → EnvAdeq V η (Fin.cons dd δ) Γ.weakenDim ρ ρd.weakenDim

Environment weakening under a dimension binder.

The list arithmetic the space forms need

theorem LambdaS.foldl_add (l : List ℝ) (a : ℝ) : List.foldl (fun (x1 x2 : ℝ) => x1 + x2) a l = a + l.sum

theorem LambdaS.zipWith_ofFn {n : ℕ} (f g : Fin n → ℝ) : List.zipWith (fun (x1 x2 : ℝ) => x1 * x2) (List.ofFn f) (List.ofFn g) = List.ofFn fun (i : Fin n) => f i * g i

theorem LambdaS.map_range_eq_ofFn {α : Type} (n : ℕ) (g : ℕ → α) : List.map g (List.range n) = List.ofFn fun (i : Fin n) => g ↑i

theorem LambdaS.colOf_ofFn {m n : ℕ} (N : Fin m → Fin n → ℝ) (i : Fin n) : colOf (List.ofFn fun (b : Fin m) => List.ofFn fun (t : Fin n) => N b t) ↑i = List.ofFn fun (b : Fin m) => N b i

@[simp]

theorem LambdaS.foldl_zipWith_ofFn {n : ℕ} (f g : Fin n → ℝ) : List.foldl (fun (x1 x2 : ℝ) => x1 + x2) (↑0) (List.zipWith (fun (x1 x2 : ℝ) => x1 * x2) (List.ofFn f) (List.ofFn g)) = ∑ i : Fin n, f i * g i

The dot product of two tabulated vectors, in the form Num.matVec unfolds to: the class default for dot is inlined, so this is the shape that appears.

theorem LambdaS.dot_ofFn {n : ℕ} (f g : Fin n → ℝ) : Num.dot (List.ofFn f) (List.ofFn g) = ∑ i : Fin n, f i * g i

The dot product of two tabulated vectors is their inner product.

theorem LambdaS.adeq_lookup {B D : Type} [Fintype B] [DecidableEq B] [Fintype D] [DecidableEq D] [UnitSys B D] (V : Scaling B 0) {j k : ℕ} {η : UEnv B k} {δ : DEnv D j} {Γ : Ctx B D j k} {τ : Ty B D j k} {ρ : List (Val ℝ B D)} {ρd : Env Γ} : EnvAdeq V η δ Γ ρ ρd → ∀ (n : ℕ) (h : Γ[n]? = some τ), ∃ (w : Val ℝ B D), ρ[n]? = some w ∧ Adeq V η δ τ w (Env.lookup n h ρd)

Looking up an adequate environment gives an adequate value.

theorem LambdaS.eval_adeq {B D : Type} [Fintype B] [DecidableEq B] [Fintype D] [DecidableEq D] [UnitSys B D] (V : Scaling B 0) {j k : ℕ} (e : Tm B D j k) (η : UEnv B k) (δ : DEnv D j) (ρ : List (Val ℝ B D)) (Δ : DCtx D j k) (Γ : Ctx B D j k) (τ : Ty B D j k) (ρd : Env Γ) (d : HasTy Δ Γ e τ) : EnvAdeq V η δ Γ ρ ρd → EnvOkD Δ η δ → ∀ (n : ℕ) (v : Val ℝ B D), eval (conv V) n j k η δ ρ e = some v → Adeq V η δ τ v (den (V.pull η) d ρd)

Adequacy. With the conversion oracle taken to be the one the valuation determines, evaluation of a well-typed term agrees with its denotation: the unit it carries and the magnitude it holds.

This is the theorem that joins the declaration story to the evaluator. The convert case is its content: the evaluator multiplies by conv V (substU η u) (substU η v) and the denotation by conv (V.pull η) u v, and Scaling.scale_pull says those agree. Everything else is bookkeeping.

What the declarations buy

LambdaS.Declare decides whether a set of unit declarations determines a valuation, and rejects the sets that do not. eval_adeq says what a valuation is worth to the evaluator. Composing them is the point of this file: the number the evaluator multiplies by is the number the declarations name.

And when the declarations conflict, not_satisfiable_of_chain says no valuation exists, so there is no oracle to run with, rather than a choice of oracles to pick wrongly between.

theorem LambdaS.evalC_adeq {B D : Type} [Fintype B] [DecidableEq B] [Fintype D] [DecidableEq D] [UnitSys B D] (V : Scaling B 0) {e : Tm B D 0 0} {u : UExp B 0} (d : HasTy (DCtx.nil D) [] e (Ty.Q u)) {n : ℕ} {v : Val ℝ B D} (hv : evalC (conv V) n [] e = some v) : v = Val.scalar { mag := den V d PUnit.unit, unit := u }

Adequacy for closed terms of scalar type.

theorem LambdaS.evalC_eq_den {B D : Type} [Fintype B] [DecidableEq B] [Fintype D] [DecidableEq D] [UnitSys B D] (V : Scaling B 0) {e : Tm B D 0 0} {u : UExp B 0} (d : HasTy (DCtx.nil D) [] e (Ty.Q u)) : ∃ (n : ℕ), evalC (conv V) n [] e = some (Val.scalar { mag := den V d PUnit.unit, unit := u })

The evaluator computes the denotation. Every well-typed closed term of scalar type evaluates (at some finite fuel, by normalization) to exactly the magnitude its denotation predicts, carrying exactly the unit its type predicts, provided the conversion oracle is the one the valuation determines.

This is the join. Before it, LambdaS.Dynamics multiplied by a number nobody had constrained and LambdaS.Fundamental reasoned about a number nobody computed.

theorem LambdaS.evalC_convert_declared {B D : Type} [Fintype B] [DecidableEq B] [Fintype D] [DecidableEq D] [UnitSys B D] {ψ : Scaling B 0} {dcl : Decl B} (hsat : Decl.Satisfies ψ dcl) {e : Tm B D 0 0} (d : HasTy (DCtx.nil D) [] e (Ty.Q (Term.ofBase dcl.lhs))) (hsd : SameDim (DCtx.nil D) (Term.ofBase dcl.lhs) dcl.rhs) : ∃ (n : ℕ), evalC (conv ψ) n [] (e.convert (Term.ofBase dcl.lhs) dcl.rhs) = some (Val.scalar { mag := den ψ d PUnit.unit * ↑dcl.factor, unit := dcl.rhs })

The evaluator multiplies by the declared factor. Converting along a declaration multiplies the magnitude by the number the declaration names: not something equal to it up to a chain of intermediate steps, but that number.

Decl.conv_eq_factor said the valuation assigns that factor; this says the evaluator uses it.