API documentation: ericeallen.github.io/lambda-s,
generated by doc-gen4 on every push to main.
Λs is a typed lambda calculus in which conversion between units of the same dimension is a primitive, and the price of admitting it is characterized exactly. This repository is the full mechanization: statics, dynamics, denotational semantics, two abstraction theorems, adequacy, erasure, and the Pi theorem of dimensional analysis, in Lean 4.
The theoretical literature on units, beginning with Kennedy, obtains parametricity theorems for calculi in which no operation can observe a unit. The practical literature provides conversion, which is what programmers ask of units, and no invariance theory, because conversion breaks the parametricity such theories rest on. Λs has both. For example, converting a measurement from meters to feet and back multiplies it by reciprocal factors; the round trip is independent of the declared foot-to-meter ratio.
Every term containing no unit constants is invariant under rescalings that respect dimension. For a first-order program with nonzero denotation, an assigned accumulated ratio is trivial exactly when the program is invariant under all rescalings. Triviality is decidable. The diagnostic reports the assigned ratio, or declines to assign one; a decline supplies no invariance verdict either way.
The development is 10,500 lines of definitions and proofs and 6,200 lines
of documentation (19,300 lines of source in all; scripts/count_lines.py
counts LambdaS/*.lean, and CI checks these figures and the table below against
it). Units and dimensions are exponent vectors over ℚ. Substitution on these
vectors is a linear map, and its algebraic laws follow by reordering finite
sums. Unit equality needs no normalization pass over unit syntax.
| Lean | 4.33.0 (pinned in lean-toolchain) |
| mathlib | pinned in lake-manifest.json |
sorry / admit |
none |
| lines of definitions and proofs | 10,500 |
| lines of documentation | 6,200 |
| theorem and lemma declarations | 568 |
| axioms | propext, Classical.choice, Quot.sound |
Examples.lean, QM.lean, and Algorithms.lean run the checker, the
drift analysis, and the evaluator at build time through #guard; if a
stated result were different, the library would not compile. The particle in
a box is checked this way, numerically as well as dimensionally: its
uncertainty product and its ground-state energy are #guard assertions. The
two-state system reaches the BLAS stubs, whose arithmetic does not run at
build time, so the compiled binary checks its numbers instead and CI asserts
that output.
Prerequisites: elan (which installs the pinned Lean toolchain on first use) and a C compiler.
lake exe cache get # fetch prebuilt mathlib oleans (multi-GB, needs network)
lake build # build the library and check every proof
lake exe lambdas # print the worked reports with their numeric self-checkslake exe cache get is the slow step; with the cache in place, a full
build of this library takes a few minutes on a laptop. The BLAS shim in
c/ links against Accelerate's cblas on macOS (through the Command Line
Tools SDK's libblas, since Lean's bundled linker has no framework search
path; if your Mac has only Xcode, adjust moreLinkArgs in lakefile.lean)
and falls back to portable C loops elsewhere; no separate BLAS installation
is required, and the binary reports which backend it is running.
The algebra. Uom defines a unit as a ℚ-valued exponent vector and
proves the group laws. Scaling gives rescalings and the pullback laws that
make substitution commute with them. Unify verifies elimination and
solution preservation for rational unit equations. It has no assembled unifier
or principal-type inference theorem; inference with conversion's dimension
constraints remains open in this development.
Space, Map, and Density give dimensioned vectors, Hart-style
rank-one matrices, and densities.
Statics. Syntax gives types and terms, scope-indexed so ill-scoped unit and dimension
syntax is unrepresentable. Term-variable indices are checked by context lookup. Typing gives both the declarative judgment
HasTy and the checker, and the checker returns derivations: soundness
holds by construction, and completeness and decidability are proved.
Notation makes programs readable.
Dynamics. Dynamics is a definitional interpreter instrumented with
units. Soundness is type soundness, and Normalization is strong
normalization by Tait reducibility on type skeletons, so the fuel a
definitional interpreter carries is produced by a theorem rather than
assumed.
Semantics. Parametricity builds the logical relation, Fundamental
proves both abstraction theorems and that coherence is the exact price of
conversion. Adequacy joins the declaration oracle to the evaluator instantiated with real
arithmetic, and
Erasure strips units and every dynamic check from run-time values without
moving the numbers.
Conversion. Conversion gives the operator, Declare the consistency
criterion for declaration sets, proved in both directions in exact rational
arithmetic. RationalSolver performs executable elimination and back-substitution
with a decidable rational-module right-hand side. LogFactor implements exact
symbolic logarithms using denominator clearing and rational product equality;
no logarithm or root is evaluated while deciding consistency.
Determinacy and DeclarationComplete prove and execute the span tests for
individual factors and global coverage of the dimension kernel. DeclareSolver
combines dimensional soundness, consistency, and completeness into a checked
certificate, and returns inspectable exact conversion factors as positive
rational radicands with positive root degrees. Rejection is proved complete.
The solver may choose reference magnitudes, but a queried factor is returned
only when declarations determine it in every satisfying valuation.
Ratio gives the first-order syntax of accumulated ratios, and Twist the drift analysis and
its decision procedure.
Dimensional analysis. Pi and PiTheorem derive Buckingham factorization
and descent to n - rank A rational dimensionless coordinates. The factorization
allows arbitrary signed outputs on positive inputs. PiCoherent supplies the
dimension-level law for converting programs in closed external unit/dimension
scope, including internal polymorphism. The stronger unit-level law applies to
parametric convert-free or drift-free programs. Definability and NonDefinability prove
that rational powers must be primitive.
Programs. Examples, QM, and Algorithms are the worked examples,
including the yard/foot/meter declarations end to end and the pendulum.
DeclarationSolverExamples executes disconnected/linked units, redundant and
conflicting cycles, dimension errors, empty bases, dependent dimension rows,
and exact rational and square-root factors. Its four kernel theorems connect
actual returned factors to every satisfying valuation. The native executable
runs this battery and exits nonzero if it fails. JacobiChecks exercises the
actual Float evaluator and native matrix operations on 125 Jacobi sweep cases
and 12 stopping cases. It checks off-diagonal elimination, symmetry, trace and
determinant preservation, unchanged diagonal inputs, and signed residuals.
These numerical checks run in the executable, separately from typing and drift
guards; a failed check makes the executable exit nonzero.
Each module carries a header docstring explaining what it is for and why it exists; those are the intended entry points for a reader, and the groups above are the intended reading order.
Our paper summarizes the developed explanations in the module headers. These
explanations originated in an earlier draft preserved by the paper repository's
long-form tag; they now describe the current artifact. Maintain the paper and
these explanations together, checking both against the definitions and theorem
statements. The current formal statements determine each claim's scope.
THEOREMS.md maps every artifact identifier the accompanying paper cites
to its Lean name, file, and line. Line numbers are re-derived from the
sources by scripts/verify_theorems_index.py (CI fails on drift;
--fix repairs the index in place). scripts/count_lines.py is the
method behind the size figures above (--check fails CI when the status
table stops matching the sources; --fix rewrites it).
lake env lean scripts/Audit.leanprints the axiom dependencies of every declaration THEOREMS.md indexes
(scripts/verify_theorems_index.py fails if any indexed declaration is
missing from the audit). CI builds the library, greps the sources for
sorry, fails if any audited theorem depends on more than the three
standard axioms, and runs the compiled binary, asserting its numeric
self-checks and the declared-conversion report.
A reader who believes a theorem trusts the Lean kernel and the three
axioms above. A reader who believes a number the binary prints trusts, in
addition, Lean's compiler and runtime, the Float carrier, and the three C
functions in c/lambdas_blas.c (lambdas_ddot, lambdas_dgemv,
lambdas_blas_backend) that reach BLAS. The abstraction and adequacy theorems use real
arithmetic and do not equate it with compiled floating-point arithmetic.
Rounding affects defined operations. The carriers also totalize partial
operations differently: for example, Float.pow returns NaN on negative
bases with non-integer exponents, while Real.rpow uses the real part of
the principal complex power. Concrete #guard checks execute through Lean's
compiler; they are distinct from kernel-checked theorem proofs. The binary
checks selected arithmetic and boundary cases, not a general correspondence.
Apache-2.0; see LICENSE.