带换算的计量单位演算
A Calculus for Units of Measure with Conversion
- Two Sigma Investments, LP（Two Sigma Investments）
机构由 AI 辅助整理，请以论文原文为准。
AI总结：
本文提出带换算的类型化lambda演算Λ_S，证明在特定重新缩放下不变性定理，并提供验证的判定过程与检查器，确保单位换算错误不改变程序结果。
AI中文摘要：
处理物理量的程序通常需要在测量单位之间进行换算，正如火星气候轨道飞行器事件所显示的，这些换算可能成为错误的丰富来源。与此同时，带类型的单位演算——我们在程序中检查物理单位的最严谨形式化方法——一直将单位换算排除在外。通过这种排除，它们确立了一个强有力的性质：良类型的程序在重新缩放（rescaling）下保持不变（任何程序都不能依赖于一米有多大）。但失去在单位之间进行换算的能力是一个重大的代价。相比之下，实用语言提供了换算功能，却没有不变性定理。我们提出Λ_S，一个带换算、对单位和维度进行量化、以及具有逐分量单位的向量和线性映射的类型化lambda演算，并精确确定在换算下有多少不变性得以保留。对于不含单位常量的项，我们证明两个抽象定理：(i) 无换算的项在每次重新缩放下都不变；(ii) 带换算的项在每次将某一维度的所有单位按相同因子缩放的重新缩放下都不变。(ii)中的条件不能被削弱：在任何其他重新缩放下，某个非零值的某些换算不是不变的。对于一阶程序，一个经过验证的判定过程返回三种裁决之一：它证明所声明的换算因子中的任何错误都不能改变程序的结果，命名通过该错误会缩放结果的累积比率，或者拒绝判定。一个经过验证的检查器决定单位声明是否一致并确定每个换算因子，并精确提取每个因子。我们还证明了充分性、擦除以及带换算的维度分析的n变量Pi定理。每个定理都在Lean 4中机械化，并且求值器编译为原生二进制。
英文摘要：
Programs that compute with physical quantities often need to convert between units of measurement, and as the Mars Climate Orbiter showed, these conversions can be a rich source of errors. Meanwhile, typed unit calculi, our most rigorous formalisms for checking physical units in a program, have excluded unit conversions. Through this exclusion, they have established a powerful property: well-typed programs are invariant under rescaling (no program can depend on how big a meter is). But losing the ability to convert between units is a significant cost. In contrast, practical languages provide conversion but no invariance theorem. We present $Λ_S$, a typed lambda calculus with conversion, quantification over units and dimensions, and vectors and linear maps with per-component units, and we determine exactly how much invariance survives conversion. For terms without unit constants we prove two abstraction theorems: (i) a convert-free term is invariant under every rescaling; (ii) a term with conversions is invariant under every rescaling that scales all units of one dimension by the same factor. The condition in (ii) cannot be weakened: under any other rescaling, some conversion of a nonzero value is not invariant. For first-order programs, a verified decision procedure returns one of three verdicts: it certifies that no error in the declared conversion factors can change the program's answer, names the accumulated ratio through which such an error would scale it, or declines. A verified checker decides whether unit declarations are consistent and determine every conversion factor, and extracts each factor exactly. We also prove adequacy, erasure, and the $n$-variable Pi theorem of dimensional analysis with conversion. Every theorem is mechanized in Lean 4, and the evaluator compiles to a native binary.
