ICFP 2026｜牛津大学Imp：不精确概率编程，BDD编译零改动，三种推理一次搞定

data Ball = Red | Green | Blue

ellsberg :: Imp '["split"] Ball
ellsberg = Imp.do
  isRed <- flip (1/3)
  isGreen <- knight @"split"
  Imp.return $ if isRed then Red
               else (if isGreen then Green else Blue)

dependent :: Imp '["a1"] Three
dependent = Imp.do
  x <- flip 0.5
  if x then Imp.do
    y <- knight @"a1"
    Imp.return (if y then R else G)
  else Imp.do
    y <- knight @"a1"
    Imp.return (if y then R else B)

independent :: Imp '["a1", "a2"] Three
independent = Imp.do
  x <- flip 0.5
  if x then Imp.do
    y <- knight @"a1"
    Imp.return (if y then R else G)
  else Imp.do
    y <- knight @"a2"
    Imp.return (if y then R else B)

枚举半环：这是朴素的方法。枚举所有2^k个Knightian变量的极端赋值（每个取0或1），对每个赋值在实数半环上做一次标准WMC，得到k维立方体顶点的概率分布集合。k较小时（比如k <= 10）很直接，但k增大后指数爆炸。

区间（Interval）半环：这是近似方法。给每个Knightian变量一个区间`[lo, hi]`表示其概率的可能范围，WMC过程在区间算术（Interval Arithmetic）下进行。以区间作为权重，BDD上的加法和乘法变成区间的加法和乘法，最后得到每个结果的一个概率区间。这个区间一定能包含真实上下界（即Sound），但不一定紧（可能偏宽）。优点是计算一次即可，不需要枚举，复杂度为O(BDD大小)的多项式时间。

对偶数（Dual Number）半环：这是一种差分推理方法。对偶数`a + b·ε`能同时计算值和导数。如果把Knightian变量的权重换成对偶数形式`w + 1·ε`，那么一次WMC就能同时得到该点的概率和对该权重的梯度。这样，就可以在信义集合上做梯度下降（或上升），寻找最优（或最劣）期望值，而不需要遍历所有顶点。这也是多项式时间的——固定步数的WMC调用。

simpleRobot :: Imp '["move1", "move2"] Position
simpleRobot = Imp.do
  move1 <- interval @"move1" 0.6 0.9
  let pos1 = step P0 move1
  move2 <- interval @"move2" 0.6 0.9
  Imp.return $ step pos1 move2

Q1: 什么是信义集合（Credal Set）？直观理解为什么它比单一分布更有用？A1: 信义集合就是所有可能概率分布组成的闭凸集。在Ellsberg瓮中，红球的概率是1/3，很确定；而绿球的概率可以是0到2/3的任意值。你无法选出“正确”的那个值，但你可以说“合理的分布存在于一条线段上”。信义集合让决策者能够量化这种模糊性：决策时既可以看最好情况（上概率），也可以看最坏情况（下概率）。在工程中，这让系统设计者避免了对单个“先验分布”的过度依赖，从而对未知更具鲁棒性。

Q2: 什么是分级单子（Graded Monad），它与普通单子有什么区别？A2: 普通单子是一个类型构造器m，有return :: a -> m a和bind :: m a -> (a -> m b) -> m b。分级单子多加了一个“分级”索引，例如Imp g a，其中的g是类型级列表。return的类型是a -> Imp '[] a，bind的类型是Imp g1 a -> (a -> Imp g2 b) -> Imp (Merge g1 g2) b。这可以让你在类型系统中记录计算所使用的“Knightian命名空间”，并在合成时自动检查重叠。普通单子无法区分这些细节，而分级单子让类型系统做了本应在编译期完成的工作。

Q3: 半环参数化推理的好处是什么？区间半环和对偶数半环有什么区别？A3: 半环参数化的好处是一次编译得到的BDD可以用于多种计算，只需要替换WMC中的加法、乘法实现。区间半环把每个权重替换为区间[lo, hi]（表示该Knightian变量的概率可能范围），计算过程使用区间算术，最终输出一个必定包含真实概率的区间——快速但偏保守。对偶数半环把权重替换为形如w + 1·ε的对偶数，一次WMC能同时得到概率值和对该Knightian变量的导数，因此可以用梯度下降找到极值点。区间方法给出的是“宽度”，对偶数方法给出的是“梯度”——前者适合快速扫视，后者适合优化。

论文创新性分数：★★★★★

实验合理度：★★★★☆

学术研究价值：★★★★★

稳定性：★★★☆☆

适应性以及泛化能力：★★★☆☆

硬件需求及成本：★★★★☆

复现难度：★★★☆☆

产品化成熟度：★☆☆☆☆

可能的问题：1) 缺乏与noDice、Gen等概率编程工具的直接性能对比；2) 梯度下降的收敛性分析未深入；3) 代码未开源，可复现性受限；4) 只能处理离散布尔分布，连续空间和不精确高斯等更复杂的不精确模型不在范围内。