Documentation

LambdaS.Erasure

Erasure, at the whole language #

Unit elimination is a compiler optimization, not part of the semantics, and its burden is to preserve the semantics. This file discharges that burden for the whole of Λs, not for an arithmetic fragment.

The erased evaluator #

eeval is eval with two things removed: the annotations (values carry no units, closures carry no type or dimension ascriptions) and the checks (add does not compare units, log and exp do not demand dimensionlessness, convert does not verify its source, and mapp and comp do not compare spaces). Nothing is checked because there is nothing left to check against, which is the point: the erased evaluator is the one a compiler would emit.

Two things deliberately survive erasure, and neither is a unit.

Shape survives: a vector is still a list, and a matrix keeps its column count, without which the composite of a zero-row matrix has no width. That is array-dimension information, and no compiler erases it. The syntax makes the same commitment at the introduction form: mnil carries its column space, so the width of a zero-row matrix is written in the term and the erased value keeps exactly the length of that space.

The unit environments survive: convert under a unit binder takes its factor from the unit the caller supplies at runtime, so the evaluator keeps η and δ: a value the size of the scope, not of the data. This is the residue of conversion: units are static except for the finitely many scale factors a polymorphic conversion must receive, exactly as a dictionary-passing compiler would arrange.

The theorems #

eeval_erase is a simulation, with no typing hypothesis: whenever the instrumented evaluator produces a value, the erased evaluator produces its erasure, step for step, at the same fuel. Typing is not needed because the instrumented evaluator's success already witnesses that every erased check would have passed.

Typing enters with the corollaries, which compose the simulation with normalization and adequacy. erasure_correct says a well-typed closed scalar term evaluates on both evaluators, to the same magnitude, at the unit the type predicts, so the type system knows statically everything the erased evaluator no longer carries. eeval_den says the erased evaluator computes the denotation, with the conversion oracle the valuation determines: the compiled program's output is the mathematical meaning, with the units gone from the values and alive in the types.

From the paper's long form: Adequacy and Erasure #

The paper's tag long-form carries this section in full; it is reproduced here, converted to Markdown, so the documentation develops what the paper now summarizes. Section references name the module that carries the section; theorem references name the declaration.

Two theorems remain to close the system end to end: that the evaluator of “Dynamics” (Normalization.lean) computes the denotation of “The Price of Conversion” (Fundamental.lean) at the declared conversion factors, and that the units it carries at run time can be erased. The first connects the declarations to the compiled evaluator; the second discharges the obligation that an instrumented semantics incurs.

Adequacy at the Declared Factors #

The evaluator takes its conversion factors from an oracle (an arbitrary function from pairs of ground units to magnitudes), because it should not fix a unit system. Adequacy pins the oracle down: take it to be conv_V for a valuation V, and evaluation agrees with denotation, magnitude and unit both, at every type and scope (eval_adeq). The proof relates closures behaviorally: two closures are related when they send related arguments to related results at every fuel bound, so the relation absorbs the fuel and no induction on it is needed. Composing adequacy with the declaration theory of “Unit Declarations” (Declare.lean) closes the chain from source text to evaluator:

Theorem (Declared factors reach the compiled evaluator; evalC_convert_declared). Let V satisfy a declaration unit b = q w relating units of one dimension. Then converting a well-typed e : Q b to w, evaluated with oracle conv_V, multiplies e's value by q.

The number the evaluator multiplies by is the number the declaration names, not a number equal to it up to a chain of intermediate steps. In the artifact the yard example runs both routes: one yard converts to three feet by the declared 3 (one_yard_is_three_feet) and to 0.9144 meters by the forced redundant factor (one_yard_in_meters). The compiled binary prints 100 yards as 300 feet, as 91.44 meters by the direct declaration, and as 91.44 meters again through feet: path independence made observable.

Erasure, with Nothing Left to Check #

Instrumenting run-time values with units invites the objection that it makes soundness trivial: the checking has merely moved to run time. The objection dissolves when erasure is a theorem. We define a second evaluator, eeval, the one a compiler would emit: values carry no unit tags, and the checks are gone with the tags. Addition does not compare units, application does not compare spaces, and conversion does not verify its source, because there is nothing left to compare against.

Theorem (Erasure; eeval_erase). Whenever the instrumented evaluator produces a value, the erased evaluator, on the erased environment at the same fuel, produces its erasure. Consequently every closed well-typed e : Q u evaluates under both evaluators to the same magnitude, at the unit u the type predicts.

The simulation needs no typing hypothesis: the instrumented evaluator's success already witnesses that every skipped check would have passed. Typing enters only in the corollary (erasure_correct), where the theorem “Unit soundness” (unit_soundness_total, Normalization.lean) supplies termination and the predicted unit.

Two things deliberately survive erasure, and neither is a unit tag on a value. The array extents survive: a matrix keeps its column count, because a matrix with zero rows has no entries from which to recover its width, and composition past it would otherwise be undefined. No compiler erases such extents. (The syntax makes the same choice: the rowless matrix literal ⟨⟩_(u⃗) of “Types and Terms” (Typing.lean) carries its domain space.) And the unit environments survive, because a polymorphic conversion takes its factor from a unit supplied at run time: the erased evaluator keeps the ground unit each binder received, substitutes it into the conversion's annotation, and asks the oracle for the factor. What remains is data the size of the scope, not of the payload, passed the way compilers pass dictionaries [Wadler and Blott 1989]. This is the residue of conversion: units are static except at the finitely many scope entries polymorphic conversion must consult.

Composing the theorem “Erasure” (eeval_erase) with adequacy, the erased evaluator computes the denotation (eeval_den): at the real-number instance of the semantics, the compiled program's output is the mathematical meaning, with units gone from the values and present in the types. “Mechanization notes” (LambdaS.lean) states what the floating-point instance adds to the trusted base.

source
inductive LambdaS.EVal (R B D : Type) :
Type

Erased runtime values. No units, no spaces, no ascriptions. A matrix keeps its column count: shape, not units.

Instances For
    source
    @[irreducible]
    def LambdaS.eeval {B D R : Type} [Num R] (cf : UExp B 0 → UExp B 0 → R) :
    ℕ → (j k : ℕ) → UEnv B k → DEnv D j → List (EVal R B D) → Tm B D j k → Option (EVal R B D)

    The erased evaluator. eval with the annotations and the checks gone.

    Equations
    Instances For
      source
      def LambdaS.Val.erase {B D R : Type} :
      Val R B D → EVal R B D

      Erasing a value: drop the units, keep the shape. A closure's captured environment is erased along with it.

      Equations
      Instances For
        source
        def LambdaS.Val.eraseList {B D R : Type} :
        List (Val R B D) → List (EVal R B D)

        Erasing an environment.

        Equations
        Instances For
          source
          theorem LambdaS.eraseList_getElem? {B D R : Type} (ρ : List (Val R B D)) (n : ℕ) :
          (Val.eraseList ρ)[n]? = Option.map Val.erase ρ[n]?

          Erasure commutes with lookup.

          source
          theorem LambdaS.eeval_erase {B D : Type} [Fintype B] [DecidableEq B] [Fintype D] [DecidableEq D] [UnitSys B D] {R : Type} [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)) (v : Val R B D) :
          eval cf n j k η δ ρ e = some v → eeval cf n j k η δ (Val.eraseList ρ) e = some v.erase

          The simulation. Whenever the instrumented evaluator produces a value, the erased evaluator produces its erasure: same term, same fuel, erased environment.

          No typing hypothesis: the instrumented evaluator's success already witnesses that every check the erased evaluator skips would have passed.

          Erasure is safe, at the whole language #

          source
          theorem LambdaS.erasure_correct {B D : Type} [Fintype B] [DecidableEq B] [Fintype D] [DecidableEq D] [UnitSys B D] {R : Type} [Num R] (cf : UExp B 0 → UExp B 0 → R) {e : Tm B D 0 0} {u : UExp B 0} (d : HasTy (DCtx.nil D) [] e (Ty.Q u)) :
          ∃ (n : ℕ) (m : R), evalC cf n [] e = some (Val.scalar { mag := m, unit := u }) ∧ eeval cf n 0 0 (nilU B) (nilU D) [] e = some (EVal.scalar m)

          Erasure preserves results: the full-language statement. A well-typed closed term of scalar type evaluates on both evaluators at some common fuel: the instrumented one to a measurement carrying exactly the unit its type predicts, the erased one to exactly that measurement's magnitude.

          Everything the erased evaluator no longer carries, the type system knew statically. This is "units are static", proved rather than asserted, with unit polymorphism, higher-order structure, spaces and conversion all included, and with no fuel hypothesis: normalization supplies the fuel.

          source
          theorem LambdaS.eeval_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 : ℕ), eeval (conv V) n 0 0 (nilU B) (nilU D) [] e = some (EVal.scalar (den V d PUnit.unit))

          The erased evaluator computes the denotation. With the conversion oracle the valuation determines, the compiled program's output is the mathematical meaning: units gone from the values, alive in the types. Adequacy composed with the simulation.