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 term evaluates for some fuel, which together with eval_sound gives the statement one actually wants: every well-typed term evaluates to a value of the predicted type.

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.

From the paper's long form: Dynamics #

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.

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 of mismatched units, indexing outside a space, applying a map to a vector of the wrong space, log 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 is stuck 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: strong normalization 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

Reducibility #

Tait's predicate. At scalar, vector and linear-map types it is just "has the right shape"; 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
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

    Reducible values are well-shaped, which is all the evaluator's matches need.

    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

      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

      Strong normalization. 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 none is not a possible answer for a well-typed term: 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.