类型、方程、维度与π定理
Types, equations, dimensions and the Pi theorem
AI总结：
本文提出一种依赖类型域特定语言，用于形式化物理维度分析的基本概念，包括维度函数、物理量、同态测量、协变原理和π定理，旨在使数学物理更易被计算机科学家理解。
摘要：
数学物理和建模的语言拥有丰富的``维度语法''，而编程语言的常见抽象未能体现。我们提出一种嵌入Idris的依赖类型域特定语言，用于捕捉这种语法。我们将其应用于形式化维度分析的基本概念：维度函数、物理量、同态测量、协变原理和π定理。我们希望该语言能使数学物理更易被计算机科学家理解，使函数式编程更易被建模者和物理学家接受。
英文摘要：
The languages of mathematical physics and modelling are endowed with a rich ``grammar of dimensions'' that common abstractions of programming languages fail to represent. We propose a dependently typed domain-specific language (embedded in Idris) that captures this grammar. We apply it to formalize basic notions of dimensional analysis: those of dimension function, physical quantity, homomorphic measurement, the covariance principle and Buckingham's Pi theorem. We hope that the language makes mathematical physics more accessible to computer scientists and functional programming more palatable to modellers and physicists.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
