Formalization of the Standard Uniform random variable
Formalization of the Standard Uniform random variable
复制标题
标准均匀随机变量的形式化
DOI：
10.1016/j.tcs.2007.05.009
复制
发表时间：
2007
期刊：
影响因子：
--
通讯作者：
S. Tahar
中科院分区：
文献类型：
--
作者：
O. Hasan;S. Tahar
连续随机变量广泛用于从数学上描述工程和物理科学中的随机现象。在本文中，我们提出了标准均匀随机变量的高阶逻辑形式化作为其离散近似序列的极限值。然后，我们通过在 HOL 定理证明器中证明相应的概率分布属性来证明该规范的正确性，总结证明步骤。通过使用各种非均匀随机数生成技术，可以将形式化的标准均匀随机变量变换为形式化的其他连续随机变量，例如均匀、指数、正态等。这些连续随机变量的形式化将使我们能够在高阶逻辑（HOL）定理证明者的框架内对系统进行无错误的概率分析。出于说明目的，我们基于形式化的标准均匀随机变量提出了连续均匀随机变量的形式化，然后利用它对 HOL 中的舍入误差进行简单的概率分析。
Continuous random variables are widely used to mathematically describe random phenomena in engineering and the physical sciences. In this paper, we present a higher-order logic formalization of the Standard Uniform random variable as the limit value of the sequence of its discrete approximations. We then show the correctness of this specification by proving the corresponding probability distribution properties within the HOL theorem prover, summarizing the proof steps. The formalized Standard Uniform random variable can be transformed to formalize other continuous random variables, such as Uniform, Exponential, Normal, etc., by using various non-uniform random number generation techniques. The formalization of these continuous random variables will enable us to perform an error free probabilistic analysis of systems within the framework of a higher-order-logic (HOL) theorem prover. For illustration purposes, we present the formalization of the Continuous Uniform random variable based on the formalized Standard Uniform random variable, and then utilize it to perform a simple probabilistic analysis of roundoff error in HOL.