Page 272 - 《软件学报》2026年第7期

买宁 等: 高铁复合无线通信信道形式化建模与验证 2957

3 基于扩展实数的数学基础形式化

高速铁路复合无线通信信道的建模需要充分考虑极端情况, 例如高速移动环境中信号幅度的剧烈波动和无
穷大值的出现. 扩展实数可以处理一些在标准实数系统中没有定义的数学运算和情况, 例如无穷大、极限和不
定值, 还可确保测度、积分和导数运算在极限处的连续性. 使用扩展实数可有效避免因标准实数系统局限性导
致的建模误差, 使得高铁信道的建模更加严谨, 从而提升信道模型的通用性和可靠性. 因此, 本文在 HOL Light
中建模了扩展实数基础定义及其数学运算, 并基于此建模信息论基础, 作为高铁复合无线通信信道形式化的定
义基础. 本文针对扩展实数的数学运算性质证明了共 170 余条定理, 用于后续高铁复合无线通信信道模型建模
与性质验证.
R, 其高阶逻辑模型如定义 1 所示.
在数学上, 扩展实数又称广义实数, 包括正无穷、负无穷和普通实数
定义 1. 扩展实数.
let extreal_INDUCT, extreal_RECURSION = define_type
"extreal = NegInf | PosInf | Normal real";;
定义 1 中的“NegInf”表示 −∞; “PosInf”表示 +∞; “Normal”表示类型转换符, 代表从实数到扩展实数的类型映
射. 以其上确界为例, 扩展实数的运算需要对无穷大进行特殊处理. 定义 2 形式化描述扩展实数上确界的计算.
定义 2. 扩展实数的上确界.
⊢ extreal_sup p = (if !x. (!y. p y ==> extreal_le y x) ==> x = PosInf then PosInf
else if !x. p x ==> x = NegInf then NegInf else Normal (sup (\r. p (Normal r))))
定义 2 可用于 Lebesgue 测度的形式化建模. 其中, “extreal_le”表示扩展实数中重定义的“ ⩽ ”运算符. “sup”是
HOL Light 中对普通实数构成的集合 P 求上确界的函数, 即 εs. ∀y. (∃x. (P(x)∧y < x) ⇔ y < s).

3.1 基于扩展实数的测度形式化
σ 有限测度, 还可以定义无穷测度. 测度用于表示几何集合的度量, 包括
利用扩展实数定义测度, 不仅能定义
长度、面积和体积等, 它是形式化积分和概率的基础. 在测度的形式化过程中, 涉及代数相关概念的定义, 本文参
考了首都师范大学尹晓娜等人 [20] 在 HOL Light 中对代数和测度基本概念的形式化, 并对部分测度定义进行了扩展
实数域上的推广. 本文通过三元组来定义测度, 使空间、代数、扩展实数上的测度函数关联起来. 测度的高阶逻辑
模型如定义 3 所示.
定义 3. 测度.
⊢ measure_ext (sp:A->bool, sts:(A->bool)->bool, mu:(A->bool)->extreal) = mu
Lebesgue 测度是欧几里得空间上的标准测度, 任何区间都是 Lebesgue 可测的, 而 Borel 测度是一种特定测度,
只能测量 Borel 可测集. 假设 X 是实数集, P 是有界半闭区间 [a,b) 的集合, S 是由 P 生成的 σ 代数, µ 是定义在 P
µ 对所有 S 都有
上的集合函数, 其表达式为 µ[a,b) = b−a. 此时 S 的集合表示 X 上的 Borel-σ 代数. 若 Borel 集合
定义, 且 S 的集合是完备的, 则测度 µ 称为 Lebesgue 测度, 其形式化描述如定义 4 所示.
定义 4. Lebesgue 测度.
⊢ lebesgue = (:real^1), {A | !n. indicator A integrable_on line_1 n},
(\A. extreal_sup {Normal (drop (integral (line_1 n) (indicator A))) | n IN (:num)})
本文在对 Lebesgue 测度形式化时参考了其数学定义和其在 Mhamdi 等人 [15,16] 的研究工作中的定义, 将其定
义为所有有限区间 [−n, n] 规范积分的上确界. 定义 4 中, “line_1”表示一维空间中边界为 [−n, n] 的线段, 即 line 1 (n) =
1
{x ∈ R |−n ⩽ x ⩽ n}, 此处用其来表示实数集 X.
本文结合 Lebesgue 测度与 Borel 可测集, 定义了 Lebesgue-Borel 测度, 使其既能够对 Borel 集合进行测量, 又
扩展了 Lebesgue 测度并继承其优点. 在对其形式化时, 本文将 Lebesgue-Borel 定义为由 Lebesgue 测度、Borel 空
间、 Borel-σ 代数构成的三元组, 如定义 5 所示, 并将高铁复合无线信道建模在该测度之上.