단위 측정에 대한 계산을 위한 미적분학 (A Calculus for Units of Measure with Conversion)

물리량으로 계산하는 프로그램은 종종 단위 측정 간의 변환이 필요하며, 화성 기후 관측기(Mars Climate Orbiter)가 보여주었듯이 이러한 변환은 오류의 풍부한 원천이 될 수 있습니다. 한편, 물리 단위를 프로그램에서 검사하기 위한 가장 엄격한 형식화 방식인 타입 단위 계산(typed unit calculi)들은 단위 변환을 배제해 왔습니다. 이러한 배제를 통해 이들은 강력한 속성을 확립했습니다: 잘 타입된 프로그램은 스케일링에 대해 불변입니다 (어떤 프로그램도 미터가 얼마나 큰지에 의존할 수 없습니다). 하지만 단위 간의 변환 능력을 잃는 것은 상당한 비용입니다. 대조적으로, 실제 언어들은 변환을 제공하지만 불변성 정리(invariance theorem)를 제공하지 않습니다. 우리는 단위 변환, 단위 및 차원에 대한 양자화, 그리고 구성 요소별 단위를 가진 벡터와 선형 사상을 갖춘 타입 람다 계산 $\Lambda_S$를 제시하고, 변환이 발생했을 때 얼마나 많은 불변성이 유지되는지 정확히 결정합니다. 단위 상수가 없는 항에 대해 우리는 두 가지 추상화 정리(abstraction theorems)를 증명합니다: (i) 변환이 없는 항은 모든 스케일링에 대해 불변입니다; (ii) 변환을 포함하는 항은 한 차원의 모든 단위를 같은 인수로 스케일링하는 모든 스케일링에 대해 불변입니다. (ii)의 조건은 약화될 수 없습니다: 다른 어떤 스케일링 하에서도, 0이 아닌 값의 일부 변환은 불변이 아닙니다. 1차 프로그램의 경우, 검증된 결정 절차(verified decision procedure)는 세 가지 판결 중 하나를 반환합니다: 선언된 변환 계수에 오류가 프로그램의 답을 변경할 수 없음을 인증하거나, 그러한 오류가 스케일링하는 축적 비율을 명명하거나, 또는 기각합니다. 검증된 체커(verified checker)는 단위 선언이 일관적인지 결정하고 모든 변환 계수를 결정하며, 각 계수를 정확하게 추출합니다. 또한 우리는 변환을 포함하는 차원 분석의 적절성(adequacy), 지우기(erasure), 그리고 $n$-변수 $\Pi$ 정리를 증명합니다. 모든 정리는 Lean 4에서 기계화되었으며, 평가기는 네이티브 바이너리로 컴파일됩니다.