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

2960 软件学报 2026 年第 37 卷第 7 期

括信源、信道与信道容量、熵、互信息等基本量, 这些核心概念在理论研究和实际通信问题中都具有重要意义.
4.1 信源和信道通用模型的形式化

信源是信息产生的来源, 信源可以看作是一个随机变量 X, 它在某个概率空间 P 上定义, 并取值于一个离散或
M. 信源的形式化如定义 14 所示.
连续的集合
定义 14. 信源.
⊢ !p X M. source X p M <=> random_variable_ext X p real_borel /\ (!a. X a IN M)
,
f(x,y) = P(Y = y | X = x) X 表示信号, Y 表示传输结果, f(x,y) 表示
信道是信息进行传输的通道, 其数学定义为
信道, 即信号在传递中的变化过程. 根据数学定义, 信道的形式化如定义 15 所示, 表示从输入至输出间的条件概率模型.
定义 15. 信道模型.
⊢ channel p X Y f <=>
random_variable_ext X p real_borel /\ random_variable_ext X p real_borel
/\ (!x y. x IN IMAGE X (p_space_ext p) /\ y IN IMAGE X (p_space_ext p)
/\ f (x, y) = conditional_distribution_ext p Y X {y} {x})
定义 15 中, “conditional_distribution_ext”定义了扩展实数上的条件分布.

信道容量的数学定义为 C = sup p(x) I(X,Y), 即信道在传输信号时所能达到速率的上确界. 故信道容量的形式化
建模依赖于互信息的形式化定义. 而互信息的形式化建模又依赖于相对熵的定义. 因此, 在形式化建模信道容量
时, 需先构建相对熵的形式化模型, 如定义 16 所示. 相对熵又称 KL 散度, 其用于衡量两个概率分布之间的差异.
定义 16. 相对熵.

⊢ KL_divergence b s u v =
extreal_ainv (L_integral (space_s s, subsets s, u)
(\x. extreal_logr b (RN_deriv u (space_s s, subsets s, v) x)))
在定义 16 中, 通过使用 RN 导数来计算测度 µ 相对于测度 v 的密度, 随后结合 Lebesgue 积分和对数函数来量
化这两个概率分布间的距离, 即相对熵. 其中, “extreal_ainv”表示扩展实数中的相反数, “extreal_logr”则表示扩展实
数的对数运算.
互信息是相对熵的一种特殊情形, 其被定义为联合分布 P(X | Y) 与独立分布乘积 P(X)P(Y) 的相对熵. 相对熵
的形式化模型如定义 17 所示.
定义 17. 互信息.
⊢ mutual_information b p s1 s2 X Y =
let prod_space =
prod_measure_space (space_s s1, subsets s1, distribution_ext p X)
(space_s s2, subsets s2, distribution_ext p Y)
in KL_divergence b (p_space_ext prod_space, events_ext prod_space)
(joint_distribution_ext p X Y) (prob_ext prod_space))
定义 17 中, “distribution_ext”和“joint_distribution_ext”分别定义了扩展实数上的分布与联合分布, “prod_
measure_space”定义了乘积测度空间. 基于上述内容, 本文将信道容量形式化为所有输入分布下互信息的最大值,
如定义 18 所示.
定义 18. 信道容量.
⊢ !b s1 s2 X Y. channel_capacity b s1 s2 X Y =
(@c. (?p. c = mutual_information b p s1 s2 X Y) /\ (!p. extreal_le (mutual_information b p s1 s2 X Y) c))
4.2 通用衰落信道模型的形式化
第 4.1 节定义了理想条件下的信道模型, 但实际通信中必须考虑信号在信道中的衰落情况. 衰落信道是无线