Documentation

LambdaS.Normalization

Normalization: enough fuel always exists #

eval_sound is preservation: if evaluation returns a value, that value has the predicted type. The if is an artifact of the evaluator being a function in a total logic: a definitional interpreter cannot be structurally recursive even for a normalizing calculus, because app recurses into a closure body, which is not a subterm. Fuel buys past that, and the price is that none conflates "ill-typed" with "ran out".

Λs is normalizing, so a large enough bound always exists. This file proves that a well-typed closed term evaluates for some fuel, which together with eval_sound gives the statement one actually wants: every well-typed closed term evaluates to a value of the predicted type (eval_total).

Why this is Tait and not Girard #

Λs's quantifiers range over units and dimensions: elements of a free abelian group, first-order algebraic data. There is no ∀X:Type, hence no impredicativity, hence no need for reducibility candidates. Erase the unit annotations from a Λs type and what remains is a plain simple type, so the reducibility predicate can recurse on that skeleton: instantiating a quantifier substitutes units, which leaves the skeleton alone.

Dynamics #

In this section, we give Λs an operational semantics in which values carry their units, and we prove that the instrumentation is redundant. This is precisely the content of the slogan “units are static,” and it is a claim the erased semantics of “Adequacy and Erasure” (Erasure.lean) cannot state.

The evaluator is a definitional interpreter over environments: a value environment for term variables, and (the only unusual part) a unit environment η and a dimension environment δ mapping unit and dimension variables to ground units and dimensions. Unit application extends η; no type-level substitution occurs at run time. Values are measurements ⟨ m, u⟩ (a magnitude with its unit), vectors and matrices tagged with their spaces, and three forms of closure. The evaluator is partial in two ways. It is checked: addition or comparison of mismatched units, indexing outside a space, applying a map to a vector of the wrong space, log or exp of a dimensioned value, and conversion whose source annotation disagrees with the run-time unit all get stuck, and these stuck states are what the progress half of type soundness rules out. And it is fuel-bounded: closure bodies are not subterms of the applications that invoke them, so the interpreter consumes fuel at β-steps and answers none when it runs out, as any definitional interpreter written in a total metalanguage such as Lean must [Amin and Rompf 2017; Owens et al. 2016; Reynolds 1972]. Note that fuel is spent only there: straight-line arithmetic evaluates at every bound, including zero. For example, the two-state quantum system in the artifact computes the expectation value of an energy operator H : Lin [1,1] [J,J] in a state ψ : Vec [1,1], where J abbreviates the joule kg m²/s², as

ψ.0 · (H ⊙ ψ).0  +  ψ.1 · (H ⊙ ψ).1  :  Q J,

with H and ψ supplied through the environment. Written first-order this way, the expectation evaluates at every bound, zero included; abstracted as λ H. λ ψ. … and applied back to the same two arguments, it evaluates at fuel one and fails at fuel zero. The artifact records this as twoStateChecks and its documentation develops the example in full (LambdaS.QM); “Mechanization notes” (LambdaS.lean) explains where such checks run.

Type soundness has its usual two halves, both proved. Preservation is a theorem about the interpreter (eval_sound): evaluation of a well-typed term, if it produces a value, produces one of the predicted type, with closures handled by a value-typing relation in the usual way. Progress arrives in a strengthened form: in a fueled interpreter a well-typed term's evaluation can return none only by exhausting its fuel, never by reaching a stuck state, and the normalization argument of this section shows a large enough fuel always exists, so a well-typed closed term does not merely avoid getting stuck, it terminates at a value of the predicted type (eval_total). At scalar type the normalization argument alone suffices: that proof interprets each scalar type as a set of terminating terms already carrying the right unit. The specialization is the main theorem of this section:

Theorem (Unit soundness; unit_soundness_total). For every closed well-typed term e : Q u there exists a fuel bound n and a magnitude m such that evaluation of e at fuel n yields exactly ⟨ m, u⟩.

Two remarks. First, the unit in the conclusion is u itself: the run-time tag provably agrees with the static type, which is what makes the tag redundant and erasure (“Adequacy and Erasure” (Erasure.lean)) possible. Second, the fuel is produced by the theorem rather than assumed by it: the termination theorem eval_terminates supplies the bound, so partiality comes from the total metalanguage's termination checker and not from Λs, and a well-typed term cannot exhaust any sufficiently large bound.

The normalization argument needs only Tait's method [Tait 1967]: interpret each type as a set of terminating terms and show by induction that every well-typed term inhabits its type's set. Girard's candidates [Girard 1972] are required when quantifiers range over types themselves, as in System F. Although Λs has two binders' worth of polymorphism, its quantifiers range over first-order algebraic data (exponent vectors), not over types. Reducibility can therefore be defined by recursion on a type's simply typed skeleton, the type with its unit and dimension indices erased, which quantifier instantiation provably preserves, and the simply typed argument goes through unchanged. The proof is a single induction over terms.

Fuel monotonicity #

More fuel never turns a success into a failure. Needed because the fundamental lemma combines sub-evaluations that each came with their own bound.

source
theorem LambdaS.eval_mono {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) (m : ℕ) (η : UEnv B k) (δ : DEnv D j) (ρ : List (Val R B D)) (v : Val R B D) :
n ≤ m → eval cf n j k η δ ρ e = some v → eval cf m j k η δ ρ e = some v

Fuel monotonicity. A value returned at fuel n is returned at every fuel m ≥ n.

Reducibility #

Tait's predicate. At scalar, vector and linear-map types it says the value has the predicted unit or spaces and the right lengths; at the three binding types it is the interesting clause: a closure is reducible when applying it to anything reducible terminates at a reducible value.

source
@[irreducible]
def LambdaS.Red {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) :
Ty B D 0 0 → Val R B D → Prop

Tait's reducibility predicate on closed values, by recursion on the type's skeleton (Ty.skel), which instantiation preserves.

Equations
Instances For
    source
    inductive LambdaS.RedEnv {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) :
    List (Val R B D) → Ctx B D 0 0 → Prop

    An environment is reducible at a context when each value is reducible at the corresponding type.

    Instances For
      source
      theorem LambdaS.RedEnv.lookup {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} {ρ : List (Val R B D)} {Γ : Ctx B D 0 0} {n : ℕ} {τ : Ty B D 0 0} :
      RedEnv cf ρ Γ → Γ[n]? = some τ → ∃ (v : Val R B D), ρ[n]? = some v ∧ Red cf τ v

      The fundamental lemma #

      Every well-typed term evaluates, for some fuel, to a reducible value. Note there is no induction on fuel here: the reducibility predicate at arrow type already carries the obligation that applying the closure terminates, so induction on the term suffices. Fuel only has to be reconciled between subterms, which is what eval_mono is for.

      source
      theorem LambdaS.red_eval {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) {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) :
      RedEnv cf ρ (groundCtx η δ Γ) → EnvOkD Δ η δ → ∀ (a✝ : HasTy Δ Γ e τ), ∃ (n : ℕ) (v : Val R B D), eval cf n j k η δ ρ e = some v ∧ Red cf (Ty.ground η δ τ) v

      The fundamental lemma of reducibility. A well-typed term, in a reducible environment whose unit environment respects the dimension context (EnvOkD), evaluates at some fuel to a value reducible at its grounded type.

      Normalization #

      The fundamental lemma at the closed scope. Ty.ground disappears because both environments are empty, so reducibility is stated at the type the checker wrote.

      source
      @[simp]
      theorem LambdaS.Ty.ground_nil {B D : Type} (τ : Ty B D 0 0) :
      ground (nilU B) (nilU D) τ = τ

      At the closed scope the environments ground nothing.

      source
      theorem LambdaS.eval_terminates {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) {e : Tm B D 0 0} {τ : Ty B D 0 0} (ht : HasTy (DCtx.nil D) [] e τ) :
      ∃ (n : ℕ) (v : Val R B D), evalC cf n [] e = some v ∧ Red cf τ v

      Termination of evaluation. Every well-typed closed term evaluates (at some finite fuel) to a value reducible at its type.

      This is what the fuel costs and what it buys. eval is a total function only because it may answer none. Here the fuel is produced rather than assumed, so for a well-typed closed term none only means the fuel was too small (by eval_mono, every fuel above the produced bound returns the same value): eval is partial in its definition and total on the language. The fuel is an artifact of Lean's termination checker, not of Λs.

      source
      theorem LambdaS.eval_total {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) {e : Tm B D 0 0} {τ : Ty B D 0 0} (ht : HasTy (DCtx.nil D) [] e τ) :
      ∃ (n : ℕ) (v : Val R B D), evalC cf n [] e = some v ∧ ValTy v τ

      Totality and soundness together. A well-typed closed term evaluates to a value, and that value has the type the checker predicted.

      Termination comes from eval_terminates, the typing of the result from eval_sound; neither implies the other, and the theorem is their conjunction.

      source
      theorem LambdaS.unit_soundness_total {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) {e : Tm B D 0 0} {u : UExp B 0} (ht : HasTy (DCtx.nil D) [] e (Ty.Q u)) :
      ∃ (n : ℕ) (m : R), evalC cf n [] e = some (Val.scalar { mag := m, unit := u })

      Unit soundness, unrestricted. Every well-typed closed term of scalar type evaluates to a scalar carrying exactly the unit its type predicted.

      There is no fragment restriction and no fuel hypothesis: the term may abstract over values, units and dimensions, and the fuel is produced by the proof. This is the statement that says the unit discipline has no runtime escape hatch.

      source
      theorem LambdaS.lin_soundness_total {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) {e : Tm B D 0 0} {V W : Sp B 0} (ht : HasTy (DCtx.nil D) [] e (Ty.lin V W)) :
      ∃ (n : ℕ) (M : List (List R)), evalC cf n [] e = some (Val.matrix M V W)

      Space soundness for linear maps. Every well-typed closed term of map type evaluates to a matrix value carrying exactly the spaces its type predicted: the Lin analogue of unit_soundness_total. With the introduction forms of LambdaS.Syntax, matrix literals are among the terms it governs.