A HOL Theory of Euclidean Space
A HOL Theory of Euclidean Space
复制标题
DOI：
10.1007/11541868_8
复制
发表时间：
2005-08
期刊：
影响因子：
--
通讯作者：
J. Harrison
中科院分区：
文献类型：
--
作者：
J. Harrison
我们在 HOL Light 定理证明器中描述了有限维欧几里得空间的初等代数、拓扑和分析的形式化。 （欧几里得空间具有通常的距离概念。）一个显着的特征是，HOL 类型系统用于以简单且有用的方式对维度 N 进行编码，即使 HOL 不允许依赖类型。在由此产生的理论中，HOL 类型系统不但不会妨碍，而且自然地施加了正确的尺寸约束，例如检查矩阵乘法的兼容性。该理论后来有趣的发展包括向量空间理论的部分决策过程（基于 Solovay 提出的更通用的算法）以及拓扑的各种经典定理的形式证明和任意 N 维欧几里德空间的分析，例如布劳威尔不动点定理和反函数的可微性。
We describe a formalization of the elementary algebra, topology and analysis of finite-dimensional Euclidean space in the HOL Light theorem prover. (Euclidean space iswith the usual notion of distance.) A notable feature is that the HOL type system is used to encode the dimensionNin a simple and useful way, even though HOL does not permit dependent types. In the resulting theory the HOL type system, far from getting in the way, naturally imposes the correct dimensional constraints, e.g. checking compatibility in matrix multiplication. Among the interesting later developments of the theory are a partial decision procedure for the theory of vector spaces (based on a more general algorithm due to Solovay) and a formal proof of various classic theorems of topology and analysis for arbitraryN-dimensional Euclidean space, e.g. Brouwer’s fixpoint theorem and the differentiability of inverse functions.